doc: grind attribute modifiers

.claude/commands/release.md

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

.gitattributes

@@ -4,9 +4,3 @@ RELEASES.md merge=union
 stage0/** binary linguist-generated
 # The following file is often manually edited, so do show it in diffs
 stage0/src/stdlib_flags.h -binary -linguist-generated
-# These files should not have line endings translated on Windows, because
-# it throws off parser tests. Later lines override earlier ones, so the
-# runner code is still treated as ordinary text.
-tests/lean/docparse/* eol=lf
-tests/lean/docparse/*.lean eol=auto
-tests/lean/docparse/*.sh eol=auto

.github/workflows/actionlint.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v5
+      uses: actions/checkout@v4
     - name: actionlint
       uses: raven-actions/actionlint@v2
       with:

.github/workflows/awaiting-manual.yml

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

.github/workflows/awaiting-mathlib.yml

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

.github/workflows/build-template.yml

@@ -3,6 +3,9 @@ name: build-template
 on:
   workflow_call:
     inputs:
+      check-level:
+        type: string
+        required: true
       config:
         type: string
         required: true
@@ -67,7 +70,7 @@ jobs:
         if: runner.os == 'macOS'
       - name: Checkout
         if: (!endsWith(matrix.os, '-with-cache'))
-        uses: actions/checkout@v5
+        uses: actions/checkout@v4
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
@@ -113,10 +116,10 @@ jobs:
             build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
-          key: ${{ matrix.name }}-build-v4-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
-            ${{ matrix.name }}-build-v4
+            ${{ matrix.name }}-build-v3
       # open nix-shell once for initial setup
       - name: Setup
         run: |
@@ -226,8 +229,8 @@ jobs:
         id: test
         run: |
           ulimit -c unlimited  # coredumps
-          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: matrix.test
+          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml
+        if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
       - name: Test Summary
         uses: test-summary/action@v2
         with:

.github/workflows/check-prelude.yml

@@ -7,7 +7,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v5
+        uses: actions/checkout@v4
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}

.github/workflows/check-stage0.yml

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

.github/workflows/ci.yml

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

.github/workflows/copyright-header.yml

@@ -6,7 +6,7 @@ jobs:
   check-lean-files:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v4
 
     - name: Verify .lean files start with a copyright header.
       run: |

.github/workflows/grove.yml

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

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

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

.github/workflows/pr-body.yml

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

.github/workflows/pr-release.yml

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

.github/workflows/pr-title.yml

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

.github/workflows/stale.yml

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

.github/workflows/update-stage0.yml

@@ -21,13 +21,11 @@ jobs:
     runs-on: nscloud-ubuntu-22.04-amd64-8x16
     env:
       CCACHE_DIR: ${{ github.workspace }}/.ccache
-      CCACHE_COMPRESS: true
-      CCACHE_MAXSIZE: 400M
     steps:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at
     # https://stackoverflow.com/a/76135647/946226
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v4
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
     - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
@@ -69,19 +67,15 @@ jobs:
           build/stage1/**/*.ir
           build/stage1/**/*.c
           build/stage1/**/*.c.o*
-        key: Linux Lake-build-v4-${{ github.sha }}
+        key: Linux Lake-build-v3-${{ github.sha }}
         # fall back to (latest) previous cache
         restore-keys: |
-          Linux Lake-build-v4
+          Linux Lake-build-v3
     - if: env.should_update_stage0 == 'yes'
-      # sync options with `Linux Lake` to ensure cache reuse
-      run: |
-        mkdir -p build
-        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
+      run: cmake --preset release
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
-      run: |
-        make -j$NPROC -C build update-stage0-commit
+      run: make -j$NPROC -C build/release  update-stage0-commit
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: git show --stat

.gitignore

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

CODEOWNERS

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

README.md

@@ -2,19 +2,19 @@ This is the repository for **Lean 4**.
 
 # About
 
