fix: comment

Co-authored-by: Markus Himmel <markus@lean-fro.org>

.claude/commands/release.md

@@ -1,69 +0,0 @@
-# Release Management Command
-
-Execute the release process for a given version by running the release checklist and following its instructions.
-
-## Before Starting
-
-**IMPORTANT**: Before beginning the release process, read the in-file documentation:
-- Read `script/release_checklist.py` for what the checklist script does
-- Read `script/release_steps.py` for what the release steps script does
-
-These comments explain the scripts' behavior, which repositories get special handling, and how errors are handled.
-
-## Arguments
-- `version`: The version to release (e.g., v4.24.0)
-
-## Process
-
-1. Run `script/release_checklist.py {version}` to check the current status
-2. **CRITICAL: If preliminary lean4 checks fail, STOP immediately and alert the user**
-   - Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes exist
-   - **IMPORTANT**: The release page is created AUTOMATICALLY by CI after pushing the tag - DO NOT create it manually
-   - Do NOT create any PRs or proceed with repository updates if these checks fail
-3. Create a todo list tracking all repositories that need updates
-4. **CRITICAL RULE: You can ONLY run `release_steps.py` for a repository if `release_checklist.py` explicitly says to do so**
-   - The checklist output will say "Run `script/release_steps.py {version} {repo_name}` to create it"
-   - If a repository shows "🟡 Dependencies not ready", you CANNOT create a PR for it yet
-   - You MUST rerun `release_checklist.py` before attempting to create PRs for any new repositories
-5. For each repository that the checklist says needs updating:
-   - Run `script/release_steps.py {version} {repo_name}` to create the PR
-   - Mark it complete when the PR is created
-6. After creating PRs, notify the user which PRs need review and merging
-7. **MANDATORY: Rerun `release_checklist.py` to check current status**
-   - Do this after creating each batch of PRs
-   - Do this after the user reports PRs have been merged
-   - NEVER assume a repository is ready without checking the checklist output
-8. As PRs are merged and tagged, dependent repositories will become ready
-9. Continue the cycle: run checklist → create PRs for ready repos → wait for merges → repeat
-10. Continue until all repositories are updated and the release is complete
-
-## Important Notes
-
-- The `release_steps.py` script is idempotent - it's safe to rerun
-- The `release_checklist.py` script is idempotent - it's safe to rerun
-- Some repositories depend on others (e.g., mathlib4 depends on batteries, aesop, etc.)
-- Wait for user to merge PRs before dependent repos can be updated
-- Alert user if anything unusual or scary happens
-- Use appropriate timeouts for long-running builds (verso can take 10+ minutes)
-- ProofWidgets4 uses semantic versioning (v0.0.X) - it's okay to create and push the next sequential tag yourself when needed for a release
-
-## PR Status Reporting
-
-Every time you run `release_checklist.py`, you MUST:
-1. Parse the output to identify ALL open PRs mentioned (lines with "✅ PR with title ... exists")
-2. Provide a summary to the user listing ALL open PRs that need review
-3. Group them by status:
-   - PRs for repositories that are blocked by dependencies (show these but note they're blocked)
-   - PRs for repositories that are ready to merge (highlight these)
-4. Format the summary clearly with PR numbers and URLs
-
-This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
-The user needs to see the complete picture of what's waiting for review.
-
-## Error Handling
-
-**CRITICAL**: If something goes wrong or a command fails:
-- **DO NOT** try to manually reproduce the failing steps yourself
-- **DO NOT** try to fix things by running git commands or other manual operations
-- Both scripts are idempotent and designed to handle partial completion gracefully
-- If a script continues to fail after retrying, report the error to the user and wait for instructions

.github/workflows/awaiting-manual.yml

@@ -12,7 +12,7 @@ jobs:
       - name: Check awaiting-manual label
         id: check-awaiting-manual-label
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const { labels, number: prNumber } = context.payload.pull_request;

.github/workflows/awaiting-mathlib.yml

@@ -12,7 +12,7 @@ jobs:
       - name: Check awaiting-mathlib label
         id: check-awaiting-mathlib-label
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const { labels, number: prNumber } = context.payload.pull_request;

.github/workflows/build-template.yml

@@ -3,6 +3,9 @@ name: build-template
 on:
   workflow_call:
     inputs:
+      check-level:
+        type: string
+        required: true
       config:
         type: string
         required: true
@@ -227,7 +230,7 @@ jobs:
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: matrix.test
+        if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
       - name: Test Summary
         uses: test-summary/action@v2
         with:

.github/workflows/check-stage0.yml

@@ -11,8 +11,8 @@ jobs:
     - uses: actions/checkout@v5
       with:
         ref: ${{ github.event.pull_request.head.sha }}
+        filter: blob:none
         fetch-depth: 0
-        filter: tree:0
 
     - name: Find base commit
       if: github.event_name == 'pull_request'
@@ -31,7 +31,7 @@ jobs:
 
     - if: github.event_name == 'pull_request'
       name: Set label
-      uses: actions/github-script@v8
+      uses: actions/github-script@v7
       with:
         script: |
           const { owner, repo, number: issue_number  } = context.issue;

.github/workflows/ci.yml

@@ -31,6 +31,10 @@ jobs:
   configure:
     runs-on: ubuntu-latest
     outputs:
+      # 0: PRs without special label
+      # 1: PRs with `merge-ci` label, merge queue checks, master commits
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
+      check-level: ${{ steps.set-level.outputs.check-level }}
       # The build matrix, dynamically generated here
       matrix: ${{ steps.set-matrix.outputs.matrix }}
       # secondary build jobs that should not block the CI success/merge queue
@@ -106,9 +110,6 @@ jobs:
           TAG_NAME="${GITHUB_REF##*/}"
           echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
 
-      # 0: PRs without special label
-      # 1: PRs with `merge-ci` label, merge queue checks, master commits
-      # 2: PRs with `release-ci` label, releases (incl. nightlies)
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -116,7 +117,6 @@ jobs:
         # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
         run: |
           check_level=0
-          fast=false
 
           if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=2
@@ -129,24 +129,19 @@ jobs:
             elif echo "$labels" | grep -q "merge-ci"; then
               check_level=1
             fi
-            if echo "$labels" | grep -q "fast-ci"; then
-              fast=true
-            fi
           fi
 
           echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
-          echo "fast=$fast" >> "$GITHUB_OUTPUT"
         env:
           GH_TOKEN: ${{ github.token }}
 
       - name: Configure build matrix
         id: set-matrix
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
-            const fast = ${{ steps.set-level.outputs.fast }};
-            console.log(`level: ${level}, fast: ${fast}`);
+            console.log(`level: ${level}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
@@ -157,8 +152,7 @@ jobs:
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -171,19 +165,17 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the
                 //    Linux lake build and adds little value in the merge queue
                 // 3. To run it in release (obviously)
                 // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
                 //    available as an artifact for Grove to use.
-                "enabled": isPr || level != 1 || isPushToMaster,
-                "test": level >= 1,
-                "secondary": level == 0,
+                "check-level": (isPr || isPushToMaster) ? 0 : 2,
+                "secondary": isPr,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -194,10 +186,10 @@ jobs:
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
+                "check-level": 0,
+                "test": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
-                "test": true,
                 // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
                 "test-speedcenter": large && level >= 2,
                 // made explicit until it can be assumed to have propagated to PRs
@@ -206,16 +198,14 @@ jobs:
               {
                 "name": "Linux Reldebug",
                 "os": "ubuntu-latest",
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "CMAKE_PRESET": "reldebug",
               },
               // TODO: suddenly started failing in CI
               /*{
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
                 // exclude seriously slow/problematic tests (laketests crash)
@@ -225,8 +215,7 @@ jobs:
                 "name": "macOS",
                 "os": "macos-15-intel",
                 "release": true,
-                "test": false,  // Tier 2 platform
-                "enabled": level >= 2,
+                "check-level": 2,
                 "shell": "bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@@ -237,7 +226,7 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
+                "os": large && !isPr ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -246,16 +235,14 @@ jobs:
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
                 // See "Linux release" for release job levels; Grove is not a concern here
-                "enabled": isPr || level != 1,
-                "test": level >= 1,
-                "secondary": level == 0,
+                "check-level": isPr ? 0 : 2,
+                "secondary": isPr,
               },
               {
                 "name": "Windows",
-                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -267,8 +254,7 @@ jobs:
                 "os": "nscloud-ubuntu-22.04-arm64-4x16",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -281,7 +267,7 @@ jobs:
               //  "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
               //  "cmultilib": true,
               //  "release": true,
-              //  "enabled": level >= 2,
+              //  "check-level": 2,
               //  "cross": true,
               //  "shell": "bash -euxo pipefail {0}"
               //}
@@ -293,7 +279,7 @@ jobs:
               //   "wasm": true,
               //   "cmultilib": true,
               //   "release": true,
-              //   "enabled": level >= 2,
+              //   "check-level": 2,
               //   "cross": true,
               //   "shell": "bash -euxo pipefail {0}",
               //   // Just a few selected tests because wasm is slow
@@ -307,7 +293,7 @@ jobs:
               }
             }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            matrix = matrix.filter((job) => job["enabled"]);
+            matrix = matrix.filter((job) => level >= job["check-level"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
             core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
 
@@ -317,6 +303,7 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix}}
+      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -332,6 +319,7 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix-secondary}}
+      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -362,7 +350,7 @@ jobs:
         content: |
           A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
     - if: contains(needs.*.result, 'failure')
-      uses: actions/github-script@v8
+      uses: actions/github-script@v7
       with:
         script: |
             core.setFailed('Some jobs failed')
@@ -379,7 +367,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -404,8 +392,6 @@ jobs:
         with:
           # needed for tagging
           fetch-depth: 0
-          # Doesn't seem to be working when additionally fetching from lean4-nightly
-          #filter: tree:0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
       - uses: actions/download-artifact@v5
         with:
@@ -425,7 +411,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/grove.yml

@@ -110,7 +110,7 @@ jobs:
       # material.
       - id: deploy-alias
         if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         name: Compute Alias
         with:
           result-encoding: string

.github/workflows/labels-from-comments.yml

@@ -17,7 +17,7 @@ jobs:
 
     steps:
     - name: Add label based on comment
-      uses: actions/github-script@v8
+      uses: actions/github-script@v7
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |

.github/workflows/pr-body.yml

@@ -11,7 +11,7 @@ jobs:
     steps:
       - name: Check PR body
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const { title, body, labels, draft } = context.payload.pull_request;

.github/workflows/pr-release.yml

@@ -48,17 +48,17 @@ jobs:
           git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
           git -C lean4.git fetch -n origin master
           git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-
+          
           # Create both the original tag and the SHA-suffixed tag
           SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
           SHORT_SHA="${SHORT_SHA:0:7}"
-
+          
           # Export the short SHA for use in subsequent steps
           echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"
 
           git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
           git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-
+          
           git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
@@ -71,7 +71,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -101,7 +101,7 @@ jobs:
 
       - name: Report release status (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             await github.rest.repos.createCommitStatus({
@@ -115,7 +115,7 @@ jobs:
 
       - name: Report release status (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             await github.rest.repos.createCommitStatus({
@@ -129,7 +129,7 @@ jobs:
 
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             await github.rest.issues.addLabels({
@@ -200,7 +200,7 @@ jobs:
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
-
+            
             if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
               echo "force-mathlib-ci label detected, forcing CI despite issues"
               MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
@@ -301,7 +301,7 @@ jobs:
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
-
+            
             if echo "$LABELS" | grep -q "^force-manual-ci$"; then
               echo "force-manual-ci label detected, forcing CI despite issues"
               MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
@@ -368,7 +368,7 @@ jobs:
 
       - name: Report mathlib base
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const description =
@@ -401,7 +401,6 @@ jobs:
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
 
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
@@ -461,7 +460,6 @@ jobs:
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
 
       - name: install elan
         run: |
@@ -532,7 +530,6 @@ jobs:
           token: ${{ secrets.MANUAL_PR_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
 
       - name: Check if tag in reference manual exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'

.github/workflows/pr-title.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR title
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;

.github/workflows/stale.yml

@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v10
+      - uses: actions/stale@v9
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

.gitignore

@@ -20,6 +20,7 @@ tasks.json
 settings.json
 .gdb_history
 .vscode/*
+!.vscode/settings.json
 script/__pycache__
 *.produced.out
 CMakeSettings.json

CODEOWNERS

@@ -7,9 +7,9 @@
 /.github/ @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
-/src/library/compiler/ @hargoniX
+/src/library/compiler/ @zwarich
 /src/lake/ @tydeu
-/src/Lean/Compiler/ @leodemoura @hargoniX
+/src/Lean/Compiler/ @leodemoura @zwarich
 /src/Lean/Data/Lsp/ @mhuisi
 /src/Lean/Elab/Deriving/ @kim-em
 /src/Lean/Elab/Tactic/ @kim-em

doc/dev/ffi.md

@@ -52,7 +52,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
 * `Nat` and `Int` are represented by `lean_object *`.
   Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
-* A universe `Sort u`, type constructor `... → Sort u`, `Void α` or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
+* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
   Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
@@ -141,8 +141,8 @@ void lean_initialize_runtime_module();
 void lean_initialize();
 char ** lean_setup_args(int argc, char ** argv);
 
-lean_object * initialize_A_B(uint8_t builtin);
-lean_object * initialize_C(uint8_t builtin);
+lean_object * initialize_A_B(uint8_t builtin, lean_object *);
+lean_object * initialize_C(uint8_t builtin, lean_object *);
 ...
 
 argv = lean_setup_args(argc, argv); // if using process-related functionality
@@ -152,7 +152,7 @@ lean_initialize_runtime_module();
 lean_object * res;
 // use same default as for Lean executables
 uint8_t builtin = 1;
-res = initialize_A_B(builtin);
+res = initialize_A_B(builtin, lean_io_mk_world());
 if (lean_io_result_is_ok(res)) {
     lean_dec_ref(res);
 } else {
@@ -160,7 +160,7 @@ if (lean_io_result_is_ok(res)) {
     lean_dec(res);
     return ...;  // do not access Lean declarations if initialization failed
 }
-res = initialize_C(builtin);
+res = initialize_C(builtin, lean_io_mk_world());
 if (lean_io_result_is_ok(res)) {
 ...
 

flake.nix

@@ -25,7 +25,6 @@
         } ({
           buildInputs = with pkgs; [
             cmake gmp libuv ccache pkg-config
-            llvmPackages.bintools  # wrapped lld
             llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI

lean.code-workspace

@@ -14,9 +14,6 @@
 		}
 	],
 	"settings": {
-		// Open terminal at root, not current workspace folder
-		// (there is not way to directly refer to the root folder included as `.` above)
-		"terminal.integrated.cwd": "${workspaceFolder:src}/..",
 		"files.insertFinalNewline": true,
 		"files.trimTrailingWhitespace": true,
 		"cmake.buildDirectory": "${workspaceFolder}/build/release",

script/Modulize.lean

@@ -1,30 +1,53 @@
 import Lake.CLI.Main
 
 /-!
-
-Usage: `lean --run script/Modulize.lean [--meta] file1.lean file2.lean ...`
-
-A simple script that inserts `module` and `public section` into un-modulized files and
+A simple script that inserts `module` and `@[expose] public section` into un-modulized files and
 bumps their imports to `public`.
-
-When `--meta` is passed, `public meta section` and `public meta import` is used instead.
 -/
 
 open Lean Parser.Module
 
 def main (args : List String) : IO Unit := do
-  let mut args := args
-  let mut doMeta := false
-  while !args.isEmpty && args[0]!.startsWith "-" do
-    match args[0]! with
-    | "--meta" => doMeta := true
-    | arg => throw <| .userError s!"unknown flag '{arg}'"
-    args := args.tail
+  initSearchPath (← findSysroot)
+  -- the list of root modules
+  let mut mods := args.toArray.map (·.toName)
+
+  if mods.isEmpty then
+    -- Determine default module(s) to run modulize on
+    mods ← try
+      let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
+      let config ← Lake.MonadError.runEIO <| Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
+      let some workspace ← Lake.loadWorkspace config |>.toBaseIO
+        | throw <| IO.userError "failed to load Lake workspace"
+      let defaultTargetModules := workspace.root.defaultTargets.flatMap fun target =>
+        if let some lib := workspace.root.findLeanLib? target then
+          lib.roots
+        else if let some exe := workspace.root.findLeanExe? target then
+          #[exe.config.root]
+        else
+          #[]
+      pure defaultTargetModules
+    catch _ =>
+      pure #[]
+
+  -- Only submodules of `pkg` will be edited or have info reported on them
+  let pkg := mods[0]!.components.head!
+
+  -- Load all the modules
+  let imps := mods.map ({ module := · })
+  let env ← importModules imps {}
+
+  let srcSearchPath ← getSrcSearchPath
+
+  for mod in env.header.moduleNames do
+    if !pkg.isPrefixOf mod then
+      continue
 
-  for path in args do
     -- Parse the input file
+    let some path ← srcSearchPath.findModuleWithExt "lean" mod
+      | throw <| .userError "error: failed to find source file for {mod}"
     let mut text ← IO.FS.readFile path
-    let inputCtx := Parser.mkInputContext text path
+    let inputCtx := Parser.mkInputContext text path.toString
     let (header, parserState, msgs) ← Parser.parseHeader inputCtx
     if !msgs.toList.isEmpty then -- skip this file if there are parse errors
       msgs.forM fun msg => msg.toString >>= IO.println
@@ -34,42 +57,35 @@ def main (args : List String) : IO Unit := do
     if moduleTk?.isSome then
       continue
 
+    let looksMeta := mod.components.any (· ∈ [`Tactic, `Linter])
+
     -- initial whitespace if empty header
     let startPos := header.raw.getPos? |>.getD parserState.pos
 
-    let dummyEnv ← mkEmptyEnvironment
-    let (initCmd, parserState', _) :=
-      Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs
-
-    -- insert section if any trailing command
-    if !initCmd.isOfKind ``Parser.Command.eoi then
-      let insertPos? :=
-          -- put below initial module docstring if any
-          guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|>
-          -- else below header
-          header.raw.getTailPos?
-      let insertPos := insertPos?.getD startPos  -- empty header
-      let mut sec := if doMeta then
+    -- insert section if any trailing text
+    if header.raw.getTrailingTailPos?.all (· < text.endPos) then
+      let insertPos := header.raw.getTailPos? |>.getD startPos  -- empty header
+      let mut sec := if looksMeta then
         "public meta section"
       else
         "@[expose] public section"
       if !imps.isEmpty then
         sec := "\n\n" ++ sec
-      if insertPos?.isNone then
+      if header.raw.getTailPos?.isNone then
         sec := sec ++ "\n\n"
-      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos
+      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.endPos
 
     -- prepend each import with `public `
     for imp in imps.reverse do
       let insertPos := imp.raw.getPos?.get!
-      let prfx := if doMeta then "public meta " else "public "
-      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
+      let prfx := if looksMeta then "public meta " else "public "
+      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.endPos
 
     -- insert `module` header
     let mut initText := text.extract 0 startPos
     if !initText.trim.isEmpty then
       -- If there is a header comment, preserve it and put `module` in the line after
       initText := initText.trimRight ++ "\n"
-    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
+    text := initText ++ "module\n\n" ++ text.extract startPos text.endPos
 
     IO.FS.writeFile path text

script/Shake.lean

@@ -563,14 +563,14 @@ def main (args : List String) : IO UInt32 := do
       if remove.contains mod || seen.contains mod then
         out := out ++ text.extract pos stx.raw.getPos?.get!
         -- We use the end position of the syntax, but include whitespace up to the first newline
-        pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + ⟨1⟩
+        pos := text.findAux (· == '\n') text.endPos stx.raw.getTailPos?.get! + ⟨1⟩
       seen := seen.insert mod
     out := out ++ text.extract pos insertion
     for mod in add do
       if !seen.contains mod then
         seen := seen.insert mod
         out := out ++ s!"{mod}\n"
-    out := out ++ text.extract insertion text.rawEndPos
+    out := out ++ text.extract insertion text.endPos
 
     IO.FS.writeFile path out
     return count + 1

script/release_checklist.py

@@ -1,58 +1,5 @@
 #!/usr/bin/env python3
 
-"""
-Release Checklist for Lean4 and Downstream Repositories
-
-This script validates the status of a Lean4 release across all dependent repositories.
-It checks whether repositories are ready for release and identifies missing steps.
-
-IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior!
-
-What this script does:
-1. Validates preliminary Lean4 release infrastructure:
-   - Checks that the release branch (releases/vX.Y.0) exists
-   - Verifies CMake version settings are correct
-   - Confirms the release tag exists
-   - Validates the release page exists on GitHub (created automatically by CI after tag push)
-   - Checks the release notes page on lean-lang.org (updated while bumping the `reference-manual` repository)
-
-   **IMPORTANT: If the release page doesn't exist, the script will skip checking
-   downstream repositories and the master branch configuration. The preliminary
-   infrastructure must be in place before the release process can proceed.**
-
-   **NOTE: The GitHub release page is created AUTOMATICALLY by CI after the tag is pushed.
-   DO NOT create it manually. Wait for CI to complete after pushing the tag.**
-
-2. For each downstream repository (batteries, mathlib4, etc.):
-   - Checks if dependencies are ready (e.g., mathlib4 depends on batteries)
-   - Verifies the main branch is on the target toolchain (or newer)
-   - Checks if a PR exists to bump the toolchain (if not yet updated)
-   - Validates tags exist for the release version
-   - Ensures tags are merged into stable branches (for non-RC releases)
-   - Verifies bump branches exist and are configured correctly
-   - Special handling for ProofWidgets4 release tags
-
-3. Optionally automates missing steps (when not in --dry-run mode):
-   - Creates missing release tags using push_repo_release_tag.py
-   - Merges tags into stable branches using merge_remote.py
-
-Usage:
-    ./release_checklist.py v4.24.0           # Check release status
-    ./release_checklist.py v4.24.0 --verbose # Show detailed debug info
-    ./release_checklist.py v4.24.0 --dry-run # Check only, don't execute fixes
-
-For automated release management with Claude Code:
-    /release v4.24.0                 # Run full release process with Claude
-
-The script reads repository configurations from release_repos.yml and reports:
-- ✅ for completed requirements
-- ❌ for missing requirements (with instructions to fix)
-- 🟡 for repositories waiting on dependencies
-- ⮕ for automated actions being taken
-
-This script is idempotent and safe to rerun multiple times.
-"""
-
 import argparse
 import yaml
 import requests
@@ -129,39 +76,6 @@ def release_page_exists(repo_url, tag_name, github_token):
     response = requests.get(api_url, headers=headers)
     return response.status_code == 200
 
-def get_tag_workflow_status(repo_url, tag_name, github_token):
-    """Get the status of CI workflows running for a specific tag."""
-    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-
-    # Get workflow runs for the tag
-    # GitHub's workflow runs API uses the branch/tag name in the 'head_branch' field
-    api_url = f"{api_base}/actions/runs?event=push&head_branch={tag_name}"
-    response = requests.get(api_url, headers=headers)
-
-    if response.status_code != 200:
-        return None
-
-    data = response.json()
-    workflow_runs = data.get('workflow_runs', [])
-
-    if not workflow_runs:
-        return None
-
-    # Get the most recent workflow run for this tag
-    run = workflow_runs[0]
-    status = run.get('status')
-    conclusion = run.get('conclusion')
-    workflow_name = run.get('name', 'CI')
-    run_id = run.get('id')
-
-    return {
-        'status': status,
-        'conclusion': conclusion,
-        'workflow_name': workflow_name,
-        'run_id': run_id
-    }
-
 def get_release_notes(tag_name):
     """Fetch release notes page title from lean-lang.org."""
     # Strip -rcX suffix if present for the URL
@@ -170,17 +84,20 @@ def get_release_notes(tag_name):
     try:
         response = requests.get(reference_url)
         response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx)
-
+        
         # Extract title using regex
         match = re.search(r"<title>(.*?)</title>", response.text, re.IGNORECASE | re.DOTALL)
         if match:
             return match.group(1).strip()
         else:
+            print(f"  ⚠️ Could not find <title> tag in {reference_url}")
             return None
-
-    except requests.exceptions.RequestException:
+            
+    except requests.exceptions.RequestException as e:
+        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
         return None
-    except Exception:
+    except Exception as e:
+        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
         return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
@@ -369,68 +286,6 @@ def check_bump_branch_toolchain(url, bump_branch, github_token):
     print(f"  ✅ Bump branch correctly uses toolchain: {content}")
     return True
 
-def get_pr_ci_status(repo_url, pr_number, github_token):
-    """Get the CI status for a pull request."""
-    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-
-    # Get PR details to find the head SHA
-    pr_response = requests.get(f"{api_base}/pulls/{pr_number}", headers=headers)
-    if pr_response.status_code != 200:
-        return "unknown", "Could not fetch PR details"
-
-    pr_data = pr_response.json()
-    head_sha = pr_data['head']['sha']
-
-    # Get check runs for the commit
-    check_runs_response = requests.get(
-        f"{api_base}/commits/{head_sha}/check-runs",
-        headers=headers
-    )
-
-    if check_runs_response.status_code != 200:
-        return "unknown", "Could not fetch check runs"
-
-    check_runs_data = check_runs_response.json()
-    check_runs = check_runs_data.get('check_runs', [])
-
-    if not check_runs:
-        # No check runs, check for status checks (legacy)
-        status_response = requests.get(
-            f"{api_base}/commits/{head_sha}/status",
-            headers=headers
-        )
-        if status_response.status_code == 200:
-            status_data = status_response.json()
-            state = status_data.get('state', 'unknown')
-            if state == 'success':
-                return "success", "All status checks passed"
-            elif state == 'failure':
-                return "failure", "Some status checks failed"
-            elif state == 'pending':
-                return "pending", "Status checks in progress"
-        return "unknown", "No CI checks found"
-
-    # Analyze check runs
-    conclusions = [run['conclusion'] for run in check_runs if run.get('status') == 'completed']
-    in_progress = [run for run in check_runs if run.get('status') in ['queued', 'in_progress']]
-
-    if in_progress:
-        return "pending", f"{len(in_progress)} check(s) in progress"
-
-    if not conclusions:
-        return "pending", "Checks queued"
-
-    if all(c == 'success' for c in conclusions):
-        return "success", f"All {len(conclusions)} checks passed"
-
-    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
-    if failed > 0:
-        return "failure", f"{failed} check(s) failed"
-
-    # Some checks are cancelled, skipped, or neutral
-    return "warning", f"Some checks did not complete normally"
-
 def pr_exists_with_title(repo_url, title, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + "/pulls"
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -549,57 +404,30 @@ def main():
             print(f"  ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.")
             lean4_success = False
 
-    release_page_ready = release_page_exists(lean_repo_url, toolchain, github_token)
-    if not release_page_ready:
-        print(f"  ❌ Release page for {toolchain} does not exist (This will be created by CI.)")
-
-        # Check CI workflow status
-        workflow_status = get_tag_workflow_status(lean_repo_url, toolchain, github_token)
-        if workflow_status:
-            status = workflow_status['status']
-            conclusion = workflow_status['conclusion']
-            workflow_name = workflow_status['workflow_name']
-            run_id = workflow_status['run_id']
-            workflow_url = f"{lean_repo_url}/actions/runs/{run_id}"
-
-            if status == 'in_progress' or status == 'queued':
-                print(f"     🔄 {workflow_name} workflow is {status}: {workflow_url}")
-            elif status == 'completed':
-                if conclusion == 'success':
-                    print(f"     ✅ {workflow_name} workflow completed successfully: {workflow_url}")
-                elif conclusion == 'failure':
-                    print(f"     ❌ {workflow_name} workflow failed: {workflow_url}")
-                else:
-                    print(f"     ⚠️  {workflow_name} workflow completed with status: {conclusion}: {workflow_url}")
-            else:
-                print(f"     ℹ️  {workflow_name} workflow status: {status}: {workflow_url}")
-
+    if not release_page_exists(lean_repo_url, toolchain, github_token):
+        print(f"  ❌ Release page for {toolchain} does not exist")
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-
-    # Check the actual release notes page title (informational only - does not block)
+        
+    # Check the actual release notes page title
     actual_title = get_release_notes(toolchain)
     expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1"
-    base_tag = toolchain.split('-')[0]
-    release_notes_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
 
     if actual_title is None:
-        print(f"  ⚠️  Release notes not found at {release_notes_url} (this will be fixed while updating the reference-manual repository)")
+        # Error already printed by get_release_notes
+        lean4_success = False
     elif not actual_title.startswith(expected_title_prefix):
-        print(f"  ⚠️  Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {release_notes_url}")
+        # Construct URL for the error message (using the base tag)
+        base_tag = toolchain.split('-')[0]
+        check_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
+        print(f"  ❌ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {check_url}")
+        lean4_success = False
     else:
         print(f"  ✅ Release notes page title looks good ('{actual_title}').")
 
     repo_status["lean4"] = lean4_success
 
-    # If the release page doesn't exist, skip repository checks and master branch checks
-    # The preliminary infrastructure must be in place first
-    if not release_page_exists(lean_repo_url, toolchain, github_token):
-        print("\n⚠️  Release process blocked: preliminary Lean4 infrastructure incomplete.")
-        print("   Complete the steps above, then rerun this script to proceed with downstream repositories.")
-        return
-
     # Load repositories and perform further checks
     print("\nChecking repositories...")
 
@@ -643,19 +471,6 @@ def main():
             if pr_info:
                 pr_number, pr_url = pr_info
                 print(f"  ✅ PR with title '{pr_title}' exists: #{pr_number} ({pr_url})")
-
-                # Check CI status
-                ci_status, ci_message = get_pr_ci_status(url, pr_number, github_token)
-                if ci_status == "success":
-                    print(f"     ✅ CI: {ci_message}")
-                elif ci_status == "failure":
-                    print(f"     ❌ CI: {ci_message}")
-                elif ci_status == "pending":
-                    print(f"     🔄 CI: {ci_message}")
-                elif ci_status == "warning":
-                    print(f"     ⚠️  CI: {ci_message}")
-                else:
-                    print(f"     ❓ CI: {ci_message}")
             else:
                 print(f"  ❌ PR with title '{pr_title}' does not exist")
                 print(f"     Run `script/release_steps.py {toolchain} {name}` to create it")

script/release_steps.py

@@ -1,53 +1,30 @@
 #!/usr/bin/env python3
 
 """
-Execute Release Steps for Lean4 Downstream Repositories
+Execute release steps for Lean4 repositories.
 
-This script automates the process of updating a downstream repository to a new Lean4 release.
-It handles creating branches, updating toolchains, merging changes, building, testing, and
-creating pull requests.
-
-IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior!
-
-What this script does:
-1. Sets up the downstream_releases/ directory for cloning repositories
-
-2. Clones or updates the target repository
-
-3. Creates a branch named bump_to_{version} for the changes
-
-4. Updates the lean-toolchain file to the target version
-
-5. Handles repository-specific variations:
-   - Different dependency update mechanisms
-   - Special merging strategies for repositories with nightly-testing branches
-   - Safety checks for repositories using bump branches
-   - Custom build and test procedures
-
-6. Commits the changes with message "chore: bump toolchain to {version}"
-
-7. Builds the project (with a clean .lake cache)
-
-8. Runs tests if available
-
-9. Pushes the branch to GitHub
-
-10. Creates a pull request (or reports if one already exists)
+This script helps automate the release process for Lean4 and its dependent repositories
+by actually executing the step-by-step instructions for updating toolchains, creating tags,
+and managing branches.
 
 Usage:
-    ./release_steps.py v4.24.0 batteries    # Update batteries to v4.24.0
-    ./release_steps.py v4.24.0-rc1 mathlib4 # Update mathlib4 to v4.24.0-rc1
+    python3 release_steps.py <version> <repo>
 
-The script reads repository configurations from release_repos.yml.
-Each repository has specific handling for merging, dependencies, and testing.
+Arguments:
+    version: The version to set in the lean-toolchain file (e.g., v4.6.0)
+    repo: The repository name as specified in release_repos.yml
 
-This script is idempotent - it's safe to rerun if it fails partway through.
-Existing branches, commits, and PRs will be reused rather than duplicated.
+Example:
+    python3 release_steps.py v4.6.0 mathlib4
+    python3 release_steps.py v4.6.0 batteries
 
-Error handling:
-- If build or tests fail, the script continues to create the PR anyway
-- Manual conflicts must be resolved by the user
-- Network issues during push/PR creation are reported with manual instructions
+The script reads repository configurations from release_repos.yml in the same directory.
+Each repository may have specific requirements for:
+- Branch management
+- Toolchain updates
+- Dependency updates
+- Tagging conventions
+- Stable branch handling
 """
 
 import argparse
@@ -589,19 +566,8 @@ def execute_release_steps(repo, version, config):
         
         # Clean lake cache for a fresh build
         print(blue("Cleaning lake cache..."))
-        run_command("lake clean", cwd=repo_path)
-
-        # Check if downstream of Mathlib and get cache if so
-        mathlib_package_dir = repo_path / ".lake" / "packages" / "mathlib"
-        if mathlib_package_dir.exists():
-            print(blue("Project is downstream of Mathlib, fetching cache..."))
-            try:
-                run_command("lake exe cache get", cwd=repo_path, stream_output=True)
-                print(green("Cache fetched successfully"))
-            except subprocess.CalledProcessError as e:
-                print(yellow("Failed to fetch cache, continuing anyway..."))
-                print(yellow(f"Cache fetch error: {e}"))
-
+        run_command("rm -rf .lake", cwd=repo_path)
+        
         try:
             run_command("lake build", cwd=repo_path, stream_output=True)
             print(green("Build completed successfully"))

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 26)
+set(LEAN_VERSION_MINOR 25)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -34,14 +34,7 @@ if (NOT LEAN_PLATFORM_TARGET)
     OUTPUT_VARIABLE LEAN_PLATFORM_TARGET OUTPUT_STRIP_TRAILING_WHITESPACE)
 endif()
 
-set(LEAN_EXTRA_LINKER_FLAGS_DEFAULT "")
-# Use lld by default, if available
-find_program(LLD_PATH lld)
-if(LLD_PATH)
-  string(APPEND LEAN_EXTRA_LINKER_FLAGS_DEFAULT " -fuse-ld=lld")
-endif()
-
-set(LEAN_EXTRA_LINKER_FLAGS ${LEAN_EXTRA_LINKER_FLAGS_DEFAULT} CACHE STRING "Additional flags used by the linker")
+set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker")
 set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler")
 set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests")
 
@@ -89,7 +82,6 @@ option(USE_MIMALLOC "use mimalloc" ON)
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
-option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
 set(LEAN_EXTRA_MAKE_OPTS  ""                           CACHE STRING "extra options to lean --make")
 set(LEANC_CC              ${CMAKE_C_COMPILER}          CACHE STRING "C compiler to use in `leanc`")
@@ -834,13 +826,10 @@ if(LEAN_INSTALL_PREFIX)
   set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
 endif()
 
-
-if (USE_LAKE_CACHE AND STAGE EQUAL 1)
-  set(LAKE_ARTIFACT_CACHE_TOML "true")
-else()
+if (STAGE GREATER 1)
   # The build of stage2+ may depend on local changes made to src/ that are not reflected by the
   # commit hash in stage1/bin/lean, so we make sure to disable the global cache
-  set(LAKE_ARTIFACT_CACHE_TOML "false")
+  string(APPEND LEAN_EXTRA_LAKEFILE_TOML "\n\nenableArtifactCache = false")
 endif()
 
 # Escape for `make`. Yes, twice.

src/Init/BinderNameHint.lean

@@ -7,6 +7,7 @@ Authors: Joachim Breitner
 module
 
 prelude
+public import Init.Prelude
 public import Init.Tactics
 
 public section

src/Init/Control/EState.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Control.State
+public import Init.Control.Except
 public import Init.Data.ToString.Basic
 
 public section

src/Init/Control/Except.lean

@@ -10,6 +10,7 @@ module
 prelude
 public import Init.Control.Basic
 public import Init.Control.Id
+public import Init.Coe
 
 @[expose] public section
 

src/Init/Control/Lawful/Basic.lean

@@ -7,6 +7,8 @@ module
 
 prelude
 public import Init.Ext
+public import Init.SimpLemmas
+public import Init.Meta
 
 public section
 
@@ -250,7 +252,6 @@ instance : LawfulMonad Id := by
 @[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
 @[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
 @[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
-@[simp] theorem pure_run (a : Id α) : pure a.run = a := rfl
 @[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
 @[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl

src/Init/Control/Lawful/Instances.lean

@@ -7,11 +7,14 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
+public import Init.Control.Except
 import all Init.Control.Except
 public import Init.Control.Option
 import all Init.Control.Option
+public import Init.Control.State
 import all Init.Control.State
 public import Init.Control.StateRef
+public import Init.Ext
 
 public section
 

src/Init/Control/Lawful/Lemmas.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
+public import Init.RCases
 public import Init.ByCases
 
 public section

src/Init/Control/Lawful/MonadLift/Instances.lean

@@ -6,13 +6,17 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
+public import Init.Control.Option
 import all Init.Control.Option
+public import Init.Control.Except
 import all Init.Control.Except
 public import Init.Control.ExceptCps
 import all Init.Control.ExceptCps
+public import Init.Control.StateRef
 import all Init.Control.StateRef
 public import Init.Control.StateCps
 import all Init.Control.StateCps
+public import Init.Control.Id
 import all Init.Control.Id
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.Instances

src/Init/Control/Option.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Option.Basic
+public import Init.Control.Basic
 public import Init.Control.Except
 
 public section
@@ -27,7 +28,7 @@ failure occurred.
 /--
 Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
   x
 
@@ -69,7 +70,7 @@ instance {m : Type u → Type v} [Pure m] : Inhabited (OptionT m α) where
 /--
 Recovers from failures. Typically used via the `<|>` operator.
 -/
-@[always_inline, inline, expose] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   match (← x) with
   | some a => pure (some a)
   | _      => y ()
@@ -77,7 +78,7 @@ Recovers from failures. Typically used via the `<|>` operator.
 /--
 A recoverable failure.
 -/
-@[always_inline, inline, expose] protected def fail : OptionT m α := OptionT.mk do
+@[always_inline, inline] protected def fail : OptionT m α := OptionT.mk do
   pure none
 
 instance : Alternative (OptionT m) where
@@ -90,7 +91,7 @@ Converts a computation from the underlying monad into one that could fail, even
 This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
 lifting](lean-manual://section/monad-lifting).
 -/
-@[always_inline, inline, expose] protected def lift (x : m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline] protected def lift (x : m α) : OptionT m α := OptionT.mk do
   return some (← x)
 
 instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
@@ -100,11 +101,11 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
 /--
 Handles failures by treating them as exceptions of type `Unit`.
 -/
-@[always_inline, inline, expose] protected def tryCatch (x : OptionT m α) (handle : PUnit → OptionT m α) : OptionT m α := OptionT.mk do
-  let some a ← x | handle ⟨⟩
+@[always_inline, inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
+  let some a ← x | handle ()
   pure <| some a
 
-instance : MonadExceptOf PUnit (OptionT m) where
+instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 

src/Init/Control/Reader.lean

@@ -8,6 +8,8 @@ The Reader monad transformer for passing immutable State.
 module
 
 prelude
+public import Init.Control.Basic
+public import Init.Control.Id
 public import Init.Control.Except
 
 public section

src/Init/Control/State.lean

@@ -8,6 +8,8 @@ The State monad transformer.
 module
 
 prelude
+public import Init.Control.Basic
+public import Init.Control.Id
 public import Init.Control.Except
 
 public section

src/Init/Core.lean

@@ -8,6 +8,7 @@ notation, basic datatypes and type classes
 module
 
 prelude
+public meta import Init.Prelude
 public import Init.SizeOf
 
 public section

src/Init/Data/AC.lean

@@ -7,6 +7,7 @@ Authors: Dany Fabian
 module
 
 prelude
+public import Init.Classical
 public import Init.ByCases
 
 @[expose] public section

src/Init/Data/Array/Attach.lean

@@ -6,7 +6,10 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
+public import Init.Data.Array.Mem
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Count
+public import Init.Data.List.Attach
 import all Init.Data.List.Attach
 
 public section

src/Init/Data/Array/Basic.lean

@@ -6,6 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.WFTactics
+public import Init.Data.Nat.Basic
+public import Init.Data.Fin.Basic
+public import Init.Data.UInt.BasicAux
 public import Init.GetElem
 public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
@@ -748,7 +752,8 @@ of results.
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
   -- Note: we cannot use `foldlM` here for the reference implementation because this calls
   -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
-  let rec map (i : Nat) (bs : Array β) : m (Array β) := do
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    map (i : Nat) (bs : Array β) : m (Array β) := do
       if hlt : i < as.size then
         map (i+1) (bs.push (← f as[i]))
       else
@@ -908,7 +913,8 @@ entire array is checked.
 @[implemented_by anyMUnsafe, expose]
 def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
   let any (stop : Nat) (h : stop ≤ as.size) :=
-    let rec loop (j : Nat) : m Bool := do
+    let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    loop (j : Nat) : m Bool := do
       if hlt : j < stop then
         have : j < as.size := Nat.lt_of_lt_of_le hlt h
         if (← p as[j]) then
@@ -1246,7 +1252,8 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -1263,7 +1270,8 @@ Examples:
 -/
 @[inline]
 def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some ⟨j, h⟩ else loop (j + 1)
     else none
@@ -1299,6 +1307,7 @@ Examples:
 @[inline, expose]
 def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def idxOfAux [BEq α] (xs : Array α) (v : α) (i : Nat) : Option (Fin xs.size) :=
   if h : i < xs.size then
     if xs[i] == v then some ⟨i, h⟩
@@ -1708,6 +1717,7 @@ Examples:
  * `#[3, 2, 3, 4].popWhile (· > 2) = #[3, 2]`
  * `(#[] : Array Nat).popWhile (· > 2) = #[]`
 -/
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
     if p (as[as.size - 1]'(Nat.sub_lt h (by decide))) then
@@ -1732,7 +1742,8 @@ Examples:
  * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]`
 -/
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec go (i : Nat) (acc : Array α) : Array α :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  go (i : Nat) (acc : Array α) : Array α :=
     if h : i < as.size then
       let a := as[i]
       if p a then
@@ -1755,6 +1766,7 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]`
 -/
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def eraseIdx (xs : Array α) (i : Nat) (h : i < xs.size := by get_elem_tactic) : Array α :=
   if h' : i + 1 < xs.size then
     let xs' := xs.swap (i + 1) i
@@ -1849,7 +1861,8 @@ Examples:
  * `#["tues", "thur", "sat"].insertIdx 3 "wed" = #["tues", "thur", "sat", "wed"]`
 -/
 @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
-  let rec loop (as : Array α) (j : Fin as.size) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (as : Array α) (j : Fin as.size) :=
     if i < j then
       let j' : Fin as.size := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
@@ -1903,6 +1916,7 @@ def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
   else
     as
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -1931,7 +1945,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[specialize]
+@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
 def zipWithMAux {m : Type v → Type w} [Monad m] (as : Array α) (bs : Array β) (f : α → β → m γ) (i : Nat) (cs : Array γ) : m (Array γ) := do
   if h : i < as.size then
     let a := as[i]
@@ -2094,6 +2108,7 @@ private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat),
     have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
     a != as[i] && allDiffAuxAux as a i this
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   if h : i < as.size then
     allDiffAuxAux as as[i] i h && allDiffAux as (i+1)

src/Init/Data/Array/BasicAux.lean

@@ -6,8 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Nat.Linear
+public import Init.NotationExtra
 
 public section
 

src/Init/Data/Array/BinSearch.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 public import Init.Data.Int.DivMod.Lemmas
+public import Init.Omega
 
 public section
 universe u v

src/Init/Data/Array/Bootstrap.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 
 public section

src/Init/Data/Array/Count.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Count

src/Init/Data/Array/DecidableEq.lean

@@ -6,9 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.BEq
 public import Init.Data.List.Nat.BEq
+public import Init.ByCases
 
 public section
 

src/Init/Data/Array/Erase.lean

@@ -6,8 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Erase
+public import Init.Data.List.Nat.Basic
 
 public section
 

src/Init/Data/Array/Extract.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
 
 public section
 

src/Init/Data/Array/FinRange.lean

@@ -6,6 +6,7 @@ Authors: François G. Dorais
 module
 
 prelude
+public import Init.Data.List.FinRange
 public import Init.Data.Array.OfFn
 
 public section

src/Init/Data/Array/Find.lean

@@ -7,7 +7,10 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Attach
 public import Init.Data.Array.Range
 
 public section

src/Init/Data/Array/InsertIdx.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.InsertIdx
 
 public section
 

src/Init/Data/Array/Lemmas.lean

@@ -6,10 +6,17 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
+public import Init.Data.Nat.Lemmas
+public import Init.Data.List.Range
+public import Init.Data.List.Nat.TakeDrop
+public import Init.Data.List.Nat.Modify
 public import Init.Data.List.Nat.Basic
+public import Init.Data.List.Monadic
+public import Init.Data.List.OfFn
 public import Init.Data.Array.Mem
 public import Init.Data.Array.DecidableEq
 public import Init.Data.Range.Lemmas
+public import Init.TacticsExtra
 public import Init.Data.List.ToArray
 import all Init.Data.List.Control
 import all Init.Data.Array.Basic
@@ -3754,7 +3761,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
 -- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
 grind_pattern contains_iff_exists_mem_beq => xs.contains a
 
-@[grind =]
+@[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp

src/Init/Data/Array/Lex/Basic.lean

@@ -6,6 +6,9 @@ Author: Kim Morrison
 module
 
 prelude
+public import Init.Core
+import Init.Data.Array.Basic
+import Init.Data.Nat.Lemmas
 public import Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Iterators.Consumers

src/Init/Data/Array/Lex/Lemmas.lean

@@ -10,7 +10,9 @@ import all Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Lex
+import Init.Data.Range.Polymorphic.Lemmas
 import Init.Data.Range.Polymorphic.NatLemmas
+import Init.Data.Order.Lemmas
 
 public section
 

src/Init/Data/Array/MapIdx.lean

@@ -6,7 +6,10 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Attach
 public import Init.Data.Array.OfFn
 public import Init.Data.List.MapIdx
 import all Init.Data.List.MapIdx

src/Init/Data/Array/Mem.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
+public import Init.Data.Array.Basic
+public import Init.Data.Nat.Linear
 public import Init.Data.List.BasicAux
 
 public section

src/Init/Data/Array/Monadic.lean

@@ -6,9 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Control
 import all Init.Data.List.Control
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
+public import Init.Data.List.Monadic
 
 public section
 

src/Init/Data/Array/OfFn.lean

@@ -6,8 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Monadic
+public import Init.Data.List.OfFn
 public import Init.Data.List.FinRange
 
 public section

src/Init/Data/Array/Perm.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Nat.Perm
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 

src/Init/Data/Array/Range.lean

@@ -6,10 +6,14 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.OfFn
 import all Init.Data.Array.OfFn
 public import Init.Data.Array.MapIdx
 public import Init.Data.Array.Zip
+public import Init.Data.List.Nat.Range
 
 public section
 

src/Init/Data/Array/Subarray.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.GetElem
 public import Init.Data.Array.Basic
 import Init.Data.Array.GetLit
 public import Init.Data.Slice.Basic

src/Init/Data/Array/Subarray/Split.lean

@@ -7,6 +7,7 @@ Authors: David Thrane Christiansen
 module
 
 prelude
+public import Init.Data.Array.Basic
 public import Init.Data.Array.Subarray
 import all Init.Data.Array.Subarray
 public import Init.Omega

src/Init/Data/Array/TakeDrop.lean

@@ -6,8 +6,10 @@ Authors: Markus Himmel
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
 
 public section
 

src/Init/Data/Array/Zip.lean

@@ -6,8 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.TakeDrop
+public import Init.Data.List.Zip
 
 public section
 

src/Init/Data/Basic.lean

@@ -6,5 +6,13 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Nat.Basic
+public import Init.Data.Fin.Basic
+public import Init.Data.List.Basic
+public import Init.Data.Char.Basic
+public import Init.Data.String.Basic
+public import Init.Data.Option.Basic
 public import Init.Data.UInt
+public import Init.Data.Repr
+public import Init.Data.ToString.Basic
 public import Init.Data.String.Extra

src/Init/Data/BitVec/Basic.lean

@@ -6,8 +6,11 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
+public import Init.Data.Fin.Basic
 public import Init.Data.Nat.Bitwise.Lemmas
+public import Init.Data.Nat.Power2
 public import Init.Data.Int.Bitwise.Basic
+public import Init.Data.BitVec.BasicAux
 
 @[expose] public section
 

src/Init/Data/BitVec/Bitblast.lean

@@ -6,11 +6,16 @@ Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 module
 
 prelude
+public import Init.Data.Nat.Bitwise.Basic
 import all Init.Data.Nat.Bitwise.Basic
+public import Init.Data.Nat.Mod
 public import Init.Data.Int.DivMod
 import all Init.Data.Int.DivMod
+public import Init.Data.Int.LemmasAux
+public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Decidable
+public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
 import Init.BinderPredicates
 

src/Init/Data/BitVec/Folds.lean

@@ -6,8 +6,10 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
+public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Lemmas
+public import Init.Data.Nat.Lemmas
 public import Init.Data.Fin.Iterate
 
 public section

src/Init/Data/BitVec/Lemmas.lean

@@ -6,14 +6,25 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B
 module
 
 prelude
+public import Init.Data.Bool
+public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
+public import Init.Data.BitVec.BasicAux
 import all Init.Data.BitVec.BasicAux
 public import Init.Data.Fin.Lemmas
+public import Init.Data.Nat.Lemmas
+public import Init.Data.Nat.Div.Lemmas
+public import Init.Data.Nat.Mod
+public import Init.Data.Nat.Div.Lemmas
 public import Init.Data.Int.Bitwise.Lemmas
 public import Init.Data.Int.LemmasAux
+public import Init.Data.Int.Pow
+public import Init.Data.Int.LemmasAux
 public import Init.Data.BitVec.Bootstrap
+public import Init.Data.Order.Factories
 public import Init.Data.List.BasicAux
 import Init.Data.List.Lemmas
+import Init.Data.BEq
 
 public section
 
@@ -3742,9 +3753,6 @@ theorem neg_add {x y : BitVec w} : - (x + y) = - x - y := by
   apply eq_of_toInt_eq
   simp [toInt_neg, toInt_add, Int.neg_add, Int.add_neg_eq_sub]
 
-theorem sub_sub (a b c : BitVec n) : a - b - c = a - (b + c) := by
-  simp [BitVec.sub_eq_add_neg, BitVec.add_assoc, BitVec.neg_add]
-
 theorem add_neg_eq_sub {x y : BitVec w} : x + - y = (x - y) := by
   apply eq_of_toInt_eq
   simp [toInt_neg, Int.sub_eq_add_neg]

src/Init/Data/ByteArray/Basic.lean

@@ -6,8 +6,11 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.DecidableEq
 public import Init.Data.UInt.Basic
+public import Init.Data.UInt.BasicAux
 import all Init.Data.UInt.BasicAux
+public import Init.Data.Option.Basic
 public import Init.Data.Array.Extract
 
 set_option doc.verso true

src/Init/Data/ByteArray/Bootstrap.lean

@@ -6,6 +6,7 @@ Author: Markus Himmel
 module
 
 prelude
+public import Init.Prelude
 public import Init.Data.List.Basic
 
 public section

src/Init/Data/ByteArray/Lemmas.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
+public import Init.Data.Array.Extract
 
 public section
 
@@ -256,19 +257,3 @@ theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : B
       dest.extract 0 destOff ++ src.extract srcOff (srcOff +len) ++ dest.extract (destOff + min len (src.data.size - srcOff)) dest.data.size := by
   ext1
   simp [copySlice]
-
-@[simp]
-theorem ByteArray.data_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} :
-    (as.set i a h).data = as.data.set i a (by simpa) := by
-  simp [set]
-
-theorem ByteArray.set_eq_push_extract_append_extract {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} :
-    as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size := by
-  ext1
-  simpa using Array.set_eq_push_extract_append_extract _
-
-@[simp]
-theorem ByteArray.append_toByteArray_singleton {as : ByteArray} {a : UInt8} :
-    as ++ [a].toByteArray = as.push a := by
-  ext1
-  simp

src/Init/Data/Char/Lemmas.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Char.Basic
 import all Init.Data.Char.Basic
 public import Init.Data.UInt.Lemmas
 

src/Init/Data/Dyadic/Basic.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.Rat.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
-import Init.Hints
+import Init.Data.Int.DivMod.Lemmas
 
 /-!
 # The dyadic rationals

src/Init/Data/Dyadic/Instances.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Dyadic.Basic
+public import Init.Grind.Ring.Basic
 public import Init.Grind.Ordered.Ring
 
 /-! # Internal `grind` algebra instances for `Dyadic`. -/

src/Init/Data/Dyadic/Inv.lean

@@ -5,6 +5,7 @@ Authors: Kim Morrison
 -/
 module
 prelude
+import Init.Data.Dyadic.Basic
 import Init.Data.Dyadic.Round
 import Init.Grind.Ordered.Ring
 

src/Init/Data/Dyadic/Round.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Dyadic.Basic
 import all Init.Data.Dyadic.Instances
+import Init.Data.Int.Bitwise.Lemmas
 import Init.Grind.Ordered.Rat
 import Init.Grind.Ordered.Field
 

src/Init/Data/Fin/Bitwise.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Nat.Bitwise
+public import Init.Data.Fin.Basic
 
 public section
 

src/Init/Data/Fin/Fold.lean

@@ -6,6 +6,7 @@ Authors: François G. Dorais
 module
 
 prelude
+public import Init.Data.Nat.Linear
 public import Init.Control.Lawful.Basic
 public import Init.Data.Fin.Lemmas
 
@@ -22,7 +23,7 @@ Example:
 -/
 @[inline] def foldl (n) (f : α → Fin n → α) (init : α) : α := loop init 0 where
   /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
-  @[specialize] loop (x : α) (i : Nat) : α :=
+  @[semireducible, specialize] loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
   termination_by n - i
 
@@ -33,7 +34,7 @@ and nesting to the right.
 Example:
  * `Fin.foldr 3 (·.val + ·) (0 : Nat) = (0 : Fin 3).val + ((1 : Fin 3).val + ((2 : Fin 3).val + 0))`
 -/
-@[inline, expose] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop n (Nat.le_refl n) init where
+@[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop n (Nat.le_refl n) init where
   /-- Inner loop for `Fin.foldr`. `Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))`  -/
   @[specialize] loop : (i : _) → i ≤ n → α → α
   | 0, _, x => x
@@ -64,7 +65,7 @@ Fin.foldlM n f x₀ = do
     pure xₙ
   ```
   -/
-  @[specialize] loop (x : α) (i : Nat) : m α := do
+  @[semireducible, specialize] loop (x : α) (i : Nat) : m α := do
     if h : i < n then f x ⟨i, h⟩ >>= (loop · (i+1)) else pure x
   termination_by n - i
   decreasing_by decreasing_trivial_pre_omega
@@ -95,7 +96,7 @@ Fin.foldrM n f xₙ = do
     pure x₀
   ```
   -/
-  @[specialize] loop : {i // i ≤ n} → α → m α
+  @[semireducible, specialize] loop : {i // i ≤ n} → α → m α
   | ⟨0, _⟩, x => pure x
   | ⟨i+1, h⟩, x => f ⟨i, h⟩ x >>= loop ⟨i, Nat.le_of_lt h⟩
 

src/Init/Data/Fin/Iterate.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.PropLemmas
+public import Init.Data.Fin.Basic
 
 public section
 

src/Init/Data/Fin/Lemmas.lean

@@ -8,9 +8,13 @@ module
 prelude
 public import Init.Data.Nat.Lemmas
 public import Init.Ext
+public import Init.ByCases
+public import Init.Conv
+public import Init.Omega
+public import Init.Data.Order.Factories
 import Init.Data.Order.Lemmas
 
-@[expose] public section
+public section
 
 open Std
 
@@ -911,21 +915,16 @@ theorem exists_fin_succ {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨
   ⟨fun ⟨i, h⟩ => Fin.cases Or.inl (fun i hi => Or.inr ⟨i, hi⟩) i h, fun h =>
     (h.elim fun h => ⟨0, h⟩) fun ⟨i, hi⟩ => ⟨i.succ, hi⟩⟩
 
-@[simp] theorem forall_fin_zero {p : Fin 0 → Prop} : (∀ i, p i) ↔ True :=
-  ⟨fun _ => trivial, fun _ ⟨_, h⟩ => False.elim <| Nat.not_lt_zero _ h⟩
-
-@[simp] theorem exists_fin_zero {p : Fin 0 → Prop} : (∃ i, p i) ↔ False := by simp
-
-@[simp] theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 :=
+theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 :=
   ⟨fun h => h _, fun h i => Subsingleton.elim i 0 ▸ h⟩
 
-@[simp] theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 :=
+theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 :=
   ⟨fun ⟨i, h⟩ => Subsingleton.elim i 0 ▸ h, fun h => ⟨_, h⟩⟩
 
-@[simp] theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 :=
+theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 :=
   forall_fin_succ.trans <| and_congr_right fun _ => forall_fin_one
 
-@[simp] theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
+theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
   exists_fin_succ.trans <| or_congr_right exists_fin_one
 
 theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by

src/Init/Data/Float.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Core
+public import Init.Data.Int.Basic
 public import Init.Data.ToString.Basic
 
 public section

src/Init/Data/Float32.lean

@@ -6,6 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Core
+public import Init.Data.Int.Basic
+public import Init.Data.ToString.Basic
 public import Init.Data.Float
 
 public section

src/Init/Data/FloatArray/Basic.lean

@@ -6,7 +6,9 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 public import Init.Data.Float
+public import Init.Data.Option.Basic
 import Init.Ext
 public import Init.Data.Array.DecidableEq
 

src/Init/Data/Format/Basic.lean

@@ -170,7 +170,7 @@ private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult
   | text s,       flatten, _, _ =>
     let p := String.Internal.posOf s '\n'
     let off := String.Internal.offsetOfPos s p
-    { foundLine := p != s.rawEndPos, foundFlattenedHardLine := flatten && p != s.rawEndPos, space := off }
+    { foundLine := p != s.endPos, foundFlattenedHardLine := flatten && p != s.endPos, space := off }
   | append f₁ f₂, flatten, m, w => merge w (spaceUptoLine f₁ flatten m w) (spaceUptoLine f₂ flatten m)
   | nest n f,     flatten, m, w => spaceUptoLine f flatten (m - n) w
   | group f _,    _,       m, w => spaceUptoLine f true m w
@@ -264,14 +264,14 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
     | nest n f => be w (gs' ({ i with f, indent := i.indent + n }::is))
     | text s =>
       let p := String.Internal.posOf s '\n'
-      if p == s.rawEndPos then
+      if p == s.endPos then
         pushOutput s
         endTags i.activeTags
         be w (gs' is)
       else
         pushOutput (String.Internal.extract s {} p)
         pushNewline i.indent.toNat
-        let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.rawEndPos) }::is
+        let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.endPos) }::is
         -- after a hard line break, re-evaluate whether to flatten the remaining group
         -- note that we shouldn't start flattening after a hard break outside a group
         if g.fla == .disallow then
@@ -411,6 +411,7 @@ Renders a `Format` to a string.
 * `column`: begin the first line wrap `column` characters earlier than usual
   (this is useful when the output String will be printed starting at `column`)
 -/
+@[export lean_format_pretty]
 def pretty (f : Format) (width : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
   let act : StateM State Unit := prettyM f width indent
   State.out <| act (State.mk "" column) |>.snd

src/Init/Data/Format/Instances.lean

@@ -6,7 +6,9 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Format.Basic
 public import Init.Data.Array.Basic
+public import Init.Data.ToString.Basic
 import Init.Data.String.Basic
 
 public section

src/Init/Data/Format/Syntax.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Format.Macro
 public import Init.Data.Format.Instances
 public import Init.Meta
+import Init.Data.String.Basic
 import Init.Data.ToString.Name
 
 public section

src/Init/Data/Function.lean

@@ -5,6 +5,7 @@ Authors: Kim Morrison
 -/
 module
 prelude
+public import Init.Core
 public import Init.Grind.Tactics
 public section
 namespace Function

src/Init/Data/Hashable.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.UInt.Basic
 public import Init.Data.String.Basic
+public import Init.Data.ByteArray.Basic
 
 public section
 universe u

src/Init/Data/Int/Basic.lean

@@ -313,7 +313,7 @@ the logical model.
 Examples:
  * `(7 : Int).natAbs = 7`
  * `(0 : Int).natAbs = 0`
- * `(-11 : Int).natAbs = 11`
+ * `((-11 : Int).natAbs = 11`
 -/
 @[extern "lean_nat_abs", expose]
 def natAbs (m : @& Int) : Nat :=

src/Init/Data/Int/Cooper.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Int.DivMod.Lemmas
 public import Init.Data.Int.Gcd
 
 public section

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -6,7 +6,13 @@ Authors: Jeremy Avigad, Mario Carneiro, Kim Morrison, Markus Himmel
 module
 
 prelude
+public import Init.Data.Int.DivMod.Bootstrap
+public import Init.Data.Nat.Lemmas
 public import Init.Data.Nat.Div.Lemmas
+public import Init.Data.Int.Order
+public import Init.Data.Int.Lemmas
+public import Init.Data.Nat.Dvd
+public import Init.RCases
 import Init.TacticsExtra
 
 public section

src/Init/Data/Int/Gcd.lean

@@ -6,6 +6,8 @@ Authors: Mario Carneiro, Markus Himmel
 module
 
 prelude
+public import Init.Data.Int.Basic
+public import Init.Data.Nat.Gcd
 public import Init.Data.Nat.Lcm
 public import Init.Data.Int.DivMod.Lemmas
 public import Init.Data.Int.Pow

src/Init/Data/Int/Lemmas.lean

@@ -6,6 +6,8 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module
 
 prelude
+public import Init.Conv
+public import Init.NotationExtra
 public import Init.PropLemmas
 
 public section

src/Init/Data/Int/LemmasAux.lean

@@ -6,7 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Int.Order
 public import Init.Data.Int.Pow
+public import Init.Omega
 
 public section
 

src/Init/Data/Int/Linear.lean

@@ -6,9 +6,15 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.ByCases
+public import Init.Data.Prod
+public import Init.Data.Int.Lemmas
 public import Init.Data.Int.LemmasAux
+public import Init.Data.Int.DivMod.Bootstrap
 public import Init.Data.Int.Cooper
+public import Init.Data.Int.Gcd
 import all Init.Data.Int.Gcd
+public import Init.Data.RArray
 public import Init.Data.AC
 import all Init.Data.AC
 import Init.LawfulBEqTactics

src/Init/Data/Int/OfNat.lean

@@ -6,8 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Int.Lemmas
+public import Init.Data.Int.DivMod
 public import Init.Data.Int.Linear
 public import Init.GrindInstances.ToInt
+public import Init.Data.RArray
 
 public section
 

src/Init/Data/Int/Order.lean

@@ -605,9 +605,6 @@ theorem natAbs_of_nonneg {a : Int} (H : 0 ≤ a) : (natAbs a : Int) = a :=
   match a, eq_ofNat_of_zero_le H with
   | _, ⟨_, rfl⟩ => rfl
 
-theorem ofNat_natAbs_of_nonneg {a : Int} (h : 0 ≤ a) : (natAbs a : Int) = a :=
-  natAbs_of_nonneg h
-
 theorem ofNat_natAbs_of_nonpos {a : Int} (H : a ≤ 0) : (natAbs a : Int) = -a := by
   rw [← natAbs_neg, natAbs_of_nonneg (Int.neg_nonneg_of_nonpos H)]
 

src/Init/Data/Int/Pow.lean

@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module
 
 prelude
+public import Init.Data.Int.Lemmas
 public import Init.Data.Nat.Lemmas
 
 public section

src/Init/Data/Iterators/Basic.lean

@@ -6,83 +6,24 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Core
 public import Init.Classical
 public import Init.Ext
-
-set_option doc.verso true
+public import Init.NotationExtra
+public import Init.TacticsExtra
 
 public section
 
 /-!
-# Definition of iterators
+### Definition of iterators
 
 This module defines iterators and what it means for an iterator to be finite and productive.
 -/
 
 namespace Std
 
-private opaque Internal.idOpaque {α} : { f : α → α // f = id } := ⟨id, rfl⟩
-
-/--
-Currently, {lean}`Shrink α` is just a wrapper around {lean}`α`.
-
-In the future, {name}`Shrink` should allow shrinking {lean}`α` into a potentially smaller universe,
-given a proof that {name}`α` is actually small, just like Mathlib's {lit}`Shrink`, except that
-the latter's conversion functions are noncomputable. Until then, {lean}`Shrink α` is always in the
-same universe as {name}`α`.
-
-This no-op type exists so that fewer breaking changes will be needed when the
-real {lit}`Shrink` type is available and the iterators will be made more flexible with regard to
-universes.
-
-The conversion functions {name (scope := "Init.Data.Iterators.Basic")}`Shrink.deflate` and
-{name (scope := "Init.Data.Iterators.Basic")}`Shrink.inflate` form an equivalence between
-{name}`α` and {lean}`Shrink α`, but this equivalence is intentionally not definitional.
--/
-public def Shrink (α : Type u) : Type u := Internal.idOpaque.1 α
-
-/-- Converts elements of {name}`α` into elements of {lean}`Shrink α`. -/
-@[always_inline]
-public def Shrink.deflate {α} (x : α) : Shrink α :=
-  cast (by simp [Shrink, Internal.idOpaque.property]) x
-
-/-- Converts elements of {lean}`Shrink α` into elements of {name}`α`. -/
-@[always_inline]
-public def Shrink.inflate {α} (x : Shrink α) : α :=
-  cast (by simp [Shrink, Internal.idOpaque.property]) x
-
-@[simp, grind =]
-public theorem Shrink.deflate_inflate {α} {x : Shrink α} :
-    Shrink.deflate x.inflate = x := by
-  simp [deflate, inflate]
-
-@[simp, grind =]
-public theorem Shrink.inflate_deflate {α} {x : α} :
-    (Shrink.deflate x).inflate = x := by
-  simp [deflate, inflate]
-
-public theorem Shrink.inflate_inj {α} {x y : Shrink α} :
-    x.inflate = y.inflate ↔ x = y := by
-  apply Iff.intro
-  · intro h
-    simpa using congrArg Shrink.deflate h
-  · rintro rfl
-    rfl
-
-public theorem Shrink.deflate_inj {α} {x y : α} :
-    Shrink.deflate x = Shrink.deflate y ↔ x = y := by
-  apply Iff.intro
-  · intro h
-    simpa using congrArg Shrink.inflate h
-  · rintro rfl
-    rfl
-
 namespace Iterators
 
--- It is not fruitful to move the following docstrings to verso right now because there are lots of
--- forward references that cannot be realized nicely.
-set_option doc.verso false
-
 /--
 An iterator that sequentially emits values of type `β` in the monad `m`. It may be finite
 or infinite.
@@ -241,16 +182,6 @@ def IterStep.successor : IterStep α β → Option α
   | .skip it => some it
   | .done => none
 
-@[simp]
-theorem IterStep.successor_yield {it : α} {out : β} :
-  (IterStep.yield it out).successor = some it := rfl
-
-@[simp]
-theorem IterStep.successor_skip {it : α} : (IterStep.skip (β := β) it).successor = some it := rfl
-
-@[simp]
-theorem IterStep.successor_done : (IterStep.done (α := α) (β := β)).successor = none := rfl
-
 /--
 If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
 with the result of the application of `f`.
@@ -353,7 +284,7 @@ step object is bundled with a proof that it is a "plausible" step for the given
 -/
 class Iterator (α : Type w) (m : Type w → Type w') (β : outParam (Type w)) where
   IsPlausibleStep : IterM (α := α) m β → IterStep (IterM (α := α) m β) β → Prop
-  step : (it : IterM (α := α) m β) → m (Shrink <| PlausibleIterStep <| IsPlausibleStep it)
+  step : (it : IterM (α := α) m β) → m (PlausibleIterStep <| IsPlausibleStep it)
 
 section Monadic
 
@@ -427,7 +358,7 @@ the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
 -/
 @[always_inline, inline, expose]
 def IterM.step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
+    (it : IterM (α := α) m β) : m it.Step :=
   Iterator.step it
 
 end Monadic
@@ -553,10 +484,6 @@ def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
     (it' it : Iter (α := α) β) : Prop :=
   it'.toIterM.IsPlausibleSuccessorOf it.toIterM
 
-theorem Iter.isPlausibleSuccessorOf_eq_invImage {α : Type w} {β : Type w} [Iterator α Id β] :
-    IsPlausibleSuccessorOf (α := α) (β := β) =
-      InvImage (IterM.IsPlausibleSuccessorOf (α := α) (β := β) (m := Id)) Iter.toIterM := rfl
-
 theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iterator α Id β]
     {it' it : Iter (α := α) β} :
     it'.IsPlausibleSuccessorOf it ↔ ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step := by
@@ -569,16 +496,6 @@ theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iter
     exact ⟨step.mapIterator Iter.toIterM,
       by cases step <;> simp_all [IterStep.successor, Iter.IsPlausibleStep]⟩
 
-theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_yield {α : Type w} {β : Type w}
-    [Iterator α Id β] {it' it : Iter (α := α) β} {out : β}
-    (h : it.IsPlausibleStep (.yield it' out)) : it'.IsPlausibleSuccessorOf it := by
-  simpa [isPlausibleSuccessorOf_iff_exists] using ⟨.yield it' out, by simp [h]⟩
-
-theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_skip {α : Type w} {β : Type w}
-    [Iterator α Id β] {it' it : Iter (α := α) β} (h : it.IsPlausibleStep (.skip it')) :
-    it'.IsPlausibleSuccessorOf it := by
-  simpa [isPlausibleSuccessorOf_iff_exists] using ⟨.skip it', by simp [h]⟩
-
 /--
 Asserts that a certain iterator `it` could plausibly yield the value `out` after an arbitrary
 number of steps.
@@ -665,7 +582,7 @@ the termination measures `it.finitelyManySteps` and `it.finitelyManySkips`.
 -/
 @[always_inline, inline, expose]
 def Iter.step {α β : Type w} [Iterator α Id β] (it : Iter (α := α) β) : it.Step :=
-  it.toIterM.step.run.inflate.toPure
+  it.toIterM.step.run.toPure
 
 end Pure
 
@@ -680,10 +597,6 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
 class Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
   wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
 
-theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
-    WellFounded (Iter.IsPlausibleSuccessorOf (α := α)) := by
-  simpa [Iter.isPlausibleSuccessorOf_eq_invImage] using InvImage.wf _ Finite.wf
-
 /--
 This type is a wrapper around `IterM` so that it becomes a useful termination measure for
 recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.finitelyManySteps`.
@@ -733,12 +646,6 @@ theorem IterM.TerminationMeasures.Finite.rel_of_skip
     Rel ⟨it'⟩ ⟨it⟩ := by
   exact .single ⟨_, rfl, h⟩
 
-theorem IterM.TerminationMeasures.Finite.rel_trans
-    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
-    {it it' it'' : TerminationMeasures.Finite α m} :
-    it.Rel it' → it'.Rel it'' → it.Rel it'' :=
-  .trans
-
 macro_rules | `(tactic| decreasing_trivial) => `(tactic|
   first
   | exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›

src/Init/Data/Iterators/Combinators.lean

@@ -8,5 +8,4 @@ module
 prelude
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
-public import Init.Data.Iterators.Combinators.FlatMap
 public import Init.Data.Iterators.Combinators.ULift

src/Init/Data/Iterators/Combinators/FlatMap.lean

@@ -1,53 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Iterators.Combinators.FilterMap
-public import Init.Data.Iterators.Combinators.Monadic.FlatMap
-
-set_option doc.verso true
-
-/-!
-# {lit}`flatMap` combinator
-
-This file provides the {lit}`flatMap` iterator combinator and variants of it.
-
-If {lit}`it` is any iterator, {lit}`it.flatMap f` maps each output of {lit}`it` to an iterator using
-{lit}`f`.
-
-{lit}`it.flatMap f` first emits all outputs of the first obtained iterator, then of the second,
-and so on. In other words, {lit}`it` flattens the iterator of iterators obtained by mapping with
-{lit}`f`.
--/
-
-namespace Std.Iterators
-
-@[always_inline, inherit_doc IterM.flatMapAfterM]
-public def Iter.flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type w}
-    {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterator α₂ m γ]
-    (f : β → m (IterM (α := α₂) m γ)) (it₁ : Iter (α := α) β) (it₂ : Option (IterM (α := α₂) m γ)) :=
-  ((it₁.mapM pure).flatMapAfterM f it₂ : IterM m γ)
-
-@[always_inline, expose, inherit_doc IterM.flatMapM]
-public def Iter.flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
-    {γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β] [Iterator α₂ m γ]
-    (f : β → m (IterM (α := α₂) m γ)) (it : Iter (α := α) β) :=
-  (it.flatMapAfterM f none : IterM m γ)
-
-@[always_inline, inherit_doc IterM.flatMapAfter]
-public def Iter.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
-    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
-    (f : β → Iter (α := α₂) γ) (it₁ : Iter (α := α) β) (it₂ : Option (Iter (α := α₂) γ)) :=
-  ((it₁.toIterM.flatMapAfter (fun b => (f b).toIterM) (Iter.toIterM <$> it₂)).toIter : Iter γ)
-
-@[always_inline, expose, inherit_doc IterM.flatMap]
-public def Iter.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
-    {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
-    (f : β → Iter (α := α₂) γ) (it : Iter (α := α) β) :=
-  (it.flatMapAfter f none : Iter γ)
-
-end Std.Iterators

src/Init/Data/Iterators/Combinators/Monadic.lean

@@ -7,5 +7,4 @@ module
 
 prelude
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
-public import Init.Data.Iterators.Combinators.Monadic.FlatMap
 public import Init.Data.Iterators.Combinators.Monadic.ULift

src/Init/Data/Iterators/Combinators/Monadic/Attach.lean

@@ -6,7 +6,9 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Internal.Termination
+public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 
 public section
@@ -41,8 +43,7 @@ instance Attach.instIterator {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] {P : β → Prop} :
     Iterator (Attach α m P) m { out : β // P out } where
   IsPlausibleStep it step := ∃ step', Monadic.modifyStep it step' = step
-  step it := (fun step => .deflate ⟨Monadic.modifyStep it step.inflate, step.inflate, rfl⟩) <$>
-      it.internalState.inner.step
+  step it := (fun step => ⟨Monadic.modifyStep it step, step, rfl⟩) <$> it.internalState.inner.step
 
 def Attach.instFinitenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m β] [Finite α m] {P : β → Prop} :

src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean

@@ -6,6 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Basic
+public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.PostconditionMonad
 public import Init.Data.Iterators.Internal.Termination
@@ -94,7 +96,7 @@ it.filterMapWithPostcondition     ---a'-----c'-------⊥
 **Termination properties:**
 
 * `Finite` instance: only if `it` is finite
-* `Productive` instance: only if `it` is finite
+* `Productive` instance: only if `it` is finite`
 
 For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
 no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then
@@ -147,13 +149,13 @@ instance FilterMap.instIterator {α β γ : Type w} {m : Type w → Type w'} {n
   step it :=
     letI : MonadLift m n := ⟨lift (α := _)⟩
     do
-      match (← it.internalState.inner.step).inflate with
+      match ← it.internalState.inner.step with
       | .yield it' out h => do
         match ← (f out).operation with
-        | ⟨none, h'⟩ => pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (by exact .yieldNone h h')
-        | ⟨some out', h'⟩ => pure <| .deflate <| .yield (it'.filterMapWithPostcondition f) out' (by exact .yieldSome h h')
-      | .skip it' h => pure <| .deflate <| .skip (it'.filterMapWithPostcondition f) (by exact .skip h)
-      | .done h => pure <| .deflate <| .done (.done h)
+        | ⟨none, h'⟩ => pure <| .skip (it'.filterMapWithPostcondition f) (by exact .yieldNone h h')
+        | ⟨some out', h'⟩ => pure <| .yield (it'.filterMapWithPostcondition f) out' (by exact .yieldSome h h')
+      | .skip it' h => pure <| .skip (it'.filterMapWithPostcondition f) (by exact .skip h)
+      | .done h => pure <| .done (.done h)
 
 instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}
@@ -461,7 +463,7 @@ For each value emitted by the base iterator `it`, this combinator calls `f`.
 @[inline, expose]
 def IterM.mapM {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Iterator α m β]
     [Monad n] [MonadLiftT m n] (f : β → n γ) (it : IterM (α := α) m β) :=
-  (it.mapWithPostcondition (fun b => PostconditionT.lift (f b)) : IterM n γ)
+  (it.filterMapWithPostcondition (fun b => some <$> PostconditionT.lift (f b)) : IterM n γ)
 
 /--
 If `it` is an iterator, then `it.filterM f` is another iterator that applies a monadic