fix: E-matching patterns containing ground universe polymorphic patterns in grind

This PR ensures `grind` can E-match patterns containing universe
polymorphic ground sub-patterns. For example, given
```
set_option pp.universes true in
attribute [grind?] Id.run_pure
```
the pattern
```
Id.run_pure.{u_1}: [@Id.run.{u_1} #1 (@pure.{u_1, u_1} `[Id.{u_1}] `[Applicative.toPure.{u_1, u_1}] _ #0)]
```
contains two nested universe polymorphic ground patterns
- `Id.{u_1}`
- `Applicative.toPure.{u_1, u_1}`

This kind of pattern is not common, but it occurs in core.

.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
@@ -33,7 +36,7 @@ jobs:
         include: ${{fromJson(inputs.config)}}
       # complete all jobs
       fail-fast: false
-    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
@@ -66,16 +69,10 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         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 }}
-      - name: Namespace Checkout
-        if: endsWith(matrix.os, '-with-cache')
-        uses: namespacelabs/nscloud-checkout-action@v7
-        with:
-          ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once
         run: true
         if: runner.os == 'Linux'
@@ -107,16 +104,16 @@ jobs:
           # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
           path: |
             .ccache
-            ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
+            ${{ matrix.name == 'Linux Lake (cached)' && 'build/stage1/**/*.trace
             build/stage1/**/*.olean*
             build/stage1/**/*.ilean
             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: |
@@ -169,24 +166,6 @@ jobs:
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
           time make $TARGET_STAGE -j$NPROC
-      # Should be done as early as possible and in particular *before* "Check rebootstrap" which
-      # changes the state of stage1/
-      - name: Save Cache
-        # Caching on cancellation created some mysterious issues perhaps related to improper build
-        # shutdown
-        if: steps.restore-cache.outputs.cache-hit != 'true' && !cancelled()
-        uses: actions/cache/save@v4
-        with:
-          # NOTE: must be in sync with `restore` above
-          path: |
-            .ccache
-            ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
-            build/stage1/**/*.olean*
-            build/stage1/**/*.ilean
-            build/stage1/**/*.ir
-            build/stage1/**/*.c
-            build/stage1/**/*.c.o*' || '' }}
-          key: ${{ steps.restore-cache.outputs.cache-primary-key }}
       - name: Install
         run: |
           make -C build/$TARGET_STAGE install
@@ -220,14 +199,14 @@ jobs:
           path: pack/*
       - name: Lean stats
         run: |
-          build/$TARGET_STAGE/bin/lean --stats src/Lean.lean -Dexperimental.module=true
+          build/stage1/bin/lean --stats src/Lean.lean -Dexperimental.module=true
         if: ${{ !matrix.cross }}
       - name: Test
         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:
@@ -274,3 +253,22 @@ jobs:
             progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
             echo bt | $GDB/bin/gdb -q $progbin $c || true
           done
+      - name: Save Cache
+        if: always() && steps.restore-cache.outputs.cache-hit != 'true'
+        uses: actions/cache/save@v4
+        with:
+          # NOTE: must be in sync with `restore` above
+          path: |
+            .ccache
+            ${{ matrix.name == 'Linux Lake (cached)' && 'build/stage1/**/*.trace
+            build/stage1/**/*.olean*
+            build/stage1/**/*.ilean
+            build/stage1/**/*.ir
+            build/stage1/**/*.c
+            build/stage1/**/*.c.o*' || '' }}
+          key: ${{ steps.restore-cache.outputs.cache-primary-key }}
+      - name: Upload Build Artifact
+        if: always() && matrix.name == 'Linux Lake (cached)'
+        uses: actions/upload-artifact@v4
+        with:
+          path: build

.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,51 +165,55 @@ 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*",
                 "binary-check": "ldd -v",
                 // foreign code may be linked against more recent glibc
-                "CTEST_OPTIONS": "-E 'foreign'",
+                "CTEST_OPTIONS": "-E 'foreign'"
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16" : "ubuntu-latest",
+                "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
+                "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
+              },
+              {
+                "name": "Linux Lake (cached)",
+                "os": "ubuntu-latest",
+                "check-level": (isPr || isPushToMaster) ? 0 : 2,
+                "secondary": true,
                 "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
               },
               {
                 "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,21 +221,19 @@ 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*",
                 "binary-check": "otool -L",
-                "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
-                "CTEST_OPTIONS": "-E 'leanlaketest_hello'", // started failing from unpack
+                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
               },
               {
                 "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,32 +242,31 @@ 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",
+                "binary-check": "ldd"
               },
               {
                 "name": "Linux aarch64",
                 "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*",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*"
               },
               // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation
               //{
@@ -281,7 +276,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,21 +288,15 @@ 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
               //   "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
               // }
             ];
-            for (const job of matrix) {
-              if (job["prepare-llvm"]) {
-                // `USE_LAKE` is not compatible with `prepare-llvm` currently
-                job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DUSE_LAKE=OFF";
-              }
-            }
             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 +306,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 +322,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 +353,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 +366,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 +391,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 +414,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

@@ -19,15 +19,11 @@ concurrency:
 jobs:
   update-stage0:
     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"
@@ -61,27 +57,18 @@ jobs:
       uses: actions/cache/restore@v4
       with:
         # NOTE: must be in sync with `restore-cache` in `build-template.yml`
+        # TODO: actually switch to USE_LAKE once it caches more; for now it just caches more often than any other build type so let's use its cache
         path: |
           .ccache
-          build/stage1/**/*.trace
-          build/stage1/**/*.olean*
-          build/stage1/**/*.ilean
-          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

CMakeLists.txt

@@ -147,10 +147,6 @@ add_custom_target(test
   COMMAND $(MAKE) -C stage1 test
   DEPENDS stage1)
 
