chore: build ProofWidgets before tests (#8416)

After leanprover/lean4#2766 this becomes critical. Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Nov 19, 2023 · 34ab8d4 · 34ab8d4
1 parent 693fd79
commit 34ab8d4
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 4 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -242,7 +242,11 @@ jobs:
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -249,7 +249,11 @@ jobs:
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -228,7 +228,11 @@ jobs:
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -246,7 +246,11 @@ jobs:
 
       - name: test mathlib
         id: test
-        run: make -j 8 test
+        run: |
+          # Tests use parts of ProofWidgets not imported by Mathlib.
+          # Ensure everything has been built.
+          lake build ProofWidgets
+          make -j 8 test
 
       - name: lint mathlib
         id: lint