chore: update comments

This PR optimizes two `String` proofs and makes sure that
`MkIffOfInductiveProp` does not import `Lean.Elab.Tactic`, which
previously pushed it to the very end of the import graph.

.claude/commands/release.md

@@ -0,0 +1,69 @@
+# 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@v7
+        uses: actions/github-script@v8
         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@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const { labels, number: prNumber } = context.payload.pull_request;

.github/workflows/build-template.yml

@@ -3,9 +3,6 @@ name: build-template
 on:
   workflow_call:
     inputs:
-      check-level:
-        type: string
-        required: true
       config:
         type: string
         required: true
@@ -230,7 +227,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.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
+        if: 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@v7
+      uses: actions/github-script@v8
       with:
         script: |
           const { owner, repo, number: issue_number  } = context.issue;

.github/workflows/ci.yml

@@ -31,10 +31,6 @@ 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
@@ -110,6 +106,9 @@ 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
@@ -117,6 +116,7 @@ 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,19 +129,24 @@ 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@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
-            console.log(`level: ${level}`);
+            const fast = ${{ steps.set-level.outputs.fast }};
+            console.log(`level: ${level}, fast: ${fast}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
@@ -152,7 +157,8 @@ jobs:
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "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*",
@@ -165,17 +171,19 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                "os": "ubuntu-latest",
+                // usually not a bottleneck so make exclusive to `fast-ci`
+                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests 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.
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1 || isPushToMaster,
+                "test": level >= 1,
+                "secondary": level == 0,
                 "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*",
@@ -186,10 +194,10 @@ jobs:
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "check-level": 0,
-                "test": true,
+                "enabled": 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
@@ -198,14 +206,16 @@ jobs:
               {
                 "name": "Linux Reldebug",
                 "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "CMAKE_PRESET": "reldebug",
               },
               // TODO: suddenly started failing in CI
               /*{
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
                 // exclude seriously slow/problematic tests (laketests crash)
@@ -215,7 +225,8 @@ jobs:
                 "name": "macOS",
                 "os": "macos-15-intel",
                 "release": true,
-                "check-level": 2,
+                "test": false,  // Tier 2 platform
+                "enabled": 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*",
@@ -226,7 +237,7 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && !isPr ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
+                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -235,14 +246,16 @@ 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
-                "check-level": isPr ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1,
+                "test": level >= 1,
+                "secondary": level == 0,
               },
               {
                 "name": "Windows",
-                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "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",
@@ -254,7 +267,8 @@ jobs:
                 "os": "nscloud-ubuntu-22.04-arm64-4x16",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "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*",
@@ -267,7 +281,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,
-              //  "check-level": 2,
+              //  "enabled": level >= 2,
               //  "cross": true,
               //  "shell": "bash -euxo pipefail {0}"
               //}
@@ -279,7 +293,7 @@ jobs:
               //   "wasm": true,
               //   "cmultilib": true,
               //   "release": true,
-              //   "check-level": 2,
+              //   "enabled": level >= 2,
               //   "cross": true,
               //   "shell": "bash -euxo pipefail {0}",
               //   // Just a few selected tests because wasm is slow
@@ -293,7 +307,7 @@ jobs:
               }
             }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            matrix = matrix.filter((job) => level >= job["check-level"]);
+            matrix = matrix.filter((job) => job["enabled"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
             core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
 
@@ -303,7 +317,6 @@ 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 }}
@@ -319,7 +332,6 @@ 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 }}
@@ -350,7 +362,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@v7
+      uses: actions/github-script@v8
       with:
         script: |
             core.setFailed('Some jobs failed')
@@ -367,7 +379,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -392,6 +404,8 @@ 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:
@@ -411,7 +425,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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         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@v7
+        uses: actions/github-script@v8
         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@v7
+      uses: actions/github-script@v8
       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@v7
+        uses: actions/github-script@v8
         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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         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@v7
+        uses: actions/github-script@v8
         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@v7
+        uses: actions/github-script@v8
         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@v7
+        uses: actions/github-script@v8
         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@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const description =
@@ -401,6 +401,7 @@ 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'
@@ -460,6 +461,7 @@ 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: |
@@ -530,6 +532,7 @@ 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@v7
+        uses: actions/github-script@v8
         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@v9
+      - uses: actions/stale@v10
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

.gitignore

@@ -20,7 +20,6 @@ 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/ @zwarich
+/src/library/compiler/ @hargoniX
 /src/lake/ @tydeu
-/src/Lean/Compiler/ @leodemoura @zwarich
+/src/Lean/Compiler/ @leodemoura @hargoniX
 /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`, 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`, `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)`
 * 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 *);
-lean_object * initialize_C(uint8_t builtin, lean_object *);
+lean_object * initialize_A_B(uint8_t builtin);
+lean_object * initialize_C(uint8_t builtin);
 ...
 
 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, lean_io_mk_world());
+res = initialize_A_B(builtin);
 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, lean_io_mk_world());
+res = initialize_C(builtin);
 if (lean_io_result_is_ok(res)) {
 ...
 

flake.nix

@@ -25,6 +25,7 @@
         } ({
           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,6 +14,9 @@
 		}
 	],
 	"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,53 +1,30 @@
 import Lake.CLI.Main
 
 /-!
-A simple script that inserts `module` and `@[expose] public section` into un-modulized files and
+
+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
 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
-  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
+  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
 
+  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.toString
+    let inputCtx := Parser.mkInputContext text path
     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
@@ -57,35 +34,42 @@ 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
 
-    -- 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
+    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
         "public meta section"
       else
         "@[expose] public section"
       if !imps.isEmpty then
         sec := "\n\n" ++ sec
-      if header.raw.getTailPos?.isNone then
+      if insertPos?.isNone then
         sec := sec ++ "\n\n"
-      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.endPos
+      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos
 
     -- prepend each import with `public `
     for imp in imps.reverse do
       let insertPos := imp.raw.getPos?.get!
-      let prfx := if looksMeta then "public meta " else "public "
-      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.endPos
+      let prfx := if doMeta then "public meta " else "public "
+      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
 
     -- 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.endPos
+    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
 
     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.endPos stx.raw.getTailPos?.get! + ⟨1⟩
+        pos := text.findAux (· == '\n') text.rawEndPos 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.endPos
+    out := out ++ text.extract insertion text.rawEndPos
 
     IO.FS.writeFile path out
     return count + 1

script/release_checklist.py

@@ -1,5 +1,58 @@
 #!/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
@@ -76,6 +129,39 @@ 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
@@ -84,20 +170,17 @@ 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 as e:
-        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
+
+    except requests.exceptions.RequestException:
         return None
-    except Exception as e:
-        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
+    except Exception:
         return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
@@ -286,6 +369,68 @@ 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 {}
@@ -404,30 +549,57 @@ 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
 
-    if not release_page_exists(lean_repo_url, toolchain, github_token):
-        print(f"  ❌ Release page for {toolchain} does not exist")
+    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}")
+
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-        
-    # Check the actual release notes page title
+
+    # Check the actual release notes page title (informational only - does not block)
     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:
-        # Error already printed by get_release_notes
-        lean4_success = False
+        print(f"  ⚠️  Release notes not found at {release_notes_url} (this will be fixed while updating the reference-manual repository)")
     elif not actual_title.startswith(expected_title_prefix):
-        # 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
+        print(f"  ⚠️  Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {release_notes_url}")
     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...")
 
@@ -471,6 +643,19 @@ 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,30 +1,53 @@
 #!/usr/bin/env python3
 
 """
-Execute release steps for Lean4 repositories.
+Execute Release Steps for Lean4 Downstream Repositories
 
-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.
+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)
 
 Usage:
-    python3 release_steps.py <version> <repo>
+    ./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
 
-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
+The script reads repository configurations from release_repos.yml.
+Each repository has specific handling for merging, dependencies, and testing.
 
-Example:
-    python3 release_steps.py v4.6.0 mathlib4
-    python3 release_steps.py v4.6.0 batteries
+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.
 
-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
+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
 """
 
 import argparse
@@ -566,8 +589,19 @@ def execute_release_steps(repo, version, config):
         
         # Clean lake cache for a fresh build
         print(blue("Cleaning lake cache..."))
-        run_command("rm -rf .lake", cwd=repo_path)
-        
+        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}"))
+
         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 25)
+set(LEAN_VERSION_MINOR 26)
 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,7 +34,14 @@ if (NOT LEAN_PLATFORM_TARGET)
     OUTPUT_VARIABLE LEAN_PLATFORM_TARGET OUTPUT_STRIP_TRAILING_WHITESPACE)
 endif()
 
-set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker")
+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_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")
 
@@ -82,6 +89,7 @@ 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`")
@@ -826,10 +834,13 @@ if(LEAN_INSTALL_PREFIX)
   set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
 endif()
 
