chore: build lean4checker with current toolchain (#8669)

After leanprover/lean4#2766 lands, the git hash of will be embedded in every olean. `lean4checker` will thus reject oleans unless it was compiled on the same toolchain as they were! We may want to relax this later, but for now, since we are building `lean4checker` in CI anyway, let's just make sure it is on the same toolchain as mathlib. Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Nov 28, 2023 · 16f64a1 · 16f64a1
1 parent 2577ef7
commit 16f64a1
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 0 deletions.
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -261,6 +261,9 @@ jobs:
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
           git checkout toolchain/v4.3.0-rc2
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -268,6 +268,9 @@ jobs:
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
           git checkout toolchain/v4.3.0-rc2
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..

diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
@@ -247,6 +247,9 @@ jobs:
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
           git checkout toolchain/v4.3.0-rc2
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..

diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -265,6 +265,9 @@ jobs:
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
           git checkout toolchain/v4.3.0-rc2
+          # Now that the git hash is embedded in each olean,
+          # we need to compile lean4checker on the same toolchain
+          cp ../lean-toolchain .
           lake build
           ./test.sh
           cd ..