-add_custom_target(clean-stdlib
-  COMMAND $(MAKE) -C stage1 clean-stdlib
-  DEPENDS stage1)
-
 install(CODE "execute_process(COMMAND make -C stage1 install)")
 
 add_custom_target(check-stage3

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/documentation/examples/)
 - [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/bootstrap.md

@@ -1,6 +1,6 @@
 # Lean Build Bootstrapping
 
-Lean is a bootstrapped program: the
+Since version 4, Lean is a partially bootstrapped program: most parts of the
 frontend and compiler are written in Lean itself and thus need to be built before
 building Lean itself - which is needed to again build those parts. This cycle is
 broken by using pre-built C files checked into the repository (which ultimately
@@ -73,11 +73,6 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
 The github repository will automatically update stage0 on `master` once
 `src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
 
-NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
-Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.
-The same is true for further stages except that a rebuild of them is retriggered on any committed change, not just to a specific directory.
-Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
-
 If you have write access to the lean4 repository, you can also manually
 trigger that process, for example to be able to use new features in the compiler itself.
 You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
@@ -87,13 +82,13 @@ gh workflow run update-stage0.yml
 ```
 
 Leaving stage0 updates to the CI automation is preferable, but should you need
-to do it locally, you can use `make -C build/release update-stage0-commit` to
-update `stage0` from `stage1` or `make -C build/release/stageN update-stage0-commit` to
+to do it locally, you can use `make update-stage0-commit` in `build/release` to
+update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
 update from another stage. This command will automatically stage the updated files
-and introduce a commit, so make sure to commit your work before that.
+and introduce a commit,so make sure to commit your work before that.
 
 If you rebased the branch (either onto a newer version of `master`, or fixing
-up some commits prior to the stage0 update), recreate the stage0 update commits.
+up some commits prior to the stage0 update, recreate the stage0 update commits.
 The script `script/rebase-stage0.sh` can be used for that.
 
 The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)

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,8 +8,8 @@ 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.
-Please see below for specific instructions for VS Code.
+You can use any of the [supported editors](../setup.md) for editing the Lean source code.
+If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
 
 ### Dev setup using elan
 
@@ -68,10 +68,6 @@ code lean.code-workspace
 ```
 on the command line.
 
-You can use the `Refresh File Dependencies` command as in other projects to rebuild modules from inside VS Code but be aware that this does not trigger any non-Lake build targets.
-In particular, after updating `stage0/` (or fetching an update to it), you will want to invoke `make` directly to rebuild `stage0/bin/lean` as described in [building Lean](../make/index.md).
-You should then run the `Restart Server` command to update all open files and the server watchdog process as well.
-
 ### `ccache`
 
 Lean's build process uses [`ccache`](https://ccache.dev/) if it is
@@ -99,19 +95,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/examples/bintree.lean

@@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    intro le
+    intros le
     exact Nat.lt_of_le_of_ne le ne
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h

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
 ------------
@@ -53,6 +53,11 @@ There are also two alternative presets that combine some of these options you ca
   Select the C/C++ compilers to use. Official Lean releases currently use Clang;
   see also `.github/workflows/ci.yml` for the CI config.
 
+* `-DUSE_LAKE=ON`\
+  Experimental option to build the core libraries using Lake instead of `lean.mk`.  Caveats:
+  * As native code compilation is still handled by cmake, changes to stage0/ (such as from `git pull`) are picked up only when invoking the build via `make`, not via `Refresh Dependencies` in the editor.
+  * `USE_LAKE` is not yet compatible with `LAKE_ARTIFACT_CACHE`
+
 Lean will automatically use [CCache](https://ccache.dev/) if available to avoid
 redundant builds, especially after stage 0 has been updated.
 

flake.nix

@@ -18,15 +18,14 @@
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
 
-      llvmPackages = pkgs.llvmPackages_15;
+      lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
-          stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
+          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
             cmake gmp libuv ccache pkg-config
-            llvmPackages.bintools  # wrapped lld
-            llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+            lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI
           ];
@@ -61,6 +60,12 @@
           GDB = pkgsDist.gdb;
         });
     in {
+      packages.${system} = {
+        # to be removed when Nix CI is not needed anymore
+        inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
+        deprecated = lean-packages;
+      };
+
       devShells.${system} = {
         # The default development shell for working on lean itself
         default = devShellWithDist pkgs;

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",

nix/bareStdenv/setup

@@ -0,0 +1,7 @@
+set -eo pipefail
+
+for pkg in $buildInputs; do
+  export PATH=$PATH:$pkg/bin
+done
+
+: ${outputs:=out}

nix/bootstrap.nix

@@ -0,0 +1,208 @@
+{ src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
+  stdenv, lib, cmake, pkg-config, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
+  ... } @ args:
+with builtins;
+lib.warn "The Nix-based build is deprecated" rec {
+  inherit stdenv;
+  sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
+  buildCMake = args: stdenv.mkDerivation ({
+    nativeBuildInputs = [ cmake pkg-config ];
+    buildInputs = [ gmp libuv llvmPackages.llvm ];
+    # https://github.com/NixOS/nixpkgs/issues/60919
+    hardeningDisable = [ "all" ];
+    dontStrip = (args.debug or debug);
+
+    postConfigure = ''
+      patchShebangs .
+    '';
+  } // args // {
+    src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
+    cmakeFlags = ["-DSMALL_ALLOCATOR=ON" "-DUSE_MIMALLOC=OFF"] ++ (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
+    preConfigure = args.preConfigure or "" + ''
+      # ignore absence of submodule
+      sed -i 's!lake/Lake.lean!!' CMakeLists.txt
+    '';
+  });
+  lean-bin-tools-unwrapped = buildCMake {
+    name = "lean-bin-tools";
+    outputs = [ "out" "leanc_src" ];
+    realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "[a-z].*" ".*\.in" "Leanc\.lean" ];
+    dontBuild = true;
+    installPhase = ''
+      mkdir $out $leanc_src
+      mv bin/ include/ share/ $out/
+      mv leanc.sh $out/bin/leanc
+      mv leanc/Leanc.lean $leanc_src/
+      substituteInPlace $out/bin/leanc --replace '$root' "$out" --replace " sed " " ${gnused}/bin/sed "
+      substituteInPlace $out/bin/leanmake --replace "make" "${gnumake}/bin/make"
+      substituteInPlace $out/share/lean/lean.mk --replace "/usr/bin/env bash" "${bash}/bin/bash"
+    '';
+  };
+  leancpp = buildCMake {
+    name = "leancpp";
+    src = src + "/src";
+    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "leanshell" "leanmain" ];
+    installPhase = ''
+      mkdir -p $out
+      mv lib/ $out/
+      mv runtime/libleanrt_initial-exec.a $out/lib
+    '';
+  };
+  stage0 = args.stage0 or (buildCMake {
+    name = "lean-stage0";
+    realSrc = src + "/stage0/src";
+    debug = stage0debug;
+    cmakeFlags = [ "-DSTAGE=0" ];
+    extraCMakeFlags = [];
+    preConfigure = ''
+      ln -s ${src + "/stage0/stdlib"} ../stdlib
+    '';
+    installPhase = ''
+      mkdir -p $out/bin $out/lib/lean
+      mv bin/lean $out/bin/
+      mv lib/lean/*.{so,dylib} $out/lib/lean
+    '';
+    meta.mainProgram = "lean";
+  });
+  stage = { stage, prevStage, self }:
+    let
+      desc = "stage${toString stage}";
+      build = args: buildLeanPackage.override {
+        lean = prevStage;
+        leanc = lean-bin-tools-unwrapped;
+        # use same stage for retrieving dependencies
+        lean-leanDeps = stage0;
+        lean-final = self;
+      } ({
+        src = src + "/src";
+        roots = [ { mod = args.name; glob = "andSubmodules"; } ];
+        fullSrc = src;
+        srcPath = "$PWD/src:$PWD/src/lake";
+        inherit debug;
+        leanFlags = [ "-DwarningAsError=true" ];
+      } // args);
+      Init' = build { name = "Init"; deps = []; };
+      Std' = build { name = "Std"; deps = [ Init' ]; };
+      Lean' = build { name = "Lean"; deps = [ Std' ]; };
+      attachSharedLib = sharedLib: pkg: pkg // {
+        inherit sharedLib;
+        mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
+      };
+    in (all: all // all.lean) rec {
+      inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
+      Init = attachSharedLib leanshared Init';
+      Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
+      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
+      Lake = build {
+        name = "Lake";
+        sharedLibName = "Lake_shared";
+        src = src + "/src/lake";
+        deps = [ Init Lean ];
+      };
+      Lake-Main = build {
+        name = "LakeMain";
+        roots = [{ glob = "one"; mod = "LakeMain"; }];
+        executableName = "lake";
+        deps = [ Lake ];
+        linkFlags = lib.optional stdenv.isLinux "-rdynamic";
+        src = src + "/src/lake";
+      };
+      stdlib = [ Init Std Lean Lake ];
+      modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
+      depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
+      iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
+      Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
+      stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
+      libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
+        mkdir $out
+        touch empty.c
+        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
+      '';
+      leanshared_1 = runCommand "leanshared_1" { buildInputs = [ stdenv.cc ]; libName = "leanshared_1${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
+        mkdir $out
+        touch empty.c
+        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
+      '';
+      leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
+        mkdir $out
+        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
+          -Wl,--whole-archive ${leancpp}/lib/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ \
+          -lm ${stdlibLinkFlags} \
+          $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
+          -o $out/$libName
+      '';
+      mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
+      print-paths = Lean.makePrintPathsFor [] mods;
+      leanc = writeShellScriptBin "leanc" ''
+        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} -L${Lake.sharedLib} "$@"
+      '';
+      lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
+        mkdir -p $out/bin
+        ${leanc}/bin/leanc ${leancpp}/lib/temp/libleanmain.a ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* -o $out/bin/lean
+      '';
+      # derivation following the directory layout of the "basic" setup, mostly useful for running tests
+      lean-all = stdenv.mkDerivation {
+        name = "lean-${desc}";
+        buildCommand = ''
+          mkdir -p $out/bin $out/lib/lean
+          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* ${Lake.sharedLib}/* $out/lib/lean/
+          # put everything in a single final derivation so `IO.appDir` references work
+          cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
+          # NOTE: `lndir` will not override existing `bin/leanc`
+          ${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
+        '';
+        meta.mainProgram = "lean";
+      };
+      cacheRoots = linkFarmFromDrvs "cacheRoots" ([
+        stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
+      ] ++ map (lib: lib.oTree) stdlib);
+      test = buildCMake {
+        name = "lean-test-${desc}";
+        realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
+        buildInputs = [ gmp libuv perl git cadical ];
+        preConfigure = ''
+          cd src
+        '';
+        extraCMakeFlags = [ "-DLLVM=OFF" ];
+        postConfigure = ''
+          patchShebangs ../../tests ../lake
+          rm -r bin lib include share
+          ln -sf ${lean-all}/* .
+        '';
+        buildPhase = ''
+         ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
+        '';
+        installPhase = ''
+          mkdir $out
+          mv test-results.xml $out
+        '';
+      };
+      update-stage0 =
+        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) (stdlib ++ [Lake-Main]); }; in
+        writeShellScriptBin "update-stage0" ''
+          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
+        '';
+      update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
+        set -euo pipefail
+        ${update-stage0}/bin/update-stage0
+        git commit -m "chore: update stage0"
+      '';
+      link-ilean = writeShellScriptBin "link-ilean" ''
+        dest=''${1:-src}
+        rm -rf $dest/build/lib || true
+        mkdir -p $dest/build/lib
+        ln -s ${iTree}/* $dest/build/lib
+      '';
+      benchmarks =
+        let
+          entries = attrNames (readDir (src + "/tests/bench"));
+          leanFiles = map (n: elemAt n 0) (filter (n: n != null) (map (match "(.*)\.lean") entries));
+        in lib.genAttrs leanFiles (n: (buildLeanPackage {
+          name = n;
+          src = filterSource (e: _: baseNameOf e == "${n}.lean") (src + "/tests/bench");
+        }).executable);
+    };
+  stage1 = stage { stage = 1; prevStage = stage0; self = stage1; };
+  stage2 = stage { stage = 2; prevStage = stage1; self = stage2; };
+  stage3 = stage { stage = 3; prevStage = stage2; self = stage3; };
+}

nix/buildLeanPackage.nix

@@ -0,0 +1,247 @@
+{ lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
+  stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs,
+  runCommand, darwin, mkShell, ... }:
+let lean-final' = lean-final; in
+lib.makeOverridable (
+{ name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
+  # Lean dependencies. Each entry should be an output of buildLeanPackage.
+  deps ? [ lean.Init lean.Std lean.Lean ],
+  # Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
+  staticLibDeps ? [],
+  # Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
+  groupStaticLibs ? false,
+  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
+  # shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
+  # These libs are also linked to in packages that depend on this one.
+  nativeSharedLibs ? [],
+  # Lean modules to include.
+  # A set of Lean modules names as strings (`"Foo.Bar"`) or attrsets (`{ name = "Foo.Bar"; glob = "one" | "submodules" | "andSubmodules"; }`);
+  # see Lake README for glob meanings. Dependencies of selected modules are always included.
+  roots ? [ name ],
+  # Output from `lean --deps-json` on package source files. Persist the corresponding output attribute to a file and pass it back in here to avoid IFD.
+  # Must be refreshed on any change in `import`s or set of source file names.
+  modDepsFile ? null,
+  # Whether to compile each module into a native shared library that is loaded whenever the module is imported in order to accelerate evaluation
+  precompileModules ? false,
+  # Whether to compile the package into a native shared library that is loaded whenever *any* of the package's modules is imported into another package.
+  # If `precompileModules` is also `true`, the latter only affects imports within the current package.
+  precompilePackage ? precompileModules,
+  # Lean plugin dependencies. Each derivation `plugin` should contain a plugin library at path `${plugin}/${plugin.name}`.
+  pluginDeps ? [],
+  # `overrideAttrs` for `buildMod`
+  overrideBuildModAttrs ? null,
+  debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
+  srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
+with builtins; let
+  # "Init.Core" ~> "Init/Core"
+  modToPath = mod: replaceStrings ["."] ["/"] mod;
+  modToAbsPath = mod: "${src}/${modToPath mod}";
+  # sanitize file name before copying to store, except when already in store
+  copyToStoreSafe = base: suffix: if lib.isDerivation base then base + suffix else
+    builtins.path { name = lib.strings.sanitizeDerivationName (baseNameOf suffix); path = base + suffix; };
+  modToLean = mod: copyToStoreSafe src "/${modToPath mod}.lean";
+  bareStdenv = ./bareStdenv;
+  mkBareDerivation = args: derivation (args // {
+    name = lib.strings.sanitizeDerivationName args.name;
+    stdenv = bareStdenv;
+    inherit (stdenv) system;
+    buildInputs = (args.buildInputs or []) ++ [ coreutils ];
+    builder = stdenv.shell;
+    args = [ "-c" ''
+      source $stdenv/setup
+      set -u
+      ${args.buildCommand}
+    '' ];
+  }) // { overrideAttrs = f: mkBareDerivation (lib.fix (lib.extends f (_: args))); };
+  runBareCommand = name: args: buildCommand: mkBareDerivation (args // { inherit name buildCommand; });
+  runBareCommandLocal = name: args: buildCommand: runBareCommand name (args // {
+    preferLocalBuild = true;
+    allowSubstitutes = false;
+  }) buildCommand;
+  mkSharedLib = name: args: runBareCommand "${name}-dynlib" {
+    buildInputs = [ stdenv.cc ] ++ lib.optional stdenv.isDarwin darwin.cctools;
+    libName = "${name}${stdenv.hostPlatform.extensions.sharedLibrary}";
+  } ''
+    mkdir -p $out
+    ${leanc}/bin/leanc -shared ${args} -o $out/$libName
+  '';
+  depRoot = name: deps: mkBareDerivation {
+    name = "${name}-depRoot";
+    inherit deps;
+    depRoots = map (drv: drv.LEAN_PATH) deps;
+
+    passAsFile = [ "deps" "depRoots" ];
+    buildCommand = ''
+      mkdir -p $out
+      for i in $(cat $depRootsPath); do
+        cp -dru --no-preserve=mode $i/. $out
+      done
+      for i in $(cat $depsPath); do
+        cp -drsu --no-preserve=mode $i/. $out
+      done
+    '';
+  };
+  srcRoot = src;
+
+  # A flattened list of Lean-module dependencies (`deps`)
+  allExternalDeps = lib.unique (lib.foldr (dep: allExternalDeps: allExternalDeps ++ [ dep ] ++ dep.allExternalDeps) [] deps);
+  allNativeSharedLibs =
+    lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
+
+  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
+  # plus every dep module itself: `dep.staticLib`
+  allStaticLibDeps =
+    lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
+
+  pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
+
+  leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${pathOfSharedLib dep}") pluginDeps);
+  loadDynlibsOfDeps = deps: lib.unique (concatMap (d: d.propagatedLoadDynlibs) deps);
+
+  # submodules "Init" = ["Init.List.Basic", "Init.Core", ...]
+  submodules = mod: let
+    dir = readDir (modToAbsPath mod);
+    f = p: t:
+      if t == "directory" then
+        submodules "${mod}.${p}"
+      else
+        let m = builtins.match "(.*)\.lean" p;
+        in lib.optional (m != null) "${mod}.${head m}";
+  in concatLists (lib.mapAttrsToList f dir);
+
+  # conservatively approximate list of source files matched by glob
+  expandGlobAllApprox = g:
+    if typeOf g == "string" then
+      # we can't know the required files without parsing dependencies (which is what we want this
+      # function for), so we approximate to the entire package.
+      let root = (head (split "\\." g));
+      in lib.optional (pathExists (src + "/${modToPath root}.lean")) root ++ lib.optionals (pathExists (modToAbsPath root)) (submodules root)
+    else if g.glob == "one" then expandGlobAllApprox g.mod
+    else if g.glob == "submodules" then submodules g.mod
+    else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
+    else throw "unknown glob kind '${g}'";
+  # list of modules that could potentially be involved in the build
+  candidateMods = lib.unique (concatMap expandGlobAllApprox roots);
+  candidateFiles = map modToLean candidateMods;
+  modDepsFile = args.modDepsFile or mkBareDerivation {
+    name = "${name}-deps.json";
+    candidateFiles = lib.concatStringsSep " " candidateFiles;
+    passAsFile = [ "candidateFiles" ];
+    buildCommand = ''
+      mkdir $out
+      ${lean-leanDeps}/bin/lean --deps-json --stdin < $candidateFilesPath > $out/$name
+    '';
+  };
+  modDeps = fromJSON (
+    # the only possible references to store paths in the JSON should be inside errors, so no chance of missed dependencies from this
+    unsafeDiscardStringContext (readFile "${modDepsFile}/${modDepsFile.name}"));
+  # map from module name to list of imports
+  modDepsMap = listToAttrs (lib.zipListsWith lib.nameValuePair candidateMods modDeps.imports);
+  maybeOverrideAttrs = f: x: if f != null then x.overrideAttrs f else x;
+  # build module (.olean and .c) given derivations of all (immediate) dependencies
+  # TODO: make `rec` parts override-compatible?
+  buildMod = mod: deps: maybeOverrideAttrs overrideBuildModAttrs (mkBareDerivation rec {
+    name = "${mod}";
+    LEAN_PATH = depRoot mod deps;
+    LEAN_ABORT_ON_PANIC = "1";
+    relpath = modToPath mod;
+    buildInputs = [ lean ];
+    leanPath = relpath + ".lean";
+    # should be either single .lean file or directory directly containing .lean file plus dependencies
+    src = copyToStoreSafe srcRoot ("/" + leanPath);
+    outputs = [ "out" "ilean" "c" ];
+    oleanPath = relpath + ".olean";
+    ileanPath = relpath + ".ilean";
+    cPath = relpath + ".c";
+    inherit leanFlags leanPluginFlags;
+    leanLoadDynlibFlags = map (p: "--load-dynlib=${pathOfSharedLib p}") (loadDynlibsOfDeps deps);
+    buildCommand = ''
+      dir=$(dirname $relpath)
+      mkdir -p $dir $out/$dir $ilean/$dir $c/$dir
+      if [ -d $src ]; then cp -r $src/. .; else cp $src $leanPath; fi
+      lean -o $out/$oleanPath -i $out/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
+    '';
+  }) // {
+    inherit deps;
+    propagatedLoadDynlibs = loadDynlibsOfDeps deps;
+  };
+  compileMod = mod: drv: mkBareDerivation {
+    name = "${mod}-cc";
+    buildInputs = [ leanc stdenv.cc ];
+    hardeningDisable = [ "all" ];
+    oPath = drv.relpath + ".o";
+    inherit leancFlags;
+    buildCommand = ''
+      mkdir -p $out/$(dirname ${drv.relpath})
+      # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
+      ln -s ${drv.c}/${drv.cPath} src.c
+      # on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
+      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
+    '';
+  };
+  mkMod = mod: deps:
+    let drv = buildMod mod deps;
+        obj = compileMod mod drv;
+        # this attribute will only be used if any dependent module is precompiled
+        sharedLib = mkSharedLib mod "${obj}/${obj.oPath} ${lib.concatStringsSep " " (map (d: pathOfSharedLib d.sharedLib) deps)}";
+    in drv // {
+      inherit obj sharedLib;
+    } // lib.optionalAttrs precompileModules {
+      propagatedLoadDynlibs = [sharedLib];
+    };
+  externalModMap = lib.foldr (dep: depMap: depMap // dep.mods) {} allExternalDeps;
+  # map from module name to derivation
+  modCandidates = mapAttrs (mod: header:
+    let
+      deps = if header.errors == []
+             then map (m: m.module) header.result.imports
+             else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
+    in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
+  expandGlob = g:
+    if typeOf g == "string" then [g]
+    else if g.glob == "one" then [g.mod]
+    else if g.glob == "submodules" then submodules g.mod
+    else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
+    else throw "unknown glob kind '${g}'";
+  # subset of `modCandidates` that is transitively reachable from `roots`
+  mods' = listToAttrs (map (e: { name = e.key; value = modCandidates.${e.key}; }) (genericClosure {
+    startSet = map (m: { key = m; }) (concatMap expandGlob roots);
+    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
+  }));
+  allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
+
+  objects   = mapAttrs (_: m: m.obj) mods';
+  bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
+  staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
+    mkdir -p $out
+    ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
+  '';
+
+  staticLibLinkWrapper = libs: if groupStaticLibs && !stdenv.isDarwin
+    then "-Wl,--start-group ${libs} -Wl,--end-group"
+    else "${libs}";
+in rec {
+  inherit name lean deps staticLibDeps allNativeSharedLibs allLinkFlags allExternalDeps src objects staticLib modDepsFile;
+  mods = mapAttrs (_: m:
+      m //
+      # if neither precompilation option was set but a dependent module wants to be precompiled, default to precompiling this package whole
+      lib.optionalAttrs (precompilePackage || !precompileModules) { inherit sharedLib; } //
+      lib.optionalAttrs precompilePackage { propagatedLoadDynlibs = [sharedLib]; })
+    mods';
+  modRoot   = depRoot name (attrValues mods);
+  depRoots  = linkFarmFromDrvs "depRoots" (map (m: m.LEAN_PATH) (attrValues mods));
+  cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
+  oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
+  iTree     = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };
+  sharedLib = mkSharedLib "lib${sharedLibName}" ''
+    ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
+    ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
+  executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
+      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
+    in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
+      mkdir -p $out/bin
+      leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \
+        -o $out/bin/${executableName} \
+        ${lib.concatStringsSep " " allLinkFlags}
+    '') {};
+})

nix/lake-dev.in

@@ -0,0 +1,42 @@
+#!@bash@/bin/bash
+
+set -euo pipefail
+
+function pebkac() {
+    echo 'This is just a simple Nix adapter for `lake print-paths|serve`.'
+    exit 1
+}
+
+[[ $# -gt 0 ]] || pebkac
+case $1 in
+    --version)
+        # minimum version for `lake serve` with fallback
+        echo 3.1.0
+        ;;
+    print-paths)
+        shift
+        deps="$@"
+        root=.
+        # fall back to initial package if not in package
+        [[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
+        target="$root#print-paths"
+        args=()
+        # HACK: use stage 0 instead of 1 inside Lean's own `src/`
+        [[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@print-paths" && args=@srcArgs@
+        for dep in $deps; do
+            target="$target.\"$dep\""
+        done
+        echo "Building dependencies..." >&2
+        # -v only has "built ...", but "-vv" is a bit too verbose
+        exec @nix@/bin/nix run "$target" ${args[*]} -v
+        ;;
+    serve)
+        shift
+        [[ ${1:-} == "--" ]] && shift
+        # `link-ilean` puts them there
+        LEAN_PATH=${LEAN_PATH:+$LEAN_PATH:}$PWD/build/lib exec $(dirname $0)/lean --server "$@"
+        ;;
+    *)
+        pebkac
+        ;;
+esac

nix/lean-dev.in

@@ -0,0 +1,28 @@
+#!@bash@/bin/bash
+
+set -euo pipefail
+
+root="."
+# find package root
+while [[ "$root" != / ]]; do
+    [ -f "$root/flake.nix" ] && break
+    root="$(realpath "$root/..")"
+done
+# fall back to initial package if not in package
+[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
+
+# use Lean w/ package unless in server mode (which has its own LEAN_PATH logic)
+target="$root#lean-package"
+for arg in "$@"; do
+    case $arg in
+        --server | --worker | -v | --version)
+            target="$root#lean"
+            ;;
+    esac
+done
+
+args=(-- "$@")
+# HACK: use stage 0 instead of 1 inside Lean's own `src/`
+[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@" && args=@srcArgs@
+
+LEAN_SYSROOT="$(dirname "$0")/.." exec @nix@/bin/nix ${LEAN_NIX_ARGS:-} run "$target" ${args[*]}

nix/packages.nix

@@ -0,0 +1,52 @@
+{ src, pkgs, ... } @ args:
+with pkgs;
+let
+  # https://github.com/NixOS/nixpkgs/issues/130963
+  llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15;
+  cc = (ccacheWrapper.override rec {
+    cc = llvmPackages.clang;
+    extraConfig = ''
+      export CCACHE_DIR=/nix/var/cache/ccache
+      export CCACHE_UMASK=007
+      export CCACHE_BASE_DIR=$NIX_BUILD_TOP
+      # https://github.com/NixOS/nixpkgs/issues/109033
+      args=("$@")
+      for ((i=0; i<"''${#args[@]}"; i++)); do
+        case ''${args[i]} in
+          -frandom-seed=*) unset args[i]; break;;
+        esac
+      done
+      set -- "''${args[@]}"
+      [ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@"
+    '';
+  }).overrideAttrs (old: {
+    # https://github.com/NixOS/nixpkgs/issues/119779
+    installPhase = builtins.replaceStrings ["use_response_file_by_default=1"] ["use_response_file_by_default=0"] old.installPhase;
+  });
+  stdenv' = if stdenv.isLinux then useGoldLinker stdenv else stdenv;
+  lean = callPackage (import ./bootstrap.nix) (args // {
+    stdenv = overrideCC stdenv' cc;
+    inherit src buildLeanPackage llvmPackages;
+  });
+  makeOverridableLeanPackage = f:
+    let newF = origArgs: f origArgs // {
+      overrideArgs = newArgs: makeOverridableLeanPackage f (origArgs // newArgs);
+    };
+    in lib.setFunctionArgs newF (lib.getFunctionArgs f) // {
+      override = args: makeOverridableLeanPackage (f.override args);
+    };
+  buildLeanPackage = makeOverridableLeanPackage (callPackage (import ./buildLeanPackage.nix) (args // {
+    inherit (lean) stdenv;
+    lean = lean.stage1;
+    inherit (lean.stage1) leanc;
+  }));
+in {
+  inherit cc buildLeanPackage llvmPackages;
+  nixpkgs = pkgs;
+  ciShell = writeShellScriptBin "ciShell" ''
+    set -o pipefail
+    export PATH=${moreutils}/bin:$PATH
+    # prefix lines with cumulative and individual execution time
+    "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
+  '';
+} // lean.stage1

nix/templates/pkg/MyPackage.lean

@@ -0,0 +1 @@
+#eval "Hello, world!"

nix/templates/pkg/flake.nix

@@ -0,0 +1,21 @@
+{
+  description = "My Lean package";
+
+  inputs.lean.url = "github:leanprover/lean4";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+
+  outputs = { self, lean, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
+    let
+      leanPkgs = lean.packages.${system};
+      pkg = leanPkgs.buildLeanPackage {
+        name = "MyPackage";  # must match the name of the top-level .lean file
+        src = ./.;
+      };
+    in {
+      packages = pkg // {
+        inherit (leanPkgs) lean;
+      };
+
+      defaultPackage = pkg.modRoot;
+    });
+}

script/AnalyzeGrindAnnotations.lean

@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 import Lean
 
 namespace Lean.Meta.Grind.Analyzer
-
-
 /-!
 A simple E-matching annotation analyzer.
 For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
@@ -74,59 +72,16 @@ def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
   if s > c.detailed then
     logInfo m!"{declName}\n{← thmsToMessageData thms}"
 
--- Not sure why this is failing: `down_pure` perhaps has an unnecessary universe parameter?
-run_meta analyzeEMatchTheorem ``Std.Do.SPred.down_pure {}
-
 /-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
 def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
   let origins := (← getEMatchTheorems).getOrigins
-  let decls := origins.filterMap fun | .decl declName => some declName | _ => none
-  for declName in decls.mergeSort Name.lt do
-    try
-      analyzeEMatchTheorem declName c
-    catch e =>
-      logError m!"{declName} failed with {e.toMessageData}"
-  logInfo m!"Finished analyzing {decls.length} theorems"
+  for o in origins do
+    let .decl declName := o | pure ()
+    analyzeEMatchTheorem declName c
 
-/-- Macro for analyzing E-match theorems with unlimited heartbeats -/
-macro "#analyzeEMatchTheorems" : command => `(
-  set_option maxHeartbeats 0 in
-  run_meta analyzeEMatchTheorems
-)
+set_option maxHeartbeats 5000000
+run_meta analyzeEMatchTheorems
 
-#analyzeEMatchTheorems
-
--- -- We can analyze specific theorems using commands such as
-set_option trace.grind.ematch.instance true
-
--- 1. grind immediately sees `(#[] : Array α) = ([] : List α).toArray` but probably this should be hidden.
--- 2. `Vector.toArray_empty` keys on `Array.mk []` rather than `#v[].toArray`
--- I guess we could add `(#[].extract _ _).extract _ _` as a stop pattern.
-run_meta analyzeEMatchTheorem ``Array.extract_empty {}
-
--- Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
--- lambdas. So we get crazy things like:
--- `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
--- We could consider replacing `filterMap_some` with
--- `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
--- to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
-run_meta analyzeEMatchTheorem ``Array.filterMap_some {}
-
--- Not entirely certain what is wrong here, but certainly
--- `eq_empty_of_append_eq_empty` is firing too often.
--- Ideally we could instantiate this is we fine `xs ++ ys` in the same equivalence class,
--- note just as soon as we see `xs ++ ys`.
--- I've tried removing this in https://github.com/leanprover/lean4/pull/10162
-run_meta analyzeEMatchTheorem ``Array.range'_succ {}
-
--- Perhaps the same story here.
-run_meta analyzeEMatchTheorem ``Array.range_succ {}
-
--- `zip_map_left` and `zip_map_right` are bad grind lemmas,
--- checking if they can be removed in https://github.com/leanprover/lean4/pull/10163
-run_meta analyzeEMatchTheorem ``Array.zip_map {}
-
--- It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
--- pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
--- I don't think any forbidden subterms can help us here. I don't know what to do. :-(
-run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}
+-- We can analyze specific theorems using commands such as
+set_option trace.grind.ematch.instance true in
+run_meta analyzeEMatchTheorem ``List.filterMap_some {}

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/bench.sh

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail
 
-cmake --preset release 1>&2
+cmake --preset release -DUSE_LAKE=ON 1>&2
 
 # We benchmark against stage2/bin to test new optimizations.
 timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2

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 23)
 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")
 