-if (STAGE GREATER 1)
+
+if (USE_LAKE_CACHE AND STAGE EQUAL 1)
+  set(LAKE_ARTIFACT_CACHE_TOML "true")
+else()
   # 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
-  string(APPEND LEAN_EXTRA_LAKEFILE_TOML "\n\nenableArtifactCache = false")
+  set(LAKE_ARTIFACT_CACHE_TOML "false")
 endif()
 
 # Escape for `make`. Yes, twice.

src/Init/BinderNameHint.lean

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

src/Init/Control/EState.lean

@@ -6,8 +6,6 @@ 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,7 +10,6 @@ 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,8 +7,6 @@ module
 
 prelude
 public import Init.Ext
-public import Init.SimpLemmas
-public import Init.Meta
 
 public section
 
@@ -252,6 +250,7 @@ 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,14 +7,11 @@ 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,7 +7,6 @@ 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,17 +6,13 @@ 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,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Option.Basic
-public import Init.Control.Basic
 public import Init.Control.Except
 
 public section
@@ -28,7 +27,7 @@ failure occurred.
 /--
 Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
   x
 
@@ -70,7 +69,7 @@ instance {m : Type u → Type v} [Pure m] : Inhabited (OptionT m α) where
 /--
 Recovers from failures. Typically used via the `<|>` operator.
 -/
