From 154cbd2feeb683838a78d8c9a04531159e89aa47 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Mon, 6 Jul 2026 14:42:00 +0000 Subject: [PATCH 1/5] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 4f88fc749..f02fef7cc 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-07-03 +leanprover/lean4-pr-releases:pr-release-13956-6baff05 From 65d8cad65cdde9d45120cb6f57816d5addbab43b Mon Sep 17 00:00:00 2001 From: Joscha Date: Tue, 7 Jul 2026 11:57:26 +0200 Subject: [PATCH 2/5] update CI from master --- .github/workflows/build-post.yml | 6 ++++++ .github/workflows/build.yml | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build-post.yml b/.github/workflows/build-post.yml index c547941b9..ee9982d76 100644 --- a/.github/workflows/build-post.yml +++ b/.github/workflows/build-post.yml @@ -89,6 +89,12 @@ jobs: github-token: ${{ github.token }} run-id: ${{ github.event.workflow_run.id }} + - name: Add run link to build report + env: + RUN_URL: ${{ github.event.workflow_run.html_url }} + run: | + echo -e "\n[View run]($RUN_URL)" >> "${{ runner.temp }}/report/report.md" + - name: Post build report uses: ./.downstream/actions/status-message with: diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 9c916b515..d554faaf5 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -1,10 +1,10 @@ name: Build subrepos on: - pull_request: push: branches: - master + - adaptation-* jobs: main: From 8009a630aef0e373c329ab270c2c69ea7ef7d7d0 Mon Sep 17 00:00:00 2001 From: Joscha Date: Tue, 7 Jul 2026 15:42:12 +0200 Subject: [PATCH 3/5] update CI more --- .github/workflows/build-post.yml | 5 +++-- .github/workflows/build.yml | 8 ++++---- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/.github/workflows/build-post.yml b/.github/workflows/build-post.yml index ee9982d76..4c73ba2ee 100644 --- a/.github/workflows/build-post.yml +++ b/.github/workflows/build-post.yml @@ -1,4 +1,4 @@ -name: Post-build on master +name: Post-build on: workflow_run: @@ -60,7 +60,8 @@ jobs: post-report: if: ${{ github.event.workflow_run.conclusion != 'cancelled' && - github.event.workflow_run.event == 'pull_request' }} + github.event.workflow_run.event == 'push' && + startsWith(github.event.workflow_run.head_branch, 'adaptation-') }} runs-on: ubuntu-slim permissions: actions: read diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index d554faaf5..25139a1ef 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -42,25 +42,25 @@ jobs: --mappings "$RUNNER_TEMP/mappings" - name: Add report to job summary - if: ${{ !cancelled() }} # Report even if build fails + if: ${{ !cancelled() }} # Even if build fails run: cat "$RUNNER_TEMP/report.md" >> "$GITHUB_STEP_SUMMARY" - name: Upload build report - if: ${{ !cancelled() }} # Upload even if build fails + if: ${{ !cancelled() }} # Even if build fails uses: actions/upload-artifact@v7 with: name: build-report path: ${{ runner.temp }}/report.md - name: Upload build mappings - if: ${{ !cancelled() }} # Upload even if build fails + if: ${{ !cancelled() }} # Even if build fails uses: actions/upload-artifact@v7 with: name: build-mappings path: ${{ runner.temp }}/mappings/ - name: Upload build cache - if: ${{ !cancelled() }} # Upload even if build fails + if: ${{ !cancelled() }} # Even if build fails uses: actions/upload-artifact@v7 with: name: build-cache From e90812908b11d605015a3866ac2a4afaa57d7308 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 7 Jul 2026 16:21:30 +0000 Subject: [PATCH 4/5] comparator: use upstreamed `Environment.replay` instead of `Lean4Checker` `#13956` adapts kernel `addDeclCore` to take a `maxRecDepth` bound, which broke `Lean4Checker.Replay`'s `env.replay'` call. The replay machinery is now upstreamed into Lean core as `Lean.Environment.replay` (available via `import Lean`), so drop the external `Lean4Checker` dependency and call the core function directly. Co-Authored-By: Claude Opus 4.8 --- comparator/Main.lean | 3 +-- comparator/lake-manifest.json | 10 ---------- comparator/lakefile.toml | 5 ----- 3 files changed, 1 insertion(+), 17 deletions(-) diff --git a/comparator/Main.lean b/comparator/Main.lean index 3fe7c5411..284f7a3c7 100644 --- a/comparator/Main.lean +++ b/comparator/Main.lean @@ -5,7 +5,6 @@ Authors: Henrik Böving -/ import Lean import Comparator -import Lean4Checker.Replay import Export.Parse namespace Comparator @@ -198,7 +197,7 @@ def runKernel (solution : Export.ExportedEnv) : M Unit := do -- Lean's kernel interprets just the addition of `Quot as adding all of these so adding them -- multiple times leads to errors. constMap := constMap.erase `Quot.mk |>.erase `Quot.lift |>.erase `Quot.ind - discard <| env.replay' constMap + discard <| env.replay constMap IO.println "Lean default kernel accepts the solution" def primitiveTargets : M (Array Lean.Name) := do diff --git a/comparator/lake-manifest.json b/comparator/lake-manifest.json index 3cbb6ab9e..4f014bf4e 100644 --- a/comparator/lake-manifest.json +++ b/comparator/lake-manifest.json @@ -10,16 +10,6 @@ "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4checker", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "b7398199245524275543dec6113229c9bb4902e5", - "name": "Lean4Checker", - "manifestFile": "lake-manifest.json", - "inputRev": "b7398199245524275543dec6113229c9bb4902e5", - "inherited": false, "configFile": "lakefile.toml"}], "name": "Comparator", "lakeDir": ".lake", diff --git a/comparator/lakefile.toml b/comparator/lakefile.toml index 1865ae821..8b55152f7 100644 --- a/comparator/lakefile.toml +++ b/comparator/lakefile.toml @@ -9,11 +9,6 @@ name = "Comparator" name = "comparator" root = "Main" -[[require]] -scope = "leanprover" -name = "Lean4Checker" -rev = "b7398199245524275543dec6113229c9bb4902e5" - [[require]] scope = "leanprover" name = "lean4export" From e2b8c7d7c000211a6bc45adb888c4dc938a757a3 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 8 Jul 2026 11:13:35 +0000 Subject: [PATCH 5/5] downstream: undo overrides --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index f02fef7cc..4f88fc749 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-13956-6baff05 +leanprover/lean4:nightly-2026-07-03