@@ -88,8 +81,7 @@ option(USE_MIMALLOC "use mimalloc" ON)
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
-option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
-option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
+option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" 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`")
@@ -477,7 +469,6 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
   string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
   string(APPEND LEANSHARED_1_LINKER_FLAGS " -install_name @rpath/libleanshared_1.dylib")
-  string(APPEND LEANSHARED_2_LINKER_FLAGS " -install_name @rpath/libleanshared_2.dylib")
   string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
   string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -install_name @rpath/libLake_shared.dylib")
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
@@ -511,7 +502,7 @@ endif()
 # are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   # import libraries created by the stdlib.make targets
-  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared")
+  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
 elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
   # The second flag is necessary to even *load* dylibs without resolved symbols, as can happen
   # if a Lake `extern_lib` depends on a symbols defined by the Lean library but is loaded even
@@ -598,7 +589,7 @@ endif()
 
 add_subdirectory(initialize)
 add_subdirectory(shell)
-# to be included in `leanshared` but not the smaller `leanshared_*` (as it would pull
+# to be included in `leanshared` but not the smaller `leanshared_1` (as it would pull
 # in the world)
 add_library(leaninitialize STATIC $<TARGET_OBJECTS:initialize>)
 set_target_properties(leaninitialize PROPERTIES
@@ -723,7 +714,6 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   )
   add_custom_target(leanshared ALL
     DEPENDS Init_shared leancpp
-    COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX}
     COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
     COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
   )