-@[always_inline, inline] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   match (← x) with
   | some a => pure (some a)
   | _      => y ()
@@ -78,7 +77,7 @@ Recovers from failures. Typically used via the `<|>` operator.
 /--
 A recoverable failure.
 -/
-@[always_inline, inline] protected def fail : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] protected def fail : OptionT m α := OptionT.mk do
   pure none
 
 instance : Alternative (OptionT m) where
@@ -91,7 +90,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] protected def lift (x : m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] protected def lift (x : m α) : OptionT m α := OptionT.mk do
   return some (← x)
 
 instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
@@ -101,11 +100,11 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
 /--
 Handles failures by treating them as exceptions of type `Unit`.
 -/
-@[always_inline, inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
-  let some a ← x | handle ()
+@[always_inline, inline, expose] protected def tryCatch (x : OptionT m α) (handle : PUnit → OptionT m α) : OptionT m α := OptionT.mk do
+  let some a ← x | handle ⟨⟩
   pure <| some a
 
-instance : MonadExceptOf Unit (OptionT m) where
+instance : MonadExceptOf PUnit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 

src/Init/Control/Reader.lean

@@ -8,8 +8,6 @@ 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,8 +8,6 @@ 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,7 +8,6 @@ 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,7 +7,6 @@ Authors: Dany Fabian
 module
 
 prelude
-public import Init.Classical
 public import Init.ByCases
 
 @[expose] public section

src/Init/Data/Array/Attach.lean

@@ -6,10 +6,7 @@ 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,10 +6,6 @@ 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
@@ -752,8 +748,7 @@ 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 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    map (i : Nat) (bs : Array β) : m (Array β) := do
+  let rec map (i : Nat) (bs : Array β) : m (Array β) := do
       if hlt : i < as.size then
         map (i+1) (bs.push (← f as[i]))
       else
@@ -913,8 +908,7 @@ 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 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    loop (j : Nat) : m Bool := do
+    let rec 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
@@ -1252,8 +1246,7 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -1270,8 +1263,7 @@ Examples:
 -/
 @[inline]
 def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some ⟨j, h⟩ else loop (j + 1)
     else none
@@ -1307,7 +1299,6 @@ 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⟩
@@ -1717,7 +1708,6 @@ 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
@@ -1742,8 +1732,7 @@ Examples:
  * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]`
 -/
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  go (i : Nat) (acc : Array α) : Array α :=
+  let rec go (i : Nat) (acc : Array α) : Array α :=
     if h : i < as.size then
       let a := as[i]
       if p a then
@@ -1766,7 +1755,6 @@ 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
@@ -1861,8 +1849,7 @@ 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 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (as : Array α) (j : Fin as.size) :=
+  let rec 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
@@ -1916,7 +1903,6 @@ 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]
@@ -1945,7 +1931,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
+@[specialize]
 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]
@@ -2108,7 +2094,6 @@ 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,10 +6,8 @@ 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,9 +6,7 @@ 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,7 +8,6 @@ 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,7 +6,6 @@ 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,11 +6,9 @@ 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,11 +6,8 @@ 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,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.TakeDrop
 
 public section
 

src/Init/Data/Array/FinRange.lean

@@ -6,7 +6,6 @@ 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,10 +7,7 @@ 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,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.InsertIdx
 
 public section
 

src/Init/Data/Array/Lemmas.lean

@@ -6,17 +6,10 @@ 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
@@ -3761,7 +3754,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,9 +6,6 @@ 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,9 +10,7 @@ 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,10 +6,7 @@ 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,8 +6,6 @@ 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,13 +6,9 @@ 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,11 +6,8 @@ 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,7 +7,6 @@ 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,14 +6,10 @@ 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,7 +6,6 @@ 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,7 +7,6 @@ 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,10 +6,8 @@ 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,10 +6,8 @@ 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,13 +6,5 @@ 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,11 +6,8 @@ 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,16 +6,11 @@ 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,10 +6,8 @@ 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,25 +6,14 @@ 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
 
@@ -3753,6 +3742,9 @@ 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,11 +6,8 @@ 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,7 +6,6 @@ Author: Markus Himmel
 module
 
 prelude
-public import Init.Prelude
 public import Init.Data.List.Basic
 
 public section

src/Init/Data/ByteArray/Lemmas.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
-public import Init.Data.Array.Extract
 
 public section
 
@@ -257,3 +256,19 @@ 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,7 +6,6 @@ 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.Data.Int.DivMod.Lemmas
+import Init.Hints
 
 /-!
 # The dyadic rationals

src/Init/Data/Dyadic/Instances.lean

@@ -7,7 +7,6 @@ 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,7 +5,6 @@ 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,7 +8,6 @@ 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,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Nat.Bitwise
-public import Init.Data.Fin.Basic
 
 public section
 

src/Init/Data/Fin/Fold.lean

@@ -6,7 +6,6 @@ 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
 
@@ -23,7 +22,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)`  -/
-  @[semireducible, specialize] loop (x : α) (i : Nat) : α :=
+  @[specialize] loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
   termination_by n - i
 
