chore: tweak error message about weak options

This PR implements the `set_option` tactic in `grind` interactive mode.

.claude/commands/release.md

@@ -0,0 +1,57 @@
+# 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. Create a todo list tracking all repositories that need updates
+3. For each repository that needs updating:
+   - Run `script/release_steps.py {version} {repo_name}` to create the PR
+   - Mark it complete when the PR is created
+4. After creating PRs, notify the user which PRs need review and merging
+5. Continuously rerun `script/release_checklist.py {version}` to check progress
+6. As PRs are merged, dependent repositories will become ready - create PRs for those as well
+7. 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
@@ -116,10 +113,10 @@ jobs:
             build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
-          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v4-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
-            ${{ matrix.name }}-build-v3
+            ${{ matrix.name }}-build-v4
       # open nix-shell once for initial setup
       - name: Setup
         run: |
@@ -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)
@@ -213,9 +223,10 @@ jobs:
               },*/
               {
                 "name": "macOS",
-                "os": "macos-13",
+                "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-sonoma-arm64-6x14" : "macos-14",
+                "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

.github/workflows/update-stage0.yml

@@ -69,10 +69,10 @@ jobs:
           build/stage1/**/*.ir
           build/stage1/**/*.c
           build/stage1/**/*.c.o*
-        key: Linux Lake-build-v3-${{ github.sha }}
+        key: Linux Lake-build-v4-${{ github.sha }}
         # fall back to (latest) previous cache
         restore-keys: |
-          Linux Lake-build-v3
+          Linux Lake-build-v4
     - if: env.should_update_stage0 == 'yes'
       # sync options with `Linux Lake` to ensure cache reuse
       run: |

.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/testing.md

@@ -59,7 +59,7 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     open Foo in
     theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
     Bla.
-      --^ textDocument/completion
+      --^ completion
     ```
     In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
     auto-completion request at `Bla.`. The expected output is stored in

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

@@ -8,9 +8,15 @@
 		},
 		{
 			"path": "tests"
+		},
+		{
+			"path": "script"
 		}
 	],
 	"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

@@ -0,0 +1,75 @@
+import Lake.CLI.Main
+
+/-!
+
+Usage: `lean --run script/Modulize.lean [--meta] file1.lean file2.lean ...`
+
+A simple script that inserts `module` and `public section` into un-modulized files and
+bumps their imports to `public`.
+
+When `--meta` is passed, `public meta section` and `public meta import` is used instead.
+-/
+
+open Lean Parser.Module
+
+def main (args : List String) : IO Unit := do
+  let mut args := args
+  let mut doMeta := false
+  while !args.isEmpty && args[0]!.startsWith "-" do
+    match args[0]! with
+    | "--meta" => doMeta := true
+    | arg => throw <| .userError s!"unknown flag '{arg}'"
+    args := args.tail
+
+  for path in args do
+    -- Parse the input file
+    let mut text ← IO.FS.readFile path
+    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
+      throw <| .userError "parse errors in file"
+    let `(header| $[module%$moduleTk?]? $imps:import*) := header
+      | throw <| .userError s!"unexpected header syntax of {path}"
+    if moduleTk?.isSome then
+      continue
+
+    -- initial whitespace if empty header
+    let startPos := header.raw.getPos? |>.getD parserState.pos
+
+    let dummyEnv ← mkEmptyEnvironment
+    let (initCmd, parserState', _) :=
+      Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs
+
+    -- insert section if any trailing command
+    if !initCmd.isOfKind ``Parser.Command.eoi then
+      let insertPos? :=
+          -- put below initial module docstring if any
+          guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|>
+          -- else below header
+          header.raw.getTailPos?
+      let insertPos := insertPos?.getD startPos  -- empty header
+      let mut sec := if doMeta then
+        "public meta section"
+      else
+        "@[expose] public section"
+      if !imps.isEmpty then
+        sec := "\n\n" ++ sec
+      if insertPos?.isNone then
+        sec := sec ++ "\n\n"
+      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.endPos
+
+    -- prepend each import with `public `
+    for imp in imps.reverse do
+      let insertPos := imp.raw.getPos?.get!
+      let prfx := if doMeta then "public meta " else "public "
+      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.endPos
+
+    -- insert `module` header
+    let mut initText := text.extract 0 startPos
+    if !initText.trim.isEmpty then
+      -- If there is a header comment, preserve it and put `module` in the line after
+      initText := initText.trimRight ++ "\n"
+    text := initText ++ "module\n\n" ++ text.extract startPos text.endPos
+
+    IO.FS.writeFile path text

script/Shake.lean

@@ -0,0 +1,584 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Sebastian Ullrich
+-/
+import Lake.CLI.Main
+import Lean.ExtraModUses
+
+/-! # `lake exe shake` command
+
+This command will check the current project (or a specified target module) and all dependencies for
+unused imports. This works by looking at generated `.olean` files to deduce required imports and
+ensuring that every import is used to contribute some constant or other elaboration dependency
+recorded by `recordExtraModUse`. Because recompilation is not needed this is quite fast (about 8
+seconds to check `Mathlib` and all dependencies).
+-/
+
+/-- help string for the command line interface -/
+def help : String := "Lean project tree shaking tool
+Usage: lake exe shake [OPTIONS] <MODULE>..
+
+Arguments:
+  <MODULE>
+    A module path like `Mathlib`. All files transitively reachable from the
+    provided module(s) will be checked.
+
+Options:
+  --force
+    Skips the `lake build --no-build` sanity check
+
+  --fix
+    Apply the suggested fixes directly. Make sure you have a clean checkout
+    before running this, so you can review the changes.
+"
+
+open Lean
+
+/-- We use `Nat` as a bitset for doing efficient set operations.
+The bit indexes will usually be a module index. -/
+structure Bitset where
+  toNat : Nat
+deriving Inhabited, DecidableEq, Repr
+
+namespace Bitset
+
+instance : EmptyCollection Bitset where
+  emptyCollection := { toNat := 0 }
+
+instance : Insert Nat Bitset where
+  insert i s := { toNat := s.toNat ||| (1 <<< i) }
+
+instance : Singleton Nat Bitset where
+  singleton i := insert i ∅
+
+instance : Inter Bitset where
+  inter a b := { toNat := a.toNat &&& b.toNat }
+
+instance : Union Bitset where
+  union a b := { toNat := a.toNat ||| b.toNat }
+
+instance : XorOp Bitset where
+  xor a b := { toNat := a.toNat ^^^ b.toNat }
+
+def has (s : Bitset) (i : Nat) : Bool := s ∩ {i} ≠ ∅
+
+end Bitset
+
+/-- The kind of a module dependency, corresponding to the homonymous `ExtraModUse` fields. -/
+structure NeedsKind where
+  isExported : Bool
+  isMeta : Bool
+deriving Inhabited, BEq, Repr, Hashable
+
+namespace NeedsKind
+
+@[match_pattern]  abbrev priv : NeedsKind := { isExported := false, isMeta := false }
+@[match_pattern]  abbrev pub  : NeedsKind := { isExported := true,  isMeta := false }
+@[match_pattern]  abbrev metaPriv : NeedsKind := { isExported := false, isMeta := true }
+@[match_pattern]  abbrev metaPub  : NeedsKind := { isExported := true,  isMeta := true }
+
+def all : Array NeedsKind := #[pub, priv, metaPub, metaPriv]
+
+def ofImport : Lean.Import → NeedsKind
+  | { isExported := true, isMeta := true, .. } => .metaPub
+  | { isExported := true, isMeta := false, .. } => .pub
+  | { isExported := false, isMeta := true, .. } => .metaPriv
+  | { isExported := false, isMeta := false, .. } => .priv
+
+end NeedsKind
+
+/-- Logically, a map `NeedsKind → Bitset`. -/
+structure Needs where
+  pub : Bitset
+  priv : Bitset
+  metaPub : Bitset
+  metaPriv : Bitset
+deriving Inhabited, Repr
+
+def Needs.empty : Needs := default
+
+def Needs.get (needs : Needs) (k : NeedsKind) : Bitset :=
+  match k with
+  | .pub => needs.pub
+  | .priv => needs.priv
+  | .metaPub => needs.metaPub
+  | .metaPriv => needs.metaPriv
+
+def Needs.has (needs : Needs) (k : NeedsKind) (i : ModuleIdx) : Bool :=
+  needs.get k |>.has i
+
+def Needs.set (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
+  match k with
+  | .pub   => { needs with pub := s }
+  | .priv  => { needs with priv := s }
+  | .metaPub => { needs with metaPub := s }
+  | .metaPriv => { needs with metaPriv := s }
+
+def Needs.modify (needs : Needs) (k : NeedsKind) (f : Bitset → Bitset) : Needs :=
+  needs.set k (f (needs.get k))
+
+def Needs.union (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
+  needs.modify k (· ∪ s)
+
+def Needs.sub (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
+  needs.modify k (fun s' => s' ^^^ (s' ∩ s))
+
+/-- The main state of the checker, containing information on all loaded modules. -/
+structure State where
+  env  : Environment
+  /--
+  `transDeps[i]` is the (non-reflexive) transitive closure of `mods[i].imports`. More specifically,
+  * `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
+  * `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
+  * `j ∈ transDeps[i].priv` if `i -(import all)->+ -(public import ...)-> _ -(public import)->* j`
+  * `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import ...)->* j`
+  * `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import ...)->* j`
+  * `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ -(public meta import ...)-> _ -(public (meta)? import ...)->* j`
+  -/
+  transDeps : Array Needs := #[]
+  /--
+  `transDepsOrig` is the initial value of `transDeps` before changes potentially resulting from
+  changes to upstream headers.
+  -/
+  transDepsOrig : Array Needs := #[]
+
+def State.mods (s : State) := s.env.header.moduleData
+def State.modNames (s : State) := s.env.header.moduleNames
+
+/--
+Given module `j`'s transitive dependencies, computes the union of `transImps` and the transitive
+dependencies resulting from importing the module via `imp` according to the rules of
+`State.transDeps`.
+-/
+def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps : Needs) : Needs := Id.run do
+  let mut transImps := transImps
+
+  -- `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
+  if imp.isExported && !imp.isMeta then
+    transImps := transImps.union .pub {j} |>.union .pub (impTransImps.get .pub)
+
+  if !imp.isExported && !imp.isMeta then
+    -- `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
+    transImps := transImps.union .priv {j} |>.union .priv (impTransImps.get .pub)
+    if imp.importAll then
+      -- `j ∈ transDeps[i].priv` if `i -(import all)->+ -(public import ...)-> _ -(public import)->* j`
+      transImps := transImps.union .priv (impTransImps.get .pub)
+
+  -- `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import ...)->* j`
+  if imp.isExported then
+    transImps := transImps.union .metaPub (impTransImps.get .metaPub)
+    if imp.isMeta then
+      transImps := transImps.union .metaPub {j} |>.union .metaPub (impTransImps.get .pub ∪ impTransImps.get .metaPub)
+
+  if !imp.isExported then
+    if imp.isMeta then
+      -- `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import ...)->* j`
+      transImps := transImps.union .metaPriv {j} |>.union .metaPriv (impTransImps.get .pub ∪ impTransImps.get .metaPub)
+    if imp.importAll then
+      -- `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ -(public meta import ...)-> _ -(public (meta)? import ...)->* j`
+      transImps := transImps.union .metaPriv (impTransImps.get .metaPub)
+
+  transImps
+
+/-- Calculates the needs for a given module `mod` from constants and recorded extra uses. -/
+def calcNeeds (env : Environment) (i : ModuleIdx) : Needs := Id.run do
+  let mut needs := default
+  for ci in env.header.moduleData[i]!.constants do
+    let pubCI? := env.setExporting true |>.find? ci.name
+    let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
+    needs := visitExpr k ci.type needs
+    if let some e := ci.value? (allowOpaque := true) then
+      -- type and value has identical visibility under `meta`
+      let k := if k.isMeta then k else
+        if pubCI?.any (·.hasValue (allowOpaque := true)) then .pub else .priv
+      needs := visitExpr k e needs
+
+  for use in getExtraModUses env i do
+    let j := env.getModuleIdx? use.module |>.get!
+    needs := needs.union { use with } {j}
+
+  return needs
+where
+  /-- Accumulate the results from expression `e` into `deps`. -/
+  visitExpr (k : NeedsKind) e deps :=
+    Lean.Expr.foldConsts e deps fun c deps => match env.getModuleIdxFor? c with
+      | some j =>
+        let k := { k with isMeta := k.isMeta && !isMeta env c }
+        if j != i then deps.union k {j} else deps
+      | _ => deps
+
+/--
+Calculates the same as `calcNeeds` but tracing each module to a use-def declaration pair or
+`none` if merely a recorded extra use.
+-/
+def getExplanations (env : Environment) (i : ModuleIdx) :
+    Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name)) := Id.run do
+  let mut deps := default
+  for ci in env.header.moduleData[i]!.constants do
+    let pubCI? := env.setExporting true |>.find? ci.name
+    let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
+    deps := visitExpr k ci.name ci.type deps
+    if let some e := ci.value? (allowOpaque := true) then
+      let k := if k.isMeta then k else
+        if pubCI?.any (·.hasValue (allowOpaque := true)) then .pub else .priv
+      deps := visitExpr k ci.name e deps
+
+  for use in getExtraModUses env i do
+    let j := env.getModuleIdx? use.module |>.get!
+    if !deps.contains (j, { use with }) then
+      deps := deps.insert (j, { use with }) none
+
+  return deps
+where
+  /-- Accumulate the results from expression `e` into `deps`. -/
+  visitExpr (k : NeedsKind) name e deps :=
+    Lean.Expr.foldConsts e deps fun c deps => match env.getModuleIdxFor? c with
+      | some i =>
+        let k := { k with isMeta := k.isMeta && !isMeta env c }
+        if
+          if let some (some (name', _)) := deps[(i, k)]? then
+            decide (name.toString.length < name'.toString.length)
+          else true
+        then
+          deps.insert (i, k) (name, c)
+        else
+          deps
+      | _ => deps
+
+partial def initStateFromEnv (env : Environment) : State := Id.run do
+  let mut s := { env }
+  for i in 0...env.header.moduleData.size do
+    let mod := env.header.moduleData[i]!
+    let mut imps := #[]
+    let mut transImps := Needs.empty
+    for imp in mod.imports do
+      let j := env.getModuleIdx? imp.module |>.get!
+      imps := imps.push j
+      transImps := addTransitiveImps transImps imp j s.transDeps[j]!
+    s := { s with transDeps := s.transDeps.push transImps }
+  s := { s with transDepsOrig := s.transDeps }
+  return s
+
+/-- The list of edits that will be applied in `--fix`. `edits[i] = (removed, added)` where:
+
+* If `j ∈ removed` then we want to delete module named `j` from the imports of `i`
+* If `j ∈ added` then we want to add module index `j` to the imports of `i`.
+-/
+abbrev Edits := Std.HashMap Name (Array Import × Array Import)
+
+/-- Register that we want to remove `tgt` from the imports of `src`. -/
+def Edits.remove (ed : Edits) (src : Name) (tgt : Import) : Edits :=
+  match ed.get? src with
+  | none => ed.insert src (#[tgt], #[])
+  | some (a, b) => ed.insert src (a.push tgt, b)
+
+/-- Register that we want to add `tgt` to the imports of `src`. -/
+def Edits.add (ed : Edits) (src : Name) (tgt : Import) : Edits :=
+  match ed.get? src with
+  | none => ed.insert src (#[], #[tgt])
+  | some (a, b) => ed.insert src (a, b.push tgt)
+
+/-- Parse a source file to extract the location of the import lines, for edits and error messages.
+
+Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
+and `endPos` is the position of the end of the header.
+-/
+def parseHeaderFromString (text path : String) :
+    IO (System.FilePath × Parser.InputContext ×
+      TSyntaxArray ``Parser.Module.import × String.Pos) := do
+  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
+    throw <| .userError "parse errors in file"
+  -- the insertion point for `add` is the first newline after the imports
+  let insertion := header.raw.getTailPos?.getD parserState.pos
+  let insertion := text.findAux (· == '\n') text.endPos insertion + ⟨1⟩
+  pure (path, inputCtx, .mk header.raw[2].getArgs, insertion)
+
+/-- Parse a source file to extract the location of the import lines, for edits and error messages.
+
+Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
+and `endPos` is the position of the end of the header.
+-/
+def parseHeader (srcSearchPath : SearchPath) (mod : Name) :
+    IO (System.FilePath × Parser.InputContext ×
+      TSyntaxArray ``Parser.Module.import × String.Pos) := do
+  -- Parse the input file
+  let some path ← srcSearchPath.findModuleWithExt "lean" mod
+    | throw <| .userError s!"error: failed to find source file for {mod}"
+  let text ← IO.FS.readFile path
+  parseHeaderFromString text path.toString
+
+def decodeImport : TSyntax ``Parser.Module.import → Import
+  | `(Parser.Module.import| $[public%$pubTk?]? $[meta%$metaTk?]? import $[all%$allTk?]? $id) =>
+    { module := id.getId, isExported := pubTk?.isSome, isMeta := metaTk?.isSome, importAll := allTk?.isSome }
+  | stx => panic! s!"unexpected syntax {stx}"
+
+/-- Analyze and report issues from module `i`. Arguments:
+
+* `srcSearchPath`: Used to find the path for error reporting purposes
+* `i`: the module index
+* `needs`: the module's calculated needs
+* `pinned`: dependencies that should be preserved even if unused
+* `edits`: accumulates the list of edits to apply if `--fix` is true
+* `addOnly`: if true, only add missing imports, do not remove unused ones
+-/
+def visitModule (srcSearchPath : SearchPath)
+    (i : Nat) (needs : Needs) (preserve : Needs) (edits : Edits)
+    (addOnly := false) (githubStyle := false) (explain := false) : StateT State IO Edits := do
+  let s ← get
+  -- Do transitive reduction of `needs` in `deps`.
+  let mut deps := needs
+  for j in [0:s.mods.size] do
+    let transDeps := s.transDeps[j]!
+    for k in NeedsKind.all do
+      if s.transDepsOrig[i]!.has k j && preserve.has k j then
+        deps := deps.union k {j}
+      if deps.has k j then
+        let transDeps := addTransitiveImps .empty { k with module := .anonymous } j transDeps
+        for k' in NeedsKind.all do
+          deps := deps.sub k' (transDeps.sub k' {j} |>.get k')
+
+  -- Any import which is not in `transDeps` was unused.
+  -- Also accumulate `newDeps` which is the transitive closure of the remaining imports
+  let mut toRemove : Array Import := #[]
+  let mut newDeps := Needs.empty
+  for imp in s.mods[i]!.imports do
+    let j := s.env.getModuleIdx? imp.module |>.get!
+    if
+        -- skip folder-nested imports
+        s.modNames[i]!.isPrefixOf imp.module ||
+        imp.importAll then
+      newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
+    else
+      let k := NeedsKind.ofImport imp
+      if !addOnly && !deps.has k j && !deps.has { k with isExported := false } j then
+        toRemove := toRemove.push imp
+      else
+        newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
+
+  -- If `newDeps` does not cover `deps`, then we have to add back some imports until it does.
+  -- To minimize new imports we pick only new imports which are not transitively implied by
+  -- another new import
+  let mut toAdd : Array Import := #[]
+  for j in [0:s.mods.size] do
+    for k in NeedsKind.all do
+      if deps.has k j && !newDeps.has k j && !newDeps.has { k with isExported := true } j then
+        let imp := { k with module := s.modNames[j]! }
+        toAdd := toAdd.push imp
+        newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
+
+  -- mark and report the removals
+  let mut edits := toRemove.foldl (init := edits) fun edits imp =>
+    edits.remove s.modNames[i]! imp
+
+  if !toAdd.isEmpty || !toRemove.isEmpty || explain then
+    if let some path ← srcSearchPath.findModuleWithExt "lean" s.modNames[i]! then
+      println! "{path}:"
+    else
+      println! "{s.modNames[i]!}:"
+
+  if !toRemove.isEmpty then
+    println! "  remove {toRemove}"
+
+  if githubStyle then
+    try
+      let (path, inputCtx, imports, endHeader) ← parseHeader srcSearchPath s.modNames[i]!
+      for stx in imports do
+        if toRemove.any fun imp => imp == decodeImport stx then
+          let pos := inputCtx.fileMap.toPosition stx.raw.getPos?.get!
+          println! "{path}:{pos.line}:{pos.column+1}: warning: unused import \
+            (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)"
+      if !toAdd.isEmpty then
+        -- we put the insert message on the beginning of the last import line
+        let pos := inputCtx.fileMap.toPosition endHeader
+        println! "{path}:{pos.line-1}:1: warning: \
+          add {toAdd} instead"
+    catch _ => pure ()
+
+  -- mark and report the additions
+  edits := toAdd.foldl (init := edits) fun edits imp =>
+    edits.add s.modNames[i]! imp
+
+  if !toAdd.isEmpty then
+    println! "  add {toAdd}"
+
+  -- recalculate transitive dependencies of downstream modules
+  let mut newTransDepsI := Needs.empty
+  for imp in s.mods[i]!.imports do
+    if !toRemove.contains imp then
+      let j := s.env.getModuleIdx? imp.module |>.get!
+      newTransDepsI := addTransitiveImps newTransDepsI imp j s.transDeps[j]!
+  for imp in toAdd do
+    let j := s.env.getModuleIdx? imp.module |>.get!
+    newTransDepsI := addTransitiveImps newTransDepsI imp j s.transDeps[j]!
+
+  set { s with transDeps := s.transDeps.set! i newTransDepsI }
+
+  if explain then
+    let explanation := getExplanations s.env i
+    let sanitize n := if n.hasMacroScopes then (sanitizeName n).run' { options := {} } else n
+    let run (imp : Import) := do
+      let j := s.env.getModuleIdx? imp.module |>.get!
+      if let some exp? := explanation[(j, NeedsKind.ofImport imp)]? then
+        println! "  note: `{imp}` required"
+        if let some (n, c) := exp? then
+          println! "    because `{sanitize n}` refers to `{sanitize c}`"
+        else
+          println! "    because of additional compile-time dependencies"
+    for j in s.mods[i]!.imports do
+      if !toRemove.contains j then
+        run j
+    for i in toAdd do run i
+
+  return edits
+
+/-- Convert a list of module names to a bitset of module indexes -/
+def toBitset (s : State) (ns : List Name) : Bitset :=
+  ns.foldl (init := ∅) fun c name =>
+    match s.env.getModuleIdxFor? name with
+    | some i => c ∪ {i}
+    | none => c
+
+/-- The parsed CLI arguments. See `help` for more information -/
+structure Args where
+  /-- `--help`: shows the help -/
+  help : Bool := false
+  /-- `--force`: skips the `lake build --no-build` sanity check -/
+  force : Bool := false
+  /-- `--gh-style`: output messages that can be parsed by `gh-problem-matcher-wrap` -/
+  githubStyle : Bool := false
+  /-- `--explain`: give constants explaining why each module is needed -/
+  explain : Bool := false
+  /-- `--fix`: apply the fixes directly -/
+  fix : Bool := false
+  /-- `<MODULE>..`: the list of root modules to check -/
+  mods : Array Name := #[]
+
+local instance : Ord Import where
+  compare a b :=
+    if a.isExported && !b.isExported then
+      Ordering.lt
+    else if !a.isExported && b.isExported then
+      Ordering.gt
+    else
+      a.module.cmp b.module
+
+/-- The main entry point. See `help` for more information on arguments. -/
+def main (args : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  -- Parse the arguments
+  let rec parseArgs (args : Args) : List String → Args
+    | [] => args
+    | "--help" :: rest => parseArgs { args with help := true } rest
+    | "--force" :: rest => parseArgs { args with force := true } rest
+    | "--fix" :: rest => parseArgs { args with fix := true } rest
+    | "--explain" :: rest => parseArgs { args with explain := true } rest
+    | "--gh-style" :: rest => parseArgs { args with githubStyle := true } rest
+    | "--" :: rest => { args with mods := args.mods ++ rest.map (·.toName) }
+    | other :: rest => parseArgs { args with mods := args.mods.push other.toName } rest
+  let args := parseArgs {} args
+
+  -- Bail if `--help` is passed
+  if args.help then
+    IO.println help
+    IO.Process.exit 0
+
+  if !args.force then
+    if (← IO.Process.output { cmd := "lake", args := #["build", "--no-build"] }).exitCode != 0 then
+      IO.println "There are out of date oleans. Run `lake build` or `lake exe cache get` first"
+      IO.Process.exit 1
+
+  -- Determine default module(s) to run shake on
+  let defaultTargetModules : Array Name ← 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 #[]
+
+  let srcSearchPath ← getSrcSearchPath
+  -- the list of root modules
+  let mods := if args.mods.isEmpty then defaultTargetModules else args.mods
+  -- 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 (_, s) ← importModulesCore imps (isExported := true) |>.run
+  let s := s.markAllExported
+  let env ← finalizeImport s (isModule := true) imps {} (leakEnv := false) (loadExts := false)
+
+  StateT.run' (s := initStateFromEnv env) do
+
+  let s ← get
+  -- Parse the config file
+
+  -- Run the calculation of the `needs` array in parallel
+  let needs := s.mods.mapIdx fun i _ =>
+    Task.spawn fun _ => calcNeeds s.env i
+
+  if args.fix then
+    println! "The following changes will be made automatically:"
+
+  -- Check all selected modules
+  let mut edits : Edits := ∅
+  let mut revNeeds : Needs := default
+  for i in [0:s.mods.size], t in needs do
+    edits ← visitModule (addOnly := !pkg.isPrefixOf s.modNames[i]!) srcSearchPath i t.get revNeeds edits args.githubStyle args.explain
+    if isExtraRevModUse s.env i then
+      revNeeds := revNeeds.union .priv {i}
+
+  if !args.fix then
+    -- return error if any issues were found
+    return if edits.isEmpty then 0 else 1
+
+  -- Apply the edits to existing files
+  let count ← edits.foldM (init := 0) fun count mod (remove, add) => do
+    let add : Array Import := add.qsortOrd
+
+    -- Parse the input file
+    let (path, inputCtx, imports, insertion) ←
+      try parseHeader srcSearchPath mod
+      catch e => println! e.toString; return count
+    let text := inputCtx.fileMap.source
+
+    -- Calculate the edit result
+    let mut pos : String.Pos := 0
+    let mut out : String := ""
+    let mut seen : Std.HashSet Import := {}
+    for stx in imports do
+      let mod := decodeImport stx
+      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⟩
+      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
+
+    IO.FS.writeFile path out
+    return count + 1
+
+  -- Since we throw an error upon encountering issues, we can be sure that everything worked
+  -- if we reach this point of the script.
+  if count > 0 then
+    println! "Successfully applied {count} suggestions."
+  else
+    println! "No edits required."
+  return 0

script/lakefile.toml

@@ -0,0 +1,9 @@
+name = "scripts"
+
+[[lean_exe]]
+name = "modulize"
+root = "Modulize"
+
+[[lean_exe]]
+name = "shake"
+root = "Shake"

script/lean-toolchain

@@ -0,0 +1 @@
+lean4

script/release_checklist.py

@@ -1,5 +1,51 @@
 #!/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
+   - Checks the release notes page on lean-lang.org
+
+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
@@ -286,6 +332,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 {}
@@ -471,6 +579,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

src/CMakeLists.txt

@@ -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`")
@@ -797,6 +805,9 @@ install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
 
 # symlink source into expected installation location for go-to-definition, if file system allows it
 file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
+# get rid of all files in `src/lean` that may have been loaded from the cache
+# (at the time of writing this, this is the case for some lake test .c files)
+file(REMOVE_RECURSE ${CMAKE_BINARY_DIR}/src/lean)
 if(${STAGE} EQUAL 0)
   file(CREATE_LINK ${CMAKE_SOURCE_DIR}/../../src ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
 else()
@@ -823,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.
@@ -844,15 +858,13 @@ endfunction()
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
-set(LEANC_OPTS_TOML "${LEANC_OPTS} ${LEANC_EXTRA_CC_FLAGS} ${LEANC_INTERNAL_FLAGS}")
-set(LINK_OPTS_TOML "${LEANC_INTERNAL_LINKER_FLAGS} -L${CMAKE_BINARY_DIR}/lib/lean ${LEAN_EXTRA_LINKER_FLAGS}")
 
 toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
-toml_escape("${LEANC_OPTS_TOML}" LEANC_OPTS_TOML)
-toml_escape("${LINK_OPTS_TOML}" LINK_OPTS_TOML)
 
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LAKE_LIB_PREFIX "lib")
+if(${CMAKE_BUILD_TYPE} MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
+  set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")
+else()
+  set(CMAKE_BUILD_TYPE_TOML "Release")
 endif()
 
 if(USE_LAKE)

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/Classical.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.PropLemmas
 
-public section
+@[expose] public section
 
 universe u v
 

src/Init/Control.lean

@@ -16,5 +16,3 @@ public import Init.Control.Option
 public import Init.Control.Lawful
 public import Init.Control.StateCps
 public import Init.Control.ExceptCps
-
-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.lean

@@ -10,5 +10,3 @@ public import Init.Control.Lawful.Basic
 public import Init.Control.Lawful.Instances
 public import Init.Control.Lawful.Lemmas
 public import Init.Control.Lawful.MonadLift
-
-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,12 +7,11 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Control.Except
 import all Init.Control.Except
-public import Init.Control.State
+public import Init.Control.Option
+import all Init.Control.Option
 import all Init.Control.State
 public import Init.Control.StateRef
-public import Init.Ext
 
 public section
 
@@ -110,6 +109,121 @@ instance : LawfulMonad (Except ε) := LawfulMonad.mk'
 instance : LawfulApplicative (Except ε) := inferInstance
 instance : LawfulFunctor (Except ε) := inferInstance
 
+/-! # OptionT -/
+
+namespace OptionT
+
+@[ext] theorem ext {x y : OptionT m α} (h : x.run = y.run) : x = y := by
+  simp [run] at h
+  assumption
+
+@[simp, grind =] theorem run_mk {m : Type u → Type v} (x : m (Option α)) :
+    OptionT.run (OptionT.mk x) = x := by rfl
+
+@[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : OptionT m α) = pure (some x) := by
+  simp [run, pure, OptionT.pure, OptionT.mk]
+
+@[simp, grind =] theorem run_lift  [Monad.{u, v} m] (x : m α) : run (OptionT.lift x : OptionT m α) = (return some (← x) : m (Option α)) := by
+  simp [run, OptionT.lift, OptionT.mk]
+
+@[simp, grind =] theorem run_throw [Monad m] : run (throw e : OptionT m β) = pure none := by
+  simp [run, throw, throwThe, MonadExceptOf.throw, OptionT.fail, OptionT.mk]
+
+@[simp, grind =] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → OptionT m β) : run (OptionT.lift x >>= f : OptionT m β) = x >>= fun a => run (f a) := by
+  simp [OptionT.run, OptionT.lift, bind, OptionT.bind, OptionT.mk]
+
+@[simp, grind =] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → OptionT m β) : (throw e >>= f) = throw e := by
+  simp [throw, throwThe, MonadExceptOf.throw, bind, OptionT.bind, OptionT.mk, OptionT.fail]
+
+@[simp, grind =] theorem run_bind (f : α → OptionT m β) [Monad m] :
+    (x >>= f).run = Option.elimM x.run (pure none) (fun x => (f x).run) := by
+  change x.run >>= _ = _
+  simp [Option.elimM]
+  exact bind_congr fun |some _ => rfl | none => rfl
+
+@[simp, grind =] theorem lift_pure [Monad m] [LawfulMonad m] {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
+  simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
+
+@[simp, grind =] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : OptionT m α)
+    : (f <$> x).run = Option.map f <$> x.run := by
+  simp [Functor.map, Option.map, ←bind_pure_comp]
+  apply bind_congr
+  intro a; cases a <;> simp [OptionT.pure, OptionT.mk]
+
+protected theorem seq_eq {α β : Type u} [Monad m] (mf : OptionT m (α → β)) (x : OptionT m α) : mf <*> x = mf >>= fun f => f <$> x :=
+  rfl
+
+protected theorem bind_pure_comp [Monad m] (f : α → β) (x : OptionT m α) : x >>= pure ∘ f = f <$> x := by
+  intros; rfl
+
+protected theorem seqLeft_eq {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : x <* y = const β <$> x <*> y := by
+  change (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
+  rw [← OptionT.bind_pure_comp]
+  apply ext
+  simp [Option.elimM, Option.elim]
+  apply bind_congr
+  intro
+  | none => simp
+  | some _ =>
+    simp [←bind_pure_comp]; apply bind_congr; intro b;
+    cases b <;> simp [const]
+
+protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : x *> y = const α id <$> x <*> y := by
+  change (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
+  rw [← OptionT.bind_pure_comp]
+  apply ext
+  simp [Option.elimM, Option.elim]
+  apply bind_congr
+  intro a; cases a <;> simp
+
+instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where
+  id_map         := by intros; apply ext; simp
+  map_const      := by intros; rfl
+  seqLeft_eq     := OptionT.seqLeft_eq
+  seqRight_eq    := OptionT.seqRight_eq
+  pure_seq       := by intros; apply ext; simp [OptionT.seq_eq, Option.elimM, Option.elim]
+  bind_pure_comp := OptionT.bind_pure_comp
+  bind_map       := by intros; rfl
+  pure_bind      := by intros; apply ext; simp [Option.elimM, Option.elim]
+  bind_assoc     := by intros; apply ext; simp [Option.elimM, Option.elim]; apply bind_congr; intro a; cases a <;> simp
+
+@[simp] theorem run_seq [Monad m] [LawfulMonad m] (f : OptionT m (α → β)) (x : OptionT m α) :
+    (f <*> x).run = Option.elimM f.run (pure none) (fun f => Option.map f <$> x.run) := by
+  simp [seq_eq_bind, Option.elimM, Option.elim]
+
+@[simp] theorem run_seqLeft [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
+    (x <* y).run = Option.elimM x.run (pure none)
+      (fun x => Option.map (Function.const β x) <$> y.run) := by
+  simp [seqLeft_eq, seq_eq_bind, Option.elimM, OptionT.run_bind]
+
+@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
+    (x *> y).run = Option.elimM x.run (pure none) (Function.const α y.run) := by
+  simp only [seqRight_eq, run_seq, Option.elimM, run_map, Option.elim, bind_map_left]
+  refine bind_congr (fun | some _ => by simp | none => by simp)
+
+@[simp, grind =] theorem run_failure [Monad m] : (failure : OptionT m α).run = pure none := by rfl
+
+@[simp] theorem map_failure [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) :
+    f <$> (failure : OptionT m α) = (failure : OptionT m β) := by
+  simp [OptionT.mk, Functor.map, Alternative.failure, OptionT.fail, OptionT.bind]
+
+@[simp] theorem run_orElse [Monad m] (x : OptionT m α) (y : OptionT m α) :
+    (x <|> y).run = Option.elimM x.run y.run (fun x => pure (some x)) :=
+  bind_congr fun | some _ => by rfl | none => by rfl
+
+end OptionT
+
+/-! # Option -/
+
+instance : LawfulMonad Option := LawfulMonad.mk'
+  (id_map := fun x => by cases x <;> rfl)
+  (pure_bind := fun _ _ => by rfl)
+  (bind_assoc := fun a _ _ => by cases a <;> rfl)
+  (bind_pure_comp := bind_pure_comp)
+
+instance : LawfulApplicative Option := inferInstance
+instance : LawfulFunctor Option := inferInstance
+
 /-! # ReaderT -/
 
 namespace ReaderT

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.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Control.Lawful.MonadLift.Basic
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.MonadLift.Instances
-
-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
@@ -64,10 +60,6 @@ namespace OptionT
 
 variable [Monad m] [LawfulMonad m]
 
-@[simp]
-theorem lift_pure {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
-  simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
-
 @[simp]
 theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
     OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by

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
@@ -39,13 +38,14 @@ variable {m : Type u → Type v} [Monad m] {α β : Type u}
 Converts an action that returns an `Option` into one that might fail, with `none` indicating
 failure.
 -/
+@[always_inline, inline, expose]
 protected def mk (x : m (Option α)) : OptionT m α :=
   x
 
 /--
 Sequences two potentially-failing actions. The second action is run only if the first succeeds.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
   match (← x) with
   | some a => f a
@@ -54,7 +54,7 @@ protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β :
 /--
 Succeeds with the provided value.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def pure (a : α) : OptionT m α := OptionT.mk do
   pure (some a)
 

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
@@ -144,8 +143,9 @@ Computed values are cached, so the value is not recomputed.
   x.fn ()
 
 -- Ensure `Thunk.fn` is still computable even if it shouldn't be accessed directly.
-@[inline] private def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
-@[csimp] private theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
+/-- Implementation detail. -/
+@[inline] def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
+@[csimp] theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
 
 /--
 Constructs a new thunk that forces `x` and then applies `x` to the result. Upon forcing, the result
@@ -1605,7 +1605,7 @@ gen_injective_theorems% PSigma
 gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
-gen_injective_theorems% String.Pos
+gen_injective_theorems% String.Pos.Raw
 gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum

src/Init/Data.lean

@@ -30,6 +30,7 @@ public import Init.Data.Random
 public import Init.Data.ToString
 public import Init.Data.Range
 public import Init.Data.Hashable
+public import Init.Data.LawfulHashable
 public import Init.Data.OfScientific
 public import Init.Data.Format
 public import Init.Data.Stream
@@ -52,5 +53,3 @@ public import Init.Data.Slice
 public import Init.Data.Order
 public import Init.Data.Rat
 public import Init.Data.Dyadic
-
-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.lean

@@ -30,5 +30,3 @@ public import Init.Data.Array.Erase
 public import Init.Data.Array.Zip
 public import Init.Data.Array.InsertIdx
 public import Init.Data.Array.Extract
-
-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
@@ -84,10 +81,10 @@ well-founded recursion mechanism to prove that the function terminates.
   simp [pmap]
 
 /-- Implementation of `pmap` using the zero-copy version of `attach`. -/
-@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
+@[inline] def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
     Array β := (xs.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
 
-@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
   funext α β p f xs H
   cases xs
   simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith_eq_pmap]
@@ -95,16 +92,16 @@ well-founded recursion mechanism to prove that the function terminates.
   intro a m h₁ h₂
   congr
 
-@[simp, grind =] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
+@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
 
-@[simp, grind =] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
+@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
     pmap f (xs.push a) h =
       (pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
   simp [pmap]
 
-@[simp, grind =] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
+@[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
 
-@[simp, grind =] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
+@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
 
 @[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
     l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
@@ -125,13 +122,11 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   simp only [List.pmap_toArray, mk.injEq]
   rw [List.pmap_congr_left _ h]
 
-@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {xs : Array α} (H) :
     map g (pmap f xs H) = pmap (fun a h => g (f a h)) xs H := by
   cases xs
   simp [List.map_pmap]
 
-@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs : Array α} (H) :
     pmap g (map f xs) H = pmap (fun a h => g (f a) h) xs fun _ h => H _ (mem_map_of_mem h) := by
   cases xs
@@ -147,14 +142,14 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
   subst w
   simp
 
-@[simp, grind =] theorem attach_push {a : α} {xs : Array α} :
+@[simp] theorem attach_push {a : α} {xs : Array α} :
     (xs.push a).attach =
       (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   cases xs
   rw [attach_congr (List.push_toArray _ _)]
   simp [Function.comp_def]
 
-@[simp, grind =] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
       (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   cases xs
@@ -176,9 +171,6 @@ theorem attach_map_val (xs : Array α) (f : α → β) :
   cases xs
   simp
 
-@[deprecated attach_map_val (since := "2025-02-17")]
-abbrev attach_map_coe := @attach_map_val
-
 -- The argument `xs : Array α` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (xs : Array α) : xs.attach.map Subtype.val = xs := by
   cases xs; simp
@@ -187,9 +179,6 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {xs : Array α} (H
     ((xs.attachWith p H).map fun (i : { i // p i}) => f i) = xs.map f := by
   cases xs; simp
 
-@[deprecated attachWith_map_val (since := "2025-02-17")]
-abbrev attachWith_map_coe := @attachWith_map_val
-
 theorem attachWith_map_subtype_val {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) :
     (xs.attachWith p H).map Subtype.val = xs := by
   cases xs; simp
@@ -294,25 +283,23 @@ theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp, grind =] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f xs.attach H =
       xs.pmap (P := fun a => ∃ h : a ∈ xs, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   ext <;> simp
 
-@[simp, grind =] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (xs.attachWith q H₁) H₂ =
       xs.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
   ext <;> simp
 
-@[grind =]
 theorem foldl_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) :
     (xs.pmap f H).foldl g x = xs.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
-@[grind =]
 theorem foldr_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : β → γ → γ) (x : γ) :
     (xs.pmap f H).foldr g x = xs.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
@@ -370,20 +357,18 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
   ext
   simpa using fun a => List.mem_of_getElem? a
 
-@[grind =]
 theorem attach_map {xs : Array α} {f : α → β} :
     (xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   cases xs
   ext <;> simp
 
-@[grind =]
 theorem attachWith_map {xs : Array α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ xs.map f → P b) :
     (xs.map f).attachWith P H = (xs.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases xs
   simp [List.attachWith_map]
 
-@[simp, grind =] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
     {f : { x // P x } → β} :
     (xs.attachWith P H).map f = xs.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   cases xs <;> simp_all
@@ -401,9 +386,6 @@ theorem map_attach_eq_pmap {xs : Array α} {f : { x // x ∈ xs } → β} :
   cases xs
   ext <;> simp
 
-@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
-abbrev map_attach := @map_attach_eq_pmap
-
 @[grind =]
 theorem attach_filterMap {xs : Array α} {f : α → Option β} :
     (xs.filterMap f).attach = xs.attach.filterMap
@@ -439,7 +421,6 @@ theorem filter_attachWith {q : α → Prop} {xs : Array α} {p : {x // q x} →
   cases xs
   simp [Function.comp_def, List.filter_map]
 
-@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {xs} (H₁ H₂) :
     pmap f (pmap g xs H₁) H₂ =
       pmap (α := { x // x ∈ xs }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) xs.attach
@@ -447,7 +428,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   cases xs
   simp [List.pmap_pmap, List.pmap_map]
 
-@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
+@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
     (h : ∀ a ∈ xs ++ ys, p a) :
     (xs ++ ys).pmap f h =
       (xs.pmap f fun a ha => h a (mem_append_left ys ha)) ++
@@ -462,7 +443,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp, grind =] theorem attach_append {xs ys : Array α} :
+@[simp] theorem attach_append {xs ys : Array α} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   cases xs
@@ -470,62 +451,59 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
   rw [attach_congr (List.append_toArray _ _)]
   simp [List.attach_append, Function.comp_def]
 
-@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
+@[simp] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp [attachWith]
 
-@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
-@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
   cases xs
   simp
 
-@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
   cases xs
   simp
 
-@[simp, grind =] theorem attach_reverse {xs : Array α} :
+@[simp] theorem attach_reverse {xs : Array α} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   rw [attach_congr List.reverse_toArray]
   simp
 
-@[grind =]
 theorem reverse_attach {xs : Array α} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   simp
 
-@[simp, grind =] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
   cases xs
   simp
 
-@[simp, grind =] theorem back?_attachWith {P : α → Prop} {xs : Array α}
+@[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
-@[simp, grind =]
+@[simp]
 theorem back?_attach {xs : Array α} :
     xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs

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
@@ -129,20 +125,11 @@ end Array
 
 namespace List
 
-@[deprecated Array.toArray_toList (since := "2025-02-17")]
-abbrev toArray_toList := @Array.toArray_toList
-
 -- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
 theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl
 
-@[deprecated toList_toArray (since := "2025-02-17")]
-abbrev _root_.Array.toList_toArray := @List.toList_toArray
-
 @[simp, grind =] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
 
-@[deprecated size_toArray (since := "2025-02-17")]
-abbrev _root_.Array.size_toArray := @List.size_toArray
-
 @[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := rfl
 
@@ -412,10 +399,6 @@ that requires a proof the array is non-empty.
 def back? (xs : Array α) : Option α :=
   xs[xs.size - 1]?
 
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), expose]
-def get? (xs : Array α) (i : Nat) : Option α :=
-  if h : i < xs.size then some xs[i] else none
-
 /--
 Swaps a new element with the element at the given index.
 
@@ -765,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
@@ -926,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
@@ -1265,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
@@ -1283,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
@@ -1320,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⟩
@@ -1730,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
@@ -1755,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
@@ -1779,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
@@ -1812,7 +1787,6 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
-@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 
@@ -1875,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
@@ -1930,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]
@@ -1959,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]
@@ -2122,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
@@ -24,29 +23,6 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Array
 
-/--
-Use the indexing notation `a[i]` instead.
-
-Access an element from an array without needing a runtime bounds checks,
-using a `Nat` index and a proof that it is in bounds.
-
-This function does not use `get_elem_tactic` to automatically find the proof that
-the index is in bounds. This is because the tactic itself needs to look up values in
-arrays.
--/
-@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
-def get {α : Type u} (xs : @& Array α) (i : @& Nat) (h : LT.lt i xs.size) : α :=
-  xs.toList.get ⟨i, h⟩
-
-/--
-Use the indexing notation `a[i]!` instead.
-
-Access an element from an array, or panic if the index is out of bounds.
--/
-@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17"), expose]
-def get! {α : Type u} [Inhabited α] (xs : @& Array α) (i : @& Nat) : α :=
-  Array.getD xs i default
-
 theorem foldlM_toList.aux [Monad m]
     {f : β → α → m β} {xs : Array α} {i j} (H : xs.size ≤ i + j) {b} :
     foldlM.loop f xs xs.size (Nat.le_refl _) i j b = (xs.toList.drop j).foldlM f b := by
@@ -108,9 +84,6 @@ abbrev push_toList := @toList_push
 
 @[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
 
-@[deprecated toList_pop (since := "2025-02-17")]
-abbrev pop_toList := @Array.toList_pop
-
 @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl
 
 @[simp, grind =] theorem toList_append {xs ys : Array α} :

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
@@ -63,7 +62,7 @@ theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + coun
   rcases xs with ⟨xs⟩
   simp [List.length_eq_countP_add_countP (p := p)]
 
-@[grind _=_]
+@[grind =]
 theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size := by
   rcases xs with ⟨xs⟩
   simp [List.countP_eq_length_filter]

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
 
@@ -324,6 +321,13 @@ abbrev erase_mkArray_ne := @erase_replicate_ne
 
 end erase
 
+/-! ### eraseIdxIfInBounds -/
+
+@[grind =]
+theorem eraseIdxIfInBounds_eq {xs : Array α} {i : Nat} :
+    xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i else xs := by
+  simp [eraseIdxIfInBounds]
+
 /-! ### eraseIdx -/
 
 theorem eraseIdx_eq_eraseIdxIfInBounds {xs : Array α} {i : Nat} (h : i < xs.size) :

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
@@ -278,9 +275,6 @@ theorem find?_flatten_eq_none_iff {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.find? p = none ↔ ∀ ys ∈ xss, ∀ x ∈ ys, !p x := by
   simp
 
-@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
-
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
@@ -306,9 +300,6 @@ theorem find?_flatten_eq_some_iff {xss : Array (Array α)} {p : α → Bool} {a
       ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
         by simpa using h₁, by simpa using h₂⟩
 
-@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
-
 @[simp, grind =] theorem find?_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
@@ -318,17 +309,11 @@ theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
-@[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
-abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
-
 @[grind =]
 theorem find?_replicate :
     find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
 
-@[deprecated find?_replicate (since := "2025-03-18")]
-abbrev find?_mkArray := @find?_replicate
-
 @[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
     find? p (replicate n a) = if p a then some a else none := by
   simp [find?_replicate, Nat.ne_of_gt h]
@@ -346,34 +331,19 @@ abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
 @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
   simp [find?_replicate, h]
 
-@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
-abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
-
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
 theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [← List.toArray_replicate, Classical.or_iff_not_imp_left]
 
-@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
-abbrev find?_mkArray_eq_none_iff := @find?_replicate_eq_none_iff
-
 @[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
-@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
-abbrev find?_mkArray_eq_some_iff := @find?_replicate_eq_some_iff
-
-@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
-abbrev find?_mkArray_eq_some := @find?_replicate_eq_some_iff
-
 @[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α → Bool} (h) :
     ((replicate n a).find? p).get h = a := by
   simp [← List.toArray_replicate]
 
-@[deprecated get_find?_replicate (since := "2025-03-18")]
-abbrev get_find?_mkArray := @get_find?_replicate
-
 @[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :

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
@@ -80,9 +73,6 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
 @[simp] theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
-@[deprecated size_eq_zero_iff (since := "2025-02-24")]
-abbrev size_eq_zero := @size_eq_zero_iff
-
 theorem eq_empty_iff_size_eq_zero : xs = #[] ↔ xs.size = 0 :=
   size_eq_zero_iff.symm
 
@@ -107,17 +97,10 @@ theorem exists_mem_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
 theorem size_pos_iff {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
   Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero_iff)
 
-@[deprecated size_pos_iff (since := "2025-02-24")]
-abbrev size_pos := @size_pos_iff
-
 theorem size_eq_one_iff {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
   cases xs
   simpa using List.length_eq_one_iff
 
-@[deprecated size_eq_one_iff (since := "2025-02-24")]
-abbrev size_eq_one := @size_eq_one_iff
-
-
 /-! ## L[i] and L[i]? -/
 
 theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i := by
@@ -371,6 +354,7 @@ abbrev getElem?_mkArray := @getElem?_replicate
 
 /-! ### mem -/
 
+@[grind ←]
 theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
 
 @[simp, grind =] theorem mem_push {xs : Array α} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by
@@ -542,18 +526,12 @@ theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
 @[simp] theorem isEmpty_iff {xs : Array α} : xs.isEmpty ↔ xs = #[] := by
   cases xs <;> simp
 
-@[deprecated isEmpty_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_true := @isEmpty_iff
-
 @[grind →]
 theorem empty_of_isEmpty {xs : Array α} (h : xs.isEmpty) : xs = #[] := Array.isEmpty_iff.mp h
 
 @[simp] theorem isEmpty_eq_false_iff {xs : Array α} : xs.isEmpty = false ↔ xs ≠ #[] := by
   cases xs <;> simp
 
-@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
-
 theorem isEmpty_iff_size_eq_zero {xs : Array α} : xs.isEmpty ↔ xs.size = 0 := by
   rw [isEmpty_iff, size_eq_zero_iff]
 
@@ -2996,11 +2974,6 @@ theorem _root_.List.toArray_drop {l : List α} {k : Nat} :
     (l.drop k).toArray = l.toArray.extract k := by
   rw [List.drop_eq_extract, List.extract_toArray, List.size_toArray]
 
-@[deprecated extract_size (since := "2025-02-27")]
-theorem take_size {xs : Array α} : xs.take xs.size = xs := by
-  cases xs
-  simp
-
 /-! ### shrink -/
 
 @[simp] private theorem size_shrink_loop {xs : Array α} {n : Nat} : (shrink.loop n xs).size = xs.size - n := by
@@ -3586,8 +3559,6 @@ theorem foldr_eq_foldl_reverse {xs : Array α} {f : α → β → β} {b} :
   subst w
   rw [foldr_eq_foldl_reverse, foldl_push_eq_append rfl, map_reverse]
 
-@[deprecated foldr_push_eq_append (since := "2025-02-09")] abbrev foldr_flip_push_eq_append := @foldr_push_eq_append
-
 theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {xs : Array α} {a₁ a₂} :
      xs.foldl op (op a₁ a₂) = op a₁ (xs.foldl op a₂) := by
   rcases xs with ⟨l⟩
@@ -3783,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
@@ -4712,44 +4683,3 @@ namespace List
       simp_all
 
 end List
-
-/-! ### Deprecations -/
-namespace Array
-
-set_option linter.deprecated false in
-@[deprecated "`get?` is deprecated" (since := "2025-02-12"), simp]
-theorem get?_eq_getElem? (xs : Array α) (i : Nat) : xs.get? i = xs[i]? := rfl
-
-@[deprecated getD_eq_getD_getElem? (since := "2025-02-12")] abbrev getD_eq_get? := @getD_eq_getD_getElem?
-
-set_option linter.deprecated false in
-@[deprecated getElem!_eq_getD (since := "2025-02-12")]
-theorem get!_eq_getD [Inhabited α] (xs : Array α) : xs.get! n = xs.getD n default := rfl
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead of `a.get! i`." (since := "2025-02-12")]
-theorem get!_eq_getD_getElem? [Inhabited α] (xs : Array α) (i : Nat) :
-    xs.get! i = xs[i]?.getD default := by
-  by_cases p : i < xs.size <;>
-  simp [get!, getD_eq_getD_getElem?, p]
-
-set_option linter.deprecated false in
-@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_getElem? := @get!_eq_getD_getElem?
-
-set_option linter.deprecated false in
-@[deprecated "`Array.get?` is deprecated, use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_get?_toList (xs : Array α) (i : Nat) : xs.get? i = xs.toList.get? i := by
-  simp [← getElem?_toList]
-
-set_option linter.deprecated false in
-@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_get? := @get!_eq_getD_getElem?
-
-/-! ### set -/
-
-@[deprecated getElem?_set_self (since := "2025-02-27")] abbrev get?_set_eq := @getElem?_set_self
-@[deprecated getElem?_set_ne (since := "2025-02-27")] abbrev get?_set_ne := @getElem?_set_ne
-@[deprecated getElem?_set (since := "2025-02-27")] abbrev get?_set := @getElem?_set
-@[deprecated get_set (since := "2025-02-27")] abbrev get_set := @getElem_set
-@[deprecated get_set_ne (since := "2025-02-27")] abbrev get_set_ne := @getElem_set_ne
-
-end Array

src/Init/Data/Array/Lex.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Lemmas
-
-public section

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

@@ -6,11 +6,8 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Core
-import Init.Data.Array.Basic
-import Init.Data.Nat.Lemmas
-import Init.Data.Range.Polymorphic.Iterators
-import Init.Data.Range.Polymorphic.Nat
+public import Init.Data.Range.Polymorphic.Iterators
+public import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Iterators.Consumers
 
 public section
@@ -31,7 +28,7 @@ Specifically, `Array.lex as bs lt` is true if
 def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
   for h : i in 0...(min as.size bs.size) do
     -- TODO: `get_elem_tactic` should be able to find this itself.
-    have : i < min as.size bs.size := Std.PRange.lt_upper_of_mem h
+    have : i < min as.size bs.size := Std.Rco.lt_upper_of_mem h
     if lt as[i] bs[i] then
       return true
     else if as[i] != bs[i] then

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
 
@@ -42,8 +40,7 @@ protected theorem not_le_iff_gt [LT α] {xs ys : Array α} :
   Classical.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
-  rw [lex, Std.PRange.forIn'_eq_match]
-  simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+  simp [lex, Std.Rco.forIn'_eq_if]
 
 private theorem cons_lex_cons.forIn'_congr_aux [Monad m] {as bs : ρ} {_ : Membership α ρ}
     [ForIn' m ρ α inferInstance] (w : as = bs)
@@ -64,13 +61,13 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
        (lt a b || a == b && xs.lex ys lt) := by
   simp only [lex, size_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add,
-    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.PRange.forIn'_eq_forIn'_toList]
+    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
   conv =>
     lhs; congr; congr
-    rw [cons_lex_cons.forIn'_congr_aux Std.PRange.toList_eq_match rfl (fun _ _ _ => rfl)]
-    simp only [Std.PRange.SupportsUpperBound.IsSatisfied, bind_pure_comp, map_pure]
+    rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if rfl (fun _ _ _ => rfl)]
+    simp only [bind_pure_comp, map_pure]
     rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.PRange.toList_Rox_eq_toList_Rcx_of_isSome_succ? (lo := 0) (h := rfl),
+  simp only [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? (lo := 0) (h := rfl),
     Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ,
     Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
     Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
@@ -83,16 +80,10 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
   | nil =>
-    cases l₂
-    · rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
-    · rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+    cases l₂ <;> simp [lex, Std.Rco.forIn'_eq_if]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil =>
-      rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+    | nil => simp [lex, Std.Rco.forIn'_eq_if]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 

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/QSort.lean

@@ -7,5 +7,3 @@ module
 
 prelude
 public import Init.Data.Array.QSort.Basic
-
-public section

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,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.GetElem
+public import Init.Data.Array.Basic
 import Init.Data.Array.GetLit
 public import Init.Data.Slice.Basic
 

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

@@ -7,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,15 +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
-
-public section

src/Init/Data/BitVec.lean

@@ -13,5 +13,3 @@ public import Init.Data.BitVec.Bitblast
 public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
-
-public section

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
 
@@ -29,10 +26,6 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
-@[inline, deprecated BitVec.ofNatLT (since := "2025-02-13"), inherit_doc BitVec.ofNatLT]
-protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n :=
-  BitVec.ofNatLT i p
-
 section Nat
 
 /--

src/Init/Data/BitVec/Bitblast.lean

@@ -6,17 +6,13 @@ 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
 
 @[expose] public section
 

src/Init/Data/BitVec/Bootstrap.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 import Init.Data.Int.Bitwise.Lemmas
+import Init.Ext
 
 public section
 

src/Init/Data/BitVec/Decidable.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Init.Data.BitVec.Bootstrap
+import Init.Ext
 
 public section
 
@@ -49,11 +50,11 @@ instance instDecidableForallBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePre
 
 instance instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
     Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+  decidable_of_iff (¬ ∀ v, ¬ P v) (by exact Classical.not_forall_not)
 
 instance instDecidableExistsBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
     [Decidable (∀ (x : Bool) (v : BitVec n), ¬ P (v.cons x))] : Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+  decidable_of_iff (¬ ∀ v, ¬ P v) (by exact Classical.not_forall_not)
 
 /--
 For small numerals this isn't necessary (as typeclass search can use the above two instances),

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,22 +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
 
 public section
 
@@ -74,10 +66,6 @@ theorem some_eq_getElem?_iff {l : BitVec w} : some a = l[n]? ↔ ∃ h : n < w,
 theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a :=
   getElem?_eq_some_iff.mp
 
-set_option linter.missingDocs false in
-@[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
-abbrev getElem?_eq_some := @getElem?_eq_some_iff
-
 theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
   simp
 
@@ -350,25 +338,14 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 @[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
   cases b <;> cases b' <;> rfl
 
-@[deprecated toNat_ofNatLT (since := "2025-02-13")]
-theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
-
 @[simp, grind =] theorem getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
   getLsbD (x#'lt) i = x.testBit i := by
   simp [getLsbD, BitVec.ofNatLT]
 
-@[deprecated getLsbD_ofNatLT (since := "2025-02-13")]
-theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
-  getLsbD (x#'lt) i = x.testBit i := getLsbD_ofNatLT x lt i
-
 @[simp, grind =] theorem getMsbD_ofNatLT {n x i : Nat} (h : x < 2^n) :
     getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
   simp [getMsbD, getLsbD]
 
-@[deprecated getMsbD_ofNatLT (since := "2025-02-13")]
-theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
-    getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := getMsbD_ofNatLT h
-
 @[grind =]
 theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n :=
   eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn])
@@ -3765,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]
@@ -6361,15 +6341,4 @@ theorem two_pow_ctz_le_toNat_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) :
   have hclz := getLsbD_true_ctz_of_ne_zero (x := x) hx
   exact Nat.ge_two_pow_of_testBit hclz
 
-/-! ### Deprecations -/
-
-set_option linter.missingDocs false
-
-@[deprecated toFin_uShiftRight (since := "2025-02-18")]
-abbrev toFin_uShiftRight := @toFin_ushiftRight
-
-
-
-
-
 end BitVec

src/Init/Data/ByteArray.lean

@@ -10,5 +10,3 @@ public import Init.Data.ByteArray.Basic
 public import Init.Data.ByteArray.Bootstrap
 public import Init.Data.ByteArray.Extra
 public import Init.Data.ByteArray.Lemmas
-
-public section

src/Init/Data/ByteArray/Basic.lean

@@ -6,13 +6,12 @@ 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
+
 @[expose] public section
 universe u
 
@@ -34,18 +33,40 @@ instance : Inhabited ByteArray where
 instance : EmptyCollection ByteArray where
   emptyCollection := ByteArray.empty
 
+/--
+Retrieves the size of the array as a platform-specific fixed-width integer.
+
+Because {name}`USize` is big enough to address all memory on every platform that Lean supports,
+there are in practice no {name}`ByteArray`s that have more elements that {name}`USize` can count.
+-/
 @[extern "lean_sarray_size", simp]
 def usize (a : @& ByteArray) : USize :=
   a.size.toUSize
 
+/--
+Retrieves the byte at the indicated index. Callers must prove that the index is in bounds. The index
+is represented by a platform-specific fixed-width integer (either 32 or 64 bits).
+
+Because {name}`USize` is big enough to address all memory on every platform that Lean supports, there are
+in practice no {name}`ByteArray`s for which {name}`uget` cannot retrieve all elements.
+-/
 @[extern "lean_byte_array_uget"]
 def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, h => bs[i]
 
+/--
+Retrieves the byte at the indicated index. Panics if the index is out of bounds.
+-/
 @[extern "lean_byte_array_get"]
 def get! : (@& ByteArray) → (@& Nat) → UInt8
   | ⟨bs⟩, i => bs[i]!
 
+/--
+Retrieves the byte at the indicated index. Callers must prove that the index is in bounds.
+
+Use {name}`uget` for a more efficient alternative or {name}`get!` for a variant that panics if the
+index is out of bounds.
+-/
 @[extern "lean_byte_array_fget"]
 def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, _ => bs[i]
@@ -56,37 +77,65 @@ instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
 instance : GetElem ByteArray USize UInt8 fun xs i => i.toFin < xs.size where
   getElem xs i h := xs.uget i h
 
+/--
+Replaces the byte at the given index.
+
+The array is modified in-place if there are no other references to it.
+
+If the index is out of bounds, the array is returned unmodified.
+-/
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
+/--
+Replaces the byte at the given index.
+
+No bounds check is performed, but the function requires a proof that the index is in bounds. This
+proof can usually be omitted, and will be synthesized automatically.
+
+The array is modified in-place if there are no other references to it.
+-/
 @[extern "lean_byte_array_fset"]
 def set : (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩
 
-@[extern "lean_byte_array_uset"]
+@[extern "lean_byte_array_uset", inherit_doc ByteArray.set]
 def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
 
+/--
+Computes a hash for a {name}`ByteArray`.
+-/
 @[extern "lean_byte_array_hash"]
 protected opaque hash (a : @& ByteArray) : UInt64
 
 instance : Hashable ByteArray where
   hash := ByteArray.hash
 
+/--
+Returns {name}`true` when {name}`s` contains zero bytes.
+-/
 def isEmpty (s : ByteArray) : Bool :=
   s.size == 0
 
 /--
-  Copy the slice at `[srcOff, srcOff + len)` in `src` to `[destOff, destOff + len)` in `dest`, growing `dest` if necessary.
-  If `exact` is `false`, the capacity will be doubled when grown. -/
+Copies the slice at `[srcOff, srcOff + len)` in {name}`src` to `[destOff, destOff + len)` in
+{name}`dest`, growing {name}`dest` if necessary. If {name}`exact` is {name}`false`, the capacity
+will be doubled when grown.
+-/
 @[extern "lean_byte_array_copy_slice"]
 def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
   ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + min len (src.data.size - srcOff)) dest.data.size⟩
 
+/--
+Copies the bytes with indices {name}`b` (inclusive) to {name}`e` (exclusive) to a new
+{name}`ByteArray`.
+-/
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)
 
+@[inline]
 protected def fastAppend (a : ByteArray) (b : ByteArray) : ByteArray :=
   -- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize
   b.copySlice 0 a a.size b.size false
@@ -113,6 +162,9 @@ theorem append_eq {a b : ByteArray} : a.append b = a ++ b := rfl
 theorem fastAppend_eq {a b : ByteArray} : a.fastAppend b = a ++ b := by
   simp [← append_eq_fastAppend]
 
+/--
+Converts a packed array of bytes to a linked list.
+-/
 def toList (bs : ByteArray) : List UInt8 :=
   let rec loop (i : Nat) (r : List UInt8) :=
     if i < bs.size then
@@ -123,16 +175,12 @@ def toList (bs : ByteArray) : List UInt8 :=
     decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
-  let rec @[specialize] loop (i : Nat) :=
-    if h : i < a.size then
-      if p a[i] then some i else loop (i+1)
-    else
-      none
-    termination_by a.size - i
-    decreasing_by decreasing_trivial_pre_omega
-  loop start
+/--
+Finds the index of the first byte in {name}`a` for which {name}`p` returns {name}`true`. If no byte
+in {name}`a` satisfies {name}`p`, then the result is {name}`none`.
 
+The index is returned along with a proof that it is a valid index in the array.
+-/
 @[inline] def findFinIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option (Fin a.size) :=
   let rec @[specialize] loop (i : Nat) :=
     if h : i < a.size then
@@ -144,11 +192,29 @@ def toList (bs : ByteArray) : List UInt8 :=
   loop start
 
 /--
-  We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
-  This is similar to the `Array` version.
+Finds the index of the first byte in {name}`a` for which {name}`p` returns {name}`true`. If no byte
+in {name}`a` satisfies {name}`p`, then the result is {name}`none`.
 
-  TODO: avoid code duplication in the future after we improve the compiler.
+The variant {name}`findFinIdx?` additionally returns a proof that the found index is in bounds.
 -/
+@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
+  let rec @[specialize] loop (i : Nat) :=
+    if h : i < a.size then
+      if p a[i] then some i else loop (i+1)
+    else
+      none
+    termination_by a.size - i
+    decreasing_by decreasing_trivial_pre_omega
+  loop start
+
+/--
+An efficient implementation of {name}`ForIn.forIn` for {name}`ByteArray` that uses {name}`USize`
+rather than {name}`Nat` for indices.
+
+We claim this unsafe implementation is correct because an array cannot have more than
+{name}`USize.size` elements in our runtime. This is similar to the {name}`Array` version.
+-/
+-- TODO: avoid code duplication in the future after we improve the compiler.
 @[inline] unsafe def forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
   let sz := as.usize
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -161,7 +227,11 @@ def toList (bs : ByteArray) : List UInt8 :=
       pure b
   loop 0 b
 
-/-- Reference implementation for `forIn` -/
+/--
+The reference implementation of {name}`ForIn.forIn` for {name}`ByteArray`.
+
+In compiled code, this is replaced by the more efficient {name}`ByteArray.forInUnsafe`.
+-/
 @[implemented_by ByteArray.forInUnsafe]
 protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
   let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
@@ -179,7 +249,13 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
 instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
-/-- See comment at `forInUnsafe` -/
+/--
+An efficient implementation of a monadic left fold on for {name}`ByteArray` that uses {name}`USize`
+rather than {name}`Nat` for indices.
+
+We claim this unsafe implementation is correct because an array cannot have more than
+{name}`USize.size` elements in our runtime. This is similar to the {name}`Array` version.
+-/
 -- TODO: avoid code duplication.
 @[inline]
 unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β :=
@@ -196,7 +272,14 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   else
     pure init
 
-/-- Reference implementation for `foldlM` -/
+/--
+A monadic left fold on {name}`ByteArray` that iterates over an array from low to high indices,
+computing a running value.
+
+Each element of the array is combined with the value from the prior elements using a monadic
+function {name}`f`. The initial value {name}`init` is the starting value before any elements have
+been processed.
+-/
 @[implemented_by foldlMUnsafe]
 def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β :=
   let fold (stop : Nat) (h : stop ≤ as.size) :=
@@ -214,11 +297,23 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
   else
     fold as.size (Nat.le_refl _)
 
+/--
+A left fold on {name}`ByteArray` that iterates over an array from low to high indices, computing a
+running value.
+
+Each element of the array is combined with the value from the prior elements using a function
+{name}`f`. The initial value {name}`init` is the starting value before any elements have been
+processed.
+
+{name}`ByteArray.foldlM` is a monadic variant of this function.
+-/
 @[inline]
 def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
   Id.run <| as.foldlM (pure <| f · ·) init start stop
 
-/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
+set_option doc.verso false -- Awaiting intra-module forward reference support
+/--
+Iterator over the bytes (`UInt8`) of a `ByteArray`.
 
 Typically created by `arr.iter`, where `arr` is a `ByteArray`.
 
@@ -242,6 +337,7 @@ structure Iterator where
   current byte is `(default : UInt8)`. -/
   idx : Nat
   deriving Inhabited
+set_option doc.verso true
 
 /-- Creates an iterator at the beginning of an array. -/
 def mkIterator (arr : ByteArray) : Iterator :=
@@ -259,16 +355,25 @@ theorem Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx :=
 
 namespace Iterator
 
-/-- Number of bytes remaining in the iterator. -/
+/--
+The number of bytes remaining in the iterator.
+-/
 def remainingBytes : Iterator → Nat
   | ⟨arr, i⟩ => arr.size - i
 
 @[inherit_doc Iterator.idx]
 def pos := Iterator.idx
 
-/-- The byte at the current position.
+/-- True if the iterator is past the array's last byte. -/
+@[inline]
+def atEnd : Iterator → Bool
+  | ⟨arr, i⟩ => i ≥ arr.size
 
-On an invalid position, returns `(default : UInt8)`. -/
+/--
+The byte at the current position.
+
+On an invalid position, returns {lean}`(default : UInt8)`.
+-/
 @[inline]
 def curr : Iterator → UInt8
   | ⟨arr, i⟩ =>
@@ -277,27 +382,28 @@ def curr : Iterator → UInt8
     else
       default
 
-/-- Moves the iterator's position forward by one byte, unconditionally.
+/--
+Moves the iterator's position forward by one byte, unconditionally.
 
 It is only valid to call this function if the iterator is not at the end of the array, *i.e.*
-`Iterator.atEnd` is `false`; otherwise, the resulting iterator will be invalid. -/
+{name}`Iterator.atEnd` is {name}`false`; otherwise, the resulting iterator will be invalid.
+-/
 @[inline]
 def next : Iterator → Iterator
   | ⟨arr, i⟩ => ⟨arr, i + 1⟩
 
-/-- Decreases the iterator's position.
+/--
+Decreases the iterator's position.
 
-If the position is zero, this function is the identity. -/
+If the position is zero, this function is the identity.
+-/
 @[inline]
 def prev : Iterator → Iterator
   | ⟨arr, i⟩ => ⟨arr, i - 1⟩
 
-/-- True if the iterator is past the array's last byte. -/
-@[inline]
-def atEnd : Iterator → Bool
-  | ⟨arr, i⟩ => i ≥ arr.size
-
-/-- True if the iterator is not past the array's last byte. -/
+/--
+True if the iterator is valid; that is, it is not past the array's last byte.
+-/
 @[inline]
 def hasNext : Iterator → Bool
   | ⟨arr, i⟩ => i < arr.size
@@ -323,17 +429,21 @@ def next' (it : Iterator) (_h : it.hasNext) : Iterator :=
 def hasPrev : Iterator → Bool
   | ⟨_, i⟩ => i > 0
 
-/-- Moves the iterator's position to the end of the array.
+/--
+Moves the iterator's position to the end of the array.
 
-Note that `i.toEnd.atEnd` is always `true`. -/
+Given {given}`i : ByteArray.Iterator`, note that {lean}`i.toEnd.atEnd` is always {name}`true`.
+-/
 @[inline]
 def toEnd : Iterator → Iterator
   | ⟨arr, _⟩ => ⟨arr, arr.size⟩
 
-/-- Moves the iterator's position several bytes forward.
+/--
+Moves the iterator's position several bytes forward.
 
 The resulting iterator is only valid if the number of bytes to skip is less than or equal to
-the number of bytes left in the iterator. -/
+the number of bytes left in the iterator.
+-/
 @[inline]
 def forward : Iterator → Nat → Iterator
   | ⟨arr, i⟩, f => ⟨arr, i + f⟩
@@ -341,9 +451,11 @@ def forward : Iterator → Nat → Iterator
 @[inherit_doc forward, inline]
 def nextn : Iterator → Nat → Iterator := forward
 
-/-- Moves the iterator's position several bytes back.
+/--
+Moves the iterator's position several bytes back.
 
-If asked to go back more bytes than available, stops at the beginning of the array. -/
+If asked to go back more bytes than available, stops at the beginning of the array.
+-/
 @[inline]
 def prevn : Iterator → Nat → Iterator
   | ⟨arr, i⟩, f => ⟨arr, i - f⟩

src/Init/Data/ByteArray/Bootstrap.lean

@@ -6,16 +6,22 @@ Author: Markus Himmel
 module
 
 prelude
-public import Init.Prelude
 public import Init.Data.List.Basic
 
 public section
+set_option doc.verso true
 
 namespace ByteArray
 
 @[simp]
 theorem data_push {a : ByteArray} {b : UInt8} : (a.push b).data = a.data.push b := rfl
 
+/--
+Appends two byte arrays.
+
+In compiled code, calls to {name}`ByteArray.append` are replaced with the much more efficient
+{name (scope:="Init.Data.ByteArray.Basic")}`ByteArray.fastAppend`.
+-/
 @[expose]
 protected def append (a b : ByteArray) : ByteArray :=
   ⟨⟨a.data.toList ++ b.data.toList⟩⟩

src/Init/Data/ByteArray/Extra.lean

@@ -9,7 +9,13 @@ prelude
 public import Init.Data.ByteArray.Basic
 import Init.Data.String.Basic
 
-/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
+set_option doc.verso true
+
+/--
+Interprets a {name}`ByteArray` of size 8 as a little-endian {name}`UInt64`.
+
+Panics if the array's size is not 8.
+-/
 public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
@@ -21,7 +27,11 @@ public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
 
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+/--
+Interprets a {name}`ByteArray` of size 8 as a big-endian {name}`UInt64`.
+
+Panics if the array's size is not 8.
+-/
 public def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 0).toUInt64 <<< 0x38 |||

src/Init/Data/ByteArray/Lemmas.lean

@@ -7,10 +7,16 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
-public import Init.Data.Array.Extract
 
 public section
 
+-- At present the preferred normal form for empty byte arrays is `ByteArray.empty`
+@[simp]
+theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl
+
+@[simp]
+theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl
+
 @[simp]
 theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
 
@@ -160,9 +166,9 @@ theorem ByteArray.append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs
   simp only [ByteArray.ext_iff, ← ByteArray.size_data, ByteArray.data_append] at *
   exact Array.append_inj_left h hl
 
-theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i : Nat} (hi : i = a.size) :
-    (a ++ b).extract i (a ++ b).size = b := by
-  subst hi
+theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) :
+    (a ++ b).extract i j = b := by
+  subst hi hj
   ext1
   simp [← size_data]
 
@@ -250,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.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Char.Basic
 public import Init.Data.Char.Lemmas
 public import Init.Data.Char.Order
-
-public section

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.lean

@@ -11,5 +11,3 @@ public import Init.Data.Fin.Log2
 public import Init.Data.Fin.Iterate
 public import Init.Data.Fin.Fold
 public import Init.Data.Fin.Lemmas
-
-public section

src/Init/Data/Fin/Basic.lean

@@ -140,7 +140,7 @@ Modulus of bounded numbers, usually invoked via the `%` operator.
 The resulting value is that computed by the `%` operator on `Nat`.
 -/
 protected def mod : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b,  Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Division of bounded numbers, usually invoked via the `/` operator.
@@ -154,7 +154,7 @@ Examples:
  * `(5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)`
 -/
 protected def div : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
 
 /--
 Modulus of bounded numbers with respect to a `Nat`.
@@ -162,7 +162,7 @@ Modulus of bounded numbers with respect to a `Nat`.
 The resulting value is that computed by the `%` operator on `Nat`.
 -/
 def modn : Fin n → Nat → Fin n
-  | ⟨a, h⟩, m => ⟨a % m, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, m => ⟨a % m, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Bitwise and.

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

@@ -7,15 +7,10 @@ module
 
 prelude
 public import Init.Data.Nat.Lemmas
-public import Init.Data.Int.DivMod.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
 
@@ -327,7 +322,9 @@ theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1 := by
   (match n with | 0 | 1 | n+2 => ?_) <;> try simp
   · exact ⟨nofun⟩
   · exact ⟨fun ⟨0, _⟩ ⟨0, _⟩ => rfl⟩
-  · exact fun h => by have := zero_lt_one (n := n); simp_all [h.elim 0 1]
+  · have : ¬ n + 2 ≤ 1 := by simp [Nat.not_le]
+    simp only [this, iff_false]
+    exact fun h => by have := zero_lt_one (n := n); simp_all [h.elim 0 1]
 
 instance subsingleton_zero : Subsingleton (Fin 0) := subsingleton_iff_le_one.2 (by decide)
 
@@ -914,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.lean

@@ -7,5 +7,3 @@ module
 
 prelude
 public import Init.Data.FloatArray.Basic
-
-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.lean

@@ -10,5 +10,3 @@ public import Init.Data.Format.Basic
 public import Init.Data.Format.Macro
 public import Init.Data.Format.Instances
 public import Init.Data.Format.Syntax
-
-public section