@@ -744,7 +734,7 @@ else()
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
     VERBATIM)
 
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -805,9 +795,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 +821,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 +842,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,10 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-import all Init.Control.Except
-public import Init.Control.Option
-import all Init.Control.Option
-import all Init.Control.State
+public import all Init.Control.Except
+public import all Init.Control.State
 public import Init.Control.StateRef
+public import Init.Ext
 
 public section
 
@@ -21,24 +20,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 +44,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 +107,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 +173,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,14 +6,12 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
-import all Init.Control.Option
-import all Init.Control.Except
-public import Init.Control.ExceptCps
-import all Init.Control.ExceptCps
-import all Init.Control.StateRef
-public import Init.Control.StateCps
-import all Init.Control.StateCps
-import all Init.Control.Id
+public import all Init.Control.Option
+public import all Init.Control.Except
+public import all Init.Control.ExceptCps
+public import all Init.Control.StateRef
+public import all Init.Control.StateCps
+public import all Init.Control.Id
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.Instances
 
@@ -60,6 +58,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/Conv.lean

@@ -290,17 +290,13 @@ macro "right" : conv => `(conv| rhs)
 /-- `intro` traverses into binders. Synonym for `ext`. -/
 macro "intro" xs:(ppSpace colGt binderIdent)* : conv => `(conv| ext $xs*)
 