@@ -34,7 +33,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] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop n (Nat.le_refl n) init where
+@[inline, expose] 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
@@ -65,7 +64,7 @@ Fin.foldlM n f x₀ = do
     pure xₙ
   ```
   -/
-  @[semireducible, specialize] loop (x : α) (i : Nat) : m α := do
+  @[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
@@ -96,7 +95,7 @@ Fin.foldrM n f xₙ = do
     pure x₀
   ```
   -/
-  @[semireducible, specialize] loop : {i // i ≤ n} → α → m α
+  @[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,7 +7,6 @@ module
 
 prelude
 public import Init.PropLemmas
-public import Init.Data.Fin.Basic
 
 public section
 

src/Init/Data/Fin/Lemmas.lean

@@ -8,13 +8,9 @@ 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
 
-public section
+@[expose] public section
 
 open Std
 
@@ -915,16 +911,21 @@ 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⟩⟩
 
-theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 :=
+@[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 :=
   ⟨fun h => h _, fun h i => Subsingleton.elim i 0 ▸ h⟩
 
-theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 :=
+@[simp] theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 :=
   ⟨fun ⟨i, h⟩ => Subsingleton.elim i 0 ▸ h, fun h => ⟨_, h⟩⟩
 
-theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 :=
+@[simp] 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
 
-theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
+@[simp] 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,8 +6,6 @@ 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,9 +6,6 @@ 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,9 +6,7 @@ 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.endPos, foundFlattenedHardLine := flatten && p != s.endPos, space := off }
+    { foundLine := p != s.rawEndPos, foundFlattenedHardLine := flatten && p != s.rawEndPos, 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.endPos then
+      if p == s.rawEndPos 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.endPos) }::is
+        let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.rawEndPos) }::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,7 +411,6 @@ 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,9 +6,7 @@ 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,7 +9,6 @@ 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,7 +5,6 @@ Authors: Kim Morrison
 -/
 module
 prelude
