From 16f64a1daa2da81b56dcff88eab90ee1559da06f Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Tue, 28 Nov 2023 04:40:08 +0000
Subject: [PATCH] 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 <scott.morrison@gmail.com>
---
 .github/workflows/bors.yml       | 3 +++
 .github/workflows/build.yml      | 3 +++
 .github/workflows/build.yml.in   | 3 +++
 .github/workflows/build_fork.yml | 3 +++
 4 files changed, 12 insertions(+)

diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index c37c4b9e587cf..596af7e75a09a 100644
--- 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
index 6c9a3cd8ea9cf..39c37a1fee1ef 100644
--- 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
index 2bd6cf432e4df..c24aac8f04cda 100644
--- 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
index 58c860d60e908..8cfcdce512e53 100644
--- 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 ..