-syntax enterPattern := "in " (occs)? term
-
-syntax enterArg := binderIdent <|> argArg <|> enterPattern
+syntax enterArg := binderIdent <|> argArg
 
 /-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
 It is a shorthand for other conv tactics as follows:
 * `enter [i]` is equivalent to `arg i`.
 * `enter [@i]` is equivalent to `arg @i`.
 * `enter [x]` (where `x` is an identifier) is equivalent to `ext x`.
-* `enter [in e]` (where `e` is a term) is equivalent to `pattern e`.
-  Occurrences can be specified with `enter [in (occs := ...) e]`.
 For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]`
 will traverse to the subterm `b`. -/
 syntax (name := enter) "enter" " [" withoutPosition(enterArg,+) "]" : conv

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
@@ -28,29 +29,6 @@ theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
 attribute [grind] id
 
-/--
-A helper gadget for instructing the kernel to eagerly reduce terms.
-
-When the gadget wraps the argument of an application, then when checking that
-the expected and inferred type of the argument match, the kernel will evaluate terms more eagerly.
-It is often used to wrap `Eq.refl true` proof terms as `eagerReduce (Eq.refl true)`
-when using proof by reflection.
-As an example, consider the theorem:
-```
-theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : (p₁.norm == p₂) = true) :
-  p₁.denote ctx = 0 → p₂.denote ctx = 0
-```
-The argument `h : (p₁.norm == p₂) = true` is a candidate for `eagerReduce`.
-When applying this theorem, we would write:
-
-```
-eq_norm ctx p q (eagerReduce (Eq.refl true)) h
-```
-to instruct the kernel to use eager reduction when establishing that `(p.norm == q) = true` is
-definitionally equal to `true = true`.
--/
-@[expose] def eagerReduce {α : Sort u} (a : α) : α := a
-
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
 since it can sometimes be used to avoid introducing variables.
@@ -143,9 +121,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
@@ -1580,7 +1557,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 +1581,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
@@ -2523,17 +2499,12 @@ class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
   antisymm (a b : α) : r a b → r b a → a = b
 
-/-- `Asymm r` means that the binary relation `r` is asymmetric, that is,
+/-- `Asymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
 `r a b → ¬ r b a`. -/
 class Asymm (r : α → α → Prop) : Prop where
   /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
   asymm : ∀ a b, r a b → ¬r b a
 
