From 9a93b1863bb5cdffe98233dd12fe4e9e0bf84df1 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Thu, 29 May 2025 05:23:10 +0100 Subject: [PATCH] try mk_all --- .github/workflows/blueprint.yml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index cf80ba8..19bf1e9 100644 --- a/.github/workflows/blueprint.yml +++ b/.github/workflows/blueprint.yml @@ -28,7 +28,16 @@ jobs: - name: Checkout project uses: actions/checkout@v4 - - name: Setup Lean + - name: Setup Elan + uses: leanprover/lean-action@v1 # setup elan and fetch the Mathlib cache + with: + auto-config: false # don't automatically run lake build, lake test, lake lint + use-github-cache: false # avoid using the GitHub cache twice in one workflow + + - name: Check mk_all + run: lake exe mk_all --check + + - name: Build project uses: leanprover/lean-action@v1 - name: Cache Mathlib Docs