wip

This PR improves the “expected type mismatch” error message by omitting
the type's types when they are defeq, and putting them into separate
lines when not.

I found it rather tediuos to parse the error message when the expected
type is long, because I had to find the `:` in the middle of a large
expression somewhere. Also, when both are of sort `Prop` or `Type` it
doesn't add much value to print the sort (and it’s only one hover away
anyways).

.github/workflows/awaiting-manual.yml

@@ -0,0 +1,38 @@
+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,6 +107,7 @@ 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 }}
@@ -248,6 +249,7 @@ 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,6 +145,7 @@ 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
               {
@@ -167,11 +168,13 @@ 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 developrs get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the
                 //    Linux lake build and adds little value in the merge queue
                 // 3. To run it in release (obviously)
-                "check-level": isPr ? 0 : 2,
+                // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
+                //    available as an artifact for Grove to use.
+                "check-level": (isPr || isPushToMaster) ? 0 : 2,
                 "secondary": isPr,
                 "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",
@@ -421,6 +424,6 @@ jobs:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
       - name: Update toolchain on mathlib4's nightly-testing branch
         run: |
-          gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
         env:
           GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/grove.yml

@@ -0,0 +1,161 @@
+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
+      - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries
         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.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")"
 
             if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
               echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
@@ -183,7 +183,6 @@ 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"
@@ -265,6 +264,108 @@ 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
@@ -355,7 +456,7 @@ jobs:
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         uses: actions/checkout@v4
         with:
-          repository: leanprover-community/mathlib4
+          repository: leanprover-community/mathlib4-nightly-testing
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
@@ -411,3 +512,63 @@ 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

@@ -31,3 +31,4 @@ 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")
+    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
       # 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. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
+Within each group the fields are ordered in declaration order. Trivial wrapper types count as their underlying wrapped type 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
-  ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
-  sc64_2 : Float -- `Float` is 64 bit
+  sc64_2 : { x : UInt64 // x > 0 } -- wrappers of scalars count as scalars
+  sc64_3 : Float -- `Float` is 64 bit
   sc8_1 : Bool
   sc16_1 : UInt16
   sc8_2 : UInt8
-  sc64_3 : UInt64
+  sc64_4 : UInt64
   usize_2 : USize
-  ptr_3 : Char -- trivial wrapper around `UInt32`
-  sc32_1 : UInt32
+  sc32_1 : Char -- trivial wrapper around `UInt32`
+  sc32_2 : UInt32
   sc16_2 : UInt16
 ```
 would get re-sorted into the following memory order:
 
 * `S.ptr_1` - `lean_ctor_get(val, 0)`
-* `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)`
+* `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)`
 
 ### Borrowing
 
@@ -131,14 +131,21 @@ 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,5 +85,13 @@ 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`
-that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
+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.
 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

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

doc/std/grove/GroveStdlib/Generated.lean

@@ -0,0 +1,14 @@
+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

@@ -0,0 +1,486 @@
+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

@@ -0,0 +1,31 @@
+/-
+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

@@ -0,0 +1,28 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,58 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,26 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,24 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,30 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,19 @@
+/-
+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

@@ -0,0 +1,18 @@
+/-
+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

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

doc/std/grove/grove-local.sh

@@ -0,0 +1,10 @@
+#!/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

@@ -0,0 +1,25 @@
+{"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

@@ -0,0 +1,18 @@
+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

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

doc/std/grove/update_invalidated.sh

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

script/mathlib-bench

@@ -5,8 +5,11 @@ 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/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-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_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
-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
+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

script/push_repo_release_tag.py

@@ -3,6 +3,32 @@ 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>")
@@ -14,6 +40,13 @@ 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:
@@ -43,12 +76,23 @@ 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, check=True)
+        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 = sha_result.stdout.strip()
 
         # Create the tag
@@ -58,11 +102,20 @@ def main():
             "-F", f"ref=refs/tags/{version_tag}",
             "-F", f"sha={sha}"
         ]
-        subprocess.run(create_tag_cmd, capture_output=True, text=True, check=True)
+        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)
 
         print(f"Successfully created and pushed tag '{version_tag}' to {repo}.")
     except subprocess.CalledProcessError as e:
-        print(f"Error while creating/pushing tag: {e.stderr.strip() if e.stderr else 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}")
         sys.exit(1)
 
 if __name__ == "__main__":

script/release_checklist.py

@@ -231,6 +231,43 @@ 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)
@@ -262,6 +299,61 @@ 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)")
@@ -386,6 +478,12 @@ 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:                
@@ -394,7 +492,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])
@@ -417,7 +515,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])
@@ -434,19 +532,49 @@ def main():
         if check_bump:
             next_version = get_next_version(toolchain)
             bump_branch = f"bump/{next_version}"