-/-- `Symm r` means that the binary relation `r` is symmetric, that is, `r a b → r b a`.  -/
-class Symm (r : α → α → Prop) : Prop where
-  /-- A symmetric relation satisfies `r a b → r b a`. -/
-  symm : ∀ a b, r a b → r b a
-
 /-- `Total X r` means that the binary relation `r` on `X` is total, that is, that for any
 `x y : X` we have `r x y` or `r y x`. -/
 class Total (r : α → α → Prop) : Prop where
@@ -2547,3 +2518,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
@@ -51,5 +50,5 @@ public import Init.Data.Iterators
 public import Init.Data.Range.Polymorphic
 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,8 +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
-import all Init.Data.List.Attach
+public import all Init.Data.List.Attach
 
 public section
 
@@ -81,10 +83,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 +94,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 +120,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 +146,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 +175,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 +186,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 +211,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 +292,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 +344,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 +363,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 +399,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 +437,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 +445,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 +460,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 +468,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 +705,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,11 +6,15 @@ 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
-public import Init.Data.Array.Set
-import all Init.Data.Array.Set
+public import all Init.Data.List.ToArrayImpl
+public import all Init.Data.Array.Set
 
 public section
 
@@ -36,11 +40,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 +108,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 +123,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,8 +162,8 @@ 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]
-def usize (xs : @& Array α) : USize := xs.size.toUSize
+@[extern "lean_array_size", simp]
+def usize (a : @& Array α) : USize := a.size.toUSize
 
 /--
 Low-level indexing operator which is as fast as a C array read.