-- [Quickstart](https://lean-lang.org/install/)
+- [Quickstart](https://lean-lang.org/documentation/setup/)
 - [Homepage](https://lean-lang.org)
 - [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
 - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
-- [Documentation Overview](https://lean-lang.org/learn/)
+- [Documentation Overview](https://lean-lang.org/documentation/)
 - [Language Reference](https://lean-lang.org/doc/reference/latest/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://lean-lang.org/examples/)
+- [Examples](https://lean-lang.org/lean4/doc/examples.html)
 - [External Contribution Guidelines](CONTRIBUTING.md)
 
 # Installation
 
-See [Install Lean](https://lean-lang.org/install/).
+See [Setting Up Lean](https://lean-lang.org/documentation/setup/).
 
 # Contributing
 

doc/dev/ffi.md

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

doc/dev/index.md

@@ -8,7 +8,7 @@ You should not edit the `stage0` directory except using the commands described i
 
 ## Development Setup
 
-You can use any of the [supported editors](https://lean-lang.org/install/manual/) for editing the Lean source code.
+You can use any of the [supported editors](../setup.md) for editing the Lean source code.
 Please see below for specific instructions for VS Code.
 
 ### Dev setup using elan
@@ -99,19 +99,3 @@ on to `nightly-with-manual` branch. (It is fine to force push after rebasing.)
 CI will generate a branch of the reference manual called `lean-pr-testing-NNNN`
 in `leanprover/reference-manual`. This branch uses the toolchain for your PR,
 and will report back to the Lean PR with results from Mathlib CI.
-
-### Avoiding rebuilds for downstream projects
-
-If you want to test changes to Lean on downstream projects and would like to avoid rebuilding modules you have already built/fetched using the project's configured Lean toolchain, you can often do so as long as your build of Lean is close enough to that Lean toolchain (compatible .olean format including structure of all relevant environment extensions).
-
-To override the toolchain without rebuilding for a single command, for example `lake build` or `lake lean`, you can use the prefix
-```
-LEAN_GITHASH=$(lean --githash) lake +lean4 ...
-```
-Alternatively, use
-```
-export LEAN_GITHASH=$(lean --githash)
-export ELAN_TOOLCHAIN=lean4
-```
-to persist these changes for the lifetime of the current shell, which will affect any processes spawned from it such as VS Code started via `code .`.
-If you use a setup where you cannot directly start your editor from the command line, such as VS Code Remote, you might want to consider using [direnv](https://direnv.net/) together with an editor extension for it instead so that you can put the lines above into `.envrc`.

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.
-      --^ completion
+      --^ textDocument/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

doc/make/index.md

@@ -1,6 +1,6 @@
 These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](../dev/index.md).
 
-We strongly suggest that new users instead follow the [Installation Instructions](https://lean-lang.org/install/) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
+We strongly suggest that new users instead follow the [Quickstart](../quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
 
 Requirements
 ------------

flake.nix

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

lean.code-workspace

@@ -8,15 +8,9 @@
 		},
 		{
 			"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",
@@ -43,15 +37,6 @@
 					"isDefault": true
 				}
 			},
-			{
-				"label": "build-old",
-				"type": "shell",
-				"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4) LAKE_EXTRA_ARGS=--old",
-				"problemMatcher": [],
-				"group": {
-					"kind": "build"
-				}
-			},
 			{
 				"label": "test",
 				"type": "shell",

script/Modulize.lean

@@ -1,75 +0,0 @@
-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.rawEndPos
-
-    -- prepend each import with `public `
-    for imp in imps.reverse do
-      let insertPos := imp.raw.getPos?.get!
-      let prfx := if doMeta then "public meta " else "public "
-      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
-
-    -- insert `module` header
-    let mut initText := text.extract 0 startPos
-    if !initText.trim.isEmpty then
-      -- If there is a header comment, preserve it and put `module` in the line after
-      initText := initText.trimRight ++ "\n"
-    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
-
-    IO.FS.writeFile path text

script/Shake.lean

@@ -1,584 +0,0 @@
-/-
-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.rawEndPos stx.raw.getTailPos?.get! + ⟨1⟩
-      seen := seen.insert mod
-    out := out ++ text.extract pos insertion
-    for mod in add do
-      if !seen.contains mod then
-        seen := seen.insert mod
-        out := out ++ s!"{mod}\n"
-    out := out ++ text.extract insertion text.rawEndPos
-
-    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

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

script/lean-toolchain

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

script/merge_remote.py

@@ -5,7 +5,6 @@ Merge a tag into a branch on a GitHub repository.
 
 This script checks if a specified tag can be merged cleanly into a branch and performs
 the merge if possible. If the merge cannot be done cleanly, it prints a helpful message.
-Merge conflicts in the lean-toolchain file are automatically resolved by accepting the incoming changes.
 
 Usage:
     python3 merge_remote.py <org/repo> <branch> <tag>
@@ -59,32 +58,6 @@ def clone_repo(repo, temp_dir):
     return True
 
 
-def get_conflicted_files():
-    """Get list of files with merge conflicts."""
-    result = run_command("git diff --name-only --diff-filter=U", check=False)
-    if result.returncode == 0:
-        return result.stdout.strip().split('\n') if result.stdout.strip() else []
-    return []
-
-
-def resolve_lean_toolchain_conflict(tag):
-    """Resolve lean-toolchain conflict by accepting incoming (tag) changes."""
-    print("Resolving lean-toolchain conflict by accepting incoming changes...")
-    # Accept theirs (incoming) version for lean-toolchain
-    result = run_command(f"git checkout --theirs lean-toolchain", check=False)
-    if result.returncode != 0:
-        print("Failed to resolve lean-toolchain conflict")
-        return False
-
-    # Add the resolved file
-    add_result = run_command("git add lean-toolchain", check=False)
-    if add_result.returncode != 0:
-        print("Failed to stage resolved lean-toolchain")
-        return False
-
-    return True
-
-
 def check_and_merge(repo, branch, tag, temp_dir):
     """Check if tag can be merged into branch and perform the merge if possible."""
     # Change to the temporary directory
@@ -125,37 +98,12 @@ def check_and_merge(repo, branch, tag, temp_dir):
     # Try merging the tag directly
     print(f"Merging {tag} into {branch}...")
     merge_result = run_command(f"git merge {tag} --no-edit", check=False)
-
+    
     if merge_result.returncode != 0:
-        # Check which files have conflicts
-        conflicted_files = get_conflicted_files()
-
-        if conflicted_files == ['lean-toolchain']:
-            # Only lean-toolchain has conflicts, resolve it
-            print("Merge conflict detected only in lean-toolchain.")
-            if resolve_lean_toolchain_conflict(tag):
-                # Continue the merge with the resolved conflict
-                print("Continuing merge with resolved lean-toolchain...")
-                continue_result = run_command(f"git commit --no-edit", check=False)
-                if continue_result.returncode != 0:
-                    print("Failed to complete merge after resolving lean-toolchain")
-                    run_command("git merge --abort")
-                    return False
-            else:
-                print("Failed to resolve lean-toolchain conflict")
-                run_command("git merge --abort")
-                return False
-        else:
-            # Other files have conflicts, or unable to determine
-            if conflicted_files:
-                print(f"Cannot merge {tag} cleanly into {branch}.")
-                print(f"Merge conflicts in: {', '.join(conflicted_files)}")
-            else:
-                print(f"Cannot merge {tag} cleanly into {branch}.")
-                print("Merge conflicts would occur.")
-            print("Aborting merge.")
-            run_command("git merge --abort")
-            return False
+        print(f"Cannot merge {tag} cleanly into {branch}.")
+        print("Merge conflicts would occur. Aborting merge.")
+        run_command("git merge --abort")
+        return False
     
     print(f"Pushing changes to remote...")
     push_result = run_command(f"git push origin {branch}")

script/release_checklist.py

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

script/release_notes.py

@@ -52,7 +52,6 @@ def sort_sections_order():
     return [
         "Language",
         "Library",
-        "Tactics",
         "Compiler",
         "Pretty Printing",
         "Documentation",

script/release_repos.yml

@@ -1,11 +1,4 @@
 repositories:
-  - name: lean4-cli
-    url: https://github.com/leanprover/lean4-cli
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
   - name: batteries
     url: https://github.com/leanprover-community/batteries
     toolchain-tag: true
@@ -14,13 +7,6 @@ repositories:
     bump-branch: true
     dependencies: []
 
-  - name: verso
-    url: https://github.com/leanprover/verso
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
   - name: lean4checker
     url: https://github.com/leanprover/lean4checker
     toolchain-tag: true
@@ -35,6 +21,20 @@ repositories:
     branch: master
     dependencies: []
 
+  - name: lean4-cli
+    url: https://github.com/leanprover/lean4-cli
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: verso
+    url: https://github.com/leanprover/verso
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: plausible
     url: https://github.com/leanprover-community/plausible
     toolchain-tag: true
@@ -96,15 +96,6 @@ repositories:
       - import-graph
       - plausible
 
-  - name: cslib
-    url: https://github.com/leanprover/cslib
-    toolchain-tag: true
-    stable-branch: true
-    branch: main
-    bump-branch: true
-    dependencies:
-      - mathlib4
-
   - name: repl
     url: https://github.com/leanprover-community/repl
     toolchain-tag: true
@@ -112,11 +103,3 @@ repositories:
     branch: master
     dependencies:
       - mathlib4
-
-  - name: lean-fro.org
-    url: https://github.com/leanprover/lean-fro.org
-    toolchain-tag: false
-    stable-branch: false
-    branch: master
-    dependencies:
-      - verso

script/release_steps.py

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

src/CMakeLists.txt

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

src/Init.lean

@@ -42,8 +42,5 @@ public import Init.While
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try
-public meta import Init.Try  -- make sure `Try.Config` can be evaluated anywhere
 public import Init.BinderNameHint
 public import Init.Task
-public import Init.MethodSpecsSimp
-public import Init.LawfulBEqTactics

src/Init/BinderNameHint.lean

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

src/Init/Classical.lean

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

src/Init/Control.lean

@@ -16,3 +16,5 @@ 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,6 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Control.State
+public import Init.Control.Except
 public import Init.Data.ToString.Basic
 
 public section
@@ -17,8 +19,8 @@ variable {ε σ α : Type u}
 
 instance [ToString ε] [ToString α] : ToString (Result ε σ α) where
   toString
-    | Result.ok a _    => String.Internal.append "ok: " (toString a)
-    | Result.error e _ => String.Internal.append "error: " (toString e)
+    | Result.ok a _    => "ok: " ++ toString a
+    | Result.error e _ => "error: " ++ toString e
 
 instance [Repr ε] [Repr α] : Repr (Result ε σ α) where
   reprPrec

src/Init/Control/Except.lean

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

src/Init/Control/Lawful.lean

@@ -10,3 +10,5 @@ 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,6 +7,8 @@ module
 
 prelude
 public import Init.Ext
+public import Init.SimpLemmas
+public import Init.Meta
 
 public section
 
@@ -145,7 +147,7 @@ class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplica
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
 attribute [simp] pure_bind bind_assoc bind_pure_comp
-attribute [grind <=] pure_bind
+attribute [grind] pure_bind
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
   change x >>= (fun a => pure (id a)) = x
@@ -250,7 +252,6 @@ instance : LawfulMonad Id := by
 @[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
 @[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
 @[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
-@[simp] theorem pure_run (a : Id α) : pure a.run = a := rfl
 @[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
 @[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl

src/Init/Control/Lawful/Instances.lean

@@ -7,11 +7,12 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
+public import Init.Control.Except
 import all Init.Control.Except
-public import Init.Control.Option
-import all Init.Control.Option
+public import Init.Control.State
 import all Init.Control.State
 public import Init.Control.StateRef
+public import Init.Ext
 
 public section
 
@@ -21,24 +22,23 @@ open Function
 
 namespace ExceptT
 
-@[ext, grind ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
+@[ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
   simp [run] at h
   assumption
 
-@[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
+@[simp] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
 
-@[simp, grind =] theorem run_lift  [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
+@[simp] theorem run_lift  [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
 
-@[simp, grind =] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
+@[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
 
-@[simp, grind =] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
+@[simp] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
   simp [ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
 
-@[simp, grind =] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
+@[simp] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
   simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]
 
-@[grind =]
-theorem run_bind [Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β)
+theorem run_bind [Monad m] (x : ExceptT ε m α)
         : run (x >>= f : ExceptT ε m β)
           =
           run x >>= fun
@@ -46,10 +46,10 @@ theorem run_bind [Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β)
                      | Except.error e => pure (Except.error e) :=
   rfl
 
-@[simp, grind =] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
+@[simp] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
   simp [ExceptT.lift, pure, ExceptT.pure]
 
-@[simp, grind =] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
+@[simp] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
     : (f <$> x).run = Except.map f <$> x.run := by
   simp [Functor.map, ExceptT.map, ←bind_pure_comp]
   apply bind_congr
@@ -109,147 +109,32 @@ 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
 
-@[ext, grind ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
+@[ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
   simp [run] at h
   exact funext h
 
-@[simp, grind =] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
+@[simp] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
 
-@[simp, grind =] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
+@[simp] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
     : (x >>= f).run ctx = x.run ctx >>= λ a => (f a).run ctx := rfl
 
-@[simp, grind =] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
+@[simp] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
     : (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx) := rfl
 
-@[simp, grind =] theorem run_map [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ)
+@[simp] theorem run_map [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ)
     : (f <$> x).run ctx = f <$> x.run ctx := rfl
 
-@[simp, grind =] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
+@[simp] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
     : (monadLift x : ReaderT ρ m α).run ctx = (monadLift x : m α) := rfl
 
-@[simp, grind =] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ)
+@[simp] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ)
     : (monadMap @f x : ReaderT ρ m α).run ctx = monadMap @f (x.run ctx) := rfl
 
-@[simp, grind =] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
+@[simp] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
 
 @[simp] theorem run_seq {α β : Type u} [Monad m] (f : ReaderT ρ m (α → β)) (x : ReaderT ρ m α) (ctx : ρ)
     : (f <*> x).run ctx = (f.run ctx <*> x.run ctx) := rfl
@@ -290,39 +175,38 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
 
 namespace StateT
 
-@[ext, grind ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
+@[ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   funext h
 
-@[simp, grind =] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
+@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
   rfl
 
-@[simp, grind =] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
+@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
 
-@[simp, grind =] theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
+@[simp] theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
     : (x >>= f).run s = x.run s >>= λ p => (f p.1).run p.2 := by
   simp [bind, StateT.bind, run]
 
-@[simp, grind =] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
+@[simp] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
   simp [Functor.map, StateT.map, run, ←bind_pure_comp]
 
-@[simp, grind =] theorem run_get [Monad m] (s : σ)    : (get : StateT σ m σ).run s = pure (s, s) := rfl
+@[simp] theorem run_get [Monad m] (s : σ)    : (get : StateT σ m σ).run s = pure (s, s) := rfl
 
-@[simp, grind =] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (⟨⟩, s') := rfl
+@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (⟨⟩, s') := rfl
 
-@[simp, grind =] theorem run_modify [Monad m] (f : σ → σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (⟨⟩, f s) := rfl
+@[simp] theorem run_modify [Monad m] (f : σ → σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (⟨⟩, f s) := rfl
 
-@[simp, grind =] theorem run_modifyGet [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
+@[simp] theorem run_modifyGet [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
   simp [modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, run]
 
-@[simp, grind =] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
+@[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
 
-@[grind =]
 theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
   simp [StateT.lift, StateT.run, bind, StateT.bind]
 
-@[simp, grind =] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
+@[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
 
-@[simp, grind =] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) :
+@[simp] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) :
     (monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
 
 @[simp] theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2) := by

src/Init/Control/Lawful/Lemmas.lean

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

src/Init/Control/Lawful/MonadLift.lean

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

src/Init/Control/Reader.lean

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

src/Init/Control/State.lean

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

src/Init/Core.lean

@@ -8,6 +8,7 @@ notation, basic datatypes and type classes
 module
 
 prelude
+public meta import Init.Prelude
 public import Init.SizeOf
 
 public section
@@ -100,6 +101,7 @@ instance : DecidableEq Empty := fun a => a.elim
 /-- Decidable equality for PEmpty -/
 instance : DecidableEq PEmpty := fun a => a.elim
 
+set_option genInjectivity false in
 /--
 Delays evaluation. The delayed code is evaluated at most once.
 
@@ -143,9 +145,8 @@ 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.
-/-- Implementation detail. -/
-@[inline] def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
-@[csimp] theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
+@[inline] private def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
+@[csimp] private 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
@@ -616,6 +617,7 @@ class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/
   sep : (α → Prop) → γ → γ
 
+set_option genInjectivity false in
 /--
 `Task α` is a primitive for asynchronous computation.
 It represents a computation that will resolve to a value of type `α`,
@@ -1580,7 +1582,6 @@ instance {p q : Prop} [d : Decidable (p ↔ q)] : Decidable (p = q) :=
 
 gen_injective_theorems% Array
 gen_injective_theorems% BitVec
-gen_injective_theorems% ByteArray
 gen_injective_theorems% Char
 gen_injective_theorems% DoResultBC
 gen_injective_theorems% DoResultPR
@@ -1605,7 +1606,7 @@ gen_injective_theorems% PSigma
 gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
-gen_injective_theorems% String.Pos.Raw
+gen_injective_theorems% String.Pos
 gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum
@@ -2547,3 +2548,7 @@ class Irrefl (r : α → α → Prop) : Prop where
   irrefl : ∀ a, ¬r a a
 
 end Std
+
+/-- Deprecated alias for `XorOp`. -/
+@[deprecated XorOp (since := "2025-07-30")]
+abbrev Xor := XorOp

src/Init/Data.lean

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

src/Init/Data/Array.lean

@@ -30,3 +30,5 @@ 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,7 +6,10 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
+public import Init.Data.Array.Mem
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Count
+public import Init.Data.List.Attach
 import all Init.Data.List.Attach
 
 public section
@@ -81,10 +84,10 @@ well-founded recursion mechanism to prove that the function terminates.
   simp [pmap]
 
 /-- Implementation of `pmap` using the zero-copy version of `attach`. -/
-@[inline] def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
+@[inline] private 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] theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] private 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]
@@ -92,16 +95,16 @@ well-founded recursion mechanism to prove that the function terminates.
   intro a m h₁ h₂
   congr
 
-@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
+@[simp, grind =] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
 
-@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
+@[simp, grind =] 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] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
+@[simp, grind =] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
 
-@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
+@[simp, grind =] 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) =
@@ -118,15 +121,17 @@ theorem pmap_eq_map {p : α → Prop} {f : α → β} {xs : Array α} (H) :
 theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (xs : Array α) {H₁ H₂}
     (h : ∀ a ∈ xs, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f xs H₁ = pmap g xs H₂ := by
   cases xs
-  simp only [List.mem_toArray] at h
+  simp only [mem_toArray] at h
   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
@@ -142,14 +147,14 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
   subst w
   simp
 
-@[simp] theorem attach_push {a : α} {xs : Array α} :
+@[simp, grind =] 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] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp, grind =] 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
@@ -171,6 +176,9 @@ 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
@@ -179,18 +187,21 @@ 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
 
-@[simp, grind ←]
+@[simp, grind]
 theorem mem_attach (xs : Array α) : ∀ x, x ∈ xs.attach
   | ⟨a, h⟩ => by
     have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
-@[simp, grind =]
+@[simp, grind]
 theorem mem_attachWith {xs : Array α} {q : α → Prop} (H) (x : {x // q x}) :
     x ∈ xs.attachWith q H ↔ x.1 ∈ xs := by
   cases xs
@@ -201,13 +212,12 @@ theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {xs H b} :
     b ∈ pmap f xs H ↔ ∃ (a : _) (h : a ∈ xs), f a (H a h) = b := by
   simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
 
+@[grind]
 theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {xs H} {a} (h : a ∈ xs) :
     f a (H a h) ∈ pmap f xs H := by
   rw [mem_pmap]
   exact ⟨a, h, rfl⟩
 
-grind_pattern mem_pmap_of_mem => _ ∈ pmap f xs H, a ∈ xs
-
 @[simp, grind =]
 theorem size_pmap {p : α → Prop} {f : ∀ a, p a → β} {xs H} : (pmap f xs H).size = xs.size := by
   cases xs; simp
@@ -283,23 +293,25 @@ 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] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp, grind =] 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] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp, grind =] 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
@@ -333,7 +345,7 @@ theorem foldl_attach {xs : Array α} {f : β → α → β} {b : β} :
     xs.attach.foldl (fun acc t => f acc t.1) b = xs.foldl f b := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
-    List.foldl_toArray', List.mem_toArray, List.foldl_subtype]
+    List.foldl_toArray', mem_toArray, List.foldl_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
@@ -352,23 +364,25 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
     xs.attach.foldr (fun t acc => f t.1 acc) b = xs.foldr f b := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
-    List.foldr_toArray', List.mem_toArray, List.foldr_subtype]
+    List.foldr_toArray', mem_toArray, List.foldr_subtype]
   congr
   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] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp, grind =] 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
@@ -386,6 +400,9 @@ 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
@@ -421,6 +438,7 @@ 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
@@ -428,7 +446,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   cases xs
   simp [List.pmap_pmap, List.pmap_map]
 
-@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
+@[simp, grind =] 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)) ++
@@ -443,7 +461,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp] theorem attach_append {xs ys : Array α} :
+@[simp, grind =] 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
@@ -451,59 +469,62 @@ 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] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
+@[simp, grind =] 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] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp, grind =] 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] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
+@[simp, grind =] 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] theorem attach_reverse {xs : Array α} :
+@[simp, grind =] 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] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp, grind =] 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] theorem back?_attachWith {P : α → Prop} {xs : Array α}
+@[simp, grind =] 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]
+@[simp, grind =]
 theorem back?_attach {xs : Array α} :
     xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs
@@ -685,7 +706,7 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → Array β} {g : α → Array β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (xs.flatMap f) = xs.unattach.flatMap g := by
   cases xs
-  simp only [List.flatMap_toArray, List.unattach_toArray,
+  simp only [List.flatMap_toArray, List.unattach_toArray, 
     mk.injEq]
   rw [List.flatMap_subtype]
   simp [hf]

src/Init/Data/Array/Basic.lean

@@ -6,6 +6,12 @@ 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.Data.Repr
+public import Init.Data.ToString.Basic
 public import Init.GetElem
 public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
@@ -36,11 +42,11 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp, grind =] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
+@[simp, grind] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
     (set xs i v h).size = xs.size :=
   List.length_set ..
 
-@[simp, grind =] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
+@[simp, grind] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
   List.length_concat ..
 
 theorem ext {xs ys : Array α}
@@ -104,19 +110,13 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-@[simp, grind =] theorem _root_.List.mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+@[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[deprecated List.mem_toArray (since := "2025-09-04")]
-theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l :=
-  List.mem_toArray
-
-@[simp] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
+@[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
 
-grind_pattern getElem_mem => xs[i] ∈ xs
-
 @[simp, grind =] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
 
 @[simp] theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
@@ -125,10 +125,19 @@ 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
 
-@[simp, grind =] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
+@[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
@@ -155,7 +164,7 @@ This is a low-level version of `Array.size` that directly queries the runtime sy
 representation of arrays. While this is not provable, `Array.usize` always returns the exact size of
 the array since the implementation only supports arrays of size less than `USize.size`.
 -/
-@[extern "lean_array_size", simp, expose]
+@[extern "lean_array_size", simp]
 def usize (xs : @& Array α) : USize := xs.size.toUSize
 
 /--
@@ -190,7 +199,7 @@ Examples:
 def pop (xs : Array α) : Array α where
   toList := xs.toList.dropLast
 
-@[simp, grind =] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
+@[simp, grind] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
   match xs with
   | ⟨[]⟩ => rfl
   | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
@@ -399,6 +408,10 @@ 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.
 
@@ -430,7 +443,7 @@ def swapAt! (xs : Array α) (i : Nat) (v : α) : α × Array α :=
     swapAt xs i v
   else
     have : Inhabited (α × Array α) := ⟨(v, xs)⟩
-    panic! String.Internal.append (String.Internal.append "index " (toString i)) " out of bounds"
+    panic! ("index " ++ toString i ++ " out of bounds")
 
 /--
 Returns the first `n` elements of an array. The resulting array is produced by repeatedly calling
@@ -748,7 +761,8 @@ of results.
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
   -- Note: we cannot use `foldlM` here for the reference implementation because this calls
   -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
-  let rec map (i : Nat) (bs : Array β) : m (Array β) := do
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    map (i : Nat) (bs : Array β) : m (Array β) := do
       if hlt : i < as.size then
         map (i+1) (bs.push (← f as[i]))
       else
@@ -908,7 +922,8 @@ entire array is checked.
 @[implemented_by anyMUnsafe, expose]
 def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
   let any (stop : Nat) (h : stop ≤ as.size) :=
-    let rec loop (j : Nat) : m Bool := do
+    let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    loop (j : Nat) : m Bool := do
       if hlt : j < stop then
         have : j < as.size := Nat.lt_of_lt_of_le hlt h
         if (← p as[j]) then
@@ -1246,7 +1261,8 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -1263,7 +1279,8 @@ Examples:
 -/
 @[inline]
 def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some ⟨j, h⟩ else loop (j + 1)
     else none
@@ -1299,6 +1316,7 @@ Examples:
 @[inline, expose]
 def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def idxOfAux [BEq α] (xs : Array α) (v : α) (i : Nat) : Option (Fin xs.size) :=
   if h : i < xs.size then
     if xs[i] == v then some ⟨i, h⟩
@@ -1708,6 +1726,7 @@ Examples:
  * `#[3, 2, 3, 4].popWhile (· > 2) = #[3, 2]`
  * `(#[] : Array Nat).popWhile (· > 2) = #[]`
 -/
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
     if p (as[as.size - 1]'(Nat.sub_lt h (by decide))) then
@@ -1732,7 +1751,8 @@ Examples:
  * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]`
 -/
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec go (i : Nat) (acc : Array α) : Array α :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  go (i : Nat) (acc : Array α) : Array α :=
     if h : i < as.size then
       let a := as[i]
       if p a then
@@ -1755,6 +1775,7 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]`
 -/
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def eraseIdx (xs : Array α) (i : Nat) (h : i < xs.size := by get_elem_tactic) : Array α :=
   if h' : i + 1 < xs.size then
     let xs' := xs.swap (i + 1) i
@@ -1787,6 +1808,7 @@ 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
 
@@ -1849,7 +1871,8 @@ Examples:
  * `#["tues", "thur", "sat"].insertIdx 3 "wed" = #["tues", "thur", "sat", "wed"]`
 -/
 @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
-  let rec loop (as : Array α) (j : Fin as.size) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (as : Array α) (j : Fin as.size) :=
     if i < j then
       let j' : Fin as.size := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
@@ -1903,6 +1926,7 @@ def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
   else
     as
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -1931,7 +1955,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[specialize]
+@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
 def zipWithMAux {m : Type v → Type w} [Monad m] (as : Array α) (bs : Array β) (f : α → β → m γ) (i : Nat) (cs : Array γ) : m (Array γ) := do
   if h : i < as.size then
     let a := as[i]
@@ -2094,6 +2118,7 @@ private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat),
     have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
     a != as[i] && allDiffAuxAux as a i this
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   if h : i < as.size then
     allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
@@ -2144,7 +2169,7 @@ instance {α : Type u} [Repr α] : Repr (Array α) where
   reprPrec xs _ := Array.repr xs
 
 instance [ToString α] : ToString (Array α) where
-  toString xs := String.Internal.append "#" (toString xs.toList)
+  toString xs := "#" ++ toString xs.toList
 
 end Array
 

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 
 public section
@@ -23,6 +24,29 @@ 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
@@ -84,6 +108,9 @@ 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,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Count
@@ -62,7 +63,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,9 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.BEq
 public import Init.Data.List.Nat.BEq
+public import Init.ByCases
 
 public section
 

src/Init/Data/Array/Erase.lean

@@ -6,8 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Erase
+public import Init.Data.List.Nat.Basic
 
 public section
 
@@ -88,7 +91,7 @@ theorem mem_of_mem_eraseP {xs : Array α} : a ∈ xs.eraseP p → a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_eraseP
 
-@[simp, grind =] theorem mem_eraseP_of_neg {xs : Array α} (pa : ¬p a) : a ∈ xs.eraseP p ↔ a ∈ xs := by
+@[simp, grind] theorem mem_eraseP_of_neg {xs : Array α} (pa : ¬p a) : a ∈ xs.eraseP p ↔ a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_eraseP_of_neg pa
 
@@ -237,7 +240,7 @@ theorem mem_of_mem_erase {a b : α} {xs : Array α} (h : a ∈ xs.erase b) : a
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_erase (by simpa using h)
 
-@[simp, grind =] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) :
+@[simp, grind] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) :
     a ∈ xs.erase b ↔ a ∈ xs :=
   erase_eq_eraseP b xs ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)
 
@@ -268,7 +271,7 @@ theorem erase_append [LawfulBEq α] {a : α} {xs ys : Array α} :
     (xs ++ ys).erase a = if a ∈ xs then xs.erase a ++ ys else xs ++ ys.erase a := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.erase_toArray, List.erase_append, List.mem_toArray]
+  simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray]
   split <;> simp
 
 @[grind =]
@@ -321,13 +324,6 @@ 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,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
 
 public section
 

src/Init/Data/Array/FinRange.lean

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

src/Init/Data/Array/Find.lean

@@ -7,7 +7,10 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Attach
 public import Init.Data.Array.Range
 
 public section
@@ -24,11 +27,11 @@ open Nat
 
 /-! ### findSome? -/
 
-@[simp, grind =] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
-@[simp, grind =] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+@[simp, grind] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
+@[simp, grind] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
   cases xs; simp [List.findSome?_append]
 
-@[grind =]
+@[grind]
 theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f = f a := by
   simp
 
@@ -225,12 +228,11 @@ theorem mem_of_find?_eq_some {xs : Array α} (h : find? p xs = some a) : a ∈ x
   simp at h
   simpa using List.mem_of_find?_eq_some h
 
+@[grind]
 theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by
   cases xs
   simp [List.get_find?_mem]
 
-grind_pattern get_find?_mem => (xs.find? p).get h
-
 @[simp, grind =] theorem find?_filter {xs : Array α} (p q : α → Bool) :
     (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
   cases xs; simp
@@ -275,6 +277,9 @@ 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`.
@@ -300,6 +305,9 @@ 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
@@ -309,11 +317,17 @@ 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]
@@ -331,19 +345,34 @@ 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} :
@@ -366,6 +395,7 @@ theorem findIdx_singleton {a : α} {p : α → Bool} :
     #[a].findIdx p = if p a then 0 else 1 := by
   simp
 
+@[grind →]
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
   rcases xs with ⟨xs⟩
   exact List.findIdx_of_getElem?_eq_some (by simpa using w)
@@ -698,7 +728,7 @@ theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
   cases xs
   simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
   rw [findFinIdx?_congr List.unattach_toArray]
-  simp only [Option.map_map, Function.comp_def, Fin.cast_cast]
+  simp only [Option.map_map, Function.comp_def, Fin.cast_trans]
   simp [Array.size]
 
 /-! ### idxOf

src/Init/Data/Array/InsertIdx.lean

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

src/Init/Data/Array/Lex.lean

@@ -8,3 +8,5 @@ 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,8 +6,11 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Data.Range.Polymorphic.Iterators
-public import Init.Data.Range.Polymorphic.Nat
+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
 import Init.Data.Iterators.Consumers
 
 public section
@@ -28,7 +31,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.Rco.lt_upper_of_mem h
+    have : i < min as.size bs.size := Std.PRange.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,7 +10,9 @@ import all Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Lex
+import Init.Data.Range.Polymorphic.Lemmas
 import Init.Data.Range.Polymorphic.NatLemmas
+import Init.Data.Order.Lemmas
 
 public section
 
@@ -40,7 +42,8 @@ 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
-  simp [lex, Std.Rco.forIn'_eq_if]
+  rw [lex, Std.PRange.forIn'_eq_match]
+  simp [Std.PRange.SupportsUpperBound.IsSatisfied]
 
 private theorem cons_lex_cons.forIn'_congr_aux [Monad m] {as bs : ρ} {_ : Membership α ρ}
     [ForIn' m ρ α inferInstance] (w : as = bs)
@@ -61,14 +64,14 @@ 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.Rco.forIn'_eq_forIn'_toList]
+    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.PRange.forIn'_eq_forIn'_toList]
   conv =>
     lhs; congr; congr
-    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 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 (if_pos (by omega)) rfl (fun _ _ _ => 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,
+  simp only [Std.PRange.toList_open_eq_toList_closed_of_isSome_succ? (lo := 0) (h := rfl),
+    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.ClosedOpen.toList_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]
   cases lt a b
@@ -80,10 +83,16 @@ 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₂ <;> simp [lex, Std.Rco.forIn'_eq_if]
+    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]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil => simp [lex, Std.Rco.forIn'_eq_if]
+    | nil =>
+      rw [lex, Std.PRange.forIn'_eq_match]
+      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 

src/Init/Data/Array/MapIdx.lean

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

src/Init/Data/Array/Mem.lean

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

src/Init/Data/Array/Monadic.lean

@@ -6,9 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Control
 import all Init.Data.List.Control
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
+public import Init.Data.List.Monadic
 
 public section
 
@@ -163,7 +167,7 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : α → β
     (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
     forIn' as b f = forIn' bs b' g := by
   cases as <;> cases bs
-  simp only [mk.injEq, List.mem_toArray, List.forIn'_toArray] at w h ⊢
+  simp only [mk.injEq, mem_toArray, List.forIn'_toArray] at w h ⊢
   exact List.forIn'_congr w hb h
 
 /--

src/Init/Data/Array/OfFn.lean

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

src/Init/Data/Array/Perm.lean

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

src/Init/Data/Array/QSort.lean

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

src/Init/Data/Array/Range.lean

@@ -6,10 +6,14 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.OfFn
 import all Init.Data.Array.OfFn
 public import Init.Data.Array.MapIdx
 public import Init.Data.Array.Zip
+public import Init.Data.List.Nat.Range
 
 public section
 
@@ -112,7 +116,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
   rw [← List.toArray_range']
-  simp only [List.find?_toArray, List.mem_toArray]
+  simp only [List.find?_toArray, mem_toArray]
   simp [List.find?_range'_eq_some]
 
 @[simp] theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :

src/Init/Data/Array/Subarray.lean

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

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

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

src/Init/Data/Array/TakeDrop.lean

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

src/Init/Data/Array/Zip.lean

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

src/Init/Data/Basic.lean

@@ -6,5 +6,15 @@ 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,3 +13,5 @@ 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,8 +6,11 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
+public import Init.Data.Fin.Basic
 public import Init.Data.Nat.Bitwise.Lemmas
+public import Init.Data.Nat.Power2
 public import Init.Data.Int.Bitwise.Basic
+public import Init.Data.BitVec.BasicAux
 
 @[expose] public section
 
@@ -26,6 +29,10 @@ 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
 
 /--
@@ -199,13 +206,10 @@ Converts a bitvector into a fixed-width hexadecimal number with enough digits to
 
 If `n` is `0`, then one digit is returned. Otherwise, `⌊(n + 3) / 4⌋` digits are returned.
 -/
--- If we ever want to prove something about this, we can avoid having to use the opaque
--- `Internal` string functions by moving this definition out to a separate file that can live
--- downstream of `Init.Data.String.Basic`.
 protected def toHex {n : Nat} (x : BitVec n) : String :=
   let s := (Nat.toDigits 16 x.toNat).asString
-  let t := (List.replicate ((n+3) / 4 - String.Internal.length s) '0').asString
-  String.Internal.append t s
+  let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
+  t ++ s
 
 /-- `BitVec` representation. -/
 protected def BitVec.repr (a : BitVec n) : Std.Format :=
@@ -867,7 +871,4 @@ def clzAuxRec {w : Nat} (x : BitVec w) (n : Nat) : BitVec w :=
 /-- Count the number of leading zeros. -/
 def clz (x : BitVec w) : BitVec w := clzAuxRec x (w - 1)
 
-/-- Count the number of trailing zeros. -/
-def ctz (x : BitVec w) : BitVec w := (x.reverse).clz
-
 end BitVec

src/Init/Data/BitVec/BasicAux.lean

@@ -21,6 +21,13 @@ namespace BitVec
 
 section Nat
 
+/--
+The bitvector with value `i mod 2^n`.
+-/
+@[expose, match_pattern]
+protected def ofNat (n : Nat) (i : Nat) : BitVec n where
+  toFin := Fin.ofNat (2^n) i
+
 instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 
 /-- Return the bound in terms of toNat. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -6,13 +6,17 @@ 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,7 +9,6 @@ prelude
 public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 import Init.Data.Int.Bitwise.Lemmas
-import Init.Ext
 
 public section
 
@@ -20,7 +19,7 @@ theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
 @[simp, grind =] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
     getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
 
-@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
+@[simp, grind] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false := by
   let ⟨x, x_lt⟩ := x
   simp only [getLsbD_ofFin]
   apply Nat.testBit_lt_two_pow

src/Init/Data/BitVec/Decidable.lean

@@ -8,7 +8,6 @@ module
 
 prelude
 public import Init.Data.BitVec.Bootstrap
-import Init.Ext
 
 public section
 
@@ -50,11 +49,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) (by exact Classical.not_forall_not)
+  decidable_of_iff (¬ ∀ v, ¬ P v) 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) (by exact Classical.not_forall_not)
+  decidable_of_iff (¬ ∀ v, ¬ P v) 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,8 +6,10 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
+public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Lemmas
+public import Init.Data.Nat.Lemmas
 public import Init.Data.Fin.Iterate
 
 public section

src/Init/Data/BitVec/Lemmas.lean

@@ -6,14 +6,22 @@ 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.List.BasicAux
-import Init.Data.List.Lemmas
+public import Init.Data.Order.Factories
 
 public section
 
@@ -29,7 +37,7 @@ namespace BitVec
 @[simp] theorem getElem_ofFin (x : Fin (2^n)) (i : Nat) (h : i < n) :
     (BitVec.ofFin x)[i] = x.val.testBit i := rfl
 
-@[simp, grind =] theorem getMsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
+@[simp, grind] theorem getMsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsbD x i = false := by
   rw [getMsbD]
   simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
   omega
@@ -66,6 +74,10 @@ 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
 
@@ -110,7 +122,7 @@ theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = t
 This normalized a bitvec using `ofFin` to `ofNat`.
 -/
 theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
-  simp only [BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
+  simp only [BitVec.ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
 
 /-- Prove nonequality of bitvectors in terms of nat operations. -/
 theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
@@ -287,7 +299,7 @@ theorem length_pos_of_ne {x y : BitVec w} (h : x ≠ y) : 0 < w :=
 
 theorem ofFin_ofNat (n : Nat) :
     ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
-  simp only [OfNat.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, BitVec.ofNat]
+  simp only [OfNat.ofNat, Fin.ofNat, BitVec.ofNat]
 
 -- We use a `grind_pattern` as `@[grind]` will not use the `no_index` term.
 grind_pattern ofFin_ofNat => ofFin (OfNat.ofNat n : Fin (2^w))
@@ -338,14 +350,25 @@ 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])
@@ -1077,10 +1100,6 @@ theorem toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} :
   rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat, Fin.coe_castLE, val_toFin,
     Nat.mod_eq_of_lt (by apply BitVec.toNat_lt_twoPow_of_le p)]
 
-theorem toNat_setWidth_of_le {w w' : Nat} {b : BitVec w} (h : w ≤ w') : (b.setWidth w').toNat = b.toNat := by
-  rw [BitVec.toNat_setWidth, Nat.mod_eq_of_lt]
-  exact BitVec.toNat_lt_twoPow_of_le h
-
 /-! ## extractLsb -/
 
 @[simp, grind =]
@@ -1268,17 +1287,6 @@ theorem extractLsb'_eq_zero {x : BitVec w} {start : Nat} :
   ext i hi
   omega
 
-theorem extractLsb'_setWidth_of_le {b : BitVec w} {start len w' : Nat} (h : start + len ≤ w') :
-    (b.setWidth w').extractLsb' start len = b.extractLsb' start len := by
-  ext i h_i
-  simp
-  omega
-
-theorem setWidth_extractLsb'_of_le {c : BitVec w} (h : len₁ ≤ len₂) :
-    (c.extractLsb' start len₂).setWidth len₁ = c.extractLsb' start len₁ := by
-  ext i hi
-  simp [show i < len₂ by omega]
-
 /-! ### allOnes -/
 
 @[simp, grind =] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by
@@ -1522,12 +1530,6 @@ theorem extractLsb_and {x : BitVec w} {hi lo : Nat} :
 @[simp, grind =] theorem ofNat_and {x y : Nat} : BitVec.ofNat w (x &&& y) = BitVec.ofNat w x &&& BitVec.ofNat w y :=
   eq_of_toNat_eq (by simp [Nat.and_mod_two_pow])
 
-theorem and_or_distrib_left {x y z : BitVec w} : x &&& (y ||| z) = (x &&& y) ||| (x &&& z) :=
-  BitVec.eq_of_getElem_eq (by simp [Bool.and_or_distrib_left])
-
-theorem and_or_distrib_right {x y z : BitVec w} : (x ||| y) &&& z = (x &&& z) ||| (y &&& z) :=
-  BitVec.eq_of_getElem_eq (by simp [Bool.and_or_distrib_right])
-
 /-! ### xor -/
 
 @[simp, grind =] theorem toNat_xor (x y : BitVec v) :
@@ -2178,10 +2180,6 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
   have := lt_of_getLsbD ha
   omega
 
-theorem setWidth_ushiftRight_eq_extractLsb {b : BitVec w} : (b >>> w').setWidth w'' = b.extractLsb' w' w'' := by
-  ext i hi
-  simp
-
 /-! ### ushiftRight reductions from BitVec to Nat -/
 
 @[simp, grind =]
@@ -2972,9 +2970,10 @@ theorem shiftLeft_eq_concat_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
 /-- Combine adjacent `extractLsb'` operations into a single `extractLsb'`. -/
 theorem extractLsb'_append_extractLsb'_eq_extractLsb' {x : BitVec w} (h : start₂ = start₁ + len₁) :
     ((x.extractLsb' start₂ len₂) ++ (x.extractLsb' start₁ len₁)) =
-      x.extractLsb' start₁ (len₂ + len₁) := by
+    (x.extractLsb' start₁ (len₁ + len₂)).cast (by omega) := by
   ext i h
-  simp only [getElem_append, getElem_extractLsb', dite_eq_ite, ite_eq_left_iff, Nat.not_lt]
+  simp only [getElem_append, getElem_extractLsb', dite_eq_ite, getElem_cast, ite_eq_left_iff,
+    Nat.not_lt]
   intro hi
   congr 1
   omega
@@ -3086,51 +3085,6 @@ theorem extractLsb'_append_eq_of_le {v w} {xhi : BitVec v} {xlo : BitVec w}
     extractLsb' start len (xhi ++ xlo) = extractLsb' (start - w) len xhi := by
   simp [extractLsb'_append_eq_ite, show ¬ start < w by omega]
 
-theorem extractLsb'_append_eq_left {a : BitVec w} {b : BitVec w'} : (a ++ b).extractLsb' w' w = a := by
-  simp [BitVec.extractLsb'_append_eq_of_le]
-
-theorem extractLsb'_append_eq_right {a : BitVec w} {b : BitVec w'} : (a ++ b).extractLsb' 0 w' = b := by
-  simp [BitVec.extractLsb'_append_eq_of_add_le]
-
-theorem setWidth_append_eq_right {a : BitVec w} {b : BitVec w'} : (a ++ b).setWidth w' = b := by
-  ext i hi
-  simp [getLsbD_append, hi]
-
-theorem append_left_inj {s₁ s₂ : BitVec w} (t : BitVec w') : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ := by
-  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
-  ext i hi
-  simpa [getElem_append, dif_neg] using congrArg (·[i + w']'(by omega)) h
-
-theorem append_right_inj (s : BitVec w) {t₁ t₂ : BitVec w'} : s ++ t₁ = s ++ t₂ ↔ t₁ = t₂ := by
-  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
-  ext i hi
-  simpa [getElem_append, hi] using congrArg (·[i]) h
-
-theorem setWidth_append_eq_shiftLeft_setWidth_or {b : BitVec w} {b' : BitVec w'} :
-    (b ++ b').setWidth w'' = (b.setWidth w'' <<< w') ||| b'.setWidth w'' := by
-  ext i hi
-  simp only [getElem_setWidth, getElem_or, getElem_shiftLeft]
-  rw [getLsbD_append]
-  split <;> simp_all
-
-theorem setWidth_append_append_eq_shiftLeft_setWidth_or {b : BitVec w} {b' : BitVec w'} {b'' : BitVec w''} :
-    (b ++ b' ++ b'').setWidth w''' = (b.setWidth w''' <<< (w' + w'')) ||| (b'.setWidth w''' <<< w'') ||| b''.setWidth w''' := by
-  rw [BitVec.setWidth_append_eq_shiftLeft_setWidth_or,
-    BitVec.setWidth_append_eq_shiftLeft_setWidth_or,
-    BitVec.shiftLeft_or_distrib, BitVec.shiftLeft_add]
-
-theorem setWidth_append_append_append_eq_shiftLeft_setWidth_or {b : BitVec w} {b' : BitVec w'} {b'' : BitVec w''} {b''' : BitVec w'''} :
-    (b ++ b' ++ b'' ++ b''').setWidth w'''' = (b.setWidth w'''' <<< (w' + w'' + w''')) ||| (b'.setWidth w'''' <<< (w'' + w''')) |||
-      (b''.setWidth w'''' <<< w''') ||| b'''.setWidth w'''' := by
-  simp only [BitVec.setWidth_append_eq_shiftLeft_setWidth_or, BitVec.shiftLeft_or_distrib, BitVec.shiftLeft_add]
-
-theorem and_setWidth_allOnes (w' w : Nat) (b : BitVec (w' + w)) :
-    b &&& (BitVec.allOnes w).setWidth (w' + w) = 0#w' ++ b.setWidth w := by
-  ext i hi
-  simp only [getElem_and, getElem_setWidth, getLsbD_allOnes]
-  rw [BitVec.getElem_append]
-  split <;> simp_all
-
 /-! ### rev -/
 
 @[grind =]
@@ -3742,9 +3696,6 @@ theorem neg_add {x y : BitVec w} : - (x + y) = - x - y := by
   apply eq_of_toInt_eq
   simp [toInt_neg, toInt_add, Int.neg_add, Int.add_neg_eq_sub]
 
-theorem sub_sub (a b c : BitVec n) : a - b - c = a - (b + c) := by
-  simp [BitVec.sub_eq_add_neg, BitVec.add_assoc, BitVec.neg_add]
-
 theorem add_neg_eq_sub {x y : BitVec w} : x + - y = (x - y) := by
   apply eq_of_toInt_eq
   simp [toInt_neg, Int.sub_eq_add_neg]
@@ -4090,9 +4041,6 @@ instance instLawfulOrderLT : LawfulOrderLT (BitVec n) := by
   apply LawfulOrderLT.of_le
   simpa using fun _ _ => BitVec.lt_asymm
 
-theorem length_pos_of_lt {b b' : BitVec w} (h : b < b') : 0 < w :=
-  length_pos_of_ne (BitVec.ne_of_lt h)
-
 protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y := by
   simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod]
   apply Nat.mod_lt
@@ -4164,14 +4112,6 @@ theorem lt_of_msb_false_of_msb_true {x y : BitVec w} (hx : x.msb = false) (hy :
   simp
   omega
 
-theorem lt_add_one {b : BitVec w} (h : b ≠ allOnes w) : b < b + 1 := by
-  simp only [ne_eq, ← toNat_inj, toNat_allOnes] at h
-  simp only [BitVec.lt_def, ofNat_eq_ofNat, toNat_add, toNat_ofNat, Nat.add_mod_mod]
-  rw [Nat.mod_eq_of_lt]
-  · exact Nat.lt_add_one _
-  · have := b.toNat_lt_twoPow_of_le (Nat.le_refl _)
-    omega
-
 /-! ### udiv -/
 
 theorem udiv_def {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat) := by
@@ -5317,7 +5257,7 @@ theorem replicate_succ' {x : BitVec w} :
     (replicate n x ++ x).cast (by rw [Nat.mul_succ]) := by
   simp [replicate_append_self]
 
-theorem setWidth_add_eq_mod {x y : BitVec w} : BitVec.setWidth i (x + y) = (BitVec.setWidth i x + BitVec.setWidth i y) % (BitVec.twoPow i w) := by
+theorem BitVec.setWidth_add_eq_mod {x y : BitVec w} : BitVec.setWidth i (x + y) = (BitVec.setWidth i x + BitVec.setWidth i y) % (BitVec.twoPow i w) := by
   apply BitVec.eq_of_toNat_eq
   rw [toNat_setWidth]
   simp only [toNat_setWidth, toNat_add, toNat_umod, Nat.add_mod_mod, Nat.mod_add_mod, toNat_twoPow]
@@ -5326,14 +5266,6 @@ theorem setWidth_add_eq_mod {x y : BitVec w} : BitVec.setWidth i (x + y) = (BitV
   · have hk : 2 ^ w < 2 ^ i := Nat.pow_lt_pow_of_lt (by decide) (Nat.lt_of_not_le h)
     rw [Nat.mod_eq_of_lt hk, Nat.mod_mod_eq_mod_mod_of_dvd (Nat.pow_dvd_pow _ (Nat.le_of_not_le h))]
 
-theorem setWidth_setWidth_eq_self {a : BitVec w} {w' : Nat} (h : a < BitVec.twoPow w w') : (a.setWidth w').setWidth w = a := by
-  by_cases hw : w' < w
-  · simp only [toNat_eq, toNat_setWidth]
-    rw [Nat.mod_mod_of_dvd' (Nat.pow_dvd_pow _ (Nat.le_of_lt hw)), Nat.mod_eq_of_lt]
-    rwa [BitVec.lt_def, BitVec.toNat_twoPow_of_lt hw] at h
-  · rw [BitVec.lt_def, BitVec.toNat_twoPow_of_le (by omega)] at h
-    simp at h
-
 /-! ### intMin -/
 
 @[grind =]
@@ -5847,25 +5779,6 @@ theorem msb_replicate {n w : Nat} {x : BitVec w} :
   simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]
   cases n <;> cases w <;> simp
 
-@[simp]
-theorem reverse_eq_zero_iff {x : BitVec w} :
-    x.reverse = 0#w ↔ x = 0#w := by
-  constructor
-  · intro hrev
-    ext i hi
-    rw [← getLsbD_eq_getElem, getLsbD_eq_getMsbD, ← getLsbD_reverse]
-    simp [hrev]
-  · intro hzero
-    ext i hi
-    rw [← getLsbD_eq_getElem, getLsbD_eq_getMsbD, getMsbD_reverse]
-    simp [hi, hzero]
-
-@[simp]
-theorem reverse_reverse_eq {x : BitVec w} :
-    x.reverse.reverse = x := by
-  ext k hk
-  rw [getElem_reverse, getMsbD_reverse, getLsbD_eq_getElem]
-
 /-! ### Inequalities (le / lt) -/
 
 theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
@@ -5996,12 +5909,6 @@ theorem getElem_eq_true_of_lt_of_le {x : BitVec w} (hk' : k < w) (hlt: x.toNat <
       omega
   · simp [show w ≤ k + k' by omega] at hk'
 
-theorem not_lt_iff {b : BitVec w} : ~~~b < b ↔ 0 < w ∧ b.msb = true := by
-  refine ⟨fun h => ?_, fun ⟨hw, hb⟩ => ?_⟩
-  · have := length_pos_of_lt h
-    exact ⟨this, by rwa [← ult_iff_lt, ult_eq_msb_of_msb_neq (by simp_all)] at h⟩
-  · rwa [← ult_iff_lt, ult_eq_msb_of_msb_neq (by simp_all)]
-
 /-! ### Count leading zeros -/
 
 theorem clzAuxRec_zero (x : BitVec w) :
@@ -6275,70 +6182,16 @@ theorem toNat_lt_two_pow_sub_clz {x : BitVec w} :
         · simp [show w + 1 ≤ i by omega]
       · simp; omega
 
-theorem clz_eq_reverse_ctz {x : BitVec w} :
-    x.clz = (x.reverse).ctz := by
-  simp [ctz]
 
-/-! ### Count trailing zeros -/
+/-! ### Deprecations -/
 
-theorem ctz_eq_reverse_clz {x : BitVec w} :
-    x.ctz = (x.reverse).clz := by
-  simp [ctz]
+set_option linter.missingDocs false
+
+@[deprecated toFin_uShiftRight (since := "2025-02-18")]
+abbrev toFin_uShiftRight := @toFin_ushiftRight
 
-/-- The number of trailing zeroes is strictly less than the bitwidth iff the bitvector is nonzero. -/
-@[simp]
-theorem ctz_lt_iff_ne_zero {x : BitVec w} :
-    ctz x < w ↔ x ≠ 0#w := by
-  simp only [ctz_eq_reverse_clz, natCast_eq_ofNat, ne_eq]
-  rw [show BitVec.ofNat w w = w by simp, ← reverse_eq_zero_iff (x := x)]
-  apply clz_lt_iff_ne_zero (x := x.reverse)
 
-/-- If a bitvec is different than zero the bits at indexes lower than `ctz x` are false. -/
-theorem getLsbD_false_of_lt_ctz {x : BitVec w} (hi : i < x.ctz.toNat) :
-    x.getLsbD i = false := by
-  rw [getLsbD_eq_getMsbD, ← getLsbD_reverse]
-  have hiff := ctz_lt_iff_ne_zero (x := x)
-  by_cases hzero : x = 0#w
-  · simp [hzero, getLsbD_reverse]
-  · simp only [ctz_eq_reverse_clz, natCast_eq_ofNat, ne_eq, hzero, not_false_eq_true,
-      iff_true] at hiff
-    simp only [ctz] at hi
-    have hi' : i < w := by simp [BitVec.lt_def] at hiff; omega
-    simp only [hi', decide_true, Bool.true_and]
-    have : (x.reverse.clzAuxRec (w - 1)).toNat ≤ w := by
-      rw [show ((x.reverse.clzAuxRec (w - 1)).toNat ≤ w) =
-            ((x.reverse.clzAuxRec (w - 1)).toNat ≤ (BitVec.ofNat w w).toNat) by simp, ← le_def]
-      apply clzAuxRec_le (x := x.reverse) (n := w - 1)
-    let j := (x.reverse.clzAuxRec (w - 1)).toNat - 1 - i
-    rw [show w - 1 - i = w - (x.reverse.clzAuxRec (w - 1)).toNat + j by
-      subst j
-      rw [Nat.sub_sub (n := (x.reverse.clzAuxRec (w - 1)).toNat),
-        ← Nat.add_sub_assoc (by exact Nat.one_add_le_iff.mpr hi)]
-      omega]
-    have hfalse : ∀ (i : Nat), w - 1 < i → x.reverse.getLsbD i = false := by
-      intros i hj
-      simp [show w ≤ i by omega]
-    exact getLsbD_false_of_clzAuxRec (x := x.reverse) (n := w - 1) hfalse (j := j)
 
-/-- If a bitvec is different than zero, the bit at index `ctz x`, i.e., the first bit after the
-  trailing zeros, is true. -/
-theorem getLsbD_true_ctz_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) :
-    x.getLsbD (ctz x).toNat = true := by
-  simp only [ctz_eq_reverse_clz, clz]
-  rw [getLsbD_eq_getMsbD, ← getLsbD_reverse]
-  have := ctz_lt_iff_ne_zero (x := x)
-  simp only [ctz_eq_reverse_clz, clz, natCast_eq_ofNat, lt_def, toNat_ofNat, Nat.mod_two_pow_self,
-    ne_eq] at this
-  simp only [this, hx, not_false_eq_true, decide_true, Bool.true_and]
-  have hnotrev : ¬x.reverse = 0#w := by simp [reverse_eq_zero_iff, hx]
-  apply getLsbD_true_of_eq_clzAuxRec_of_ne_zero (x := x.reverse) (n := w - 1) hnotrev
-  intro i hi
-  simp [show w ≤ i by omega]
 
-/-- A nonzero bitvector is lower-bounded by its trailing zeroes. -/
-theorem two_pow_ctz_le_toNat_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) :
-    2 ^ (ctz x).toNat ≤ x.toNat := by
-  have hclz := getLsbD_true_ctz_of_ne_zero (x := x) hx
-  exact Nat.ge_two_pow_of_testBit hclz
 
 end BitVec

src/Init/Data/Bool.lean

@@ -10,6 +10,7 @@ public import Init.NotationExtra
 
 public section
 
+
 namespace Bool
 
 /--

src/Init/Data/ByteArray.lean

@@ -7,6 +7,5 @@ module
 
 prelude
 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,15 +6,25 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
+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.Array.Extract
-
-set_option doc.verso true
+public import Init.Data.Option.Basic
 
 @[expose] public section
 universe u
 
+set_option genInjectivity false in
+structure ByteArray where
+  data : Array UInt8
+
+attribute [extern "lean_byte_array_mk"] ByteArray.mk
+attribute [extern "lean_byte_array_data"] ByteArray.data
+
+gen_injective_theorems% ByteArray
+
 namespace ByteArray
 
 deriving instance BEq for ByteArray
@@ -24,49 +34,41 @@ attribute [ext] ByteArray
 instance : DecidableEq ByteArray :=
   fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
 
+@[extern "lean_mk_empty_byte_array"]
+def emptyWithCapacity (c : @& Nat) : ByteArray :=
+  { data := #[] }
+
 @[deprecated emptyWithCapacity (since := "2025-03-12")]
 abbrev mkEmpty := emptyWithCapacity
 
+def empty : ByteArray := emptyWithCapacity 0
+
 instance : Inhabited ByteArray where
   default := empty
 
 instance : EmptyCollection ByteArray where
   emptyCollection := ByteArray.empty
 
-/--
-Retrieves the size of the array as a platform-specific fixed-width integer.
+@[extern "lean_byte_array_push"]
+def push : ByteArray → UInt8 → ByteArray
+  | ⟨bs⟩, b => ⟨bs.push b⟩
+
+@[extern "lean_byte_array_size"]
+def size : (@& ByteArray) → Nat
+  | ⟨bs⟩ => bs.size
 
-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]
@@ -77,94 +79,43 @@ 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", inherit_doc ByteArray.set]
+@[extern "lean_byte_array_uset"]
 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
 
 /--
-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.
--/
+  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. -/
 @[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 :=
+protected def append (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
 
-@[simp]
-theorem size_data {a : ByteArray} :
-  a.data.size = a.size := rfl
+instance : Append ByteArray := ⟨ByteArray.append⟩
 
-@[csimp]
-theorem append_eq_fastAppend : @ByteArray.append = @ByteArray.fastAppend := by
-  funext a b
-  ext1
-  apply Array.ext'
-  simp [ByteArray.fastAppend, copySlice, ← size_data, - Array.append_assoc]
-
--- Needs to come after the `csimp` lemma
-instance : Append ByteArray where
-  append := ByteArray.append
-
-@[simp]
-theorem append_eq {a b : ByteArray} : a.append b = a ++ b := rfl
-
-@[simp]
-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
@@ -175,12 +126,16 @@ def toList (bs : ByteArray) : List UInt8 :=
     decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-/--
-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`.
+@[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
 
-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
@@ -192,29 +147,11 @@ The index is returned along with a proof that it is a valid index in the array.
   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`.
+  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.
 
-The variant {name}`findFinIdx?` additionally returns a proof that the found index is in bounds.
+  TODO: avoid code duplication in the future after we improve the compiler.
 -/
-@[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
@@ -227,11 +164,7 @@ We claim this unsafe implementation is correct because an array cannot have more
       pure b
   loop 0 b
 
-/--
-The reference implementation of {name}`ForIn.forIn` for {name}`ByteArray`.
-
-In compiled code, this is replaced by the more efficient {name}`ByteArray.forInUnsafe`.
--/
+/-- Reference implementation for `forIn` -/
 @[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
@@ -249,13 +182,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
 instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
-/--
-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.
--/
+/-- See comment at `forInUnsafe` -/
 -- 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 β :=
@@ -272,14 +199,7 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   else
     pure init
 
-/--
-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.
--/
+/-- Reference implementation for `foldlM` -/
 @[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) :=
@@ -297,23 +217,11 @@ 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
 
-set_option doc.verso false -- Awaiting intra-module forward reference support
-/--
-Iterator over the bytes (`UInt8`) of a `ByteArray`.
+/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
 
 Typically created by `arr.iter`, where `arr` is a `ByteArray`.
 
@@ -337,7 +245,6 @@ 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 :=
@@ -355,25 +262,16 @@ theorem Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx :=
 
 namespace Iterator
 
-/--
-The number of bytes remaining in the iterator.
--/
+/-- Number of bytes remaining in the iterator. -/
 def remainingBytes : Iterator → Nat
   | ⟨arr, i⟩ => arr.size - i
 
 @[inherit_doc Iterator.idx]
 def pos := Iterator.idx
 
-/-- True if the iterator is past the array's last byte. -/
-@[inline]
-def atEnd : Iterator → Bool
-  | ⟨arr, i⟩ => i ≥ arr.size
+/-- The byte at the current position.
 
-/--
-The byte at the current position.
-
-On an invalid position, returns {lean}`(default : UInt8)`.
--/
+On an invalid position, returns `(default : UInt8)`. -/
 @[inline]
 def curr : Iterator → UInt8
   | ⟨arr, i⟩ =>
@@ -382,28 +280,27 @@ 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.*
-{name}`Iterator.atEnd` is {name}`false`; otherwise, the resulting iterator will be invalid.
--/
+`Iterator.atEnd` is `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 valid; that is, it is not past the array's last byte.
--/
+/-- 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. -/
 @[inline]
 def hasNext : Iterator → Bool
   | ⟨arr, i⟩ => i < arr.size
@@ -429,21 +326,17 @@ 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.
 
-Given {given}`i : ByteArray.Iterator`, note that {lean}`i.toEnd.atEnd` is always {name}`true`.
--/
+Note that `i.toEnd.atEnd` is always `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⟩
@@ -451,11 +344,9 @@ 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⟩
@@ -463,4 +354,37 @@ def prevn : Iterator → Nat → Iterator
 end Iterator
 end ByteArray
 
+/--
+Converts a list of bytes into a `ByteArray`.
+-/
+def List.toByteArray (bs : List UInt8) : ByteArray :=
+  let rec loop
+    | [],    r => r
+    | b::bs, r => loop bs (r.push b)
+  loop bs ByteArray.empty
+
 instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
+
+/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
+def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 7).toUInt64 <<< 0x38 |||
+  (bs.get! 6).toUInt64 <<< 0x30 |||
+  (bs.get! 5).toUInt64 <<< 0x28 |||
+  (bs.get! 4).toUInt64 <<< 0x20 |||
+  (bs.get! 3).toUInt64 <<< 0x18 |||
+  (bs.get! 2).toUInt64 <<< 0x10 |||
+  (bs.get! 1).toUInt64 <<< 0x8  |||
+  (bs.get! 0).toUInt64
+
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 0).toUInt64 <<< 0x38 |||
+  (bs.get! 1).toUInt64 <<< 0x30 |||
+  (bs.get! 2).toUInt64 <<< 0x28 |||
+  (bs.get! 3).toUInt64 <<< 0x20 |||
+  (bs.get! 4).toUInt64 <<< 0x18 |||
+  (bs.get! 5).toUInt64 <<< 0x10 |||
+  (bs.get! 6).toUInt64 <<< 0x8  |||
+  (bs.get! 7).toUInt64

src/Init/Data/ByteArray/Bootstrap.lean

@@ -1,59 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Markus Himmel
--/
-module
-
-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⟩⟩
-
-@[simp]
-theorem toList_data_append' {a b : ByteArray} :
-    (a.append b).data.toList = a.data.toList ++ b.data.toList := by
-  have ⟨⟨a⟩⟩ := a
-  have ⟨⟨b⟩⟩ := b
-  rfl
-
-theorem ext : {x y : ByteArray} → x.data = y.data → x = y
-  | ⟨_⟩, ⟨_⟩, rfl => rfl
-
-end ByteArray
-
-@[simp]
-theorem List.toList_data_toByteArray {l : List UInt8} :
-    l.toByteArray.data.toList = l := by
-  rw [List.toByteArray]
-  suffices ∀ a b, (List.toByteArray.loop a b).data.toList = b.data.toList ++ a by
-    simpa using this l ByteArray.empty
-  intro a b
-  fun_induction List.toByteArray.loop a b with simp_all [toList_push]
-where
-  toList_push {xs : Array UInt8} {x : UInt8} : (xs.push x).toList = xs.toList ++ [x] := by
-    have ⟨xs⟩ := xs
-    simp [Array.push, List.concat_eq_append]
-
-theorem List.toByteArray_append' {l l' : List UInt8} :
-    (l ++ l').toByteArray = l.toByteArray.append l'.toByteArray :=
-  ByteArray.ext (ext (by simp))
-where
-  ext : {x y : Array UInt8} → x.toList = y.toList → x = y
-  | ⟨_⟩, ⟨_⟩, rfl => rfl

src/Init/Data/ByteArray/Extra.lean

@@ -1,44 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-module
-
-prelude
-public import Init.Data.ByteArray.Basic
-import Init.Data.String.Basic
-
-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 |||
-  (bs.get! 6).toUInt64 <<< 0x30 |||
-  (bs.get! 5).toUInt64 <<< 0x28 |||
-  (bs.get! 4).toUInt64 <<< 0x20 |||
-  (bs.get! 3).toUInt64 <<< 0x18 |||
-  (bs.get! 2).toUInt64 <<< 0x10 |||
-  (bs.get! 1).toUInt64 <<< 0x8  |||
-  (bs.get! 0).toUInt64
-
-/--
-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 |||
-  (bs.get! 1).toUInt64 <<< 0x30 |||
-  (bs.get! 2).toUInt64 <<< 0x28 |||
-  (bs.get! 3).toUInt64 <<< 0x20 |||
-  (bs.get! 4).toUInt64 <<< 0x18 |||
-  (bs.get! 5).toUInt64 <<< 0x10 |||
-  (bs.get! 6).toUInt64 <<< 0x8  |||
-  (bs.get! 7).toUInt64

src/Init/Data/ByteArray/Lemmas.lean

@@ -1,274 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.ByteArray.Basic
-
-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
-
-@[simp]
-theorem ByteArray.data_extract {a : ByteArray} {b e : Nat} :
-    (a.extract b e).data = a.data.extract b e := by
-  simp [extract, copySlice]
-  by_cases b ≤ e
-  · rw [(by omega : b + (e - b) = e)]
-  · rw [Array.extract_eq_empty_of_le (by omega), Array.extract_eq_empty_of_le (by omega)]
-
-@[simp]
-theorem ByteArray.extract_zero_size {b : ByteArray} : b.extract 0 b.size = b := by
-  ext1
-  simp
-
-@[simp]
-theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by
-  ext1
-  simp [Nat.min_le_left]
-
-theorem ByteArray.fastAppend_eq_copySlice {a b : ByteArray} :
-  a.fastAppend b = b.copySlice 0 a a.size b.size false := rfl
-
-@[simp]
-theorem List.toByteArray_append {l l' : List UInt8} :
-    (l ++ l').toByteArray = l.toByteArray ++ l'.toByteArray := by
-  simp [List.toByteArray_append']
-
-@[simp]
-theorem ByteArray.toList_data_append {l l' : ByteArray} :
-    (l ++ l').data.toList = l.data.toList ++ l'.data.toList := by
-  simp [← append_eq]
-
-@[simp]
-theorem ByteArray.data_append {l l' : ByteArray} :
-    (l ++ l').data = l.data ++ l'.data := by
-  simp [← Array.toList_inj]
-
-@[simp]
-theorem ByteArray.size_empty : ByteArray.empty.size = 0 := by
-  simp [← ByteArray.size_data]
-
-@[simp]
-theorem List.data_toByteArray {l : List UInt8} :
-    l.toByteArray.data = l.toArray := by
-  rw [List.toByteArray]
-  suffices ∀ a b, (List.toByteArray.loop a b).data = b.data ++ a.toArray by
-    simpa using this l ByteArray.empty
-  intro a b
-  fun_induction List.toByteArray.loop a b with simp_all
-
-@[simp]
-theorem List.size_toByteArray {l : List UInt8} :
-    l.toByteArray.size = l.length := by
-  simp [← ByteArray.size_data]
-
-@[simp]
-theorem List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl
-
-@[simp]
-theorem ByteArray.empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by
-  ext1
-  simp
-
-@[simp]
-theorem ByteArray.append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
-  ext1
-  simp
-
-@[simp, grind =]
-theorem ByteArray.size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size := by
-  simp [← size_data]
-
-@[simp]
-theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by
-  refine ⟨fun h => ?_, fun h => h ▸ ByteArray.size_empty⟩
-  ext1
-  simp [← Array.size_eq_zero_iff, h]
-
-theorem ByteArray.getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
-    a[i] = a.data[i]'(by simpa [← size_data]) := rfl
-
-@[simp]
-theorem ByteArray.getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
-    (hlt : i < a.size) : (a ++ b)[i] = a[i] := by
-  simp only [getElem_eq_getElem_data, data_append]
-  rw [Array.getElem_append_left (by simpa)]
-
-theorem ByteArray.getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
-    (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by
-  simp only [getElem_eq_getElem_data, data_append]
-  rw [Array.getElem_append_right (by simpa)]
-  simp
-
-@[simp]
-theorem List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} :
-    l.toByteArray[i]'h = l[i]'(by simp_all) := by
-  simp [ByteArray.getElem_eq_getElem_data]
-
-theorem List.getElem_eq_getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.length} :
-    l[i]'h = l.toByteArray[i]'(by simp_all) := by
-  simp
-
-@[simp]
-theorem ByteArray.size_extract {a : ByteArray} {b e : Nat} :
-    (a.extract b e).size = min e a.size - b := by
-  simp [← size_data]
-
-@[simp]
-theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by
-  rw [← size_eq_zero_iff, size_extract]
-  omega
-
-@[simp]
-theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by
-  simp only [extract_eq_empty_iff]
-  exact Nat.le_trans (Nat.min_le_left _ _) (by simp)
-
-@[simp]
-theorem ByteArray.append_eq_empty_iff {a b : ByteArray} :
-    a ++ b = ByteArray.empty ↔ a = ByteArray.empty ∧ b = ByteArray.empty := by
-  simp [← size_eq_zero_iff, size_append]
-
-@[simp]
-theorem List.toByteArray_eq_empty {l : List UInt8} :
-    l.toByteArray = ByteArray.empty ↔ l = [] := by
-  simp [← ByteArray.size_eq_zero_iff]
-
-theorem ByteArray.append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) :
-    xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂ := by
-  simp [ByteArray.ext_iff, Array.append_right_inj]
-
-@[simp]
-theorem ByteArray.extract_append_extract {a : ByteArray} {i j k : Nat} :
-    a.extract i j ++ a.extract j k = a.extract (min i j) (max j k) := by
-  ext1
-  simp
-
-theorem ByteArray.extract_eq_extract_append_extract {a : ByteArray} {i k : Nat} (j : Nat)
-    (hi : i ≤ j) (hk : j ≤ k) :
-    a.extract i k = a.extract i j ++ a.extract j k := by
-  simp
-  rw [Nat.min_eq_left hi, Nat.max_eq_right hk]
-
-theorem ByteArray.append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂ := by
-  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 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]
-
-theorem ByteArray.extract_append_eq_left {a b : ByteArray} {i : Nat} (hi : i = a.size) :
-    (a ++ b).extract 0 i = a := by
-  subst hi
-  ext1
-  simp
-
-theorem ByteArray.extract_append_size_left {a b : ByteArray} {i : Nat} :
-    (a ++ b).extract i a.size = a.extract i a.size := by
-  ext1
-  simp
-
-theorem ByteArray.extract_append_size_add {a b : ByteArray} {i j : Nat} :
-    (a ++ b).extract (a.size + i) (a.size + j) = b.extract i j := by
-  ext1
-  simp
-
-theorem ByteArray.extract_append  {as bs : ByteArray} {i j : Nat} :
-    (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size) := by
-  ext1
-  simp
-
-theorem ByteArray.extract_append_size_add' {a b : ByteArray} {i j k : Nat} (h : k = a.size) :
-    (a ++ b).extract (k + i) (k + j) = b.extract i j := by
-  cases h
-  rw [extract_append_size_add]
-
-theorem ByteArray.extract_extract {a : ByteArray} {i j k l : Nat} :
-    (a.extract i j).extract k l = a.extract (i + k) (min (i + l) j) := by
-  ext1
-  simp
-
-theorem ByteArray.getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.extract start stop).size) :
-    start + i < xs.size := by
-  rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
-  apply Nat.sub_le_sub_right; apply Nat.min_le_right
-
-theorem ByteArray.getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat}
-    (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by
-  simp [getElem_eq_getElem_data]
-
-theorem ByteArray.extract_eq_extract_left {a : ByteArray} {i i' j : Nat} :
-    a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by
-  simp [ByteArray.ext_iff, Array.extract_eq_extract_left]
-
-theorem ByteArray.extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
-    a.extract i (i + 1) = [a[i]].toByteArray := by
-  ext
-  · simp
-    omega
-  · rename_i j hj hj'
-    obtain rfl : j = 0 := by simpa using hj'
-    simp [ByteArray.getElem_eq_getElem_data]
-
-theorem ByteArray.extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) :
-    a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by
-  rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
-    extract_add_one (by omega), extract_add_one (by omega)]
-  simp [← List.toByteArray_append]
-
-theorem ByteArray.extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) :
-    a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by
-  rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
-    extract_add_one (by omega), extract_add_two (by omega)]
-  simp [← List.toByteArray_append]
-
-theorem ByteArray.extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) :
-    a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by
-  rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
-    extract_add_one (by omega), extract_add_three (by omega)]
-  simp [← List.toByteArray_append]
-
-theorem ByteArray.append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by
-  ext1
-  simp
-
-@[simp]
-theorem ByteArray.toList_empty : ByteArray.empty.toList = [] := by
-  simp [ByteArray.toList, ByteArray.toList.loop]
-
-theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} :
-    ByteArray.copySlice src srcOff dest destOff len exact =
-      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,3 +9,5 @@ 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,6 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Char.Basic
 import all Init.Data.Char.Basic
 public import Init.Data.UInt.Lemmas
 
@@ -65,6 +66,11 @@ instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
 def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
   total := fun x y => by simpa using Char.le_total y x
 
+theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4 := by
+  have := c.utf8Size_pos
+  have := c.utf8Size_le_four
+  omega
+
 @[simp] theorem ofNat_toNat (c : Char) : Char.ofNat c.toNat = c := by
   rw [Char.ofNat, dif_pos]
   rfl

src/Init/Data/Dyadic.lean

@@ -9,4 +9,3 @@ prelude
 public import Init.Data.Dyadic.Basic
 public import Init.Data.Dyadic.Instances
 public import Init.Data.Dyadic.Round
-public import Init.Data.Dyadic.Inv