-            if not branch_exists(url, bump_branch, github_token):
+            
+            # 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 args.dry_run:
-                    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.")
+                    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}.")
                     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/{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/{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)
                 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")
-            if not check_bump_branch_toolchain(url, bump_branch, github_token):
+            
+            # 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):
                 repo_status[name] = False
                 continue
 

script/release_steps.py

@@ -1,10 +1,10 @@
 #!/usr/bin/env python3
 
 """
-Generate release steps script for Lean4 repositories.
+Execute release steps for Lean4 repositories.
 
 This script helps automate the release process for Lean4 and its dependent repositories
-by generating step-by-step instructions for updating toolchains, creating tags,
+by actually executing the 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: A substring of the repository name as specified in release_repos.yml
+    repo: The repository name as specified in release_repos.yml
 
 Example:
-    python3 release_steps.py v4.6.0 mathlib
-    python3 release_steps.py v4.6.0 batt
+    python3 release_steps.py v4.6.0 mathlib4
+    python3 release_steps.py v4.6.0 batteries
 
 The script reads repository configurations from release_repos.yml in the same directory.
 Each repository may have specific requirements for:
@@ -32,23 +32,124 @@ 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_substring, config):
-    pattern = re.compile(re.escape(repo_substring), re.IGNORECASE)
-    matching_repos = [r for r in config if pattern.search(r["name"])]
+def find_repo(repo_name, config):
+    matching_repos = [r for r in config if r["name"] == repo_name]
     if not matching_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)}")
+        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)}"))
         sys.exit(1)
     return matching_repos[0]
 
-def generate_script(repo, version, config):
+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):
     repo_config = find_repo(repo, config)
     repo_name = repo_config['name']
     repo_url = repo_config['url']
@@ -59,92 +160,481 @@ def generate_script(repo, version, config):
     requires_tagging = repo_config.get("toolchain-tag", True)
     has_stable_branch = repo_config.get("stable-branch", True)
 
-    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",
-    ]
+    # 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}"))
 
     # Special cases for specific repositories
     if repo_name == "repl":
-        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"
-        ])
+        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}"))
     elif dependencies:
-        script_lines.append('perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*')
-        script_lines.append("lake update")
+        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("")
-
-    script_lines.extend([
-        f'git commit -am "chore: bump toolchain to {version}"',
-        ""
-    ])
+    # 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
 
+    # Handle special merging cases
     if re.search(r'rc\d+$', version) and repo_name in ["batteries", "mathlib4"]:
-        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",
-            ""
-        ])
+        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([
-        'gh pr create --title "chore: bump toolchain to ' + version + '" --body ""',
-        "echo 'Please review the PR and merge or rebase it.'",
-        ""
-    ])
+    # 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"))
 
-    return "\n".join(script_lines)
+    # 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."))
 
 def main():
     parser = argparse.ArgumentParser(
-        description="Generate release steps script for Lean4 repositories.",
+        description="Execute release steps for Lean4 repositories.",
         formatter_class=argparse.RawDescriptionHelpFormatter,
         epilog="""
 Examples:
-  %(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
+  %(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
   
-The script will generate shell commands to:
-1. Update the lean-toolchain file
-2. Create appropriate branches and commits
-3. Create pull requests
+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
 
 (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="A substring of the repository name as specified in release_repos.yml")
+    parser.add_argument("repo", help="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)
 
-    script = generate_script(args.repo, args.version, config)
-    print(script)
+    execute_release_steps(args.repo, args.version, config)
 
 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 22)
+set(LEAN_VERSION_MINOR 23)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init.lean

@@ -6,41 +6,41 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+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

src/Init/BinderNameHint.lean

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

src/Init/BinderPredicates.lean

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

src/Init/ByCases.lean

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

src/Init/Classical.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-import Init.PropLemmas
+public import Init.PropLemmas
+
+public section
 
 universe u v
 

src/Init/Coe.lean

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

src/Init/Control.lean

@@ -6,13 +6,15 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+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

src/Init/Control/Basic.lean

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

src/Init/Control/EState.lean

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

src/Init/Control/Except.lean

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

src/Init/Control/ExceptCps.lean

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

src/Init/Control/Id.lean

@@ -8,7 +8,9 @@ The identity Monad.
 module
 
 prelude
-import Init.Core
+public import Init.Core
+
+public section
 
 universe u
 
@@ -62,4 +64,7 @@ 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,7 +6,9 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-import Init.Control.Lawful.Basic
-import Init.Control.Lawful.Instances
-import Init.Control.Lawful.Lemmas
-import Init.Control.Lawful.MonadLift
+public import Init.Control.Lawful.Basic
+public import Init.Control.Lawful.Instances
+public import Init.Control.Lawful.Lemmas
+public import Init.Control.Lawful.MonadLift
+
+public section

src/Init/Control/Lawful/Basic.lean

@@ -6,9 +6,11 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-import Init.Ext
-import Init.SimpLemmas
-import Init.Meta
+public import Init.Ext
+public import Init.SimpLemmas
+public import Init.Meta
+
+public section
 
 open Function
 

src/Init/Control/Lawful/Instances.lean

@@ -6,11 +6,13 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-import Init.Control.Lawful.Basic
-import all Init.Control.Except
-import all Init.Control.State
-import Init.Control.StateRef
-import Init.Ext
+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
 
 open Function
 

src/Init/Control/Lawful/Lemmas.lean

@@ -6,9 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Control.Lawful.Basic
-import Init.RCases
-import Init.ByCases
+public import Init.Control.Lawful.Basic
+public import Init.RCases
+public import Init.ByCases
+
+public section
 
 -- 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,6 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-import Init.Control.Lawful.MonadLift.Basic
-import Init.Control.Lawful.MonadLift.Lemmas
-import Init.Control.Lawful.MonadLift.Instances
+public import Init.Control.Lawful.MonadLift.Basic
+public import Init.Control.Lawful.MonadLift.Lemmas
+public import Init.Control.Lawful.MonadLift.Instances
+
+public section

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

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

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

@@ -6,13 +6,16 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
-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
+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
 
 universe u v w x
 
@@ -135,3 +138,11 @@ 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,8 +6,10 @@ Authors: Quang Dao
 module
 
 prelude
-import Init.Control.Lawful.Basic
-import Init.Control.Lawful.MonadLift.Basic
+public import Init.Control.Lawful.Basic
+public import Init.Control.Lawful.MonadLift.Basic
+
+public section
 
 universe u v w
 

src/Init/Control/Option.lean

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

src/Init/Control/Reader.lean

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

src/Init/Control/State.lean

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

src/Init/Control/StateCps.lean

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

src/Init/Control/StateRef.lean

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

src/Init/Conv.lean

@@ -8,8 +8,10 @@ Notation for operators defined at Prelude.lean
 module
 
 prelude
-import Init.Tactics
-meta import Init.Meta
+public import Init.Tactics
+public meta import Init.Meta
+
+public section
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -321,7 +323,7 @@ macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
 /--
-Extracts `let` and `let_fun` expressions from within the target expression.
+Extracts `let` and `have` 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.
@@ -334,11 +336,17 @@ 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 `let_fun` expressions within the target expression as far out as possible.
+Lifts `let` and `have` 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,8 +8,10 @@ notation, basic datatypes and type classes
 module
 
 prelude
-meta import Init.Prelude
-import Init.SizeOf
+public meta import Init.Prelude
+public import Init.SizeOf
+
+public section
 set_option linter.missingDocs true -- keep it documented
 
 @[expose] section

src/Init/Data.lean

@@ -6,44 +6,48 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+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

src/Init/Data/AC.lean

@@ -7,8 +7,10 @@ Authors: Dany Fabian
 module
 
 prelude
-import Init.Classical
-import Init.ByCases
+public import Init.Classical
+public import Init.ByCases
+
+public section
 
 namespace Lean.Data.AC
 inductive Expr

src/Init/Data/Array.lean

@@ -6,27 +6,29 @@ Authors: Gabriel Ebner
 module
 
 prelude
-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
+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

src/Init/Data/Array/Attach.lean

@@ -6,10 +6,12 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
-import Init.Data.Array.Mem
-import Init.Data.Array.Lemmas
-import Init.Data.Array.Count
-import all Init.Data.List.Attach
+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
 
 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/Basic.lean

@@ -6,15 +6,17 @@ Authors: Leonardo de Moura
 module
 
 prelude
-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
+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
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -261,7 +263,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"]
+@[extern "lean_array_swap", grind]
 def swapIfInBounds (xs : Array α) (i j : @& Nat) : Array α :=
   if h₁ : i < xs.size then
   if h₂ : j < xs.size then swap xs i j
@@ -1806,6 +1808,7 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
+@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 
@@ -1916,6 +1919,7 @@ 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,9 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Nat.Linear
-import Init.NotationExtra
+public import all Init.Data.Array.Basic
+public import Init.Data.Nat.Linear
+public import Init.NotationExtra
+
+public section
 
 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,9 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
-import Init.Data.Int.DivMod.Lemmas
-import Init.Omega
+public import Init.Data.Array.Basic
+public import Init.Data.Int.DivMod.Lemmas
+public import Init.Omega
+
+public section
 universe u v
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.

src/Init/Data/Array/Bootstrap.lean

@@ -7,8 +7,10 @@ Authors: Mario Carneiro
 module
 
 prelude
-import Init.Data.List.TakeDrop
-import all Init.Data.Array.Basic
+public import Init.Data.List.TakeDrop
+public import all Init.Data.Array.Basic
+
+public section
 
 /-!
 ## Bootstrapping theorems about arrays

src/Init/Data/Array/Count.lean

@@ -6,9 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.Count
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Count
+
+public section
 
 /-!
 # Lemmas about `Array.countP` and `Array.count`.

src/Init/Data/Array/DecidableEq.lean

@@ -6,10 +6,12 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.BEq
-import Init.Data.List.Nat.BEq
-import Init.ByCases
+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
 
 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/Erase.lean

@@ -6,10 +6,12 @@ Authors: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.Erase
-import Init.Data.List.Nat.Basic
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Erase
+public import Init.Data.List.Nat.Basic
+
+public section
 
 /-!
 # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.eraseIdx`.

src/Init/Data/Array/Extract.lean

@@ -6,8 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.TakeDrop
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
+
+public section
 
 /-!
 # Lemmas about `Array.extract`
@@ -46,15 +48,45 @@ theorem size_extract_of_le {as : Array α} {i j : Nat} (h : j ≤ as.size) :
   simp
   omega
 
-@[simp, grind =]
-theorem extract_push {as : Array α} {b : α} {start stop : Nat} (h : stop ≤ as.size) :
+@[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) :
     (as.push b).extract start stop = as.extract start stop := by
-  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)]
+  rw [extract_push, if_pos h]
 
 @[simp, grind =]
 theorem extract_eq_pop {as : Array α} {stop : Nat} (h : stop = as.size - 1) :

src/Init/Data/Array/FinRange.lean

@@ -6,8 +6,10 @@ Authors: François G. Dorais
 module
 
 prelude
-import Init.Data.List.FinRange
-import Init.Data.Array.OfFn
+public import Init.Data.List.FinRange
+public import Init.Data.Array.OfFn
+
+public section
 
 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,11 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`.

src/Init/Data/Array/GetLit.lean

@@ -7,7 +7,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+
+public section
 
 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,8 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.InsertIdx
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.InsertIdx
+
+public section
 
 /-!
 # insertIdx

src/Init/Data/Array/InsertionSort.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+
+public section
 
 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,21 +6,23 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 ## Theorems about `Array`.

src/Init/Data/Array/Lex.lean

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

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

@@ -6,9 +6,11 @@ Author: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Basic
-import Init.Data.Nat.Lemmas
-import Init.Data.Range
+public import Init.Data.Array.Basic
+public import Init.Data.Nat.Lemmas
+public import Init.Data.Range
+
+public section
 
 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,9 +6,11 @@ Author: Kim Morrison
 module
 
 prelude
-import all Init.Data.Array.Lex.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.List.Lex
+public import all Init.Data.Array.Lex.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Lex
+
+public section
 
 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/MapIdx.lean

@@ -6,11 +6,13 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-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
+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
 
 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/Mem.lean

@@ -6,9 +6,11 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
-import Init.Data.Array.Basic
-import Init.Data.Nat.Linear
-import Init.Data.List.BasicAux
+public import Init.Data.Array.Basic
+public import Init.Data.Nat.Linear
+public import Init.Data.List.BasicAux
+
+public section
 
 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,11 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 # Lemmas about `Array.forIn'` and `Array.forIn`.

src/Init/Data/Array/OfFn.lean

@@ -6,11 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 # Theorems about `Array.ofFn`

src/Init/Data/Array/Perm.lean

@@ -6,9 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.List.Nat.Perm
-import all Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Perm
+public import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+
+public section
 
 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,4 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.QSort.Basic
+public import Init.Data.Array.QSort.Basic
+
+public section

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

@@ -6,8 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Vector.Basic
-import Init.Data.Ord
+public import Init.Data.Vector.Basic
+public import Init.Data.Ord
+
+public section
 
 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.
@@ -55,7 +57,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+1]` in-place using `lt` to compare elements.
+`qsort as lt lo hi` sorts the subarray `as[lo...=hi]` in-place using `lt` to compare elements.
 -/
 @[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
     (lo := 0) (hi := as.size - 1) : Array α :=
@@ -65,7 +67,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,12 +6,14 @@ Authors: Kim Morrison
 module
 
 prelude
-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
+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
 
 /-!
 # Lemmas about `Array.range'`, `Array.range`, and `Array.zipIdx`

src/Init/Data/Array/Set.lean

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