@@ -164,8 +171,8 @@ Low-level indexing operator which is as fast as a C array read.
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
 @[extern "lean_array_uget", simp, expose]
-def uget (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
-  xs[i.toNat]
+def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
+  a[i.toNat]
 
 /--
 Low-level modification operator which is as fast as a C array write. The modification is performed
@@ -190,7 +197,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 +406,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 +441,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 +759,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 +920,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 +1259,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 +1277,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 +1314,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 +1724,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 +1749,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 +1773,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 +1806,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 +1869,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 +1924,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 +1953,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 +2116,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 +2167,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,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Array.Basic
+public 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,7 +8,7 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 
 public section
 
@@ -23,6 +23,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} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
+  a.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 α] (a : @& Array α) (i : @& Nat) : α :=
+  Array.getD a 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 +107,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,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Count
 
@@ -62,7 +62,7 @@ theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + coun
   rcases xs with ⟨xs⟩
   simp [List.length_eq_countP_add_countP (p := p)]
 
-@[grind =]
+@[grind _=_]
 theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size := by
   rcases xs with ⟨xs⟩
   simp [List.countP_eq_length_filter]

src/Init/Data/Array/DecidableEq.lean

@@ -6,9 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Array.Basic
+public 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,10 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
+public 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 +90,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 +239,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 +270,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 +323,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,9 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
-import all Init.Data.Array.Basic
+public 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 +26,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 +227,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 +276,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 +304,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 +316,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 +344,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 +394,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 +727,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,10 +6,11 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
+public 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
+public import all Init.Data.List.MapIdx
 
 public section
 

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,11 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.List.Control
-import all Init.Data.Array.Basic
+public import all Init.Data.List.Control
+public 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 +165,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,10 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Monadic
+public import Init.Data.List.OfFn
 public import Init.Data.List.FinRange
 
 public section

