feat: add doc-string to grind algebra typeclasses

.github/workflows/awaiting-manual.yml

@@ -1,38 +0,0 @@
-name: Check awaiting-manual label
-
-on:
-  merge_group:
-  pull_request:
-    types: [opened, synchronize, reopened, labeled, unlabeled]
-
-jobs:
-  check-awaiting-manual:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check awaiting-manual label
-        id: check-awaiting-manual-label
-        if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
-        with:
-          script: |
-            const { labels, number: prNumber } = context.payload.pull_request;
-            const hasAwaiting = labels.some(label => label.name == "awaiting-manual");
-            const hasBreaks = labels.some(label => label.name == "breaks-manual");
-            const hasBuilds = labels.some(label => label.name == "builds-manual");
-
-            if (hasAwaiting && hasBreaks) {
-              core.setFailed('PR has both "awaiting-manual" and "breaks-manual" labels.');
-            } else if (hasAwaiting && !hasBreaks && !hasBuilds) {
-              core.info('PR is marked "awaiting-manual" but neither "breaks-manual" nor "builds-manual" labels are present.');
-              core.setOutput('awaiting', 'true');
-            }
-      
-      - name: Wait for manual compatibility
-        if: github.event_name == 'pull_request' && steps.check-awaiting-manual-label.outputs.awaiting == 'true'
-        run: |
-          echo "::notice title=Awaiting manual::PR is marked 'awaiting-manual' but neither 'breaks-manual' nor 'builds-manual' labels are present."
-          echo "This check will remain in progress until the PR is updated with appropriate manual compatibility labels."
-          # Keep the job running indefinitely to show "in progress" status
-          while true; do
-            sleep 3600  # Sleep for 1 hour at a time
-          done

.github/workflows/build-template.yml

