fix: run pr branch version of mk_all (#25624)

bryangingechen · bryangingechen · commit e99fde22b357 · 2025-06-09T17:35:50.000Z
If `master` is on a different toolchain than the PR, then its `mk_all` doesn't work; we fix that by just running the PR branch's version of `mk_all` inside `landrun`.
diff --git a/.github/build.in.yml b/.github/build.in.yml
@@ -136,9 +136,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -219,13 +218,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
@@ -146,9 +146,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -229,13 +228,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -153,9 +153,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -236,13 +235,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
@@ -150,9 +150,8 @@ jobs:
         shell: bash # We're only building the `master` branch version of the tools, so don't need to run inside landrun.
         run: |
           cd master-branch
-          lake build cache mk_all check-yaml graph
+          lake build cache check-yaml graph
           ls .lake/build/bin/cache
-          ls .lake/build/bin/mk_all
           ls .lake/build/bin/check-yaml
           ls .lake/packages/importGraph/.lake/build/bin/graph
 
@@ -233,13 +232,11 @@ jobs:
       - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
         id: mk_all
         continue-on-error: true # Allow workflow to continue, outcome checked later
-        # This only runs `mk_all --check` from the `master-branch`, so doesn't need to be inside landrun
-        shell: bash
+        # This runs `mk_all --check` from the `pr-branch` inside landrun
         run: |
           cd pr-branch
-
-          echo "Running mk_all --check (from master-branch)..."
-          LAKE_HOME="$TOOLCHAIN_DIR" ../master-branch/.lake/build/bin/mk_all --check
+          echo "Running mk_all --check (from pr-branch)..."
+          lake exe mk_all --check
 
       - name: begin gh-problem-match-wrap for build step
         uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