-public import Init.Core
 public import Init.Grind.Tactics
 public section
 namespace Function

src/Init/Data/Hashable.lean

@@ -6,9 +6,7 @@ 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,7 +6,6 @@ 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,13 +6,7 @@ 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,8 +6,6 @@ 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,8 +6,6 @@ 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,9 +6,7 @@ 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,15 +6,9 @@ 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,11 +6,8 @@ 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,6 +605,9 @@ 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,7 +6,6 @@ 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,24 +6,83 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Core
 public import Init.Classical
 public import Init.Ext
-public import Init.NotationExtra
-public import Init.TacticsExtra
+
+set_option doc.verso true
 
 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.
@@ -182,6 +241,16 @@ 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`.
@@ -284,7 +353,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 (PlausibleIterStep <| IsPlausibleStep it)
+  step : (it : IterM (α := α) m β) → m (Shrink <| PlausibleIterStep <| IsPlausibleStep it)
 
 section Monadic
 
@@ -358,7 +427,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 it.Step :=
+    (it : IterM (α := α) m β) : m (Shrink it.Step) :=
   Iterator.step it
 
 end Monadic
@@ -484,6 +553,10 @@ 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
@@ -496,6 +569,16 @@ 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.
@@ -582,7 +665,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.toPure
+  it.toIterM.step.run.inflate.toPure
 
 end Pure
 
@@ -597,6 +680,10 @@ 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`.
@@ -646,6 +733,12 @@ 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,4 +8,5 @@ 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

@@ -0,0 +1,53 @@
+/-
+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,4 +7,5 @@ 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,9 +6,7 @@ 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
@@ -43,7 +41,8 @@ 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 => ⟨Monadic.modifyStep it step, step, rfl⟩) <$> it.internalState.inner.step
+  step it := (fun step => .deflate ⟨Monadic.modifyStep it step.inflate, step.inflate, 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,8 +6,6 @@ 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
@@ -96,7 +94,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
@@ -149,13 +147,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 with
+      match (← it.internalState.inner.step).inflate with
       | .yield it' out h => do
         match ← (f out).operation with
-        | ⟨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)
+        | ⟨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)
 
 instance {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n] [Iterator α m β]
     {lift : ⦃α : Type w⦄ → m α → n α}
@@ -463,7 +461,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.filterMapWithPostcondition (fun b => some <$> PostconditionT.lift (f b)) : IterM n γ)
+  (it.mapWithPostcondition (fun b => PostconditionT.lift (f b)) : IterM n γ)
 
 /--
 If `it` is an iterator, then `it.filterM f` is another iterator that applies a monadic