src/Init/Data/Array/Perm.lean

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

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

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Vector.Basic
-public import Init.Data.Ord.Basic
+public import Init.Data.Ord
 
 public section
 

src/Init/Data/Array/Range.lean

@@ -6,10 +6,12 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
-import all Init.Data.Array.OfFn
+public import Init.Data.Array.Lemmas
+public import all Init.Data.Array.Basic
+public 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 +114,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,8 +7,8 @@ Authors: David Thrane Christiansen
 module
 
 prelude
-public import Init.Data.Array.Subarray
-import all Init.Data.Array.Subarray
+public import Init.Data.Array.Basic
+public import all Init.Data.Array.Subarray
 public import Init.Omega
 
 public section

src/Init/Data/Array/TakeDrop.lean

@@ -6,8 +6,9 @@ Authors: Markus Himmel
 module
 
 prelude
-import all Init.Data.Array.Basic
+public 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,9 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.TakeDrop
+public import Init.Data.List.Zip
 
 public section
 
@@ -229,9 +230,11 @@ theorem zip_map {f : α → γ} {g : β → δ} {as : Array α} {bs : Array β}
   cases bs
   simp [List.zip_map]
 
+@[grind _=_]
 theorem zip_map_left {f : α → γ} {as : Array α} {bs : Array β} :
     zip (as.map f) bs = (zip as bs).map (Prod.map f id) := by rw [← zip_map, map_id]
 
+@[grind _=_]
 theorem zip_map_right {f : β → γ} {as : Array α} {bs : Array β} :
     zip as (bs.map f) = (zip as bs).map (Prod.map id f) := by rw [← zip_map, map_id]
 

src/Init/Data/BEq.lean

@@ -23,14 +23,11 @@ class PartialEquivBEq (α) [BEq α] : Prop where
   /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
   trans : (a : α) == b → b == c → a == c
 
-instance [BEq α] [PartialEquivBEq α] : Std.Symm (α := α) (· == ·) where
-  symm _ _ h := PartialEquivBEq.symm h
-
 /-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
 class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 
-theorem BEq.symm [BEq α] [Std.Symm (α := α) (· == ·)] {a b : α} : a == b → b == a :=
-  Std.Symm.symm a b (r := (· == ·))
+theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
+  PartialEquivBEq.symm
 
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩

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