@@ -107,7 +107,6 @@ jobs:
             ${{ matrix.name == 'Linux Lake' && false && 'build/stage1/**/*.trace
             build/stage1/**/*.olean*
             build/stage1/**/*.ilean
-            build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ matrix.name }}-build-v3-${{ github.sha }}
@@ -249,7 +248,6 @@ jobs:
             ${{ matrix.name == 'Linux Lake' && false && '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 }}

.github/workflows/ci.yml

@@ -145,7 +145,6 @@ jobs:
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
-            const isPushToMaster = "${{ github.event_name }}" == "push" && "${{ github.ref_name }}" == "master";
             let matrix = [
               /* TODO: to be updated to new LLVM
               {
@@ -168,13 +167,11 @@ jobs:
                 "os": large && level < 2 ? "nscloud-ubuntu-22.04-amd64-4x16" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developrs 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.
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
+                "check-level": isPr ? 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",
@@ -424,6 +421,6 @@ jobs:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
       - name: Update toolchain on mathlib4's nightly-testing branch
         run: |
-          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
         env:
           GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/grove.yml

@@ -1,161 +0,0 @@
-name: Grove
-
-on:
-  workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
-    workflows: [CI]
-    types: [completed]
-
-permissions:
-  pull-requests: write
-
-jobs:
-  grove-build:
-    runs-on: ubuntu-latest
-    if: github.event.workflow_run.conclusion == 'success' && github.repository == 'leanprover/lean4'
-
-    steps:
-      - name: Retrieve information about the original workflow
-        uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
-        # This action is deprecated and archived, but it seems hard to find a
-        # better solution for getting the PR number
-        # see https://github.com/orgs/community/discussions/25220 for some discussion
-        id: workflow-info
-        with:
-          token: ${{ secrets.GITHUB_TOKEN }}
-          sourceRunId: ${{ github.event.workflow_run.id }}
-
-      - name: Check if should run
-        id: should-run
-        run: |
-          # Check if it's a push to master (no PR number and target branch is master)
-          if [ -z "${{ steps.workflow-info.outputs.pullRequestNumber }}" ]; then
-            if [ "${{ github.event.workflow_run.head_branch }}" = "master" ]; then
-              echo "Push to master detected. Skipping for now, to be enabled later."
-              echo "should-run=false" >> "$GITHUB_OUTPUT"
-            else
-              echo "Push to non-master branch, skipping"
-              echo "should-run=false" >> "$GITHUB_OUTPUT"
-            fi
-          else
-            # Check if it's a PR with grove label
-            PR_LABELS='${{ steps.workflow-info.outputs.pullRequestLabels }}'
-            if echo "$PR_LABELS" | grep -q '"grove"'; then
-              echo "PR with grove label detected"
-              echo "should-run=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "PR without grove label, skipping"
-              echo "should-run=false" >> "$GITHUB_OUTPUT"
-            fi
-          fi
-
-      - name: Fetch upstream invalidated facts
-        if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: fetch-upstream
-        uses: TwoFx/grove-action/fetch-upstream@v0.3
-        with:
-          artifact-name: grove-invalidated-facts
-          base-ref: master
-
-      - name: Download toolchain for this commit
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: download-toolchain
-        uses: dawidd6/action-download-artifact@v11
-        with:
-          commit: ${{ steps.workflow-info.outputs.sourceHeadSha }}
-          workflow: ci.yml
-          path: artifacts
-          name: build-Linux.*
-          name_is_regexp: true
-
-      - name: Unpack toolchain
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: unpack-toolchain
-        run: |
-          cd artifacts
-          # Find the tar.zst file
-          TAR_FILE=$(find . -name "lean-*.tar.zst" -type f | head -1)
-          if [ -z "$TAR_FILE" ]; then
-            echo "Error: No lean-*.tar.zst file found"
-            exit 1
-          fi
-          echo "Found archive: $TAR_FILE"
-
-          # Extract the archive
-          tar --zstd -xf "$TAR_FILE"
-
-          # Find the extracted directory name
-          LEAN_DIR=$(find . -maxdepth 1 -name "lean-*" -type d | head -1)
-          if [ -z "$LEAN_DIR" ]; then
-            echo "Error: No lean-* directory found after extraction"
-            exit 1
-          fi
-          echo "Extracted directory: $LEAN_DIR"
-          echo "lean-dir=$LEAN_DIR" >> "$GITHUB_OUTPUT"
-
-      - name: Build
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: build
-        uses: TwoFx/grove-action/build@v0.3
-        with:
-          project-path: doc/std/grove
-          script-name: grove-stdlib
-          invalidated-facts-artifact-name: grove-invalidated-facts
-          comment-artifact-name: grove-comment
-          toolchain-id: lean4
-          toolchain-path: artifacts/${{ steps.unpack-toolchain.outputs.lean-dir }}
-          project-ref: ${{ steps.workflow-info.outputs.sourceHeadSha }}
-
-      # deploy-alias computes a URL component for the PR preview. This
-      # is so we can have a stable name to use for feedback on draft
-      # material.
-      - id: deploy-alias
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        uses: actions/github-script@v7
-        name: Compute Alias
-        with:
-          result-encoding: string
-          script: |
-            if (process.env.PR) {
-                return `pr-${process.env.PR}`
-            } else {
-                return 'deploy-preview-main';
-            }
-        env:
-          PR: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-
-      - name: Deploy to Netlify
-        if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        id: deploy-draft
-        uses: nwtgck/actions-netlify@v3.0
-        with:
-          publish-dir: ${{ steps.build.outputs.out-path }}
-          production-deploy: false
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          alias: ${{ steps.deploy-alias.outputs.result }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          fails-without-credentials: true
-          enable-github-deployment: false
-          enable-commit-status: false
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "1cacfa39-a11c-467c-99e7-2e01d7b4089e"
-
-      # actions-netlify cannot add deploy links to a PR because it assumes a
-      # pull_request context, not a workflow_run context, see
-      # https://github.com/nwtgck/actions-netlify/issues/545
-      # We work around by using a comment to post the latest link
-      - name: "Comment on PR with preview links"
-        uses: marocchino/sticky-pull-request-comment@v2
-        if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }}
-        with:
-          number: ${{ env.PR_NUMBER }}
-          header: preview-comment
-          recreate: true
-          message: |
-            [Grove](${{ steps.deploy-draft.outputs.deploy-url }}) for revision ${{ steps.workflow-info.outputs.sourceHeadSha }}.
-
-            ${{ steps.build.outputs.comment-text }}
-        env:
-          PR_NUMBER: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-          PR_HEADSHA: ${{ steps.workflow-info.outputs.sourceHeadSha }}

.github/workflows/pr-release.yml

@@ -154,7 +154,7 @@ jobs:
         uses: dcarbone/install-jq-action@v3.1.1
 
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
-      - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries
+      - name: Check merge-base and nightly-testing-YYYY-MM-DD
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: ready
         run: |
@@ -167,7 +167,7 @@ jobs:
             echo "The merge base of this PR coincides with the nightly release"
 
             BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4-nightly-testing.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
             if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
               echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
@@ -183,6 +183,7 @@ jobs:
               echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
             fi
+
           else
             echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
@@ -264,108 +265,6 @@ jobs:
             echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
           fi
 
-      - name: Check merge-base and nightly-testing-YYYY-MM-DD for reference manual
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: reference-manual-ready
-        run: |
-          echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY"
-          NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}")
-          echo "SHA of most recent nightly release: $NIGHTLY_SHA"
-          MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
-          echo "SHA of merge-base: $MERGE_BASE_SHA"
-          if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
-            echo "The merge base of this PR coincides with the nightly release"
-
-            MANUAL_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/reference-manual.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-            if [[ -n "$MANUAL_REMOTE_TAGS" ]]; then
-              echo "... and the reference manual has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE=""
-            else
-              echo "... but the reference manual does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Reference manual CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-manual\`, reference manual CI should run now."
-            fi
-          else
-            echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
-            echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
-            git -C lean4.git log -10 origin/master
-
-            git -C lean4.git fetch origin nightly-with-manual
-            NIGHTLY_WITH_MANUAL_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-manual")"
-            MESSAGE="- ❗ Reference manual CI will not be attempted unless your PR branches off the \`nightly-with-manual\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MANUAL_SHA\`."
-          fi
-
-          if [[ -n "$MESSAGE" ]]; then
-            # Check if force-manual-ci label is present
-            LABELS="$(curl --retry 3 --location --silent \
-                          -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-                          -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"
-              FORCE_CI=true
-            else
-              MESSAGE="$MESSAGE You can force reference manual CI using the \`force-manual-ci\` label."
-            fi
-
-            echo "Checking existing messages"
-
-            # The code for updating comments is duplicated in the reference manual's
-            # scripts/lean-pr-testing-comments.sh
-            # so keep in sync
-
-            # Use GitHub API to check if a comment already exists
-            existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-                                    -H "Accept: application/vnd.github.v3+json" \
-                                    "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Manual") or startswith("Reference manual CI status")) | select(.user.login == "leanprover-bot"))')"
-            existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
-            existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
-
-            if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then
-              MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))"
-
-              echo "Posting message to the comments: $MESSAGE"
-
-              # Append new result to the existing comment or post a new comment
-              # It's essential we use the MANUAL_COMMENT_BOT token here, so that reference manual CI can subsequently edit the comment.
-              if [ -z "$existing_comment_id" ]; then
-                INTRO="Reference manual CI status:"
-                # Post new comment with a bullet point
-                echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
-                curl -L -s \
-                  -X POST \
-                  -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-                  -H "Accept: application/vnd.github.v3+json" \
-                  -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
-                  "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
-              else
-                # Append new result to the existing comment
-                echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
-                curl -L -s \
-                  -X PATCH \
-                  -H "Authorization: token ${{ secrets.MANUAL_COMMENT_BOT }}" \
-                  -H "Accept: application/vnd.github.v3+json" \
-                  -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
-                  "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
-              fi
-            else
-              echo "The message already exists in the comment body."
-            fi
-
-            if [[ "$FORCE_CI" == "true" ]]; then
-              echo "manual_ready=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "manual_ready=false" >> "$GITHUB_OUTPUT"
-            fi
-          else
-            echo "manual_ready=true" >> "$GITHUB_OUTPUT"
-          fi
-
-
       - name: Report mathlib base
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
         uses: actions/github-script@v7
@@ -456,7 +355,7 @@ jobs:
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         uses: actions/checkout@v4
         with:
-          repository: leanprover-community/mathlib4-nightly-testing
+          repository: leanprover-community/mathlib4
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
@@ -512,63 +411,3 @@ jobs:
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
           git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-
-      # We next automatically create a reference manual branch using this toolchain.
-      # Reference manual CI will be responsible for reporting back success or failure
-      # to the PR comments asynchronously (and thus transitively SubVerso/Verso).
-      - name: Cleanup workspace
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        run: |
-          sudo rm -rf ./*
-
-      # 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@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.
-
-      - name: Check if tag in reference manual exists
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        id: check_manual_tag
-        run: |
-          git config user.name "leanprover-bot"
-          git config user.email "leanprover-bot@lean-fro.org"
-
-          if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
-            BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
-          else
-            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch in the reference manual. Falling back to 'nightly-testing'."
-            BASE=nightly-testing
-          fi
-
-          echo "Using base tag: $BASE"
-
-          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
-          echo "Branch exists: $EXISTS"
-          if [ "$EXISTS" = "0" ]; then
-            echo "Branch does not exist, creating it."
-            git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            git add lakefile.lean lake-manifest.json
-            git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          else
-            echo "Branch already exists, updating lean-toolchain."
-            git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The reference manual's `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
-            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
-            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
-            git add lean-toolchain
-            git add lake-manifest.json
-            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          fi
-
-      - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        run: |
-          git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}

.gitignore

@@ -6,6 +6,7 @@
 lake-manifest.json
 /build
 /src/lakefile.toml
+/tests/lakefile.toml
 /lakefile.toml
 GPATH
 GRTAGS
@@ -31,4 +32,3 @@ fwOut.txt
 wdErr.txt
 wdIn.txt
 wdOut.txt
-downstream_releases/

CMakeLists.txt

@@ -16,7 +16,7 @@ foreach(var ${vars})
     list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
+    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")

doc/dev/ffi.md

@@ -68,7 +68,7 @@ The memory order of the fields is derived from the types and order of the fields
 * Fields of type `USize`
 * Other scalar fields, in decreasing order by size
 
-Within each group the fields are ordered in declaration order. Trivial wrapper types count as their underlying wrapped type for this purpose.
+Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
 
 * To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
 * To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
@@ -80,32 +80,32 @@ structure S where
   ptr_1 : Array Nat
   usize_1 : USize
   sc64_1 : UInt64
-  sc64_2 : { x : UInt64 // x > 0 } -- wrappers of scalars count as scalars
-  sc64_3 : Float -- `Float` is 64 bit
+  ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
+  sc64_2 : Float -- `Float` is 64 bit
   sc8_1 : Bool
   sc16_1 : UInt16
   sc8_2 : UInt8
-  sc64_4 : UInt64
+  sc64_3 : UInt64
   usize_2 : USize
-  sc32_1 : Char -- trivial wrapper around `UInt32`
-  sc32_2 : UInt32
+  ptr_3 : Char -- trivial wrapper around `UInt32`
+  sc32_1 : UInt32
   sc16_2 : UInt16
 ```
 would get re-sorted into the following memory order:
 
 * `S.ptr_1` - `lean_ctor_get(val, 0)`
-* `S.usize_1` - `lean_ctor_get_usize(val, 1)`
-* `S.usize_2` - `lean_ctor_get_usize(val, 2)`
-* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*3)`
-* `S.sc64_2` - `lean_ctor_get_uint64(val, sizeof(void*)*3 + 8)`
-* `S.sc64_3` - `lean_ctor_get_float(val, sizeof(void*)*3 + 16)`
-* `S.sc64_4` - `lean_ctor_get_uint64(val, sizeof(void*)*3 + 24)`
-* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*3 + 32)`
-* `S.sc32_2` - `lean_ctor_get_uint32(val, sizeof(void*)*3 + 36)`
-* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*3 + 40)`
-* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*3 + 42)`
-* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*3 + 44)`
-* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*3 + 45)`
+* `S.ptr_2` - `lean_ctor_get(val, 1)`
+* `S.ptr_3` - `lean_ctor_get(val, 2)`
+* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
+* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
+* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
+* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
+* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
+* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
+* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
+* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
+* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
+* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
 
 ### Borrowing
 
@@ -131,21 +131,14 @@ Thus `[init]` functions are run iff their module is imported, regardless of whet
 
 The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
 Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
-
-**Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
-
 Together with initialization of the Lean runtime, you should execute code like the following exactly once before accessing any Lean declarations:
-
 ```c
 void lean_initialize_runtime_module();
 void lean_initialize();
-char ** lean_setup_args(int argc, char ** argv);
-
 lean_object * initialize_A_B(uint8_t builtin, lean_object *);
 lean_object * initialize_C(uint8_t builtin, lean_object *);
 ...
 
-argv = lean_setup_args(argc, argv); // if using process-related functionality
 lean_initialize_runtime_module();
 //lean_initialize();  // necessary (and replaces `lean_initialize_runtime_module`) if you (indirectly) access the `Lean` package
 

doc/dev/index.md

@@ -85,13 +85,5 @@ such that changing files in `Init` doesn't force a full rebuild of `Lean`.
 You can test a Lean PR against Mathlib and Batteries by rebasing your PR
 on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.)
 CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
-on the `leanprover-community/mathlib4-nightly-testing` fork of Mathlib.
-This branch uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
+that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
 See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.
-
-### Testing against the Lean Language Reference
-You can test a Lean PR against the reference manual by rebasing your PR
-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.

doc/std/grove/.gitignore

@@ -1,4 +0,0 @@
-/.lake
-!lake-manifest.json
-metadata.json
-invalidated.json

doc/std/grove/GroveStdlib/Generated.lean

@@ -1,14 +0,0 @@
-import Grove.Framework
-import GroveStdlib.Generated.«associative-query-operations»
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated
-
-def restoreState : RestoreStateM Unit := do
-  «associative-query-operations».restoreState

doc/std/grove/GroveStdlib/Generated/associative-query-operations.lean

@@ -1,486 +0,0 @@
-import Grove.Framework
-
-/-
-This file is autogenerated by grove. You can manually edit it, for example to resolve merge
-conflicts, but be careful.
--/
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Generated.«associative-query-operations»
-
-def «01f88623-fa5f-4380-9772-b30f2fec5c94» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-  rowId := "01f88623-fa5f-4380-9772-b30f2fec5c94"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.isEmpty,
-      renderedStatement := "Std.DHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.DHashMap α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.Raw.isEmpty,
-      renderedStatement := "Std.DHashMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDHashMap.isEmpty,
-      renderedStatement := "Std.ExtDHashMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n  [LawfulHashable α] (m : Std.ExtDHashMap α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.isEmpty,
-      renderedStatement := "Std.DTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.isEmpty,
-      renderedStatement := "Std.DTreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp) :\n  Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.isEmpty,
-      renderedStatement := "Std.ExtDTreeMap.isEmpty.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.ExtDTreeMap α β cmp) :\n  Bool",
-      isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.isEmpty,
-      renderedStatement := "Std.HashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.Raw.isEmpty,
-      renderedStatement := "Std.HashMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashMap.isEmpty,
-      renderedStatement := "Std.ExtHashMap.isEmpty.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashMap α β) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.isEmpty,
-      renderedStatement := "Std.TreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.isEmpty,
-      renderedStatement := "Std.TreeMap.Raw.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.isEmpty,
-      renderedStatement := "Std.ExtTreeMap.isEmpty.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.ExtTreeMap α β cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.isEmpty,
-      renderedStatement := "Std.HashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.isEmpty,
-      renderedStatement := "Std.HashSet.Raw.isEmpty.{u} {α : Type u} (m : Std.HashSet.Raw α) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashSet.isEmpty,
-      renderedStatement := "Std.ExtHashSet.isEmpty.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashSet α) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.isEmpty,
-      renderedStatement := "Std.TreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.isEmpty,
-      renderedStatement := "Std.TreeSet.Raw.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.isEmpty", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.isEmpty,
-      renderedStatement := "Std.ExtTreeSet.isEmpty.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.ExtTreeSet α cmp) : Bool",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-def «f084f852-af71-45b6-8ab3-d251a8144f72» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "f084f852-af71-45b6-8ab3-d251a8144f72"
-  rowId := "f084f852-af71-45b6-8ab3-d251a8144f72"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.size,
-      renderedStatement := "Std.DHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.DHashMap α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DHashMap.Raw.size,
-      renderedStatement := "Std.DHashMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} (self : Std.DHashMap.Raw α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDHashMap.size,
-      renderedStatement := "Std.ExtDHashMap.size.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α]\n  [LawfulHashable α] (m : Std.ExtDHashMap α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap", "Std.DTreeMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.size,
-      renderedStatement := "Std.DTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.size,
-      renderedStatement := "Std.DTreeMap.Raw.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.size,
-      renderedStatement := "Std.ExtDTreeMap.size.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.ExtDTreeMap α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.HashMap", "Std.HashMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.size,
-      renderedStatement := "Std.HashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashMap.Raw.size,
-      renderedStatement := "Std.HashMap.Raw.size.{u, v} {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashMap.size,
-      renderedStatement := "Std.ExtHashMap.size.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashMap α β) : Nat",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.size,
-      renderedStatement := "Std.TreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.size,
-      renderedStatement := "Std.TreeMap.Raw.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.size,
-      renderedStatement := "Std.ExtTreeMap.size.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.ExtTreeMap α β cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.size,
-      renderedStatement := "Std.HashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) : Nat",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.size,
-      renderedStatement := "Std.HashSet.Raw.size.{u} {α : Type u} (m : Std.HashSet.Raw α) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtHashSet.size,
-      renderedStatement := "Std.ExtHashSet.size.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashSet α) : Nat",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.size,
-      renderedStatement := "Std.TreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.size,
-      renderedStatement := "Std.TreeSet.Raw.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) : Nat",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.size", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.size,
-      renderedStatement := "Std.ExtTreeSet.size.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.ExtTreeSet α cmp) : Nat",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-def «f4e6fa70-5aed-439d-aaad-5f4ced65bf7b» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "f4e6fa70-5aed-439d-aaad-5f4ced65bf7b"
-  rowId := "f4e6fa70-5aed-439d-aaad-5f4ced65bf7b"
-  rowState := #[⟨"Std.DTreeMap", "Std.DTreeMap.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.any,
-      renderedStatement := "Std.DTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp)\n  (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.DTreeMap.Raw.any,
-      renderedStatement := "Std.DTreeMap.Raw.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp)\n  (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtDTreeMap.any,
-      renderedStatement := "Std.ExtDTreeMap.any.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap", "Std.TreeMap.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.any,
-      renderedStatement := "Std.TreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (p : α → β → Bool) :\n  Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeMap.Raw.any,
-      renderedStatement := "Std.TreeMap.Raw.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp)\n  (p : α → β → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeMap.any,
-      renderedStatement := "Std.ExtTreeMap.any.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet", "Std.HashSet.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.any,
-      renderedStatement := "Std.HashSet.any.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.HashSet.Raw.any,
-      renderedStatement := "Std.HashSet.Raw.any.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet", "Std.TreeSet.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.any,
-      renderedStatement := "Std.TreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.TreeSet.Raw.any,
-      renderedStatement := "Std.TreeSet.Raw.any.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.any", Grove.Framework.Subexpression.State.declaration
-  (Grove.Framework.Declaration.def
-    { name := `Std.ExtTreeSet.any,
-      renderedStatement := "Std.ExtTreeSet.any.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.ExtTreeSet α cmp)\n  (p : α → Bool) : Bool",
-      isDeprecated := false })⟩,]
-  metadata := {
-    status := .bad
-    comment := "Missing for some containers"
-  }
-def «c1d181f6-3204-4956-946f-e81619f9feb4» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "c1d181f6-3204-4956-946f-e81619f9feb4"
-  rowId := "c1d181f6-3204-4956-946f-e81619f9feb4"
-  rowState := #[⟨"Std.DTreeMap", "Std.DTreeMap.all", .declaration (Declaration.def {
-    name := `Std.DTreeMap.all
-    renderedStatement := "Std.DTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp)\n  (p : (a : α) → β a → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all", .declaration (Declaration.def {
-    name := `Std.DTreeMap.Raw.all
-    renderedStatement := "Std.DTreeMap.Raw.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap.Raw α β cmp)\n  (p : (a : α) → β a → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.all", .declaration (Declaration.def {
-    name := `Std.ExtDTreeMap.all
-    renderedStatement := "Std.ExtDTreeMap.all.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeMap", "Std.TreeMap.all", .declaration (Declaration.def {
-    name := `Std.TreeMap.all
-    renderedStatement := "Std.TreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (p : α → β → Bool) :\n  Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.all", .declaration (Declaration.def {
-    name := `Std.TreeMap.Raw.all
-    renderedStatement := "Std.TreeMap.Raw.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp)\n  (p : α → β → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.all", .declaration (Declaration.def {
-    name := `Std.ExtTreeMap.all
-    renderedStatement := "Std.ExtTreeMap.all.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeMap α β cmp) (p : α → β → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.HashSet", "Std.HashSet.all", .declaration (Declaration.def {
-    name := `Std.HashSet.all
-    renderedStatement := "Std.HashSet.all.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashSet α) (p : α → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.all", .declaration (Declaration.def {
-    name := `Std.HashSet.Raw.all
-    renderedStatement := "Std.HashSet.Raw.all.{u} {α : Type u} (m : Std.HashSet.Raw α) (p : α → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeSet", "Std.TreeSet.all", .declaration (Declaration.def {
-    name := `Std.TreeSet.all
-    renderedStatement := "Std.TreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (p : α → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.all", .declaration (Declaration.def {
-    name := `Std.TreeSet.Raw.all
-    renderedStatement := "Std.TreeSet.Raw.all.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (p : α → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.all", .declaration (Declaration.def {
-    name := `Std.ExtTreeSet.all
-    renderedStatement := "Std.ExtTreeSet.all.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.ExtTreeSet α cmp)\n  (p : α → Bool) : Bool"
-    isDeprecated := false
-  }
-)⟩,]
-  metadata := {
-    status := .bad
-    comment := "Missing for some containers"
-  }
-def «efe57f41-7db7-4303-b3a6-5216a70c43ce» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "efe57f41-7db7-4303-b3a6-5216a70c43ce"
-  rowId := "efe57f41-7db7-4303-b3a6-5216a70c43ce"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.getD", .declaration (Declaration.def {
-    name := `Std.DHashMap.getD
-    renderedStatement := "Std.DHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n  (m : Std.DHashMap α β) (a : α) (fallback : β a) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.getD", .declaration (Declaration.def {
-    name := `Std.DHashMap.Raw.getD
-    renderedStatement := "Std.DHashMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Raw α β)\n  (a : α) (fallback : β a) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.getD", .declaration (Declaration.def {
-    name := `Std.ExtDHashMap.getD
-    renderedStatement := "Std.ExtDHashMap.getD.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n  (m : Std.ExtDHashMap α β) (a : α) (fallback : β a) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.DTreeMap", "Std.DTreeMap.getD", .declaration (Declaration.def {
-    name := `Std.DTreeMap.getD
-    renderedStatement := "Std.DTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n  (t : Std.DTreeMap α β cmp) (a : α) (fallback : β a) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD", .declaration (Declaration.def {
-    name := `Std.DTreeMap.Raw.getD
-    renderedStatement := "Std.DTreeMap.Raw.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n  (t : Std.DTreeMap.Raw α β cmp) (a : α) (fallback : β a) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.getD", .declaration (Declaration.def {
-    name := `Std.ExtDTreeMap.getD
-    renderedStatement := "Std.ExtDTreeMap.getD.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (fallback : β a) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.HashMap", "Std.HashMap.getD", .declaration (Declaration.def {
-    name := `Std.HashMap.getD
-    renderedStatement := "Std.HashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} (m : Std.HashMap α β) (a : α)\n  (fallback : β) : β"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.getD", .declaration (Declaration.def {
-    name := `Std.HashMap.Raw.getD
-    renderedStatement := "Std.HashMap.Raw.getD.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.HashMap.Raw α β) (a : α)\n  (fallback : β) : β"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.getD", .declaration (Declaration.def {
-    name := `Std.ExtHashMap.getD
-    renderedStatement := "Std.ExtHashMap.getD.{u, v} {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashMap α β) (a : α) (fallback : β) : β"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeMap", "Std.TreeMap.getD", .declaration (Declaration.def {
-    name := `Std.TreeMap.getD
-    renderedStatement := "Std.TreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap α β cmp) (a : α)\n  (fallback : β) : β"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.getD", .declaration (Declaration.def {
-    name := `Std.TreeMap.Raw.getD
-    renderedStatement := "Std.TreeMap.Raw.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : Std.TreeMap.Raw α β cmp) (a : α)\n  (fallback : β) : β"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.getD", .declaration (Declaration.def {
-    name := `Std.ExtTreeMap.getD
-    renderedStatement := "Std.ExtTreeMap.getD.{u, v} {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  (t : Std.ExtTreeMap α β cmp) (a : α) (fallback : β) : β"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.HashSet", "Std.HashSet.getD", .declaration (Declaration.def {
-    name := `Std.HashSet.getD
-    renderedStatement := "Std.HashSet.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a fallback : α) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.getD", .declaration (Declaration.def {
-    name := `Std.HashSet.Raw.getD
-    renderedStatement := "Std.HashSet.Raw.getD.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α) (a fallback : α) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.getD", .declaration (Declaration.def {
-    name := `Std.ExtHashSet.getD
-    renderedStatement := "Std.ExtHashSet.getD.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashSet α) (a fallback : α) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeSet", "Std.TreeSet.getD", .declaration (Declaration.def {
-    name := `Std.TreeSet.getD
-    renderedStatement := "Std.TreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (a fallback : α) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.getD", .declaration (Declaration.def {
-    name := `Std.TreeSet.Raw.getD
-    renderedStatement := "Std.TreeSet.Raw.getD.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (a fallback : α) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.getD", .declaration (Declaration.def {
-    name := `Std.ExtTreeSet.getD
-    renderedStatement := "Std.ExtTreeSet.getD.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.ExtTreeSet α cmp)\n  (a fallback : α) : α"
-    isDeprecated := false
-  }
-)⟩,]
-  metadata := {
-    status := .done
-    comment := ""
-  }
-def «e23b1119-3b57-433e-a68d-68fd70b9943d» : AssociationTable.Fact .subexpression where
-  widgetId := "associative-query-operations"
-  factId := "e23b1119-3b57-433e-a68d-68fd70b9943d"
-  rowId := "e23b1119-3b57-433e-a68d-68fd70b9943d"
-  rowState := #[⟨"Std.DHashMap", "Std.DHashMap.get", .declaration (Declaration.def {
-    name := `Std.DHashMap.get
-    renderedStatement := "Std.DHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n  (m : Std.DHashMap α β) (a : α) (h : a ∈ m) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.Const.get", .declaration (Declaration.def {
-    name := `Std.DHashMap.Raw.Const.get
-    renderedStatement := "Std.DHashMap.Raw.Const.get.{u, v} {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Raw α fun x => β)\n  (a : α) (h : a ∈ m) : β"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.get", .declaration (Declaration.def {
-    name := `Std.ExtDHashMap.get
-    renderedStatement := "Std.ExtDHashMap.get.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [LawfulBEq α]\n  (m : Std.ExtDHashMap α β) (a : α) (h : a ∈ m) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.DTreeMap", "Std.DTreeMap.get", .declaration (Declaration.def {
-    name := `Std.DTreeMap.get
-    renderedStatement := "Std.DTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n  (t : Std.DTreeMap α β cmp) (a : α) (h : a ∈ t) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.get", .declaration (Declaration.def {
-    name := `Std.DTreeMap.Raw.get
-    renderedStatement := "Std.DTreeMap.Raw.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp]\n  (t : Std.DTreeMap.Raw α β cmp) (a : α) (h : a ∈ t) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.get", .declaration (Declaration.def {
-    name := `Std.ExtDTreeMap.get
-    renderedStatement := "Std.ExtDTreeMap.get.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp]\n  [Std.LawfulEqCmp cmp] (t : Std.ExtDTreeMap α β cmp) (a : α) (h : a ∈ t) : β a"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.HashMap", "app (GetElem.getElem) (Std.HashMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.HashMap*)", displayShort := "Std.HashMap[·]" }⟩,⟨"Std.HashMap.Raw", "app (GetElem.getElem) (Std.HashMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.HashMap.Raw*)", displayShort := "Std.HashMap.Raw[·]" }⟩,⟨"Std.ExtHashMap", "app (GetElem.getElem) (Std.ExtHashMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.ExtHashMap*)", displayShort := "Std.ExtHashMap[·]" }⟩,⟨"Std.TreeMap", "app (GetElem.getElem) (Std.TreeMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.TreeMap*)", displayShort := "Std.TreeMap[·]" }⟩,⟨"Std.TreeMap.Raw", "app (GetElem.getElem) (Std.TreeMap.Raw*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.TreeMap.Raw*)", displayShort := "Std.TreeMap.Raw[·]" }⟩,⟨"Std.ExtTreeMap", "app (GetElem.getElem) (Std.ExtTreeMap*)", Grove.Framework.Subexpression.State.predicate
-  { key := "app (GetElem.getElem) (Std.ExtTreeMap*)", displayShort := "Std.ExtTreeMap[·]" }⟩,⟨"Std.HashSet", "Std.HashSet.get", .declaration (Declaration.def {
-    name := `Std.HashSet.get
-    renderedStatement := "Std.HashSet.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (a : α) (h : a ∈ m) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.get", .declaration (Declaration.def {
-    name := `Std.HashSet.Raw.get
-    renderedStatement := "Std.HashSet.Raw.get.{u} {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet.Raw α) (a : α) (h : a ∈ m) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.get", .declaration (Declaration.def {
-    name := `Std.ExtHashSet.get
-    renderedStatement := "Std.ExtHashSet.get.{u} {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α]\n  (m : Std.ExtHashSet α) (a : α) (h : a ∈ m) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeSet", "Std.TreeSet.get", .declaration (Declaration.def {
-    name := `Std.TreeSet.get
-    renderedStatement := "Std.TreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp) (a : α) (h : a ∈ t) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.get", .declaration (Declaration.def {
-    name := `Std.TreeSet.Raw.get
-    renderedStatement := "Std.TreeSet.Raw.get.{u} {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp) (a : α) (h : a ∈ t) : α"
-    isDeprecated := false
-  }
-)⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.get", .declaration (Declaration.def {
-    name := `Std.ExtTreeSet.get
-    renderedStatement := "Std.ExtTreeSet.get.{u} {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] (t : Std.ExtTreeSet α cmp) (a : α)\n  (h : a ∈ t) : α"
-    isDeprecated := false
-  }
-)⟩,]
-  metadata := {
-    status := .bad
-    comment := "Should *Set have GetElem?"
-  }
-
-def table : AssociationTable.Data .subexpression where
-  widgetId := "associative-query-operations"
-  rows := #[
-    ⟨"01f88623-fa5f-4380-9772-b30f2fec5c94", "isEmpty", #[⟨"Std.DHashMap", "Std.DHashMap.isEmpty"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.isEmpty"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.isEmpty"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.isEmpty"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.isEmpty"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.isEmpty"⟩,⟨"Std.HashMap", "Std.HashMap.isEmpty"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.isEmpty"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.isEmpty"⟩,⟨"Std.TreeMap", "Std.TreeMap.isEmpty"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.isEmpty"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.isEmpty"⟩,⟨"Std.HashSet", "Std.HashSet.isEmpty"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.isEmpty"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.isEmpty"⟩,⟨"Std.TreeSet", "Std.TreeSet.isEmpty"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.isEmpty"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.isEmpty"⟩,]⟩,
-    ⟨"f084f852-af71-45b6-8ab3-d251a8144f72", "size", #[⟨"Std.DHashMap", "Std.DHashMap.size"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.size"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.size"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.size"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.size"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.size"⟩,⟨"Std.HashMap", "Std.HashMap.size"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.size"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.size"⟩,⟨"Std.TreeMap", "Std.TreeMap.size"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.size"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.size"⟩,⟨"Std.HashSet", "Std.HashSet.size"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.size"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.size"⟩,⟨"Std.TreeSet", "Std.TreeSet.size"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.size"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.size"⟩,]⟩,
-    ⟨"f4e6fa70-5aed-439d-aaad-5f4ced65bf7b", "any", #[⟨"Std.DTreeMap", "Std.DTreeMap.any"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.any"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.any"⟩,⟨"Std.TreeMap", "Std.TreeMap.any"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.any"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.any"⟩,⟨"Std.HashSet", "Std.HashSet.any"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.any"⟩,⟨"Std.TreeSet", "Std.TreeSet.any"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.any"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.any"⟩,]⟩,
-    ⟨"c1d181f6-3204-4956-946f-e81619f9feb4", "all", #[⟨"Std.DTreeMap", "Std.DTreeMap.all"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.all"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.all"⟩,⟨"Std.TreeMap", "Std.TreeMap.all"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.all"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.all"⟩,⟨"Std.HashSet", "Std.HashSet.all"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.all"⟩,⟨"Std.TreeSet", "Std.TreeSet.all"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.all"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.all"⟩,]⟩,
-    ⟨"efe57f41-7db7-4303-b3a6-5216a70c43ce", "getD", #[⟨"Std.DHashMap", "Std.DHashMap.getD"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.getD"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.getD"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.getD"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.getD"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.getD"⟩,⟨"Std.HashMap", "Std.HashMap.getD"⟩,⟨"Std.HashMap.Raw", "Std.HashMap.Raw.getD"⟩,⟨"Std.ExtHashMap", "Std.ExtHashMap.getD"⟩,⟨"Std.TreeMap", "Std.TreeMap.getD"⟩,⟨"Std.TreeMap.Raw", "Std.TreeMap.Raw.getD"⟩,⟨"Std.ExtTreeMap", "Std.ExtTreeMap.getD"⟩,⟨"Std.HashSet", "Std.HashSet.getD"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.getD"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.getD"⟩,⟨"Std.TreeSet", "Std.TreeSet.getD"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.getD"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.getD"⟩,]⟩,
-    ⟨"e23b1119-3b57-433e-a68d-68fd70b9943d", "getElem", #[⟨"Std.DHashMap", "Std.DHashMap.get"⟩,⟨"Std.DHashMap.Raw", "Std.DHashMap.Raw.Const.get"⟩,⟨"Std.ExtDHashMap", "Std.ExtDHashMap.get"⟩,⟨"Std.DTreeMap", "Std.DTreeMap.get"⟩,⟨"Std.DTreeMap.Raw", "Std.DTreeMap.Raw.get"⟩,⟨"Std.ExtDTreeMap", "Std.ExtDTreeMap.get"⟩,⟨"Std.HashMap", "app (GetElem.getElem) (Std.HashMap*)"⟩,⟨"Std.HashMap.Raw", "app (GetElem.getElem) (Std.HashMap.Raw*)"⟩,⟨"Std.ExtHashMap", "app (GetElem.getElem) (Std.ExtHashMap*)"⟩,⟨"Std.TreeMap", "app (GetElem.getElem) (Std.TreeMap*)"⟩,⟨"Std.TreeMap.Raw", "app (GetElem.getElem) (Std.TreeMap.Raw*)"⟩,⟨"Std.ExtTreeMap", "app (GetElem.getElem) (Std.ExtTreeMap*)"⟩,⟨"Std.HashSet", "Std.HashSet.get"⟩,⟨"Std.HashSet.Raw", "Std.HashSet.Raw.get"⟩,⟨"Std.ExtHashSet", "Std.ExtHashSet.get"⟩,⟨"Std.TreeSet", "Std.TreeSet.get"⟩,⟨"Std.TreeSet.Raw", "Std.TreeSet.Raw.get"⟩,⟨"Std.ExtTreeSet", "Std.ExtTreeSet.get"⟩,]⟩,
-  ]
-  facts := #[
-    «01f88623-fa5f-4380-9772-b30f2fec5c94»,
-    «f084f852-af71-45b6-8ab3-d251a8144f72»,
-    «f4e6fa70-5aed-439d-aaad-5f4ced65bf7b»,
-    «c1d181f6-3204-4956-946f-e81619f9feb4»,
-    «efe57f41-7db7-4303-b3a6-5216a70c43ce»,
-    «e23b1119-3b57-433e-a68d-68fd70b9943d»,
-  ]
-
-def restoreState : RestoreStateM Unit := do
-  addAssociationTable table

doc/std/grove/GroveStdlib/Std.lean

@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import GroveStdlib.Std.CoreTypesAndOperations
-import GroveStdlib.Std.LanguageConstructs
-import GroveStdlib.Std.Libraries
-import GroveStdlib.Std.OperatingSystemAbstractions
-
-open Grove.Framework Widget
-
-namespace GroveStdlib
-
-namespace Std
-
-def introduction : Node :=
-  .text "Welcome to the interactive Lean standard library outline!"
-
-end Std
-
-def std : Node :=
-  .section "stdlib" "The Lean standard library" #[
-    Std.introduction,
-    Std.coreTypesAndOperations,
-    Std.languageConstructs,
-    Std.libraries,
-    Std.operatingSystemAbstractions
-  ]
-
-end GroveStdlib

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations.lean

@@ -1,28 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-import GroveStdlib.Std.CoreTypesAndOperations.BasicTypes
-import GroveStdlib.Std.CoreTypesAndOperations.Containers
-import GroveStdlib.Std.CoreTypesAndOperations.Numbers
-import GroveStdlib.Std.CoreTypesAndOperations.StringsAndFormatting
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std
-
-namespace CoreTypesAndOperations
-
-end CoreTypesAndOperations
-
-def coreTypesAndOperations : Node :=
-  .section "core-types-and-operations" "Core types and operations" #[
-    CoreTypesAndOperations.basicTypes,
-    CoreTypesAndOperations.containers,
-    CoreTypesAndOperations.numbers,
-    CoreTypesAndOperations.stringsAndFormatting
-  ]
-
-end GroveStdlib.Std

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/BasicTypes.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace BasicTypes
-
-end BasicTypes
-
-def basicTypes : Node :=
-  .section "basic-types" "Basic types" #[]
-
-end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Containers.lean

@@ -1,58 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace Containers
-
-namespace SequentialContainers
-
-end SequentialContainers
-
-def sequentialContainers : Node :=
-  .section "sequential-containers" "Sequential containers" #[]
-
-namespace AssociativeContainers
-
-def associativeQueryOperations : AssociationTable .subexpression
-    [`Std.DHashMap, `Std.DHashMap.Raw, `Std.ExtDHashMap, `Std.DTreeMap, `Std.DTreeMap.Raw, `Std.ExtDTreeMap, `Std.HashMap,
-     `Std.HashMap.Raw, `Std.ExtHashMap, `Std.TreeMap, `Std.TreeMap.Raw, `Std.ExtTreeMap, `Std.HashSet, `Std.HashSet.Raw, `Std.ExtHashSet,
-     `Std.TreeSet, `Std.TreeSet.Raw, `Std.ExtTreeSet] where
-  id := "associative-query-operations"
-  title := "Associative query operations"
-  description := "Operations that take as input an associative container and return a 'single' piece of information (e.g., `GetElem` or `isEmpty`, but not `toList`)."
-  dataSources n :=
-    (DataSource.declarationsInNamespace n .definitionsOnly)
-      |>.map Subexpression.declaration
-      |>.or (DataSource.getElem n)
-
-end AssociativeContainers
-
-def associativeContainers : Node :=
-  .section "associative-containers" "Associative containers" #[
-    .associationTable AssociativeContainers.associativeQueryOperations
-  ]
-
-namespace PersistentDataStructures
-
-end PersistentDataStructures
-
-def persistentDataStructures : Node :=
-  .section "persistent-data-structures" "Persistent data structures" #[]
-
-end Containers
-
-def containers : Node :=
-  .section "containers" "Containers" #[
-    Containers.sequentialContainers,
-    Containers.associativeContainers,
-    Containers.persistentDataStructures
-  ]
-
-end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/Numbers.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace Numbers
-
-end Numbers
-
-def numbers : Node :=
-  .section "numbers" "Numbers" #[]
-
-end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/GroveStdlib/Std/CoreTypesAndOperations/StringsAndFormatting.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.CoreTypesAndOperations
-
-namespace StringsAndFormatting
-
-end StringsAndFormatting
-
-def stringsAndFormatting : Node :=
-  .section "strings-and-formatting" "Strings and formatting" #[]
-
-end GroveStdlib.Std.CoreTypesAndOperations

doc/std/grove/GroveStdlib/Std/LanguageConstructs.lean

@@ -1,26 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-import GroveStdlib.Std.LanguageConstructs.ComparisonOrderingHashing
-import GroveStdlib.Std.LanguageConstructs.Monads
-import GroveStdlib.Std.LanguageConstructs.RangesAndIterators
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std
-
-namespace LanguageConstructs
-
-end LanguageConstructs
-
-def languageConstructs : Node :=
-  .section "language-constructs" "Language constructs" #[
-    LanguageConstructs.comparisonOrderingHashing,
-    LanguageConstructs.monads,
-    LanguageConstructs.rangesAndIterators
-  ]
-
-end GroveStdlib.Std

doc/std/grove/GroveStdlib/Std/LanguageConstructs/ComparisonOrderingHashing.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.LanguageConstructs
-
-namespace ComparisonOrderingHashing
-
-end ComparisonOrderingHashing
-
-def comparisonOrderingHashing : Node :=
-  .section "comparison-ordering-hashing" "Comparison, ordering, hashing" #[]
-
-end GroveStdlib.Std.LanguageConstructs

doc/std/grove/GroveStdlib/Std/LanguageConstructs/Monads.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.LanguageConstructs
-
-namespace Monads
-
-end Monads
-
-def monads : Node :=
-  .section "monads" "Monads" #[]
-
-end GroveStdlib.Std.LanguageConstructs

doc/std/grove/GroveStdlib/Std/LanguageConstructs/RangesAndIterators.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.LanguageConstructs
-
-namespace RangesAndIterators
-
-end RangesAndIterators
-
-def rangesAndIterators : Node :=
-  .section "ranges-and-iterators" "Ranges and iterators" #[]
-
-end GroveStdlib.Std.LanguageConstructs

doc/std/grove/GroveStdlib/Std/Libraries.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-import GroveStdlib.Std.Libraries.DateAndTime
-import GroveStdlib.Std.Libraries.RandomNumbers
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std
-
-namespace Libraries
-
-end Libraries
-
-def libraries : Node :=
-  .section "libraries" "Libraries" #[
-    Libraries.dateAndTime,
-    Libraries.randomNumbers
-  ]
-
-end GroveStdlib.Std

doc/std/grove/GroveStdlib/Std/Libraries/DateAndTime.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.Libraries
-
-namespace DateAndTime
-
-end DateAndTime
-
-def dateAndTime : Node :=
-  .section "date-and-time" "Date and time" #[]
-
-end GroveStdlib.Std.Libraries

doc/std/grove/GroveStdlib/Std/Libraries/RandomNumbers.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.Libraries
-
-namespace RandomNumbers
-
-end RandomNumbers
-
-def randomNumbers : Node :=
-  .section "random-numbers" "Random numbers" #[]
-
-end GroveStdlib.Std.Libraries

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions.lean

@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-import GroveStdlib.Std.OperatingSystemAbstractions.AsynchronousIO
-import GroveStdlib.Std.OperatingSystemAbstractions.BasicIO
-import GroveStdlib.Std.OperatingSystemAbstractions.ConcurrencyAndParallelism
-import GroveStdlib.Std.OperatingSystemAbstractions.EnvironmentFileSystemProcesses
-import GroveStdlib.Std.OperatingSystemAbstractions.Locales
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std
-
-namespace OperatingSystemAbstractions
-
-end OperatingSystemAbstractions
-
-def operatingSystemAbstractions : Node :=
-  .section "operating-system-abstractions" "Operating system abstractions" #[
-    OperatingSystemAbstractions.asynchronousIO,
-    OperatingSystemAbstractions.basicIO,
-    OperatingSystemAbstractions.concurrencyAndParallelism,
-    OperatingSystemAbstractions.environmentFileSystemProcesses,
-    OperatingSystemAbstractions.locales
-  ]
-
-end GroveStdlib.Std

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/AsynchronousIO.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace AsynchronousIO
-
-end AsynchronousIO
-
-def asynchronousIO : Node :=
-  .section "asynchronous-io" "Asynchronous I/O" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/BasicIO.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace BasicIO
-
-end BasicIO
-
-def basicIO : Node :=
-  .section "basic-io" "Basic I/O" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/ConcurrencyAndParallelism.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace ConcurrencyAndParallelism
-
-end ConcurrencyAndParallelism
-
-def concurrencyAndParallelism : Node :=
-  .section "concurrency-and-parallelism" "Concurrency and parallelism" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/EnvironmentFileSystemProcesses.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace EnvironmentFileSystemProcesses
-
-end EnvironmentFileSystemProcesses
-
-def environmentFileSystemProcesses : Node :=
-  .section "environment-filesystem-processes" "Environment, file system, processes" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/GroveStdlib/Std/OperatingSystemAbstractions/Locales.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Grove.Framework
-
-open Grove.Framework Widget
-
-namespace GroveStdlib.Std.OperatingSystemAbstractions
-
-namespace Locales
-
-end Locales
-
-def locales : Node :=
-  .section "locales" "Locales" #[]
-
-end GroveStdlib.Std.OperatingSystemAbstractions

doc/std/grove/Main.lean

@@ -1,18 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import GroveStdlib.Std
-import GroveStdlib.Generated
-
-def config : Grove.Framework.Project.Configuration where
-  projectNamespace := `GroveStdlib
-
-def project : Grove.Framework.Project where
-  config := config
-  rootNode := GroveStdlib.std
-  restoreState := GroveStdlib.Generated.restoreState
-
-def main (args : List String) : IO UInt32 :=
-  Grove.Framework.main project #[`Init, `Std, `Lean] args

doc/std/grove/README.md

@@ -1,3 +0,0 @@
-# Standard library QA
-
-This directory contains the [Grove](github.com/TwoFX/grove) data files for the standard library.

doc/std/grove/grove-local.sh

@@ -1,10 +0,0 @@
-#!/bin/sh
-
-lake exe grove-stdlib --full metadata.json
-cd .lake/packages/grove/frontend
-npm install
-if [ -f "../../../../invalidated.json" ]; then
-    GROVE_DATA_LOCATION=../../../../metadata.json GROVE_UPSTREAM_INVALIDATED_FACTS_LOCATION=../../../../invalidated.json npm run dev
-else
-    GROVE_DATA_LOCATION=../../../../metadata.json npm run dev
-fi

doc/std/grove/lake-manifest.json

@@ -1,25 +0,0 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/TwoFx/grove.git",
-   "type": "git",
-   "subDir": "backend",
-   "scope": "",
-   "rev": "e8127fc6554b99fb988ecdceb770a5e112afbe24",
-   "name": "grove",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "1604206fcd0462da9a241beeac0e2df471647435",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"}],
- "name": "grovestdlib",
- "lakeDir": ".lake"}

doc/std/grove/lakefile.toml

@@ -1,18 +0,0 @@
-name = "grovestdlib"
-version = "0.1.0"
-defaultTargets = ["grove-stdlib"]
-
-[[require]]
-name = "grove"
-git = "https://github.com/TwoFx/grove.git"
-rev = "master"
-subDir = "backend"
-
-[[lean_lib]]
-name = "GroveStdlib"
-root = "GroveStdlib"
-
-[[lean_exe]]
-name = "grove-stdlib"
-supportInterpreter = true
-root = "Main"

doc/std/grove/lean-toolchain

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

doc/std/grove/update_invalidated.sh

@@ -1,3 +0,0 @@
-#!/bin/sh
-
-lake exe grove-stdlib --invalidated invalidated.json

script/mathlib-bench

@@ -5,11 +5,8 @@ set -euo pipefail
 
 [ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
 
-echo "Warning: the speedcenter is probably not listening on mathlib4-nightly-testing yet."
-echo "If you're using this script, please contact @kim-em or @Kha to get this set up, and then remove this notice."
-
 LEAN_PR=$1
-PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4-nightly-testing/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
+PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
 PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
-echo "opened https://github.com/leanprover-community/mathlib4-nightly-testing/pull/$PR_NUMBER"
-gh api repos/leanprover-community/mathlib4-nightly-testing/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null
+echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
+gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null

script/prepare-llvm-mingw.sh

@@ -50,4 +50,5 @@ echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -Wl,-Bstatic
 # when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
 # do not set `LEAN_CC` for tests
+echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"
 echo -n " -DLEAN_TEST_VARS=''"

script/push_repo_release_tag.py

@@ -3,32 +3,6 @@ import sys
 import subprocess
 import requests
 
-def check_gh_auth():
-    """Check if GitHub CLI is properly authenticated."""
-    try:
-        result = subprocess.run(["gh", "auth", "status"], capture_output=True, text=True)
-        if result.returncode != 0:
-            return False, result.stderr
-        return True, None
-    except FileNotFoundError:
-        return False, "GitHub CLI (gh) is not installed. Please install it first."
-    except Exception as e:
-        return False, f"Error checking authentication: {e}"
-
-def handle_gh_error(error_output):
-    """Handle GitHub CLI errors and provide helpful messages."""
-    if "Not Found (HTTP 404)" in error_output:
-        return "Repository not found or access denied. Please check:\n" \
-               "1. The repository name is correct\n" \
-               "2. You have access to the repository\n" \
-               "3. Your GitHub CLI authentication is valid"
-    elif "Bad credentials" in error_output or "invalid" in error_output.lower():
-        return "Authentication failed. Please run 'gh auth login' to re-authenticate."
-    elif "rate limit" in error_output.lower():
-        return "GitHub API rate limit exceeded. Please try again later."
-    else:
-        return f"GitHub API error: {error_output}"
-
 def main():
     if len(sys.argv) != 4:
         print("Usage: ./push_repo_release_tag.py <repo> <branch> <version_tag>")
@@ -40,13 +14,6 @@ def main():
         print(f"Error: Branch '{branch}' is not 'master' or 'main'.")
         sys.exit(1)
 
-    # Check GitHub CLI authentication first
-    auth_ok, auth_error = check_gh_auth()
-    if not auth_ok:
-        print(f"Authentication error: {auth_error}")
-        print("\nTo fix this, run: gh auth login")
-        sys.exit(1)
-
     # Get the `lean-toolchain` file content
     lean_toolchain_url = f"https://raw.githubusercontent.com/{repo}/{branch}/lean-toolchain"
     try:
@@ -76,23 +43,12 @@ def main():
                 for tag in existing_tags:
                     print(tag.replace("refs/tags/", ""))
                 sys.exit(1)
-        elif list_tags_output.returncode != 0:
-            # Handle API errors when listing tags
-            error_msg = handle_gh_error(list_tags_output.stderr)
-            print(f"Error checking existing tags: {error_msg}")
-            sys.exit(1)
 
         # Get the SHA of the branch
         get_sha_cmd = [
             "gh", "api", f"repos/{repo}/git/ref/heads/{branch}", "--jq", ".object.sha"
         ]
-        sha_result = subprocess.run(get_sha_cmd, capture_output=True, text=True)
-        
-        if sha_result.returncode != 0:
-            error_msg = handle_gh_error(sha_result.stderr)
-            print(f"Error getting branch SHA: {error_msg}")
-            sys.exit(1)
-            
+        sha_result = subprocess.run(get_sha_cmd, capture_output=True, text=True, check=True)
         sha = sha_result.stdout.strip()
 
         # Create the tag
@@ -102,20 +58,11 @@ def main():
             "-F", f"ref=refs/tags/{version_tag}",
             "-F", f"sha={sha}"
         ]
-        create_result = subprocess.run(create_tag_cmd, capture_output=True, text=True)
-        
-        if create_result.returncode != 0:
-            error_msg = handle_gh_error(create_result.stderr)
-            print(f"Error creating tag: {error_msg}")
-            sys.exit(1)
+        subprocess.run(create_tag_cmd, capture_output=True, text=True, check=True)
 
         print(f"Successfully created and pushed tag '{version_tag}' to {repo}.")
     except subprocess.CalledProcessError as e:
-        error_msg = handle_gh_error(e.stderr.strip() if e.stderr else str(e))
-        print(f"Error while creating/pushing tag: {error_msg}")
-        sys.exit(1)
-    except Exception as e:
-        print(f"Unexpected error: {e}")
+        print(f"Error while creating/pushing tag: {e.stderr.strip() if e.stderr else e}")
         sys.exit(1)
 
 if __name__ == "__main__":

script/release_checklist.py

@@ -231,43 +231,6 @@ def get_next_version(version):
     # Next version is always .0
     return f"v{major}.{minor + 1}.0"
 
-def get_latest_nightly_tag(github_token):
-    """Get the most recent nightly tag from leanprover/lean4-nightly."""
-    api_url = "https://api.github.com/repos/leanprover/lean4-nightly/tags"
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-    response = requests.get(api_url, headers=headers)
-    if response.status_code != 200:
-        return None
-    tags = response.json()
-    if not tags:
-        return None
-    # Return the most recent tag name
-    return tags[0]['name']
-
-def update_lean_toolchain_in_branch(org_repo, branch, toolchain_content, github_token):
-    """Update the lean-toolchain file in a specific branch."""
-    api_url = f"https://api.github.com/repos/{org_repo}/contents/lean-toolchain"
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-    
-    # First get the current file to get its SHA
-    response = requests.get(f"{api_url}?ref={branch}", headers=headers)
-    if response.status_code != 200:
-        return False
-    
-    current_file = response.json()
-    file_sha = current_file['sha']
-    
-    # Update the file
-    update_data = {
-        "message": f"chore: update lean-toolchain to {toolchain_content}",
-        "content": base64.b64encode(toolchain_content.encode('utf-8')).decode('utf-8'),
-        "sha": file_sha,
-        "branch": branch
-    }
-    
-    response = requests.put(api_url, json=update_data, headers=headers)
-    return response.status_code in [200, 201]
-
 def check_bump_branch_toolchain(url, bump_branch, github_token):
     """Check if the lean-toolchain file in bump branch starts with either 'leanprover/lean4:nightly-' or the next version."""
     content = get_branch_content(url, bump_branch, "lean-toolchain", github_token)
@@ -299,61 +262,6 @@ def pr_exists_with_title(repo_url, title, github_token):
             return pr['number'], pr['html_url']
     return None
 
-def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
-    """Check if ProofWidgets4 has a release tag that uses the target toolchain."""
-    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-    
-    # Get all tags matching v0.0.* pattern
-    response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers)
-    if response.status_code != 200:
-        print(f"  ❌ Could not fetch ProofWidgets4 tags")
-        return False
-    
-    tags = response.json()
-    if not tags:
-        print(f"  ❌ No v0.0.* tags found for ProofWidgets4")
-        return False
-    
-    # Extract tag names and sort by version number (descending)
-    tag_names = []
-    for tag in tags:
-        ref = tag['ref']
-        if ref.startswith('refs/tags/v0.0.'):
-            tag_name = ref.replace('refs/tags/', '')
-            try:
-                # Extract the number after v0.0.
-                version_num = int(tag_name.split('.')[-1])
-                tag_names.append((version_num, tag_name))
-            except (ValueError, IndexError):
-                continue
-    
-    if not tag_names:
-        print(f"  ❌ No valid v0.0.* tags found for ProofWidgets4")
-        return False
-    
-    # Sort by version number (descending) and take the most recent 10
-    tag_names.sort(reverse=True)
-    recent_tags = tag_names[:10]
-    
-    # Check each recent tag to see if it uses the target toolchain
-    for version_num, tag_name in recent_tags:
-        toolchain_content = get_branch_content(repo_url, tag_name, "lean-toolchain", github_token)
-        if toolchain_content is None:
-            continue
-        
-        if is_version_gte(toolchain_content.strip(), target_toolchain):
-            print(f"  ✅ Found release {tag_name} using compatible toolchain (>= {target_toolchain})")
-            return True
-    
-    # If we get here, no recent release uses the target toolchain
-    # Find the highest version number to suggest the next one
-    highest_version = max(version_num for version_num, _ in recent_tags)
-    next_version = highest_version + 1
-    print(f"  ❌ No recent ProofWidgets4 release uses toolchain >= {target_toolchain}")
-    print(f"     You will need to create and push a tag v0.0.{next_version}")
-    return False
-
 def main():
     parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
     parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
@@ -478,12 +386,6 @@ def main():
             continue
         print(f"  ✅ On compatible toolchain (>= {toolchain})")
 
-        # Special handling for ProofWidgets4
-        if name == "ProofWidgets4":
-            if not check_proofwidgets4_release(url, toolchain, github_token):
-                repo_status[name] = False
-                continue
-
         if check_tag:
             tag_exists_initially = tag_exists(url, toolchain, github_token)
             if not tag_exists_initially:                
@@ -492,7 +394,7 @@ def main():
                     repo_status[name] = False
                     continue
                 else:
-                    print(f"  ⮕ Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...")
+                    print(f"  … Tag {toolchain} does not exist. Running `script/push_repo_release_tag.py {org_repo} {branch} {toolchain}`...")
                     
                     # Run the script to create the tag
                     subprocess.run(["script/push_repo_release_tag.py", org_repo, branch, toolchain])
@@ -515,7 +417,7 @@ def main():
                     repo_status[name] = False
                     continue
                 else:
-                    print(f"  ⮕ Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...")
+                    print(f"  … Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...")
                     
                     # Run the script to merge the tag
                     subprocess.run(["script/merge_remote.py", org_repo, "stable", toolchain])
@@ -532,49 +434,19 @@ def main():
         if check_bump:
             next_version = get_next_version(toolchain)
             bump_branch = f"bump/{next_version}"
-            
-            # For mathlib4, use the nightly-testing fork for bump branches
-            bump_org_repo = org_repo
-            bump_url = url
-            if name == "mathlib4":
-                bump_org_repo = "leanprover-community/mathlib4-nightly-testing"
-                bump_url = "https://github.com/leanprover-community/mathlib4-nightly-testing"
-            
-            branch_created = False
-            if not branch_exists(bump_url, bump_branch, github_token):
+            if not branch_exists(url, bump_branch, github_token):
                 if args.dry_run:
-                    latest_nightly = get_latest_nightly_tag(github_token)
-                    nightly_note = f" (will set lean-toolchain to {latest_nightly})" if name in ["batteries", "mathlib4"] and latest_nightly else ""
-                    print(f"  ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{bump_org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)` to create it{nightly_note}.")
+                    print(f"  ❌ Bump branch {bump_branch} does not exist. Run `gh api -X POST /repos/{org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)` to create it.")
                     repo_status[name] = False
                     continue
-                print(f"  ⮕ Bump branch {bump_branch} does not exist. Creating it...")
-                result = run_command(f"gh api -X POST /repos/{bump_org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)", check=False)
+                print(f"  … Bump branch {bump_branch} does not exist. Creating it...")
+                result = run_command(f"gh api -X POST /repos/{org_repo}/git/refs -f ref=refs/heads/{bump_branch} -f sha=$(gh api /repos/{org_repo}/git/refs/heads/{branch} --jq .object.sha)", check=False)
                 if result.returncode != 0:
                     print(f"  ❌ Failed to create bump branch {bump_branch}")
                     repo_status[name] = False
                     continue
-                branch_created = True
-            
             print(f"  ✅ Bump branch {bump_branch} exists")
-            
-            # For batteries and mathlib4, update the lean-toolchain to the latest nightly
-            if branch_created and name in ["batteries", "mathlib4"]:
-                latest_nightly = get_latest_nightly_tag(github_token)
-                if latest_nightly:
-                    nightly_toolchain = f"leanprover/lean4:{latest_nightly}"
-                    print(f"  ⮕ Updating lean-toolchain to {nightly_toolchain}...")
-                    if update_lean_toolchain_in_branch(bump_org_repo, bump_branch, nightly_toolchain, github_token):
-                        print(f"  ✅ Updated lean-toolchain to {nightly_toolchain}")
-                    else:
-                        print(f"  ❌ Failed to update lean-toolchain to {nightly_toolchain}")
-                        repo_status[name] = False
-                        continue
-                else:
-                    print(f"  ❌ Could not fetch latest nightly tag")
-                    repo_status[name] = False
-                    continue
-            if not check_bump_branch_toolchain(bump_url, bump_branch, github_token):
+            if not check_bump_branch_toolchain(url, bump_branch, github_token):
                 repo_status[name] = False
                 continue
 

script/release_steps.py

@@ -1,10 +1,10 @@
 #!/usr/bin/env python3
 
 """
-Execute release steps for Lean4 repositories.
+Generate release steps script for Lean4 repositories.
 
 This script helps automate the release process for Lean4 and its dependent repositories
-by actually executing the step-by-step instructions for updating toolchains, creating tags,
+by generating step-by-step instructions for updating toolchains, creating tags,
 and managing branches.
 
 Usage:
@@ -12,11 +12,11 @@ Usage:
 
 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
+    repo: A substring of the repository name as specified in release_repos.yml
 
 Example:
-    python3 release_steps.py v4.6.0 mathlib4
-    python3 release_steps.py v4.6.0 batteries
+    python3 release_steps.py v4.6.0 mathlib
+    python3 release_steps.py v4.6.0 batt
 
 The script reads repository configurations from release_repos.yml in the same directory.
 Each repository may have specific requirements for:
@@ -32,124 +32,23 @@ import yaml
 import os
 import sys
 import re
-import subprocess
-import shutil
-import json
-from pathlib import Path
-
-# Color functions for terminal output
-def blue(text):
-    """Blue text for 'I'm doing something' messages."""
-    return f"\033[94m{text}\033[0m"
-
-def green(text):
-    """Green text for 'successful step' messages."""
-    return f"\033[92m{text}\033[0m"
-
-def red(text):
-    """Red text for 'this looks bad' messages."""
-    return f"\033[91m{text}\033[0m"
-
-def yellow(text):
-    """Yellow text for warnings."""
-    return f"\033[93m{text}\033[0m"
-
-def run_command(cmd, cwd=None, check=True, stream_output=False):
-    """Run a shell command and return the result."""
-    print(blue(f"Running: {cmd}"))
-    try:
-        if stream_output:
-            # Stream output in real-time for long-running commands
-            result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, text=True)
-            return result
-        else:
-            # Capture output for commands where we need to process the result
-            result = subprocess.run(cmd, shell=True, cwd=cwd, check=check, 
-                                  capture_output=True, text=True)
-            if result.stdout:
-                # Command output in plain white (default terminal color)
-                print(result.stdout)
-            return result
-    except subprocess.CalledProcessError as e:
-        print(red(f"Error running command: {cmd}"))
-        print(red(f"Exit code: {e.returncode}"))
-        if not stream_output:
-            print(f"Stdout: {e.stdout}")
-            print(f"Stderr: {e.stderr}")
-        raise
 
 def load_repos_config(file_path):
     with open(file_path, "r") as f:
         return yaml.safe_load(f)["repositories"]
 
-def find_repo(repo_name, config):
-    matching_repos = [r for r in config if r["name"] == repo_name]
+def find_repo(repo_substring, config):
+    pattern = re.compile(re.escape(repo_substring), re.IGNORECASE)
+    matching_repos = [r for r in config if pattern.search(r["name"])]
     if not matching_repos:
-        print(red(f"Error: No repository named '{repo_name}' found in configuration."))
-        available_repos = [r["name"] for r in config]
-        print(yellow(f"Available repositories: {', '.join(available_repos)}"))
+        print(f"Error: No repository matching '{repo_substring}' found in configuration.")
+        sys.exit(1)
+    if len(matching_repos) > 1:
+        print(f"Error: Multiple repositories matching '{repo_substring}' found in configuration: {', '.join(r['name'] for r in matching_repos)}")
         sys.exit(1)
     return matching_repos[0]
 
-def setup_downstream_releases_dir():
-    """Create the downstream_releases directory if it doesn't exist."""
-    downstream_dir = Path("downstream_releases")
-    if not downstream_dir.exists():
-        print(blue(f"Creating {downstream_dir} directory..."))
-        downstream_dir.mkdir()
-        print(green(f"Created {downstream_dir} directory"))
-    return downstream_dir
-
-def clone_or_update_repo(repo_url, repo_dir, downstream_dir):
-    """Clone the repository if it doesn't exist, or update it if it does."""
-    repo_path = downstream_dir / repo_dir
-    
-    if repo_path.exists():
-        print(blue(f"Repository {repo_dir} already exists, updating..."))
-        run_command("git fetch", cwd=repo_path)
-        print(green(f"Updated repository {repo_dir}"))
-    else:
-        print(blue(f"Cloning {repo_url} to {repo_path}..."))
-        run_command(f"git clone {repo_url}", cwd=downstream_dir)
-        print(green(f"Cloned repository {repo_dir}"))
-    
-    return repo_path
-
-def get_remotes_for_repo(repo_name):
-    """Get the appropriate remotes for bump and nightly-testing branches based on repository."""
-    if repo_name == "mathlib4":
-        return "nightly-testing", "nightly-testing"
-    else:
-        return "origin", "origin"
-
-def check_and_abort_merge(repo_path):
-    """Check if repository is in the middle of a merge and abort it if so."""
-    merge_head_file = repo_path / ".git" / "MERGE_HEAD"
-    
-    if merge_head_file.exists():
-        print(yellow(f"Repository {repo_path.name} is in the middle of a merge. Aborting merge..."))
-        run_command("git merge --abort", cwd=repo_path)
-        print(green("Merge aborted successfully"))
-        return True
-    
-    # Also check git status for other merge-related states
-    try:
-        result = run_command("git status --porcelain=v1", cwd=repo_path, check=False)
-        if result.returncode == 0:
-            # Check for unmerged paths (indicated by 'UU', 'AA', etc. in git status)
-            for line in result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    print(yellow(f"Repository {repo_path.name} has unmerged paths. Aborting merge..."))
-                    run_command("git merge --abort", cwd=repo_path)
-                    print(green("Merge aborted successfully"))
-                    return True
-    except subprocess.CalledProcessError:
-        # If git status fails, we'll let the main process handle it
-        pass
-    
-    return False
-
-def execute_release_steps(repo, version, config):
+def generate_script(repo, version, config):
     repo_config = find_repo(repo, config)
     repo_name = repo_config['name']
     repo_url = repo_config['url']
@@ -160,481 +59,92 @@ def execute_release_steps(repo, version, config):
     requires_tagging = repo_config.get("toolchain-tag", True)
     has_stable_branch = repo_config.get("stable-branch", True)
 
-    # Setup downstream releases directory
-    downstream_dir = setup_downstream_releases_dir()
-    
-    # Clone or update the repository
-    repo_path = clone_or_update_repo(repo_url, repo_dir, downstream_dir)
-    
-    # Special remote setup for mathlib4
-    if repo_name == "mathlib4":
-        print(blue("Setting up special remotes for mathlib4..."))
-        try:
-            # Check if nightly-testing remote already exists
-            result = run_command("git remote get-url nightly-testing", cwd=repo_path, check=False)
-            if result.returncode != 0:
-                # Add the nightly-testing remote
-                run_command("git remote add nightly-testing https://github.com/leanprover-community/mathlib4-nightly-testing.git", cwd=repo_path)
-                print(green("Added nightly-testing remote"))
-            else:
-                print(green("nightly-testing remote already exists"))
-            
-            # Fetch from the nightly-testing remote
-            run_command("git fetch nightly-testing", cwd=repo_path)
-            print(green("Fetched from nightly-testing remote"))
-        except subprocess.CalledProcessError as e:
-            print(red(f"Error setting up mathlib4 remotes: {e}"))
-            print(yellow("Continuing with default remote setup..."))
-    
-    print(blue(f"\n=== Executing release steps for {repo_name} ==="))
-    
-    # Check if repository is in the middle of a merge and abort it if necessary
-    check_and_abort_merge(repo_path)
-    
-    # Execute the release steps
-    run_command(f"git checkout {default_branch} && git pull", cwd=repo_path)
-    
-    # Special rc1 safety check for batteries and mathlib4 (before creating any branches)
-    if re.search(r'rc\d+$', version) and repo_name in ["batteries", "mathlib4"] and version.endswith('-rc1'):
-        print(blue("This repo has nightly-testing infrastructure"))
-        print(blue(f"Checking if nightly-testing can be safely merged into bump/{version.split('-rc')[0]}..."))
-        
-        # Get the base version (e.g., v4.6.0 from v4.6.0-rc1)
-        base_version = version.split('-rc')[0]
-        bump_branch = f"bump/{base_version}"
-        
-        # Determine which remote to use for bump and nightly-testing branches
-        bump_remote, nightly_remote = get_remotes_for_repo(repo_name)
-        
-        try:
-            # Fetch latest changes from the appropriate remote
-            run_command(f"git fetch {bump_remote}", cwd=repo_path)
-            
-            # Check if the bump branch exists
-            result = run_command(f"git show-ref --verify --quiet refs/remotes/{bump_remote}/{bump_branch}", cwd=repo_path, check=False)
-            if result.returncode != 0:
-                print(red(f"Bump branch {bump_remote}/{bump_branch} does not exist. Cannot perform safety check."))
-                print(yellow("Please ensure the bump branch exists before proceeding."))
-                return
-            
-            # Create a temporary branch for testing the merge
-            temp_branch = f"temp-merge-test-{base_version}"
-            
-            # Clean up any existing temp branch from previous runs
-            result = run_command(f"git show-ref --verify --quiet refs/heads/{temp_branch}", cwd=repo_path, check=False)
-            if result.returncode == 0:
-                print(blue(f"Cleaning up existing temp branch {temp_branch}..."))
-                # Make sure we're not on the temp branch before deleting it
-                run_command(f"git checkout {default_branch}", cwd=repo_path)
-                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
-                print(green(f"Deleted existing temp branch {temp_branch}"))
-            
-            run_command(f"git checkout -b {temp_branch} {bump_remote}/{bump_branch}", cwd=repo_path)
-            
-            # Try to merge nightly-testing
-            try:
-                run_command(f"git merge {nightly_remote}/nightly-testing", cwd=repo_path)
-                
-                # Check what files have changed compared to the bump branch
-                changed_files = run_command(f"git diff --name-only {bump_remote}/{bump_branch}..HEAD", cwd=repo_path)
-                
-                # Filter out allowed changes
-                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-                problematic_files = []
-                
-                for file in changed_files.stdout.strip().split('\n'):
-                    if file.strip():  # Skip empty lines
-                        is_allowed = any(pattern in file for pattern in allowed_patterns)
-                        if not is_allowed:
-                            problematic_files.append(file)
-                
-                # Clean up temporary branch and return to default branch
-                run_command(f"git checkout {default_branch}", cwd=repo_path)
-                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
-                
-                if problematic_files:
-                    print(red("❌ Safety check failed!"))
-                    print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:"))
-                    for file in problematic_files:
-                        print(red(f"  - {file}"))
-                    print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first."))
-                    print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes."))
-                    return
-                else:
-                    print(green("✅ Safety check passed - only lean-toolchain and/or lake-manifest.json would change"))
-                    
-            except subprocess.CalledProcessError:
-                # Merge failed due to conflicts - check which files are conflicted
-                print(blue("Merge failed, checking which files are affected..."))
-                
-                # Get all changed files using git status
-                status_result = run_command("git status --porcelain", cwd=repo_path)
-                changed_files = []
-                
-                for line in status_result.stdout.splitlines():
-                    if line.strip():  # Skip empty lines
-                        # Extract filename (skip the first 3 characters which are status codes)
-                        changed_files.append(line[3:])
-                
-                # Filter out allowed files
-                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-                problematic_files = []
-                
-                for file in changed_files:
-                    is_allowed = any(pattern in file for pattern in allowed_patterns)
-                    if not is_allowed:
-                        problematic_files.append(file)
-                
-                if problematic_files:
-                    # There are changes in non-allowed files - fail the safety check
-                    # First abort the merge to clean up the conflicted state
-                    run_command("git merge --abort", cwd=repo_path)
-                    run_command(f"git checkout {default_branch}", cwd=repo_path)
-                    run_command(f"git branch -D {temp_branch}", cwd=repo_path)
-                    print(red("❌ Safety check failed!"))
-                    print(red(f"Merging nightly-testing into {bump_branch} would result in changes to:"))
-                    for file in problematic_files:
-                        print(red(f"  - {file}"))
-                    print(yellow("\nYou need to make a PR merging the changes from nightly-testing into the bump branch first."))
-                    print(yellow(f"Create a PR from nightly-testing targeting {bump_branch} to resolve these changes."))
-                    return
-                else:
-                    # Only allowed files are changed - resolve them and continue
-                    print(green(f"✅ Only allowed files changed: {', '.join(changed_files)}"))
-                    print(blue("Resolving conflicts by taking nightly-testing version..."))
-                    
-                    # For each changed allowed file, take the nightly-testing version
-                    for file in changed_files:
-                        run_command(f"git checkout --theirs {file}", cwd=repo_path)
-                    
-                    # Complete the merge
-                    run_command("git add .", cwd=repo_path)
-                    run_command("git commit --no-edit", cwd=repo_path)
-                    
-                    print(green("✅ Safety check passed - changes only in allowed files"))
-                
-                # Clean up temporary branch and return to default branch
-                run_command(f"git checkout {default_branch}", cwd=repo_path)
-                run_command(f"git branch -D {temp_branch}", cwd=repo_path)
-                
-        except subprocess.CalledProcessError as e:
-            # Ensure we're back on the default branch even if setup failed
-            try:
-                run_command(f"git checkout {default_branch}", cwd=repo_path)
-            except subprocess.CalledProcessError:
-                print(red(f"Cannot return to {default_branch} branch. Repository is in an inconsistent state."))
-                print(red("Please manually check the repository state and fix any issues."))
-                return
-            print(red(f"Error during safety check: {e}"))
-            print(yellow("Skipping safety check and proceeding with normal merge..."))
-    
-    # Check if the branch already exists
-    branch_name = f"bump_to_{version}"
-    try:
-        # Check if branch exists locally
-        result = run_command(f"git show-ref --verify --quiet refs/heads/{branch_name}", cwd=repo_path, check=False)
-        if result.returncode == 0:
-            print(blue(f"Branch {branch_name} already exists, checking it out..."))
-            run_command(f"git checkout {branch_name}", cwd=repo_path)
-            print(green(f"Checked out existing branch {branch_name}"))
-        else:
-            print(blue(f"Creating new branch {branch_name}..."))
-            run_command(f"git checkout -b {branch_name}", cwd=repo_path)
-            print(green(f"Created new branch {branch_name}"))
-    except subprocess.CalledProcessError:
-        print(blue(f"Creating new branch {branch_name}..."))
-        run_command(f"git checkout -b {branch_name}", cwd=repo_path)
-        print(green(f"Created new branch {branch_name}"))
-    
-    # Update lean-toolchain
-    print(blue("Updating lean-toolchain file..."))
-    toolchain_file = repo_path / "lean-toolchain"
-    with open(toolchain_file, "w") as f:
-        f.write(f"leanprover/lean4:{version}\n")
-    print(green(f"Updated lean-toolchain to leanprover/lean4:{version}"))
+    script_lines = [
+        f"cd {repo_dir}",
+        "git fetch",
+        f"git checkout {default_branch} && git pull",
+        f"git checkout -b bump_to_{version}",
+        f"echo leanprover/lean4:{version} > lean-toolchain",
+    ]
 
     # Special cases for specific repositories
     if repo_name == "repl":
-        run_command("lake update", cwd=repo_path, stream_output=True)
-        mathlib_test_dir = repo_path / "test" / "Mathlib"
-        run_command(f'perl -pi -e \'s/rev = "v\\d+\\.\\d+\\.\\d+(-rc\\d+)?"/rev = "{version}"/g\' lakefile.toml', cwd=mathlib_test_dir)
-        
-        # Update lean-toolchain in test/Mathlib
-        print(blue("Updating test/Mathlib/lean-toolchain..."))
-        mathlib_toolchain = mathlib_test_dir / "lean-toolchain"
-        with open(mathlib_toolchain, "w") as f:
-            f.write(f"leanprover/lean4:{version}\n")
-        print(green(f"Updated test/Mathlib/lean-toolchain to leanprover/lean4:{version}"))
-        
-        run_command("lake update", cwd=mathlib_test_dir, stream_output=True)
-        try:
-            result = run_command("./test.sh", cwd=repo_path, stream_output=True, check=False)
-            if result.returncode == 0:
-                print(green("Tests completed successfully"))
-            else:
-                print(red("Tests failed, but continuing with PR creation..."))
-                print(red(f"Test exit code: {result.returncode}"))
-        except subprocess.CalledProcessError as e:
-            print(red("Tests failed, but continuing with PR creation..."))
-            print(red(f"Test error: {e}"))
+        script_lines.extend([
+            "lake update",
+            "cd test/Mathlib",
+            f"perl -pi -e 's/rev = \"v\\d+\\.\\d+\\.\\d+(-rc\\d+)?\"/rev = \"{version}\"/g' lakefile.toml",
+            f"echo leanprover/lean4:{version} > lean-toolchain",
+            "lake update",
+            "cd ../..",
+            "./test.sh"
+        ])
     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)
+        script_lines.append('perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*')
+        script_lines.append("lake update")
 
-    # Commit changes (only if there are changes)
-    print(blue("Checking for changes to commit..."))
-    try:
-        # Check if there are any changes to commit (staged or unstaged)
-        result = run_command("git status --porcelain", cwd=repo_path, check=False)
-        if result.stdout.strip():  # There are changes
-            print(blue("Committing changes..."))
-            run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path)
-            print(green(f"Committed changes: chore: bump toolchain to {version}"))
-        else:
-            print(green("No changes to commit - toolchain already up to date"))
-    except subprocess.CalledProcessError:
-        print(yellow("Failed to check for changes, attempting commit anyway..."))
-        try:
-            run_command(f'git commit -am "chore: bump toolchain to {version}"', cwd=repo_path)
-        except subprocess.CalledProcessError as e:
-            if "nothing to commit" in e.stderr:
-                print(green("No changes to commit - toolchain already up to date"))
-            else:
-                raise
+    script_lines.append("")
+
+    script_lines.extend([
+        f'git commit -am "chore: bump toolchain to {version}"',
+        ""
+    ])
 
-    # Handle special merging cases
     if re.search(r'rc\d+$', version) and repo_name in ["batteries", "mathlib4"]:
-        print(blue("This repo uses `bump/v4.X.0` branches for reviewed content from nightly-testing."))
-        
-        # Determine which remote to use for bump branches
-        bump_remote, nightly_remote = get_remotes_for_repo(repo_name)
-        
-        # Fetch latest changes to ensure we have the most up-to-date bump branch
-        print(blue(f"Fetching latest changes from {bump_remote}..."))
-        run_command(f"git fetch {bump_remote}", cwd=repo_path)
-        
-        try:
-            print(blue(f"Merging {bump_remote}/bump/{version.split('-rc')[0]}..."))
-            run_command(f"git merge {bump_remote}/bump/{version.split('-rc')[0]}", cwd=repo_path)
-            print(green("Merge completed successfully"))
-        except subprocess.CalledProcessError:
-            # Merge failed due to conflicts - check which files are conflicted
-            print(blue("Merge conflicts detected, checking which files are affected..."))
-            
-            # Get conflicted files using git status
-            status_result = run_command("git status --porcelain", cwd=repo_path)
-            conflicted_files = []
-            
-            for line in status_result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    # Extract filename (skip the first 3 characters which are status codes)
-                    conflicted_files.append(line[3:])
-            
-            # Filter out allowed files
-            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-            problematic_files = []
-            
-            for file in conflicted_files:
-                is_allowed = any(pattern in file for pattern in allowed_patterns)
-                if not is_allowed:
-                    problematic_files.append(file)
-            
-            if problematic_files:
-                # There are conflicts in non-allowed files - fail
-                print(red("❌ Merge failed!"))
-                print(red(f"Merging {bump_remote}/bump/{version.split('-rc')[0]} resulted in conflicts in:"))
-                for file in problematic_files:
-                    print(red(f"  - {file}"))
-                print(red("Please resolve these conflicts manually."))
-                return
-            else:
-                # Only allowed files are conflicted - resolve them automatically
-                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                print(blue("Resolving conflicts automatically..."))
-                
-                # Overwrite lean-toolchain with our target version
-                if 'lean-toolchain' in conflicted_files:
-                    print(blue(f"Overwriting lean-toolchain with target version {version}"))
-                    toolchain_file = repo_path / "lean-toolchain"
-                    with open(toolchain_file, "w") as f:
-                        f.write(f"leanprover/lean4:{version}\n")
-                
-                # For other allowed files, take our version (since we want our changes)
-                for file in conflicted_files:
-                    if file != 'lean-toolchain':
-                        run_command(f"git checkout --ours {file}", cwd=repo_path)
-                
-                # Run lake update to rebuild lake-manifest.json
-                print(blue("Running lake update to rebuild lake-manifest.json..."))
-                run_command("lake update", cwd=repo_path, stream_output=True)
-                
-                # Complete the merge
-                run_command("git add .", cwd=repo_path)
-                run_command("git commit --no-edit", cwd=repo_path)
-                
-                print(green("✅ Merge completed successfully with automatic conflict resolution"))
-    
-    elif re.search(r'rc\d+$', version):
-        # For all other repos with rc versions, merge nightly-testing
-        if repo_name in ["verso", "reference-manual"]:
-            print(yellow("This repo does development on nightly-testing: remember to rebase merge the PR."))
-        
-        # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
-        print(blue("Fetching latest changes from origin..."))
-        run_command("git fetch origin", cwd=repo_path)
-        
-        try:
-            print(blue("Merging origin/nightly-testing..."))
-            run_command("git merge origin/nightly-testing", cwd=repo_path)
-            print(green("Merge completed successfully"))
-        except subprocess.CalledProcessError:
-            # Merge failed due to conflicts - check which files are conflicted
-            print(blue("Merge conflicts detected, checking which files are affected..."))
-            
-            # Get conflicted files using git status
-            status_result = run_command("git status --porcelain", cwd=repo_path)
-            conflicted_files = []
-            
-            for line in status_result.stdout.splitlines():
-                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                    # Extract filename (skip the first 3 characters which are status codes)
-                    conflicted_files.append(line[3:])
-            
-            # Filter out allowed files
-            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-            problematic_files = []
-            
-            for file in conflicted_files:
-                is_allowed = any(pattern in file for pattern in allowed_patterns)
-                if not is_allowed:
-                    problematic_files.append(file)
-            
-            if problematic_files:
-                # There are conflicts in non-allowed files - fail
-                print(red("❌ Merge failed!"))
-                print(red(f"Merging nightly-testing resulted in conflicts in:"))
-                for file in problematic_files:
-                    print(red(f"  - {file}"))
-                print(red("Please resolve these conflicts manually."))
-                return
-            else:
-                # Only allowed files are conflicted - resolve them automatically
-                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                print(blue("Resolving conflicts automatically..."))
-                
-                # For lean-toolchain and lake-manifest.json, keep our versions
-                for file in conflicted_files:
-                    print(blue(f"Keeping our version of {file}"))
-                    run_command(f"git checkout --ours {file}", cwd=repo_path)
-                
-                # Complete the merge
-                run_command("git add .", cwd=repo_path)
-                run_command("git commit --no-edit", cwd=repo_path)
-                
-                print(green("✅ Merge completed successfully with automatic conflict resolution"))
+        script_lines.extend([
+            "echo 'This repo has nightly-testing infrastructure'",
+            f"git merge origin/bump/{version.split('-rc')[0]}",
+            "echo 'Please resolve any conflicts.'",
+            "grep nightly-testing lakefile.* && echo 'Please ensure the lakefile does not include nightly-testing versions.'",
+            ""
+        ])
+    if re.search(r'rc\d+$', version) and repo_name in ["verso", "reference-manual"]:
+        script_lines.extend([
+            "echo 'This repo does development on nightly-testing: remember to rebase merge the PR.'",
+            f"git merge origin/nightly-testing",
+            "echo 'Please resolve any conflicts.'",
+            ""
+        ])
+    if repo_name != "Mathlib":
+        script_lines.extend([
+            "lake build && if lake check-test; then lake test; fi",
+            ""
+        ])
 
-    # Build and test (skip for Mathlib)
-    if repo_name not in ["mathlib4"]:
-        print(blue("Building project..."))
-        
-        # Clean lake cache for a fresh build
-        print(blue("Cleaning lake cache..."))
-        run_command("rm -rf .lake", cwd=repo_path)
-        
-        try:
-            run_command("lake build", cwd=repo_path, stream_output=True)
-            print(green("Build completed successfully"))
-        except subprocess.CalledProcessError as e:
-            print(red("Build failed, but continuing with PR creation..."))
-            print(red(f"Build error: {e}"))
-        
-        # Check if lake check-test exists before running tests
-        print(blue("Running tests..."))
-        check_test_result = run_command("lake check-test", cwd=repo_path, check=False)
-        if check_test_result.returncode == 0:
-            try:
-                run_command("lake test", cwd=repo_path, stream_output=True)
-                print(green("Tests completed successfully"))
-            except subprocess.CalledProcessError as e:
-                print(red("Tests failed, but continuing with PR creation..."))
-                print(red(f"Test error: {e}"))
-        else:
-            print(yellow("lake check-test reports that there is no test suite"))
+    script_lines.extend([
+        'gh pr create --title "chore: bump toolchain to ' + version + '" --body ""',
+        "echo 'Please review the PR and merge or rebase it.'",
+        ""
+    ])
 
-    # Push the branch to remote before creating PR
-    print(blue("Checking remote branch status..."))
-    try:
-        # Check if branch exists on remote
-        result = run_command(f"git ls-remote --heads origin {branch_name}", cwd=repo_path, check=False)
-        if not result.stdout.strip():
-            print(blue(f"Pushing branch {branch_name} to remote..."))
-            run_command(f"git push -u origin {branch_name}", cwd=repo_path)
-            print(green(f"Successfully pushed branch {branch_name} to remote"))
-        else:
-            print(blue(f"Branch {branch_name} already exists on remote, pushing any new commits..."))
-            run_command(f"git push", cwd=repo_path)
-            print(green("Successfully pushed commits to remote"))
-    except subprocess.CalledProcessError:
-        print(red("Failed to push branch to remote. Please check your permissions and network connection."))
-        print(yellow(f"You may need to run: git push -u origin {branch_name}"))
-        return
-
-    # Create pull request (only if one doesn't already exist)
-    print(blue("Checking for existing pull request..."))
-    try:
-        # Check if PR already exists for this branch
-        result = run_command(f'gh pr list --head {branch_name} --json number', cwd=repo_path, check=False)
-        if result.returncode == 0 and result.stdout.strip() != "[]":
-            print(green(f"Pull request already exists for branch {branch_name}"))
-            # Get the PR URL
-            pr_result = run_command(f'gh pr view {branch_name} --json url', cwd=repo_path, check=False)
-            if pr_result.returncode == 0:
-                pr_data = json.loads(pr_result.stdout)
-                print(green(f"PR URL: {pr_data.get('url', 'N/A')}"))
-        else:
-            # Create new PR
-            print(blue("Creating new pull request..."))
-            run_command(f'gh pr create --title "chore: bump toolchain to {version}" --body ""', cwd=repo_path)
-            print(green("Pull request created successfully!"))
-    except subprocess.CalledProcessError:
-        print(red("Failed to check for existing PR or create new PR."))
-        print(yellow("This could be due to:"))
-        print(yellow("1. GitHub CLI not authenticated"))
-        print(yellow("2. No push permissions to the repository"))
-        print(yellow("3. Network issues"))
-        print(f"Branch: {branch_name}")
-        print(f"Title: chore: bump toolchain to {version}")
-        print(yellow("Please create the PR manually if needed."))
+    return "\n".join(script_lines)
 
 def main():
     parser = argparse.ArgumentParser(
-        description="Execute release steps for Lean4 repositories.",
+        description="Generate release steps script for Lean4 repositories.",
         formatter_class=argparse.RawDescriptionHelpFormatter,
         epilog="""
 Examples:
-  %(prog)s v4.6.0 mathlib4   Execute steps for updating Mathlib to v4.6.0
-  %(prog)s v4.6.0 batteries  Execute steps for updating Batteries to v4.6.0
+  %(prog)s v4.6.0 mathlib    Generate steps for updating Mathlib to v4.6.0
+  %(prog)s v4.6.0 batt       Generate steps for updating Batteries to v4.6.0
   
-The script will:
-1. Create a downstream_releases/ directory
-2. Clone or update the target repository
-3. Update the lean-toolchain file
-4. Create appropriate branches and commits
-5. Build and test the project
-6. Create pull requests
+The script will generate shell commands to:
+1. Update the lean-toolchain file
+2. Create appropriate branches and commits
+3. Create pull requests
 
 (Note that the steps of creating toolchain version tags, and merging these into `stable` branches,
 are handled by `script/release_checklist.py`.)
 """
     )
     parser.add_argument("version", help="The version to set in the lean-toolchain file (e.g., v4.6.0)")
-    parser.add_argument("repo", help="The repository name as specified in release_repos.yml")
+    parser.add_argument("repo", help="A substring of the repository name as specified in release_repos.yml")
     args = parser.parse_args()
 
     config_path = os.path.join(os.path.dirname(__file__), "release_repos.yml")
     config = load_repos_config(config_path)
 
-    execute_release_steps(args.repo, args.version, config)
+    script = generate_script(args.repo, args.version, config)
+    print(script)
 
 if __name__ == "__main__":
     main()

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 23)
+set(LEAN_VERSION_MINOR 22)
 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'")
@@ -58,6 +58,9 @@ option(USE_GITHASH        "GIT_HASH"           ON)
 option(INSTALL_LICENSE "INSTALL_LICENSE" ON)
 # When ON we install a copy of cadical
 option(INSTALL_CADICAL "Install a copy of cadical" ON)
+# When ON thread storage is automatically finalized, it assumes platform support pthreads.
+# This option is important when using Lean as library that is invoked from a different programming language (e.g., Haskell).
+option(AUTO_THREAD_FINALIZATION "AUTO_THREAD_FINALIZATION" ON)
 
 # FLAGS for disabling optimizations and debugging
 option(FREE_VAR_RANGE_OPT  "FREE_VAR_RANGE_OPT"   ON)
@@ -179,6 +182,10 @@ else()
   string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_MULTI_THREAD")
 endif()
 
+if(AUTO_THREAD_FINALIZATION AND NOT MSVC)
+  string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_AUTO_THREAD_FINALIZATION")
+endif()
+
 # Set Module Path
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 

src/Init.lean

@@ -6,41 +6,41 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Prelude
-public import Init.Notation
-public import Init.Tactics
-public import Init.TacticsExtra
-public import Init.ByCases
-public import Init.RCases
-public import Init.Core
-public import Init.Control
-public import Init.Data.Basic
-public import Init.WF
-public import Init.WFTactics
-public import Init.Data
-public import Init.System
-public import Init.Util
-public import Init.Dynamic
-public import Init.ShareCommon
-public import Init.MetaTypes
-public import Init.Meta
-public import Init.NotationExtra
-public import Init.SimpLemmas
-public import Init.PropLemmas
-public import Init.Hints
-public import Init.Conv
-public import Init.Guard
-public import Init.Simproc
-public import Init.SizeOfLemmas
-public import Init.BinderPredicates
-public import Init.Ext
-public import Init.Omega
-public import Init.MacroTrace
-public import Init.Grind
-public import Init.GrindInstances
-public import Init.While
-public import Init.Syntax
-public import Init.Internal
-public import Init.Try
-public import Init.BinderNameHint
-public import Init.Task
+import Init.Prelude
+import Init.Notation
+import Init.Tactics
+import Init.TacticsExtra
+import Init.ByCases
+import Init.RCases
+import Init.Core
+import Init.Control
+import Init.Data.Basic
+import Init.WF
+import Init.WFTactics
+import Init.Data
+import Init.System
+import Init.Util
+import Init.Dynamic
+import Init.ShareCommon
+import Init.MetaTypes
+import Init.Meta
+import Init.NotationExtra
+import Init.SimpLemmas
+import Init.PropLemmas
+import Init.Hints
+import Init.Conv
+import Init.Guard
+import Init.Simproc
+import Init.SizeOfLemmas
+import Init.BinderPredicates
+import Init.Ext
+import Init.Omega
+import Init.MacroTrace
+import Init.Grind
+import Init.GrindInstances
+import Init.While
+import Init.Syntax
+import Init.Internal
+import Init.Try
+import Init.BinderNameHint
+import Init.Task

src/Init/BinderNameHint.lean

@@ -7,10 +7,8 @@ Authors: Joachim Breitner
 module
 
 prelude
-public import Init.Prelude
-public import Init.Tactics
-
-public section
+import Init.Prelude
+import Init.Tactics
 
 set_option linter.unusedVariables false in
 /--

src/Init/BinderPredicates.lean

@@ -6,9 +6,7 @@ Authors: Gabriel Ebner
 module
 
 prelude
-public import Init.NotationExtra
-
-public section
+import Init.NotationExtra
 
 namespace Lean
 

src/Init/ByCases.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Classical
-
-public section
+import Init.Classical
 
 /-! # by_cases tactic and if-then-else support -/
 

src/Init/Classical.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.PropLemmas
-
-public section
+import Init.PropLemmas
 
 universe u v
 
@@ -47,7 +45,7 @@ theorem em (p : Prop) : p ∨ ¬p :=
     | Or.inr h, _ => Or.inr h
     | _, Or.inr h => Or.inr h
     | Or.inl hut, Or.inl hvf =>
-      have hne : u ≠ v := by simp [hvf, hut]
+      have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
       Or.inl hne
   have p_implies_uv : p → u = v :=
     fun hp =>

src/Init/Coe.lean

@@ -6,10 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Prelude
-public meta import Init.Prelude
-
-public section
+import Init.Prelude
+meta import Init.Prelude
 set_option linter.missingDocs true -- keep it documented
 
 /-!

src/Init/Control.lean

@@ -6,15 +6,13 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.Basic
-public import Init.Control.State
-public import Init.Control.StateRef
-public import Init.Control.Id
-public import Init.Control.Except
-public import Init.Control.Reader
-public import Init.Control.Option
-public import Init.Control.Lawful
-public import Init.Control.StateCps
-public import Init.Control.ExceptCps
-
-public section
+import Init.Control.Basic
+import Init.Control.State
+import Init.Control.StateRef
+import Init.Control.Id
+import Init.Control.Except
+import Init.Control.Reader
+import Init.Control.Option
+import Init.Control.Lawful
+import Init.Control.StateCps
+import Init.Control.ExceptCps

src/Init/Control/Basic.lean

@@ -6,10 +6,8 @@ Author: Leonardo de Moura, Sebastian Ullrich
 module
 
 prelude
-public import Init.Core
-public import Init.BinderNameHint
-
-public section
+import Init.Core
+import Init.BinderNameHint
 
 universe u v w
 

src/Init/Control/EState.lean

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.State
-public import Init.Control.Except
-public import Init.Data.ToString.Basic
-
-public section
+import Init.Control.State
+import Init.Control.Except
+import Init.Data.ToString.Basic
 universe u v
 
 namespace EStateM

src/Init/Control/Except.lean

@@ -8,11 +8,9 @@ The Except monad transformer.
 module
 
 prelude
-public import Init.Control.Basic
-public import Init.Control.Id
-public import Init.Coe
-
-public section
+import Init.Control.Basic
+import Init.Control.Id
+import Init.Coe
 
 namespace Except
 variable {ε : Type u}

src/Init/Control/ExceptCps.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-
-public section
+import Init.Control.Lawful.Basic
 
 /-!
 The Exception monad transformer using CPS style.

src/Init/Control/Id.lean

@@ -8,9 +8,7 @@ The identity Monad.
 module
 
 prelude
-public import Init.Core
-
-public section
+import Init.Core
 
 universe u
 
@@ -64,7 +62,4 @@ protected def run (x : Id α) : α := x
 instance [OfNat α n] : OfNat (Id α) n :=
   inferInstanceAs (OfNat α n)
 
-instance {m : Type u → Type v} [Pure m] : MonadLiftT Id m where
-  monadLift x := pure x.run
-
 end Id

src/Init/Control/Lawful.lean

@@ -6,9 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-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
+import Init.Control.Lawful.Basic
+import Init.Control.Lawful.Instances
+import Init.Control.Lawful.Lemmas
+import Init.Control.Lawful.MonadLift

src/Init/Control/Lawful/Basic.lean

@@ -6,11 +6,9 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Ext
-public import Init.SimpLemmas
-public import Init.Meta
-
-public section
+import Init.Ext
+import Init.SimpLemmas
+import Init.Meta
 
 open Function
 
@@ -52,7 +50,7 @@ attribute [simp] id_map
   (comp_map _ _ _).symm
 
 theorem Functor.map_unit [Functor f] [LawfulFunctor f] {a : f PUnit} : (fun _ => PUnit.unit) <$> a = a := by
-  simp
+  simp [map]
 
 /--
 An applicative functor satisfies the laws of an applicative functor.

src/Init/Control/Lawful/Instances.lean

@@ -6,13 +6,11 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-public import all Init.Control.Except
-public import all Init.Control.State
-public import Init.Control.StateRef
-public import Init.Ext
-
-public section
+import Init.Control.Lawful.Basic
+import all Init.Control.Except
+import all Init.Control.State
+import Init.Control.StateRef
+import Init.Ext
 
 open Function
 
@@ -69,7 +67,7 @@ protected theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad
   | Except.error _ => simp
   | Except.ok _ =>
     simp [←bind_pure_comp]; apply bind_congr; intro b;
-    cases b <;> simp [Except.map, const]
+    cases b <;> simp [comp, Except.map, const]
 
 protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x *> y = const α id <$> x <*> y := by
   change (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y

src/Init/Control/Lawful/Lemmas.lean

@@ -6,11 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-public import Init.RCases
-public import Init.ByCases
-
-public section
+import Init.Control.Lawful.Basic
+import Init.RCases
+import Init.ByCases
 
 -- Mapping by a function with a left inverse is injective.
 theorem map_inj_of_left_inverse [Functor m] [LawfulFunctor m] {f : α → β}

src/Init/Control/Lawful/MonadLift.lean

@@ -6,8 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Control.Lawful.MonadLift.Basic
-public import Init.Control.Lawful.MonadLift.Lemmas
-public import Init.Control.Lawful.MonadLift.Instances
-
-public section
+import Init.Control.Lawful.MonadLift.Basic
+import Init.Control.Lawful.MonadLift.Lemmas
+import Init.Control.Lawful.MonadLift.Instances

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

@@ -6,9 +6,7 @@ Authors: Quang Dao
 module
 
 prelude
-public import Init.Control.Basic
-
-public section
+import Init.Control.Basic
 
 /-!
 # LawfulMonadLift and LawfulMonadLiftT

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

@@ -6,16 +6,13 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
-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
-
-public section
+import all Init.Control.Option
+import all Init.Control.Except
+import all Init.Control.ExceptCps
+import all Init.Control.StateRef
+import all Init.Control.StateCps
+import Init.Control.Lawful.MonadLift.Lemmas
+import Init.Control.Lawful.Instances
 
 universe u v w x
 
@@ -138,11 +135,3 @@ instance {ε : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT
     simp only [bind_assoc]
 
 end ExceptCpsT
-
-namespace Id
-
-instance [Monad m] [LawfulMonad m] : LawfulMonadLiftT Id m where
-  monadLift_pure a := by simp [monadLift]
-  monadLift_bind a f := by simp [monadLift]
-
-end Id

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

@@ -6,10 +6,8 @@ Authors: Quang Dao
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-public import Init.Control.Lawful.MonadLift.Basic
-
-public section
+import Init.Control.Lawful.Basic
+import Init.Control.Lawful.MonadLift.Basic
 
 universe u v w
 

src/Init/Control/Option.lean

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 module
 
 prelude
-public import Init.Data.Option.Basic
-public import Init.Control.Basic
-public import Init.Control.Except
-
-public section
+import Init.Data.Option.Basic
+import Init.Control.Basic
+import Init.Control.Except
 
 set_option linter.missingDocs true
 

src/Init/Control/Reader.lean

@@ -8,11 +8,9 @@ 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
+import Init.Control.Basic
+import Init.Control.Id
+import Init.Control.Except
 
 set_option linter.missingDocs true
 

src/Init/Control/State.lean

@@ -8,11 +8,9 @@ The State monad transformer.
 module
 
 prelude
-public import Init.Control.Basic
-public import Init.Control.Id
-public import Init.Control.Except
-
-public section
+import Init.Control.Basic
+import Init.Control.Id
+import Init.Control.Except
 
 set_option linter.missingDocs true
 

src/Init/Control/StateCps.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Control.Lawful.Basic
-
-public section
+import Init.Control.Lawful.Basic
 
 set_option linter.missingDocs true
 

src/Init/Control/StateRef.lean

@@ -8,9 +8,7 @@ The State monad transformer using IO references.
 module
 
 prelude
-public import Init.System.ST
-
-public section
+import Init.System.ST
 
 set_option linter.missingDocs true
 

src/Init/Conv.lean

@@ -8,10 +8,8 @@ Notation for operators defined at Prelude.lean
 module
 
 prelude
-public import Init.Tactics
-public meta import Init.Meta
-
-public section
+import Init.Tactics
+meta import Init.Meta
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -323,7 +321,7 @@ macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
 /--
-Extracts `let` and `have` expressions from within the target expression.
+Extracts `let` and `let_fun` expressions from within the target expression.
 This is the conv mode version of the `extract_lets` tactic.
 
 - `extract_lets` extracts all the lets from the target.
@@ -336,17 +334,11 @@ See also `lift_lets`, which does not extract lets as local declarations.
 syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* : conv
 
 /--
-Lifts `let` and `have` expressions within the target expression as far out as possible.
+Lifts `let` and `let_fun` expressions within the target expression as far out as possible.
 This is the conv mode version of the `lift_lets` tactic.
 -/
 syntax (name := liftLets) "lift_lets " optConfig : conv
 
-/--
-Transforms `let` expressions into `have` expressions within th etarget expression when possible.
-This is the conv mode version of the `let_to_have` tactic.
--/
-syntax (name := letToHave) "let_to_have" : conv
-
 /--
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
 by focusing on particular subexpressions.

src/Init/Core.lean

@@ -8,10 +8,8 @@ notation, basic datatypes and type classes
 module
 
 prelude
-public meta import Init.Prelude
-public import Init.SizeOf
-
-public section
+meta import Init.Prelude
+import Init.SizeOf
 set_option linter.missingDocs true -- keep it documented
 
 @[expose] section

src/Init/Data.lean

@@ -6,48 +6,44 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Basic
-public import Init.Data.Nat
-public import Init.Data.Bool
-public import Init.Data.BitVec
-public import Init.Data.Cast
-public import Init.Data.Char
-public import Init.Data.String
-public import Init.Data.List
-public import Init.Data.Int
-public import Init.Data.Array
-public import Init.Data.Array.Subarray.Split
-public import Init.Data.ByteArray
-public import Init.Data.FloatArray
-public import Init.Data.Fin
-public import Init.Data.UInt
-public import Init.Data.SInt
-public import Init.Data.Float
-public import Init.Data.Float32
-public import Init.Data.Option
-public import Init.Data.Ord
-public import Init.Data.Random
-public import Init.Data.ToString
-public import Init.Data.Range
-public import Init.Data.Hashable
-public import Init.Data.OfScientific
-public import Init.Data.Format
-public import Init.Data.Stream
-public import Init.Data.Prod
-public import Init.Data.AC
-public import Init.Data.Queue
-public import Init.Data.Sum
-public import Init.Data.BEq
-public import Init.Data.Subtype
-public import Init.Data.ULift
-public import Init.Data.PLift
-public import Init.Data.Zero
-public import Init.Data.NeZero
-public import Init.Data.Function
-public import Init.Data.RArray
-public import Init.Data.Vector
-public import Init.Data.Iterators
-public import Init.Data.Range.Polymorphic
-public import Init.Data.Slice
-
-public section
+import Init.Data.Basic
+import Init.Data.Nat
+import Init.Data.Bool
+import Init.Data.BitVec
+import Init.Data.Cast
+import Init.Data.Char
+import Init.Data.String
+import Init.Data.List
+import Init.Data.Int
+import Init.Data.Array
+import Init.Data.Array.Subarray.Split
+import Init.Data.ByteArray
+import Init.Data.FloatArray
+import Init.Data.Fin
+import Init.Data.UInt
+import Init.Data.SInt
+import Init.Data.Float
+import Init.Data.Float32
+import Init.Data.Option
+import Init.Data.Ord
+import Init.Data.Random
+import Init.Data.ToString
+import Init.Data.Range
+import Init.Data.Hashable
+import Init.Data.OfScientific
+import Init.Data.Format
+import Init.Data.Stream
+import Init.Data.Prod
+import Init.Data.AC
+import Init.Data.Queue
+import Init.Data.Sum
+import Init.Data.BEq
+import Init.Data.Subtype
+import Init.Data.ULift
+import Init.Data.PLift
+import Init.Data.Zero
+import Init.Data.NeZero
+import Init.Data.Function
+import Init.Data.RArray
+import Init.Data.Vector
+import Init.Data.Iterators

src/Init/Data/AC.lean

@@ -7,10 +7,8 @@ Authors: Dany Fabian
 module
 
 prelude
-public import Init.Classical
-public import Init.ByCases
-
-public section
+import Init.Classical
+import Init.ByCases
 
 namespace Lean.Data.AC
 inductive Expr
@@ -211,7 +209,7 @@ theorem Context.evalList_sort_congr
   induction c generalizing a b with
   | nil => simp [sort.loop, h₂]
   | cons c _  ih =>
-    simp [sort.loop]; apply ih; simp [evalList_insert ctx h]
+    simp [sort.loop]; apply ih; simp [evalList_insert ctx h, evalList]
     cases a with
     | nil => apply absurd h₃; simp
     | cons a as =>
@@ -284,7 +282,7 @@ theorem Context.toList_nonEmpty (e : Expr) : e.toList ≠ [] := by
     simp [Expr.toList]
     cases h : l.toList with
     | nil => contradiction
-    | cons => simp
+    | cons => simp [List.append]
 
 theorem Context.unwrap_isNeutral
   {ctx : Context α}
@@ -330,13 +328,13 @@ theorem Context.eval_toList (ctx : Context α) (e : Expr) : evalList α ctx e.to
   induction e with
   | var x => rfl
   | op l r ih₁ ih₂ =>
-    simp [Expr.toList, eval, ←ih₁, ←ih₂]
+    simp [evalList, Expr.toList, eval, ←ih₁, ←ih₂]
     apply evalList_append <;> apply toList_nonEmpty
 
 theorem Context.eval_norm (ctx : Context α) (e : Expr) : evalList α ctx (norm ctx e) = eval α ctx e := by
   simp [norm]
   cases h₁ : ContextInformation.isIdem ctx <;> cases h₂ : ContextInformation.isComm ctx <;>
-  simp_all [evalList_removeNeutrals, eval_toList, evalList_mergeIdem, evalList_sort]
+  simp_all [evalList_removeNeutrals, eval_toList, toList_nonEmpty, evalList_mergeIdem, evalList_sort]
 
 theorem Context.eq_of_norm (ctx : Context α) (a b : Expr) (h : norm ctx a == norm ctx b) : eval α ctx a = eval α ctx b := by
   have h := congrArg (evalList α ctx) (eq_of_beq h)

src/Init/Data/Array.lean

@@ -6,29 +6,27 @@ Authors: Gabriel Ebner
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import Init.Data.Array.QSort
-public import Init.Data.Array.BinSearch
-public import Init.Data.Array.InsertionSort
-public import Init.Data.Array.DecidableEq
-public import Init.Data.Array.Mem
-public import Init.Data.Array.Attach
-public import Init.Data.Array.BasicAux
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.TakeDrop
-public import Init.Data.Array.Bootstrap
-public import Init.Data.Array.GetLit
-public import Init.Data.Array.MapIdx
-public import Init.Data.Array.Set
-public import Init.Data.Array.Monadic
-public import Init.Data.Array.FinRange
-public import Init.Data.Array.Perm
-public import Init.Data.Array.Find
-public import Init.Data.Array.Lex
-public import Init.Data.Array.Range
-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
+import Init.Data.Array.Basic
+import Init.Data.Array.QSort
+import Init.Data.Array.BinSearch
+import Init.Data.Array.InsertionSort
+import Init.Data.Array.DecidableEq
+import Init.Data.Array.Mem
+import Init.Data.Array.Attach
+import Init.Data.Array.BasicAux
+import Init.Data.Array.Lemmas
+import Init.Data.Array.TakeDrop
+import Init.Data.Array.Bootstrap
+import Init.Data.Array.GetLit
+import Init.Data.Array.MapIdx
+import Init.Data.Array.Set
+import Init.Data.Array.Monadic
+import Init.Data.Array.FinRange
+import Init.Data.Array.Perm
+import Init.Data.Array.Find
+import Init.Data.Array.Lex
+import Init.Data.Array.Range
+import Init.Data.Array.Erase
+import Init.Data.Array.Zip
+import Init.Data.Array.InsertIdx
+import Init.Data.Array.Extract

src/Init/Data/Array/Attach.lean

@@ -6,12 +6,10 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
-public import Init.Data.Array.Mem
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.Count
-public import all Init.Data.List.Attach
-
-public section
+import Init.Data.Array.Mem
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Count
+import all Init.Data.List.Attach
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -157,7 +155,7 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
     (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
-  simp
+  simp [attachWith_congr (List.push_toArray _ _)]
 
 theorem pmap_eq_map_attach {p : α → Prop} {f : ∀ a, p a → β} {xs : Array α} (H) :
     pmap f xs H = xs.attach.map fun x => f x.1 (H _ x.2) := by
@@ -344,7 +342,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', mem_toArray, List.foldl_subtype]
+    List.length_pmap, List.foldl_toArray', mem_toArray, List.foldl_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
@@ -363,7 +361,7 @@ 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', mem_toArray, List.foldr_subtype]
+    List.length_pmap, List.foldr_toArray', mem_toArray, List.foldr_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
@@ -472,7 +470,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
     {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 [attachWith, attach_append, map_pmap, pmap_append]
 
 @[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
@@ -705,7 +703,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.size_toArray, List.flatMap_toArray, List.unattach_toArray, List.length_unattach,
     mk.injEq]
   rw [List.flatMap_subtype]
   simp [hf]

src/Init/Data/Array/Basic.lean

@@ -6,17 +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 all Init.Data.List.ToArrayImpl
-public import all Init.Data.Array.Set
-
-public section
+import Init.WFTactics
+import Init.Data.Nat.Basic
+import Init.Data.Fin.Basic
+import Init.Data.UInt.BasicAux
+import Init.Data.Repr
+import Init.Data.ToString.Basic
+import Init.GetElem
+import all Init.Data.List.ToArrayImpl
+import all Init.Data.Array.Set
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -263,7 +261,7 @@ Examples:
 * `#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]`
 * `#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]`
 -/
-@[extern "lean_array_swap", grind]
+@[extern "lean_array_swap"]
 def swapIfInBounds (xs : Array α) (i j : @& Nat) : Array α :=
   if h₁ : i < xs.size then
   if h₂ : j < xs.size then swap xs i j
@@ -1790,7 +1788,7 @@ decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
   induction xs, i, h using Array.eraseIdx.induct with
   | @case1 xs i h h' xs' ih =>
     unfold eraseIdx
-    simp +zetaDelta [h', ih]
+    simp +zetaDelta [h', xs', ih]
   | case2 xs i h h' =>
     unfold eraseIdx
     simp [h']
@@ -1808,7 +1806,6 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
-@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 
@@ -1919,7 +1916,6 @@ Examples:
  * `#["tues", "thur", "sat"].insertIdxIfInBounds 3 "wed" = #["tues", "thur", "sat", "wed"]`
  * `#["tues", "thur", "sat"].insertIdxIfInBounds 4 "wed" = #["tues", "thur", "sat"]`
 -/
-@[grind]
 def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
   if h : i ≤ as.size then
     insertIdx as i a

src/Init/Data/Array/BasicAux.lean

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import all Init.Data.Array.Basic
-public import Init.Data.Nat.Linear
-public import Init.NotationExtra
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.Nat.Linear
+import Init.NotationExtra
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/BinSearch.lean

@@ -6,11 +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
+import Init.Data.Array.Basic
+import Init.Data.Int.DivMod.Lemmas
+import Init.Omega
 universe u v
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.

src/Init/Data/Array/Bootstrap.lean

@@ -7,10 +7,8 @@ Authors: Mario Carneiro
 module
 
 prelude
-public import Init.Data.List.TakeDrop
-public import all Init.Data.Array.Basic
-
-public section
+import Init.Data.List.TakeDrop
+import all Init.Data.Array.Basic
 
 /-!
 ## Bootstrapping theorems about arrays
@@ -121,13 +119,13 @@ abbrev pop_toList := @Array.toList_pop
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
 @[simp, grind =] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
-  apply ext'; simp only [toList_append, List.append_nil]
+  apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
 @[deprecated append_empty (since := "2025-01-13")]
 abbrev append_nil := @append_empty
 
 @[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
-  apply ext'; simp only [toList_append, List.nil_append]
+  apply ext'; simp only [toList_append, toList_empty, List.nil_append]
 
 @[deprecated empty_append (since := "2025-01-13")]
 abbrev nil_append := @empty_append

src/Init/Data/Array/Count.lean

@@ -6,11 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.Count
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.Count
 
 /-!
 # Lemmas about `Array.countP` and `Array.count`.
@@ -225,7 +223,7 @@ theorem boole_getElem_le_count {xs : Array α} {i : Nat} {a : α} (h : i < xs.si
 @[grind =]
 theorem count_set {xs : Array α} {i : Nat} {a b : α} (h : i < xs.size) :
     (xs.set i a).count b = xs.count b - (if xs[i] == b then 1 else 0) + (if a == b then 1 else 0) := by
-  simp [count_eq_countP, countP_set]
+  simp [count_eq_countP, countP_set, h]
 
 variable [LawfulBEq α]
 
@@ -233,7 +231,7 @@ variable [LawfulBEq α]
   simp [count_push]
 
 @[simp] theorem count_push_of_ne {xs : Array α} (h : b ≠ a) : count a (xs.push b) = count a xs := by
-  simp_all [count_push]
+  simp_all [count_push, h]
 
 theorem count_singleton_self {a : α} : count a #[a] = 1 := by simp
 
@@ -294,17 +292,17 @@ abbrev mkArray_count_eq_of_count_eq_size := @replicate_count_eq_of_count_eq_size
 theorem count_le_count_map [BEq β] [LawfulBEq β] {xs : Array α} {f : α → β} {x : α} :
     count x xs ≤ count (f x) (map f xs) := by
   rcases xs with ⟨xs⟩
-  simp [List.count_le_count_map]
+  simp [List.count_le_count_map, countP_map]
 
 theorem count_filterMap {α} [BEq β] {b : β} {f : α → Option β} {xs : Array α} :
     count b (filterMap f xs) = countP (fun a => f a == some b) xs := by
   rcases xs with ⟨xs⟩
-  simp [List.count_filterMap]
+  simp [List.count_filterMap, countP_filterMap]
 
 theorem count_flatMap {α} [BEq β] {xs : Array α} {f : α → Array β} {x : β} :
     count x (xs.flatMap f) = sum (map (count x ∘ f) xs) := by
   rcases xs with ⟨xs⟩
-  simp [List.count_flatMap, Function.comp_def]
+  simp [List.count_flatMap, countP_flatMap, Function.comp_def]
 
 theorem countP_replace {a b : α} {xs : Array α} {p : α → Bool} :
     (xs.replace a b).countP p =

src/Init/Data/Array/DecidableEq.lean

@@ -6,12 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+import all Init.Data.Array.Basic
+import Init.Data.BEq
+import Init.Data.List.Nat.BEq
+import Init.ByCases
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -25,7 +23,7 @@ private theorem rel_of_isEqvAux
   induction i with
   | zero => contradiction
   | succ i ih =>
-    simp only [Array.isEqvAux, Bool.and_eq_true] at heqv
+    simp only [Array.isEqvAux, Bool.and_eq_true, decide_eq_true_eq] at heqv
     by_cases hj' : j < i
     next =>
       exact ih _ heqv.right hj'

src/Init/Data/Array/Erase.lean

@@ -6,12 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.Erase
+import Init.Data.List.Nat.Basic
 
 /-!
 # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`.
@@ -208,7 +206,7 @@ theorem erase_eq_eraseP [LawfulBEq α] (a : α) (xs : Array α) : xs.erase a = x
 theorem erase_ne_empty_iff [LawfulBEq α] {xs : Array α} {a : α} :
     xs.erase a ≠ #[] ↔ xs ≠ #[] ∧ xs ≠ #[a] := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [List.erase_ne_nil_iff]
 
 theorem exists_erase_eq [LawfulBEq α] {a : α} {xs : Array α} (h : a ∈ xs) :
     ∃ ys zs, a ∉ ys ∧ xs = ys.push a ++ zs ∧ xs.erase a = ys ++ zs := by
@@ -308,7 +306,7 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {xs : Array α} :
 @[simp] theorem erase_replicate_self [LawfulBEq α] {a : α} :
     (replicate n a).erase a = replicate (n - 1) a := by
   simp only [← List.toArray_replicate, List.erase_toArray]
-  simp
+  simp [List.erase_replicate]
 
 @[deprecated erase_replicate_self (since := "2025-03-18")]
 abbrev erase_mkArray_self := @erase_replicate_self
@@ -354,7 +352,7 @@ theorem getElem?_eraseIdx_of_lt {xs : Array α} {i : Nat} (h : i < xs.size) {j :
 theorem getElem?_eraseIdx_of_ge {xs : Array α} {i : Nat} (h : i < xs.size) {j : Nat} (h' : i ≤ j) :
     (xs.eraseIdx i)[j]? = xs[j + 1]? := by
   rw [getElem?_eraseIdx]
-  simp only [ite_eq_right_iff]
+  simp only [dite_eq_ite, ite_eq_right_iff]
   intro h'
   omega
 

src/Init/Data/Array/Extract.lean

@@ -6,10 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.TakeDrop
-
-public section
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.TakeDrop
 
 /-!
 # Lemmas about `Array.extract`
@@ -31,7 +29,7 @@ namespace Array
   · simp
     omega
   · simp only [size_extract] at h₁ h₂
-    simp
+    simp [h]
 
 theorem size_extract_le {as : Array α} {i j : Nat} :
     (as.extract i j).size ≤ j - i := by
@@ -48,45 +46,15 @@ theorem size_extract_of_le {as : Array α} {i j : Nat} (h : j ≤ as.size) :
   simp
   omega
 
-@[grind =]
-theorem extract_push {as : Array α} {b : α} {start stop : Nat} :
-    (as.push b).extract start stop =
-      if stop ≤ as.size then
-        as.extract start stop
-      else if start ≤ as.size then
-        (as.extract start as.size).push b
-      else #[] := by
-  split
-  · ext i h₁ h₂
-    · simp
-      omega
-    · simp only [size_extract, size_push] at h₁ h₂
-      simp only [getElem_extract, getElem_push]
-      rw [dif_pos (by omega)]
-  · split
-    · ext i h₁ h₂
-      · simp
-        omega
-      · simp only [size_extract, size_push] at h₁ h₂
-        simp only [getElem_extract, getElem_push]
-        split <;> rename_i h₃
-        · split
-          · rfl
-          · simp_all
-            omega
-        · split <;> rename_i h₄
-          · simp at h₄
-            omega
-          · rfl
-    · ext i h₁ h₂
-      · simp
-        omega
-      · simp at h₂
-
-@[simp]
-theorem extract_push_of_le {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
+@[simp, grind =]
+theorem extract_push {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
     (as.push b).extract start stop = as.extract start stop := by
-  rw [extract_push, if_pos h]
+  ext i h₁ h₂
+  · simp
+    omega
+  · simp only [size_extract, size_push] at h₁ h₂
+    simp only [getElem_extract, getElem_push]
+    rw [dif_pos (by omega)]
 
 @[simp, grind =]
 theorem extract_eq_pop {as : Array α} {stop : Nat} (h : stop = as.size - 1) :
@@ -194,7 +162,7 @@ theorem extract_sub_one {as : Array α} {i j : Nat} (h : j < as.size) :
 @[simp]
 theorem getElem?_extract_of_lt {as : Array α} {i j k : Nat} (h : k < min j as.size - i) :
     (as.extract i j)[k]? = some (as[i + k]'(by omega)) := by
-  simp [h]
+  simp [getElem?_extract, h]
 
 theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
     (as.extract 0 (j + 1))[j]? = as[j]? := by

src/Init/Data/Array/FinRange.lean

@@ -6,10 +6,8 @@ Authors: François G. Dorais
 module
 
 prelude
-public import Init.Data.List.FinRange
-public import Init.Data.Array.OfFn
-
-public section
+import Init.Data.List.FinRange
+import Init.Data.Array.OfFn
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Find.lean

@@ -6,13 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.List.Nat.Find
-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
+import Init.Data.List.Nat.Find
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+import Init.Data.Array.Range
 
 /-!
 # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`.
@@ -83,7 +81,7 @@ theorem find?_eq_findSome?_guard {xs : Array α} : find? p xs = findSome? (Optio
 
 @[simp, grind =] theorem getElem_zero_filterMap {f : α → Option β} {xs : Array α} (h) :
     (xs.filterMap f)[0] = (xs.findSome? f).get (by cases xs; simpa [List.length_filterMap_eq_countP] using h) := by
-  cases xs; simp [← getElem?_zero_filterMap]
+  cases xs; simp [← List.head_eq_getElem, ← getElem?_zero_filterMap]
 
 @[simp, grind =] theorem back?_filterMap {f : α → Option β} {xs : Array α} : (xs.filterMap f).back? = xs.findSomeRev? f := by
   cases xs; simp
@@ -124,7 +122,7 @@ theorem getElem_zero_flatten.proof {xss : Array (Array α)} (h : 0 < xss.flatten
 theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
     (flatten xss)[0] = (xss.findSome? fun xs => xs[0]?).get (getElem_zero_flatten.proof h) := by
   have t := getElem?_zero_flatten xss
-  simp at t
+  simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
 @[grind =]
@@ -310,7 +308,7 @@ 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
-  simp [List.find?_flatMap]
+  simp [List.find?_flatMap, Array.flatMap_toArray]
 
 theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
@@ -350,7 +348,7 @@ 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]
+  simp [← List.toArray_replicate, List.find?_replicate_eq_none_iff, 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
@@ -490,7 +488,7 @@ theorem findIdx_push {xs : Array α} {a : α} {p : α → Bool} :
   simp only [push_eq_append, findIdx_append]
   split <;> rename_i h
   · rfl
-  · simp [Nat.add_comm]
+  · simp [findIdx_singleton, Nat.add_comm]
 
 theorem findIdx_le_findIdx {xs : Array α} {p q : α → Bool} (h : ∀ x ∈ xs, p x → q x) : xs.findIdx q ≤ xs.findIdx p := by
   rcases xs with ⟨xs⟩
@@ -555,7 +553,7 @@ theorem findIdx?_eq_some_of_exists {xs : Array α} {p : α → Bool} (h : ∃ x,
 theorem findIdx?_eq_none_iff_findIdx_eq {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = none ↔ xs.findIdx p = xs.size := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [List.findIdx?_eq_none_iff_findIdx_eq]
 
 theorem findIdx?_eq_guard_findIdx_lt {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = Option.guard (fun i => i < xs.size) (xs.findIdx p) := by
@@ -800,7 +798,7 @@ The lemmas below should be made consistent with those for `findFinIdx?` (and pro
 
 theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
-  simp [idxOf?, finIdxOf?]
+  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
 
 @[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
 

src/Init/Data/Array/GetLit.lean

@@ -7,9 +7,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-
-public section
+import Init.Data.Array.Basic
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/InsertIdx.lean

@@ -6,10 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.InsertIdx
-
-public section
+import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.InsertIdx
 
 /-!
 # insertIdx
@@ -111,19 +109,19 @@ theorem getElem_insertIdx {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.siz
         else
           xs[k-1]'(by simp [size_insertIdx] at h; omega) := by
   cases xs
-  simp [List.getElem_insertIdx]
+  simp [List.getElem_insertIdx, w]
 
 theorem getElem_insertIdx_of_lt {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < i) :
     (xs.insertIdx i x)[k]'(by simp; omega) = xs[k] := by
-  simp [getElem_insertIdx, h]
+  simp [getElem_insertIdx, w, h]
 
 theorem getElem_insertIdx_self {xs : Array α} {x : α} {i : Nat} (w : i ≤ xs.size) :
     (xs.insertIdx i x)[i]'(by simp; omega) = x := by
-  simp [getElem_insertIdx]
+  simp [getElem_insertIdx, w]
 
 theorem getElem_insertIdx_of_gt {xs : Array α} {x : α} {i k : Nat} (w : k ≤ xs.size) (h : k > i) :
     (xs.insertIdx i x)[k]'(by simp; omega) = xs[k - 1]'(by omega) := by
-  simp [getElem_insertIdx]
+  simp [getElem_insertIdx, w, h]
   rw [dif_neg (by omega), dif_neg (by omega)]
 
 @[grind =]
@@ -137,7 +135,7 @@ theorem getElem?_insertIdx {xs : Array α} {x : α} {i k : Nat} (h : i ≤ xs.si
         else
           xs[k-1]? := by
   cases xs
-  simp [List.getElem?_insertIdx]
+  simp [List.getElem?_insertIdx, h]
 
 theorem getElem?_insertIdx_of_lt {xs : Array α} {x : α} {i k : Nat} (w : i ≤ xs.size) (h : k < i) :
     (xs.insertIdx i x)[k]? = xs[k]? := by

src/Init/Data/Array/InsertionSort.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-
-public section
+import Init.Data.Array.Basic
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Lemmas.lean

@@ -6,23 +6,21 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-public import Init.Data.Nat.Lemmas
-public import Init.Data.List.Range
-public import all Init.Data.List.Control
-public import Init.Data.List.Nat.TakeDrop
-public import Init.Data.List.Nat.Modify
-public import Init.Data.List.Nat.Basic
-public import Init.Data.List.Monadic
-public import Init.Data.List.OfFn
-public import all Init.Data.Array.Bootstrap
-public import Init.Data.Array.Mem
-public import Init.Data.Array.DecidableEq
-public import Init.Data.Array.Lex.Basic
-public import Init.Data.Range.Lemmas
-public import Init.TacticsExtra
-public import Init.Data.List.ToArray
-
-public section
+import Init.Data.Nat.Lemmas
+import Init.Data.List.Range
+import all Init.Data.List.Control
+import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Nat.Modify
+import Init.Data.List.Nat.Basic
+import Init.Data.List.Monadic
+import Init.Data.List.OfFn
+import all Init.Data.Array.Bootstrap
+import Init.Data.Array.Mem
+import Init.Data.Array.DecidableEq
+import Init.Data.Array.Lex.Basic
+import Init.Data.Range.Lemmas
+import Init.TacticsExtra
+import Init.Data.List.ToArray
 
 /-!
 ## Theorems about `Array`.
@@ -127,7 +125,7 @@ theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.si
   simp
 
 theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := by
-  simp [h]
+  simp [getElem?_eq_none_iff, h]
 
 grind_pattern Array.getElem?_eq_none => xs.size ≤ i, xs[i]?
 
@@ -156,16 +154,16 @@ theorem getElem_eq_iff {xs : Array α} {i : Nat} {h : i < xs.size} : xs[i] = x
   exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩
 
 theorem getElem_eq_getElem?_get {xs : Array α} {i : Nat} (h : i < xs.size) :
-    xs[i] = xs[i]?.get (by simp [h]) := by
-  simp
+    xs[i] = xs[i]?.get (by simp [getElem?_eq_getElem, h]) := by
+  simp [getElem_eq_iff]
 
 theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} :
     xs[i]?.getD d = if p : i < xs.size then xs[i]'p else d := by
   if h : i < xs.size then
-    simp [h]
+    simp [h, getElem?_def]
   else
     have p : i ≥ xs.size := Nat.le_of_not_gt h
-    simp [h]
+    simp [getElem?_eq_none p, h]
 
 @[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl
 
@@ -177,14 +175,14 @@ theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
 
 @[simp] theorem getElem_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size] = x := by
   simp only [push, ← getElem_toList, List.concat_eq_append]
-  rw [List.getElem_append_right] <;> simp
+  rw [List.getElem_append_right] <;> simp [← getElem_toList, Nat.zero_lt_one]
 
 @[grind =] theorem getElem_push {xs : Array α} {x : α} {i : Nat} (h : i < (xs.push x).size) :
     (xs.push x)[i] = if h : i < xs.size then xs[i] else x := by
   by_cases h' : i < xs.size
   · simp [getElem_push_lt, h']
   · simp at h
-    simp [Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
+    simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
 
 @[grind =] theorem getElem?_push {xs : Array α} {x} : (xs.push x)[i]? = if i = xs.size then some x else xs[i]? := by
   simp [getElem?_def, getElem_push]
@@ -908,7 +906,7 @@ theorem all_push [BEq α] {xs : Array α} {a : α} {p : α → Bool} :
 abbrev getElem_set_eq := @getElem_set_self
 
 @[simp] theorem getElem?_set_self {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} :
-    (xs.set i v)[i]? = some v := by simp [h]
+    (xs.set i v)[i]? = some v := by simp [getElem?_eq_getElem, h]
 
 @[deprecated getElem?_set_self (since := "2024-12-11")]
 abbrev getElem?_set_eq := @getElem?_set_self
@@ -920,7 +918,7 @@ abbrev getElem?_set_eq := @getElem?_set_self
 
 @[simp] theorem getElem?_set_ne {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} {j : Nat}
     (ne : i ≠ j) : (xs.set i v)[j]? = xs[j]? := by
-  by_cases h : j < xs.size <;> simp [ne, h]
+  by_cases h : j < xs.size <;> simp [getElem?_eq_getElem, getElem?_eq_none, Nat.ge_of_not_lt, ne, h]
 
 @[grind] theorem getElem_set {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
     (h : j < (xs.set i v).size) :
@@ -1046,7 +1044,7 @@ theorem getElem?_setIfInBounds_self {xs : Array α} {i : Nat} {a : α} :
 @[simp]
 theorem getElem?_setIfInBounds_self_of_lt {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
     (xs.setIfInBounds i a)[i]? = some a := by
-  simp [h]
+  simp [getElem?_setIfInBounds, h]
 
 @[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
 abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
@@ -1090,7 +1088,7 @@ theorem mem_or_eq_of_mem_setIfInBounds
 @[simp] theorem getD_getElem?_setIfInBounds {xs : Array α} {i : Nat} {v d : α} :
     (xs.setIfInBounds i v)[i]?.getD d = if i < xs.size then v else d := by
   by_cases h : i < xs.size <;>
-    simp [setIfInBounds, h,  ]
+    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]
 
 @[simp, grind =] theorem toList_setIfInBounds {xs : Array α} {i : Nat} {x : α} :
     (xs.setIfInBounds i x).toList = xs.toList.set i x := by
@@ -1202,7 +1200,7 @@ where
       mapM.map f xs i bs = (xs.toList.drop i).foldlM (fun bs a => bs.push <$> f a) bs := by
     unfold mapM.map; split
     · rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
-      simp only [aux (i + 1), map_eq_pure_bind, List.foldlM_cons, bind_assoc,
+      simp only [aux (i + 1), map_eq_pure_bind, length_toList, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
     · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
@@ -1757,7 +1755,7 @@ theorem forall_mem_filterMap {f : α → Option β} {xs : Array α} {P : β →
 
 theorem map_filterMap_of_inv {f : α → Option β} {g : β → α} (H : ∀ x : α, (f x).map g = some x) {xs : Array α} :
     map g (filterMap f xs) = xs := by
-  simp only [map_filterMap, H, filterMap_some]
+  simp only [map_filterMap, H, filterMap_some, id]
 
 @[grind →]
 theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : ∀ x ∈ xs, f x = none := by
@@ -1896,7 +1894,7 @@ theorem getElem?_append_left {xs ys : Array α} {i : Nat} (hn : i < xs.size) :
     (xs ++ ys)[i]? = xs[i]? := by
   have hn' : i < (xs ++ ys).size := Nat.lt_of_lt_of_le hn <|
     size_append .. ▸ Nat.le_add_right ..
-  simp_all
+  simp_all [getElem?_eq_getElem, getElem_append]
 
 theorem getElem?_append_right {xs ys : Array α} {i : Nat} (h : xs.size ≤ i) :
     (xs ++ ys)[i]? = ys[i - xs.size]? := by
@@ -2027,7 +2025,7 @@ theorem append_eq_singleton_iff {xs ys : Array α} {x : α} :
     xs ++ ys = #[x] ↔ (xs = #[] ∧ ys = #[x]) ∨ (xs = #[x] ∧ ys = #[]) := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, mk.injEq, List.append_eq_singleton_iff]
+  simp only [List.append_toArray, mk.injEq, List.append_eq_singleton_iff, toArray_eq_append_iff]
 
 theorem singleton_eq_append_iff {xs ys : Array α} {x : α} :
     #[x] = xs ++ ys ↔ (xs = #[] ∧ ys = #[x]) ∨ (xs = #[x] ∧ ys = #[]) := by
@@ -2353,7 +2351,7 @@ theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
 theorem size_flatMap {xs : Array α} {f : α → Array β} :
     (xs.flatMap f).size = sum (map (fun a => (f a).size) xs) := by
   rcases xs with ⟨l⟩
-  simp
+  simp [Function.comp_def]
 
 @[simp, grind] theorem mem_flatMap {f : α → Array β} {b} {xs : Array α} : b ∈ xs.flatMap f ↔ ∃ a, a ∈ xs ∧ b ∈ f a := by
   simp [flatMap_def, mem_flatten]
@@ -2571,7 +2569,7 @@ abbrev map_mkArray := @map_replicate
 @[grind] theorem filter_replicate (w : stop = n) :
     (replicate n a).filter p 0 stop = if p a then replicate n a else #[] := by
   apply Array.ext'
-  simp only [w]
+  simp only [w, toList_filter', toList_replicate, List.filter_replicate]
   split <;> simp_all
 
 @[deprecated filter_replicate (since := "2025-03-18")]
@@ -2611,7 +2609,7 @@ abbrev filterMap_mkArray_of_some := @filterMap_replicate_of_some
 @[simp] theorem filterMap_replicate_of_isSome {f : α → Option β} (h : (f a).isSome) :
     (replicate n a).filterMap f = replicate n (Option.get _ h) := by
   match w : f a, h with
-  | some b, _ => simp [filterMap_replicate, w]
+  | some b, _ => simp [filterMap_replicate, h, w]
 
 @[deprecated filterMap_replicate_of_isSome (since := "2025-03-18")]
 abbrev filterMap_mkArray_of_isSome := @filterMap_replicate_of_isSome
@@ -2646,7 +2644,7 @@ abbrev flatten_mkArray_replicate := @flatten_replicate_replicate
 
 theorem flatMap_replicate {f : α → Array β} : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
   rw [← toList_inj]
-  simp [List.flatMap_replicate]
+  simp [flatMap_toList, List.flatMap_replicate]
 
 @[deprecated flatMap_replicate (since := "2025-03-18")]
 abbrev flatMap_mkArray := @flatMap_replicate
@@ -4144,7 +4142,7 @@ theorem getElem_modify_of_ne {xs : Array α} {i : Nat} (h : i ≠ j)
 
 @[simp] theorem getElem_swap_right {xs : Array α} {i j : Nat} {hi hj} :
     (xs.swap i j hi hj)[j]'(by simpa using hj) = xs[i] := by
-  simp [swap_def]
+  simp [swap_def, getElem_set]
 
 @[simp] theorem getElem_swap_left {xs : Array α} {i j : Nat} {hi hj} :
     (xs.swap i j hi hj)[i]'(by simpa using hi) = xs[j] := by
@@ -4441,7 +4439,7 @@ theorem size_uset {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size) :
 
 @[simp] theorem getD_eq_getD_getElem? {xs : Array α} {i : Nat} {d : α} :
     xs.getD i d = xs[i]?.getD d := by
-  simp only [getD]; split <;> simp [*]
+  simp only [getD]; split <;> simp [getD_getElem?, *]
 
 theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i default := by
   rfl
@@ -4469,13 +4467,13 @@ theorem getElem?_size_le {xs : Array α} {i : Nat} (h : xs.size ≤ i) : xs[i]?
   simp [getElem?_neg, h]
 
 theorem getElem_mem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs.toList := by
-  simp only [← getElem_toList, List.getElem_mem]
+  simp only [← getElem_toList, List.getElem_mem, ugetElem_eq_getElem]
 
 theorem back!_eq_back? [Inhabited α] {xs : Array α} : xs.back! = xs.back?.getD default := by
   simp [back!, back?, getElem!_def, Option.getD]; rfl
 
 @[simp, grind] theorem back?_push {xs : Array α} {x : α} : (xs.push x).back? = some x := by
-  simp [back?]
+  simp [back?, ← getElem?_toList]
 
 @[simp] theorem back!_push [Inhabited α] {xs : Array α} {x : α} : (xs.push x).back! = x := by
   simp [back!_eq_back?]
@@ -4624,7 +4622,7 @@ theorem uset_toArray {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray
 @[simp, grind =] theorem flatten_toArray {L : List (List α)} :
     (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   apply ext'
-  simp
+  simp [Function.comp_def]
 
 end List
 
@@ -4716,7 +4714,7 @@ namespace List
       intro h'
       specialize ih (by omega)
       have : as.length - (i + 1) + 1 = as.length - i := by omega
-      simp_all
+      simp_all [ih]
     · simp only [size_toArray, Nat.not_lt] at h
       have : as.length = 0 := by omega
       simp_all
@@ -4727,7 +4725,7 @@ end List
 namespace Array
 
 @[deprecated size_toArray (since := "2024-12-11")]
-theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp
+theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
 @[deprecated getElem?_eq_getElem (since := "2024-12-11")]
 theorem getElem?_lt
@@ -4743,7 +4741,7 @@ theorem get?_eq_getElem? (xs : Array α) (i : Nat) : xs.get? i = xs[i]? := rfl
 
 @[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_len_le (xs : Array α) {i : Nat} (h : xs.size ≤ i) : xs[i]? = none := by
-  simp [h]
+  simp [getElem?_eq_none, h]
 
 @[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
 
@@ -4758,7 +4756,7 @@ set_option linter.deprecated false in
 theorem get!_eq_getD_getElem? [Inhabited α] (xs : Array α) (i : Nat) :
     xs.get! i = xs[i]?.getD default := by
   by_cases p : i < xs.size <;>
-  simp [get!, getD_eq_getD_getElem?, p]
+  simp [get!, getElem!_eq_getD, getD_eq_getD_getElem?, getD_getElem?, p]
 
 set_option linter.deprecated false in
 @[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_getElem? := @get!_eq_getD_getElem?

src/Init/Data/Array/Lex.lean

@@ -6,7 +6,5 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Lex.Basic
-public import Init.Data.Array.Lex.Lemmas
-
-public section
+import Init.Data.Array.Lex.Basic
+import Init.Data.Array.Lex.Lemmas

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

@@ -6,11 +6,9 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Range
-
-public section
+import Init.Data.Array.Basic
+import Init.Data.Nat.Lemmas
+import Init.Data.Range
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

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

@@ -6,11 +6,9 @@ Author: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Lex.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Lex
-
-public section
+import all Init.Data.Array.Lex.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.List.Lex
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -164,7 +162,7 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
     {xs ys : Array α} : lex xs ys = false ↔ ys ≤ xs := by
   cases xs
   cases ys
-  simp
+  simp [List.not_lt_iff_ge]
 
 instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Array α) :=
   fun xs ys => decidable_of_iff (lex xs ys = true) lex_eq_true_iff_lt

src/Init/Data/Array/MapIdx.lean

@@ -6,13 +6,11 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-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 all Init.Data.List.MapIdx
-
-public section
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+import Init.Data.Array.OfFn
+import all Init.Data.List.MapIdx
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -137,7 +135,7 @@ abbrev getElem_zipWithIndex := @getElem_zipIdx
 
 @[simp, grind =] theorem zipIdx_toArray {l : List α} {k : Nat} :
     l.toArray.zipIdx k = (l.zipIdx k).toArray := by
-  ext i hi₁ hi₂ <;> simp
+  ext i hi₁ hi₂ <;> simp [Nat.add_comm]
 
 @[deprecated zipIdx_toArray (since := "2025-01-21")]
 abbrev zipWithIndex_toArray := @zipIdx_toArray

src/Init/Data/Array/Mem.lean

@@ -6,11 +6,9 @@ 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
+import Init.Data.Array.Basic
+import Init.Data.Nat.Linear
+import Init.Data.List.BasicAux
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/Monadic.lean

@@ -6,13 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+import all Init.Data.List.Control
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+import Init.Data.List.Monadic
 
 /-!
 # Lemmas about `Array.forIn'` and `Array.forIn`.
@@ -61,7 +59,7 @@ theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] {f : α → m β} {xs : Ar
   rcases xs with ⟨xs⟩
   simp only [List.mapM_toArray, bind_pure_comp, List.size_toArray, List.foldlM_toArray']
   rw [List.mapM_eq_reverse_foldlM_cons]
-  simp only [Functor.map_map]
+  simp only [bind_pure_comp, Functor.map_map]
   suffices ∀ (l), (fun l' => l'.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) l xs =
       List.foldlM (fun acc a => acc.push <$> f a) l.reverse.toArray xs by
     exact this []
@@ -236,14 +234,14 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
     forIn xs init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
       xs.foldlM (fun b a => g a b <$> f a b) init := by
   rcases xs with ⟨xs⟩
-  simp
+  simp [List.foldlM_map]
 
 @[simp] theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
     {xs : Array α} (f : α → β → β) (init : β) :
     forIn xs init (fun a b => pure (.yield (f a b))) =
       pure (f := m) (xs.foldl (fun b a => f a b) init) := by
   rcases xs with ⟨xs⟩
-  simp [List.forIn_pure_yield_eq_foldl]
+  simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
 
 theorem idRun_forIn_yield_eq_foldl
     {xs : Array α} (f : α → β → Id β) (init : β) :

src/Init/Data/Array/OfFn.lean

@@ -6,13 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Monadic
+import Init.Data.List.OfFn
+import Init.Data.List.FinRange
 
 /-!
 # Theorems about `Array.ofFn`

src/Init/Data/Array/Perm.lean

@@ -6,11 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.List.Nat.Perm
-public import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-
-public section
+import Init.Data.List.Nat.Perm
+import all Init.Data.Array.Basic
+import Init.Data.Array.Lemmas
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.

src/Init/Data/Array/QSort.lean

@@ -6,6 +6,4 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.QSort.Basic
-
-public section
+import Init.Data.Array.QSort.Basic

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

@@ -6,10 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Vector.Basic
-public import Init.Data.Ord
-
-public section
+import Init.Data.Vector.Basic
+import Init.Data.Ord
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
@@ -57,7 +55,7 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w
 /--
 In-place quicksort.
 
-`qsort as lt lo hi` sorts the subarray `as[lo...=hi]` in-place using `lt` to compare elements.
+`qsort as lt lo hi` sorts the subarray `as[lo:hi+1]` in-place using `lt` to compare elements.
 -/
 @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
     (lo := 0) (hi := as.size - 1) : Array α :=
@@ -67,7 +65,7 @@ In-place quicksort.
       let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
       if h₂ : mid ≥ hi then
         -- This only occurs when `hi ≤ lo`,
-        -- and thus `as[lo...(hi+1)]` is trivially already sorted.
+        -- and thus `as[lo:hi+1]` is trivially already sorted.
         as
       else
         -- Otherwise, we recursively sort the two subarrays.

src/Init/Data/Array/Range.lean

@@ -6,14 +6,12 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+import Init.Data.Array.Lemmas
+import all Init.Data.Array.Basic
+import all Init.Data.Array.OfFn
+import Init.Data.Array.MapIdx
+import Init.Data.Array.Zip
+import Init.Data.List.Nat.Range
 
 /-!
 # Lemmas about `Array.range'`, `Array.range`, and `Array.zipIdx`
@@ -221,7 +219,7 @@ theorem getElem?_zipIdx {xs : Array α} {i j} : (zipIdx xs i)[j]? = xs[j]?.map f
 
 theorem map_snd_add_zipIdx_eq_zipIdx {xs : Array α} {n k : Nat} :
     map (Prod.map id (· + n)) (zipIdx xs k) = zipIdx xs (n + k) :=
-  ext_getElem? fun i ↦ by simp [Nat.add_comm, Nat.add_left_comm]; rfl
+  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl
 
 -- Arguments are explicit for parity with `zipIdx_map_fst`.
 @[simp]