From 34ab8d46e2122dd9a5600e735c01237adb448b6a Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 19 Nov 2023 20:53:09 +0000 Subject: [PATCH] chore: build ProofWidgets before tests (#8416) After leanprover/lean4#2766 this becomes critical. Co-authored-by: Scott Morrison --- .github/workflows/bors.yml | 6 +++++- .github/workflows/build.yml | 6 +++++- .github/workflows/build.yml.in | 6 +++++- .github/workflows/build_fork.yml | 6 +++++- 4 files changed, 20 insertions(+), 4 deletions(-) diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index 8fc6d556a045f..8ff4874f54a80 100644 --- 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 index 880aafba8cba8..f58020b785549 100644 --- 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 index 998af8203f4f0..059fcd36bbd89 100644 --- 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 index db68e7834f65c..98e5c5ae28b7e 100644 --- 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