chore: tweak error message about weak options

feat: set_option tactic in grind interactive mode (#10843 )
This PR implements the `set_option` tactic in `grind` interactive mode.
2026-03-24 05:44:15 +00:00 · 2025-10-20 04:21:19 +02:00 · 2025-10-20 00:44:59 +00:00 · 2025-10-19 23:35:27 +00:00 · 2025-10-19 23:45:51 +00:00 · 2025-10-19 22:57:47 +00:00
2157 changed files with 5435 additions and 3445 deletions
--- a/.github/workflows/build-template.yml
+++ b/.github/workflows/build-template.yml
@@ -3,9 +3,6 @@ name: build-template
 on:
  workflow_call:
    inputs:
-      check-level:
-        type: string
-        required: true
      config:
        type: string
        required: true
@@ -230,7 +227,7 @@ jobs:
        run: |
          ulimit -c unlimited  # coredumps
          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
+        if: matrix.test
      - name: Test Summary
        uses: test-summary/action@v2
        with:
--- a/.github/workflows/check-stage0.yml
+++ b/.github/workflows/check-stage0.yml
@@ -11,8 +11,8 @@ jobs:
    - uses: actions/checkout@v5
      with:
        ref: ${{ github.event.pull_request.head.sha }}
-        filter: blob:none
        fetch-depth: 0
+        filter: tree:0

    - name: Find base commit
      if: github.event_name == 'pull_request'
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -31,10 +31,6 @@ jobs:
  configure:
    runs-on: ubuntu-latest
    outputs:
-      # 0: PRs without special label
-      # 1: PRs with `merge-ci` label, merge queue checks, master commits
-      # 2: PRs with `release-ci` label, releases (incl. nightlies)
-      check-level: ${{ steps.set-level.outputs.check-level }}
      # The build matrix, dynamically generated here
      matrix: ${{ steps.set-matrix.outputs.matrix }}
      # secondary build jobs that should not block the CI success/merge queue
@@ -110,6 +106,9 @@ jobs:
          TAG_NAME="${GITHUB_REF##*/}"
          echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"

+      # 0: PRs without special label
+      # 1: PRs with `merge-ci` label, merge queue checks, master commits
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
      - name: Set check level
        id: set-level
        # We do not use github.event.pull_request.labels.*.name here because
@@ -117,6 +116,7 @@ jobs:
        # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
        run: |
          check_level=0
+          fast=false

          if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
            check_level=2
@@ -129,9 +129,13 @@ jobs:
            elif echo "$labels" | grep -q "merge-ci"; then
              check_level=1
            fi
+            if echo "$labels" | grep -q "fast-ci"; then
+              fast=true
+            fi
          fi

          echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
+          echo "fast=$fast" >> "$GITHUB_OUTPUT"
        env:
          GH_TOKEN: ${{ github.token }}

@@ -141,7 +145,8 @@ jobs:
        with:
          script: |
            const level = ${{ steps.set-level.outputs.check-level }};
-            console.log(`level: ${level}`);
+            const fast = ${{ steps.set-level.outputs.fast }};
+            console.log(`level: ${level}, fast: ${fast}`);
            // use large runners where available (original repo)
            let large = ${{ github.repository == 'leanprover/lean4' }};
            const isPr = "${{ github.event_name }}" == "pull_request";
@@ -152,7 +157,8 @@ jobs:
                "name": "Linux LLVM",
                "os": "ubuntu-latest",
                "release": false,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -165,17 +171,19 @@ jobs:
              {
                // portable release build: use channel with older glibc (2.26)
                "name": "Linux release",
-                "os": "ubuntu-latest",
+                // usually not a bottleneck so make exclusive to `fast-ci`
+                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                "release": true,
                // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
                // 2. To skip it in merge queues as it takes longer than the
                //    Linux lake build and adds little value in the merge queue
                // 3. To run it in release (obviously)
                // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
                //    available as an artifact for Grove to use.
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1 || isPushToMaster,
+                "test": level >= 1,
+                "secondary": level == 0,
                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -186,10 +194,9 @@ jobs:
              {
                "name": "Linux Lake",
                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "check-level": 0,
+                "enabled": true,
                "check-rebootstrap": level >= 1,
                "check-stage3": level >= 2,
-                // only check-level >= 1 opts into tests implicitly. TODO: Clean up this logic.
                "test": true,
                // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
                "test-speedcenter": large && level >= 2,
@@ -199,14 +206,16 @@ jobs:
              {
                "name": "Linux Reldebug",
                "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                "CMAKE_PRESET": "reldebug",
              },
              // TODO: suddenly started failing in CI
              /*{
                "name": "Linux fsanitize",
                "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                // turn off custom allocator & symbolic functions to make LSAN do its magic
                "CMAKE_PRESET": "sanitize",
                // exclude seriously slow/problematic tests (laketests crash)
@@ -217,7 +226,7 @@ jobs:
                "os": "macos-15-intel",
                "release": true,
                "test": false,  // Tier 2 platform
-                "check-level": 2,
+                "enabled": level >= 2,
                "shell": "bash -euxo pipefail {0}",
                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@@ -228,7 +237,7 @@ jobs:
              {
                "name": "macOS aarch64",
                // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && !isPr ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
+                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                "release": true,
                "shell": "bash -euxo pipefail {0}",
@@ -237,14 +246,16 @@ jobs:
                "binary-check": "otool -L",
                "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
                // See "Linux release" for release job levels; Grove is not a concern here
-                "check-level": isPr ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1,
+                "test": level >= 1,
+                "secondary": level == 0,
              },
              {
                "name": "Windows",
-                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                "shell": "msys2 {0}",
                "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -256,7 +267,8 @@ jobs:
                "os": "nscloud-ubuntu-22.04-arm64-4x16",
                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -269,7 +281,7 @@ jobs:
              //  "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
              //  "cmultilib": true,
              //  "release": true,
-              //  "check-level": 2,
+              //  "enabled": level >= 2,
              //  "cross": true,
              //  "shell": "bash -euxo pipefail {0}"
              //}
@@ -281,7 +293,7 @@ jobs:
              //   "wasm": true,
              //   "cmultilib": true,
              //   "release": true,
-              //   "check-level": 2,
+              //   "enabled": level >= 2,
              //   "cross": true,
              //   "shell": "bash -euxo pipefail {0}",
              //   // Just a few selected tests because wasm is slow
@@ -295,7 +307,7 @@ jobs:
              }
            }
            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            matrix = matrix.filter((job) => level >= job["check-level"]);
+            matrix = matrix.filter((job) => job["enabled"]);
            core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
            core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));

@@ -305,7 +317,6 @@ jobs:
    uses: ./.github/workflows/build-template.yml
    with:
      config: ${{needs.configure.outputs.matrix}}
-      check-level: ${{ needs.configure.outputs.check-level }}
      nightly: ${{ needs.configure.outputs.nightly }}
      LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
      LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -321,7 +332,6 @@ jobs:
    uses: ./.github/workflows/build-template.yml
    with:
      config: ${{needs.configure.outputs.matrix-secondary}}
-      check-level: ${{ needs.configure.outputs.check-level }}
      nightly: ${{ needs.configure.outputs.nightly }}
      LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
      LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -394,6 +404,8 @@ jobs:
        with:
          # needed for tagging
          fetch-depth: 0
+          # Doesn't seem to be working when additionally fetching from lean4-nightly
+          #filter: tree:0
          token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
      - uses: actions/download-artifact@v5
        with:
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -48,17 +48,17 @@ jobs:
          git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
          git -C lean4.git fetch -n origin master
          git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-          
+
          # Create both the original tag and the SHA-suffixed tag
          SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
          SHORT_SHA="${SHORT_SHA:0:7}"
-          
+
          # Export the short SHA for use in subsequent steps
          echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"

          git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
          git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-          
+
          git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
          git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
          git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
@@ -200,7 +200,7 @@ jobs:
                          -H "Accept: application/vnd.github.v3+json" \
                          "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                          | jq -r '.[].name')"
-            
+
            if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
              echo "force-mathlib-ci label detected, forcing CI despite issues"
              MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
@@ -301,7 +301,7 @@ jobs:
                          -H "Accept: application/vnd.github.v3+json" \
                          "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                          | jq -r '.[].name')"
-            
+
            if echo "$LABELS" | grep -q "^force-manual-ci$"; then
              echo "force-manual-ci label detected, forcing CI despite issues"
              MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
@@ -401,6 +401,7 @@ jobs:
          token: ${{ secrets.MATHLIB4_BOT }}
          ref: nightly-testing
          fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0

      - name: Check if tag exists
        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
@@ -460,6 +461,7 @@ jobs:
          token: ${{ secrets.MATHLIB4_BOT }}
          ref: nightly-testing
          fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0

      - name: install elan
        run: |
@@ -530,6 +532,7 @@ jobs:
          token: ${{ secrets.MANUAL_PR_BOT }}
          ref: nightly-testing
          fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0

      - name: Check if tag in reference manual exists
        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
--- a/.gitignore
+++ b/.gitignore
@@ -20,7 +20,6 @@ tasks.json
 settings.json
 .gdb_history
 .vscode/*
-!.vscode/settings.json
 script/__pycache__
 *.produced.out
 CMakeSettings.json
--- a/lean.code-workspace
+++ b/lean.code-workspace
@@ -15,7 +15,8 @@
 	],
 	"settings": {
 		// Open terminal at root, not current workspace folder
-		"terminal.integrated.cwd": "${workspaceFolder:.}",
+		// (there is not way to directly refer to the root folder included as `.` above)
+		"terminal.integrated.cwd": "${workspaceFolder:src}/..",
 		"files.insertFinalNewline": true,
 		"files.trimTrailingWhitespace": true,
 		"cmake.buildDirectory": "${workspaceFolder}/build/release",
--- a/src/Init/BinderNameHint.lean
+++ b/src/Init/BinderNameHint.lean
@@ -7,7 +7,6 @@ Authors: Joachim Breitner
 module

 prelude
-public import Init.Prelude
 public import Init.Tactics

 public section
--- a/src/Init/Control/EState.lean
+++ b/src/Init/Control/EState.lean
@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Control.State
-public import Init.Control.Except
 public import Init.Data.ToString.Basic

 public section
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -10,7 +10,6 @@ module
 prelude
 public import Init.Control.Basic
 public import Init.Control.Id
-public import Init.Coe

@[expose] public section

--- a/src/Init/Control/Lawful/Basic.lean
+++ b/src/Init/Control/Lawful/Basic.lean
@@ -7,8 +7,6 @@ module

 prelude
 public import Init.Ext
-public import Init.SimpLemmas
-public import Init.Meta

 public section

--- a/src/Init/Control/Lawful/Instances.lean
+++ b/src/Init/Control/Lawful/Instances.lean
@@ -7,14 +7,11 @@ module

 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Control.Except
 import all Init.Control.Except
 public import Init.Control.Option
 import all Init.Control.Option
-public import Init.Control.State
 import all Init.Control.State
 public import Init.Control.StateRef
-public import Init.Ext

 public section

--- a/src/Init/Control/Lawful/Lemmas.lean
+++ b/src/Init/Control/Lawful/Lemmas.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Control.Lawful.Basic
-public import Init.RCases
 public import Init.ByCases

 public section
--- a/src/Init/Control/Lawful/MonadLift/Instances.lean
+++ b/src/Init/Control/Lawful/MonadLift/Instances.lean
@@ -6,17 +6,13 @@ Authors: Quang Dao, Paul Reichert
 module

 prelude
-public import Init.Control.Option
 import all Init.Control.Option
-public import Init.Control.Except
 import all Init.Control.Except
 public import Init.Control.ExceptCps
 import all Init.Control.ExceptCps
-public import Init.Control.StateRef
 import all Init.Control.StateRef
 public import Init.Control.StateCps
 import all Init.Control.StateCps
-public import Init.Control.Id
 import all Init.Control.Id
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.Instances
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Data.Option.Basic
-public import Init.Control.Basic
 public import Init.Control.Except

 public section
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -8,8 +8,6 @@ The Reader monad transformer for passing immutable State.
 module

 prelude
-public import Init.Control.Basic
-public import Init.Control.Id
 public import Init.Control.Except

 public section
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -8,8 +8,6 @@ The State monad transformer.
 module

 prelude
-public import Init.Control.Basic
-public import Init.Control.Id
 public import Init.Control.Except

 public section
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -8,7 +8,6 @@ notation, basic datatypes and type classes
 module

 prelude
-public meta import Init.Prelude
 public import Init.SizeOf

 public section
--- a/src/Init/Data/AC.lean
+++ b/src/Init/Data/AC.lean
@@ -7,7 +7,6 @@ Authors: Dany Fabian
 module

 prelude
-public import Init.Classical
 public import Init.ByCases

@[expose] public section
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -6,10 +6,7 @@ Authors: Joachim Breitner, Mario Carneiro
 module

 prelude
-public import Init.Data.Array.Mem
-public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Count
-public import Init.Data.List.Attach
 import all Init.Data.List.Attach

 public section
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -6,10 +6,6 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.WFTactics
-public import Init.Data.Nat.Basic
-public import Init.Data.Fin.Basic
-public import Init.Data.UInt.BasicAux
 public import Init.GetElem
 public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
--- a/src/Init/Data/Array/BasicAux.lean
+++ b/src/Init/Data/Array/BasicAux.lean
@@ -6,10 +6,8 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Nat.Linear
-public import Init.NotationExtra

 public section

--- a/src/Init/Data/Array/BinSearch.lean
+++ b/src/Init/Data/Array/BinSearch.lean
@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Data.Array.Basic
 public import Init.Data.Int.DivMod.Lemmas
-public import Init.Omega

 public section
 universe u v
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -8,7 +8,6 @@ module

 prelude
 public import Init.Data.List.TakeDrop
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic

 public section
--- a/src/Init/Data/Array/Count.lean
+++ b/src/Init/Data/Array/Count.lean
@@ -6,7 +6,6 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Count
--- a/src/Init/Data/Array/DecidableEq.lean
+++ b/src/Init/Data/Array/DecidableEq.lean
@@ -6,11 +6,9 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.BEq
 public import Init.Data.List.Nat.BEq
-public import Init.ByCases

 public section

--- a/src/Init/Data/Array/Erase.lean
+++ b/src/Init/Data/Array/Erase.lean
@@ -6,11 +6,8 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.Erase
-public import Init.Data.List.Nat.Basic

 public section

--- a/src/Init/Data/Array/Extract.lean
+++ b/src/Init/Data/Array/Extract.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.TakeDrop

 public section

--- a/src/Init/Data/Array/FinRange.lean
+++ b/src/Init/Data/Array/FinRange.lean
@@ -6,7 +6,6 @@ Authors: François G. Dorais
 module

 prelude
-public import Init.Data.List.FinRange
 public import Init.Data.Array.OfFn

 public section
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@@ -7,10 +7,7 @@ module

 prelude
 public import Init.Data.List.Nat.Find
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.Attach
 public import Init.Data.Array.Range

 public section
--- a/src/Init/Data/Array/InsertIdx.lean
+++ b/src/Init/Data/Array/InsertIdx.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.InsertIdx

 public section

--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -6,17 +6,10 @@ Authors: Mario Carneiro, Kim Morrison
 module

 prelude
-public import Init.Data.Nat.Lemmas
-public import Init.Data.List.Range
-public import Init.Data.List.Nat.TakeDrop
-public import Init.Data.List.Nat.Modify
 public import Init.Data.List.Nat.Basic
-public import Init.Data.List.Monadic
-public import Init.Data.List.OfFn
 public import Init.Data.Array.Mem
 public import Init.Data.Array.DecidableEq
 public import Init.Data.Range.Lemmas
-public import Init.TacticsExtra
 public import Init.Data.List.ToArray
 import all Init.Data.List.Control
 import all Init.Data.Array.Basic
@@ -3761,7 +3754,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
 -- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
 grind_pattern contains_iff_exists_mem_beq => xs.contains a

-@[grind _=_]
+@[grind =]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
    xs.contains a ↔ a ∈ xs := by
  simp
--- a/src/Init/Data/Array/Lex/Basic.lean
+++ b/src/Init/Data/Array/Lex/Basic.lean
@@ -6,9 +6,6 @@ Author: Kim Morrison
 module

 prelude
-public import Init.Core
-import Init.Data.Array.Basic
-import Init.Data.Nat.Lemmas
 public import Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Iterators.Consumers
--- a/src/Init/Data/Array/Lex/Lemmas.lean
+++ b/src/Init/Data/Array/Lex/Lemmas.lean
@@ -10,9 +10,7 @@ import all Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Lex
-import Init.Data.Range.Polymorphic.Lemmas
 import Init.Data.Range.Polymorphic.NatLemmas
-import Init.Data.Order.Lemmas

 public section

--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -6,10 +6,7 @@ Authors: Mario Carneiro, Kim Morrison
 module

 prelude
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.Attach
 public import Init.Data.Array.OfFn
 public import Init.Data.List.MapIdx
 import all Init.Data.List.MapIdx
--- a/src/Init/Data/Array/Mem.lean
+++ b/src/Init/Data/Array/Mem.lean
@@ -6,8 +6,6 @@ Authors: Leonardo de Moura, Joachim Breitner
 module

 prelude
-public import Init.Data.Array.Basic
-public import Init.Data.Nat.Linear
 public import Init.Data.List.BasicAux

 public section
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -6,13 +6,9 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.List.Control
 import all Init.Data.List.Control
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
-public import Init.Data.List.Monadic

 public section

--- a/src/Init/Data/Array/OfFn.lean
+++ b/src/Init/Data/Array/OfFn.lean
@@ -6,11 +6,8 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Monadic
-public import Init.Data.List.OfFn
 public import Init.Data.List.FinRange

 public section
--- a/src/Init/Data/Array/Perm.lean
+++ b/src/Init/Data/Array/Perm.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Data.List.Nat.Perm
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas

--- a/src/Init/Data/Array/Range.lean
+++ b/src/Init/Data/Array/Range.lean
@@ -6,14 +6,10 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.Array.Lemmas
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
-public import Init.Data.Array.OfFn
 import all Init.Data.Array.OfFn
 public import Init.Data.Array.MapIdx
 public import Init.Data.Array.Zip
-public import Init.Data.List.Nat.Range

 public section

--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.GetElem
 public import Init.Data.Array.Basic
 import Init.Data.Array.GetLit
 public import Init.Data.Slice.Basic
--- a/src/Init/Data/Array/Subarray/Split.lean
+++ b/src/Init/Data/Array/Subarray/Split.lean
@@ -7,7 +7,6 @@ Authors: David Thrane Christiansen
 module

 prelude
-public import Init.Data.Array.Basic
 public import Init.Data.Array.Subarray
 import all Init.Data.Array.Subarray
 public import Init.Omega
--- a/src/Init/Data/Array/TakeDrop.lean
+++ b/src/Init/Data/Array/TakeDrop.lean
@@ -6,10 +6,8 @@ Authors: Markus Himmel
 module

 prelude
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.TakeDrop

 public section

--- a/src/Init/Data/Array/Zip.lean
+++ b/src/Init/Data/Array/Zip.lean
@@ -6,10 +6,8 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.TakeDrop
-public import Init.Data.List.Zip

 public section

--- a/src/Init/Data/Basic.lean
+++ b/src/Init/Data/Basic.lean
@@ -6,13 +6,5 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Data.Nat.Basic
-public import Init.Data.Fin.Basic
-public import Init.Data.List.Basic
-public import Init.Data.Char.Basic
-public import Init.Data.String.Basic
-public import Init.Data.Option.Basic
 public import Init.Data.UInt
-public import Init.Data.Repr
-public import Init.Data.ToString.Basic
 public import Init.Data.String.Extra
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -6,11 +6,8 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module

 prelude
-public import Init.Data.Fin.Basic
 public import Init.Data.Nat.Bitwise.Lemmas
-public import Init.Data.Nat.Power2
 public import Init.Data.Int.Bitwise.Basic
-public import Init.Data.BitVec.BasicAux

@[expose] public section

--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -6,16 +6,11 @@ Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 module

 prelude
-public import Init.Data.Nat.Bitwise.Basic
 import all Init.Data.Nat.Bitwise.Basic
-public import Init.Data.Nat.Mod
 public import Init.Data.Int.DivMod
 import all Init.Data.Int.DivMod
-public import Init.Data.Int.LemmasAux
-public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Decidable
-public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
 import Init.BinderPredicates

--- a/src/Init/Data/BitVec/Folds.lean
+++ b/src/Init/Data/BitVec/Folds.lean
@@ -6,10 +6,8 @@ Authors: Joe Hendrix, Harun Khan
 module

 prelude
-public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Lemmas
-public import Init.Data.Nat.Lemmas
 public import Init.Data.Fin.Iterate

 public section
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -6,25 +6,14 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B
 module

 prelude
-public import Init.Data.Bool
-public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
-public import Init.Data.BitVec.BasicAux
 import all Init.Data.BitVec.BasicAux
 public import Init.Data.Fin.Lemmas
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Nat.Div.Lemmas
-public import Init.Data.Nat.Mod
-public import Init.Data.Nat.Div.Lemmas
 public import Init.Data.Int.Bitwise.Lemmas
 public import Init.Data.Int.LemmasAux
-public import Init.Data.Int.Pow
-public import Init.Data.Int.LemmasAux
 public import Init.Data.BitVec.Bootstrap
-public import Init.Data.Order.Factories
 public import Init.Data.List.BasicAux
 import Init.Data.List.Lemmas
-import Init.Data.BEq

 public section

--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -6,11 +6,8 @@ Author: Leonardo de Moura
 module

 prelude
-public import Init.Data.Array.DecidableEq
 public import Init.Data.UInt.Basic
-public import Init.Data.UInt.BasicAux
 import all Init.Data.UInt.BasicAux
-public import Init.Data.Option.Basic
 public import Init.Data.Array.Extract

 set_option doc.verso true
--- a/src/Init/Data/ByteArray/Bootstrap.lean
+++ b/src/Init/Data/ByteArray/Bootstrap.lean
@@ -6,7 +6,6 @@ Author: Markus Himmel
 module

 prelude
-public import Init.Prelude
 public import Init.Data.List.Basic

 public section
--- a/src/Init/Data/ByteArray/Lemmas.lean
+++ b/src/Init/Data/ByteArray/Lemmas.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Data.ByteArray.Basic
-public import Init.Data.Array.Extract

 public section

@@ -257,3 +256,19 @@ theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : B
      dest.extract 0 destOff ++ src.extract srcOff (srcOff +len) ++ dest.extract (destOff + min len (src.data.size - srcOff)) dest.data.size := by
  ext1
  simp [copySlice]
+
+@[simp]
+theorem ByteArray.data_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} :
+    (as.set i a h).data = as.data.set i a (by simpa) := by
+  simp [set]
+
+theorem ByteArray.set_eq_push_extract_append_extract {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} :
+    as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size := by
+  ext1
+  simpa using Array.set_eq_push_extract_append_extract _
+
+@[simp]
+theorem ByteArray.append_toByteArray_singleton {as : ByteArray} {a : UInt8} :
+    as ++ [a].toByteArray = as.push a := by
+  ext1
+  simp
--- a/src/Init/Data/Char/Lemmas.lean
+++ b/src/Init/Data/Char/Lemmas.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Data.Char.Basic
 import all Init.Data.Char.Basic
 public import Init.Data.UInt.Lemmas

--- a/src/Init/Data/Dyadic/Basic.lean
+++ b/src/Init/Data/Dyadic/Basic.lean
@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Rat.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
-import Init.Data.Int.DivMod.Lemmas
 import Init.Hints

 /-!
--- a/src/Init/Data/Dyadic/Instances.lean
+++ b/src/Init/Data/Dyadic/Instances.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Data.Dyadic.Basic
-public import Init.Grind.Ring.Basic
 public import Init.Grind.Ordered.Ring

 /-! # Internal `grind` algebra instances for `Dyadic`. -/
--- a/src/Init/Data/Dyadic/Inv.lean
+++ b/src/Init/Data/Dyadic/Inv.lean
@@ -5,7 +5,6 @@ Authors: Kim Morrison
 -/
 module
 prelude
-import Init.Data.Dyadic.Basic
 import Init.Data.Dyadic.Round
 import Init.Grind.Ordered.Ring

--- a/src/Init/Data/Dyadic/Round.lean
+++ b/src/Init/Data/Dyadic/Round.lean
@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Dyadic.Basic
 import all Init.Data.Dyadic.Instances
-import Init.Data.Int.Bitwise.Lemmas
 import Init.Grind.Ordered.Rat
 import Init.Grind.Ordered.Field

--- a/src/Init/Data/Fin/Bitwise.lean
+++ b/src/Init/Data/Fin/Bitwise.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.Data.Nat.Bitwise
-public import Init.Data.Fin.Basic

 public section

--- a/src/Init/Data/Fin/Fold.lean
+++ b/src/Init/Data/Fin/Fold.lean
@@ -6,7 +6,6 @@ Authors: François G. Dorais
 module

 prelude
-public import Init.Data.Nat.Linear
 public import Init.Control.Lawful.Basic
 public import Init.Data.Fin.Lemmas

--- a/src/Init/Data/Fin/Iterate.lean
+++ b/src/Init/Data/Fin/Iterate.lean
@@ -7,7 +7,6 @@ module

 prelude
 public import Init.PropLemmas
-public import Init.Data.Fin.Basic

 public section

--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -8,10 +8,6 @@ module
 prelude
 public import Init.Data.Nat.Lemmas
 public import Init.Ext
-public import Init.ByCases
-public import Init.Conv
-public import Init.Omega
-public import Init.Data.Order.Factories
 import Init.Data.Order.Lemmas

@[expose] public section
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -6,8 +6,6 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Core
-public import Init.Data.Int.Basic
 public import Init.Data.ToString.Basic

 public section
--- a/src/Init/Data/Float32.lean
+++ b/src/Init/Data/Float32.lean
@@ -6,9 +6,6 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Core
-public import Init.Data.Int.Basic
-public import Init.Data.ToString.Basic
 public import Init.Data.Float

 public section
--- a/src/Init/Data/FloatArray/Basic.lean
+++ b/src/Init/Data/FloatArray/Basic.lean
@@ -6,9 +6,7 @@ Author: Leonardo de Moura
 module

 prelude
-public import Init.Data.Array.Basic
 public import Init.Data.Float
-public import Init.Data.Option.Basic
 import Init.Ext
 public import Init.Data.Array.DecidableEq

--- a/src/Init/Data/Format/Instances.lean
+++ b/src/Init/Data/Format/Instances.lean
@@ -6,9 +6,7 @@ Author: Leonardo de Moura
 module

 prelude
-public import Init.Data.Format.Basic
 public import Init.Data.Array.Basic
-public import Init.Data.ToString.Basic
 import Init.Data.String.Basic

 public section
--- a/src/Init/Data/Format/Syntax.lean
+++ b/src/Init/Data/Format/Syntax.lean
@@ -9,7 +9,6 @@ prelude
 public import Init.Data.Format.Macro
 public import Init.Data.Format.Instances
 public import Init.Meta
-import Init.Data.String.Basic
 import Init.Data.ToString.Name

 public section
--- a/src/Init/Data/Function.lean
+++ b/src/Init/Data/Function.lean
@@ -5,7 +5,6 @@ Authors: Kim Morrison
 -/
 module
 prelude
-public import Init.Core
 public import Init.Grind.Tactics
 public section
 namespace Function
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Data.UInt.Basic
 public import Init.Data.String.Basic
-public import Init.Data.ByteArray.Basic

 public section
 universe u
--- a/src/Init/Data/Int/Cooper.lean
+++ b/src/Init/Data/Int/Cooper.lean
@@ -6,7 +6,6 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.Int.DivMod.Lemmas
 public import Init.Data.Int.Gcd

 public section
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -6,13 +6,7 @@ Authors: Jeremy Avigad, Mario Carneiro, Kim Morrison, Markus Himmel
 module

 prelude
-public import Init.Data.Int.DivMod.Bootstrap
-public import Init.Data.Nat.Lemmas
 public import Init.Data.Nat.Div.Lemmas
-public import Init.Data.Int.Order
-public import Init.Data.Int.Lemmas
-public import Init.Data.Nat.Dvd
-public import Init.RCases
 import Init.TacticsExtra

 public section
--- a/src/Init/Data/Int/Gcd.lean
+++ b/src/Init/Data/Int/Gcd.lean
@@ -6,8 +6,6 @@ Authors: Mario Carneiro, Markus Himmel
 module

 prelude
-public import Init.Data.Int.Basic
-public import Init.Data.Nat.Gcd
 public import Init.Data.Nat.Lcm
 public import Init.Data.Int.DivMod.Lemmas
 public import Init.Data.Int.Pow
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -6,8 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module

 prelude
-public import Init.Conv
-public import Init.NotationExtra
 public import Init.PropLemmas

 public section
--- a/src/Init/Data/Int/LemmasAux.lean
+++ b/src/Init/Data/Int/LemmasAux.lean
@@ -6,9 +6,7 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.Int.Order
 public import Init.Data.Int.Pow
-public import Init.Omega

 public section

--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -6,15 +6,9 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.ByCases
-public import Init.Data.Prod
-public import Init.Data.Int.Lemmas
 public import Init.Data.Int.LemmasAux
-public import Init.Data.Int.DivMod.Bootstrap
 public import Init.Data.Int.Cooper
-public import Init.Data.Int.Gcd
 import all Init.Data.Int.Gcd
-public import Init.Data.RArray
 public import Init.Data.AC
 import all Init.Data.AC
 import Init.LawfulBEqTactics
--- a/src/Init/Data/Int/OfNat.lean
+++ b/src/Init/Data/Int/OfNat.lean
@@ -6,11 +6,8 @@ Authors: Leonardo de Moura
 module

 prelude
-public import Init.Data.Int.Lemmas
-public import Init.Data.Int.DivMod
 public import Init.Data.Int.Linear
 public import Init.GrindInstances.ToInt
-public import Init.Data.RArray

 public section

--- a/src/Init/Data/Int/Pow.lean
+++ b/src/Init/Data/Int/Pow.lean
@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module

 prelude
-public import Init.Data.Int.Lemmas
 public import Init.Data.Nat.Lemmas

 public section
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -6,11 +6,8 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Core
 public import Init.Classical
 public import Init.Ext
-public import Init.NotationExtra
-public import Init.TacticsExtra

 set_option doc.verso true

--- a/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/Attach.lean
@@ -6,9 +6,7 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Internal.Termination
-public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop

 public section
--- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -6,8 +6,6 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Data.Iterators.Basic
-public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.PostconditionMonad
 public import Init.Data.Iterators.Internal.Termination
--- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic

--- a/src/Init/Data/Iterators/Consumers/Access.lean
+++ b/src/Init/Data/Iterators/Consumers/Access.lean
@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Data.Iterators.Consumers.Partial
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Monadic.Access

--- a/src/Init/Data/Iterators/Consumers/Collect.lean
+++ b/src/Init/Data/Iterators/Consumers/Collect.lean
@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Consumers.Partial
 public import Init.Data.Iterators.Consumers.Monadic.Collect

--- a/src/Init/Data/Iterators/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Loop.lean
@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Monadic.Loop
-public import Init.Data.Iterators.Consumers.Partial

 public section

--- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean
@@ -6,8 +6,6 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.RCases
-public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Consumers.Monadic.Partial
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction

--- a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean
+++ b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean
@@ -6,9 +6,6 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Control.Basic
-public import Init.Control.Lawful.Basic
-public import Init.NotationExtra
 public import Init.Control.Lawful.MonadLift

 public section
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean
@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Iterators.Combinators.Attach
 import all Init.Data.Iterators.Combinators.Attach
-public import Init.Data.Iterators.Combinators.Monadic.Attach
 import all Init.Data.Iterators.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -6,10 +6,8 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic
-public import Init.Data.Iterators.Consumers.Monadic.Collect
 import all Init.Data.Iterators.Consumers.Monadic.Collect

 public section
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean
@@ -10,7 +10,6 @@ public import Init.Data.Iterators.Lemmas.Basic
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 public import Init.Data.Iterators.Consumers.Access
 import all Init.Data.Iterators.Consumers.Access
-public import Init.Data.Iterators.Consumers.Collect
 import all Init.Data.Iterators.Consumers.Collect

 public section
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -6,13 +6,10 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Control.Lawful.MonadLift.Instances
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
 import all Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
-public import Init.Data.Iterators.Consumers.Loop
 import all Init.Data.Iterators.Consumers.Loop
-public import Init.Data.Iterators.Consumers.Monadic.Collect
 import all Init.Data.Iterators.Consumers.Monadic.Collect
 import Init.Data.Array.Monadic

--- a/src/Init/Data/Iterators/ToIterator.lean
+++ b/src/Init/Data/Iterators/ToIterator.lean
@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module

 prelude
-public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop

 public section
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -6,11 +6,9 @@ Authors: Mario Carneiro
 module

 prelude
-public import Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
 import all Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
 public import Init.Data.List.Count
 public import Init.Data.Subtype.Basic
-public import Init.BinderNameHint

 public section

--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -6,8 +6,6 @@ Author: Leonardo de Moura
 module

 prelude
-public import Init.SimpLemmas
-public import Init.Data.Nat.Basic
 public import Init.Data.List.Notation
 public import Init.Data.Nat.Div.Basic

--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -6,8 +6,6 @@ Author: Leonardo de Moura
 module

 prelude
-public import Init.Control.Basic
-public import Init.Control.Id
 public import Init.Control.Lawful

 public section
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -7,7 +7,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module

 prelude
-public import Init.Data.List.Pairwise
 public import Init.Data.List.Find

 public section
--- a/src/Init/Data/List/FinRange.lean
+++ b/src/Init/Data/List/FinRange.lean
@@ -6,7 +6,6 @@ Authors: François G. Dorais
 module

 prelude
-public import Init.Data.List.OfFn
 import all Init.Data.List.OfFn
 public import Init.Data.List.Monadic

--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -7,11 +7,8 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module

 prelude
-public import Init.Data.List.Lemmas
-public import Init.Data.List.Sublist
 public import Init.Data.List.Range
 public import Init.Data.List.Impl
-public import Init.Data.List.Attach
 import all Init.Data.List.Attach
 public import Init.Data.Fin.Lemmas

--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -7,13 +7,11 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module

 prelude
-public import Init.Data.Bool
 public import Init.Data.Option.Lemmas
 public import Init.Data.List.BasicAux
 import all Init.Data.List.BasicAux
 public import Init.Data.List.Control
 import all Init.Data.List.Control
-public import Init.Control.Lawful.Basic
 public import Init.BinderPredicates

 public section
@@ -2932,7 +2930,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
 -- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
 grind_pattern contains_iff_exists_mem_beq => l.contains a

-@[grind _=_]
+@[grind =]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
    l.contains a ↔ a ∈ l := by
  simp
--- a/src/Init/Data/List/Lex.lean
+++ b/src/Init/Data/List/Lex.lean
@@ -6,9 +6,7 @@ Authors: Kim Morrison
 module

 prelude
-public import Init.Data.List.Lemmas
 public import Init.Data.List.Nat.TakeDrop
-public import Init.Data.Order.Factories
 import Init.Data.Order.Lemmas

 public section
--- a/src/Init/Data/List/MapIdx.lean
+++ b/src/Init/Data/List/MapIdx.lean
@@ -7,10 +7,7 @@ Authors: Kim Morrison, Mario Carneiro
 module

 prelude
-public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Range
-public import Init.Data.List.OfFn
-public import Init.Data.Fin.Lemmas
 public import Init.Data.Option.Attach

 public section
--- a/src/Init/Data/List/MinMax.lean
+++ b/src/Init/Data/List/MinMax.lean
@@ -6,9 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module

 prelude
-public import Init.Data.List.Lemmas
 public import Init.Data.List.Pairwise
-public import Init.Data.Order.Factories
 public import Init.Data.Subtype.Order
 import Init.Data.Order.Lemmas

--- a/src/Init/Data/List/Monadic.lean
+++ b/src/Init/Data/List/Monadic.lean
@@ -6,11 +6,9 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module

 prelude
-public import Init.Data.List.TakeDrop
 public import Init.Data.List.Attach
 public import Init.Data.List.OfFn
 public import Init.Data.Array.Bootstrap
-public import Init.Data.List.Control
 import all Init.Data.List.Control

 public section
--- a/Show More
+++ b/Show More
Author	SHA1	Message	Date
Kim Morrison	fd470dab48	chore: tweak error message about weak options	2025-10-20 04:21:19 +02:00
Leonardo de Moura	823671f744	feat: `set_option` tactic in `grind` interactive mode (#10843 ) This PR implements the `set_option` tactic in `grind` interactive mode.	2025-10-20 00:44:59 +00:00
Leonardo de Moura	681724a8cf	feat: generate `instantiate only [...]` at `finish?` (#10841 ) This PR improves the `grind` tactic generated by the `instantiate` action in tracing mode. It also updates the syntax for the `instantiate` tactic, making it similar to `simp`. For example: * `instantiate only [thm1, thm2]` instantiates only theorems `thm1` and `thm2`. * `instantiate [thm1, thm2]` instantiates theorems marked with the `@[grind]` attribute and theorems `thm1` and `thm2`. The action produces `instantiate only [...]` tactics. Example: ```lean /-- info: Try this: [apply] ⏎ instantiate only [= Array.getElem_set] instantiate only [= Array.getElem_set] -/ #guard_msgs in example (as bs cs : Array α) (v₁ v₂ : α) (i₁ i₂ j : Nat) (h₁ : i₁ < as.size) (h₂ : bs = as.set i₁ v₁) (h₃ : i₂ < bs.size) (h₄ : cs = bs.set i₂ v₂) (h₅ : i₁ ≠ j ∧ i₂ ≠ j) (h₆ : j < cs.size) (h₇ : j < as.size) : cs[j] = as[j] := by grind => finish? ``` Recall that `finish?` replays generated tactics before suggesting them. The `instantiate` action inspects the generated proof term to decide which theorems to include as parameters in the `instantiate only [...]` tactic. However, in some cases, a theorem contributes only by adding a term to the state. In such cases, the generated tactic cannot be fully replayed, and the action uses `instantiate approx [<thms instantiated>]` to indicate which parts of the tactic script are approximate. The `approx` is just a hint for users.	2025-10-19 23:35:27 +00:00
Lean stage0 autoupdater	28dd72d514	chore: update stage0	2025-10-19 23:45:51 +00:00
Leonardo de Moura	61ee3b2711	feat: expose `optionValue` parser (#10839 ) This PR exposes the `optionValue` parser used to implement the `set_option` notation.	2025-10-19 22:57:47 +00:00
Leonardo de Moura	206eb73cd9	feat: `finish?` tactic for `grind` interactive mode (#10837 ) This PR implements the `finish?` tactic for the `grind` interactive mode. When it successfully closes the goal, it produces a code action that allows the user to close the goal using explicit grind tactic steps, i.e., without any search. It also makes explicit which solvers have been used. This is just the first version, we will add many "bells and whistles" later. For example, `instantiate` steps will clearly show which theorems have been instantiated. Example: ```lean /-- info: Try this: [apply] ⏎ cases #b0f4 next => cases #50fc next => cases #50fc <;> lia -/ #guard_msgs in example (p : Nat → Prop) (x y z w : Int) : (x = 1 ∨ x = 2) → (w = 1 ∨ w = 4) → (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) → (z = 1 ∨ z = 0) → x + y ≤ 6 := by grind => finish? ``` The anchors in the generated script are based on stable hash codes. Moreover, users can hover over them to see the exact term used in the case split. `grind?` will also be implemented using the new framework.	2025-10-19 03:52:32 +00:00
Leonardo de Moura	09f22203f8	feat: add `SolverExtension.action` and `Solvers.mkAction` (#10836 ) This PR implements support for `Action` in the `grind` solver extensions (`SolverExtension`). It also provides the `Solvers.mkAction` function that constructs an `Action` using all registered solvers. The generated action is "fair," that is, a solver cannot prevent other solvers from making progress.	2025-10-19 00:53:45 +00:00
Leonardo de Moura	ef23782608	feat: `ring` action (#10834 ) This PR implements the `ring` action for `grind`.	2025-10-18 22:01:51 +00:00
Leonardo de Moura	e2b5747f4b	feat: `evalTactic` in `GrindM` (#10833 ) This PR implements infrastructure for evaluating `grind` tactics in the `GrindM` monad. We are going to use it to check whether auto-generated tactics can effectively close the original goal.	2025-10-18 17:02:36 +00:00
Markus Himmel	dad541265c	refactor: move operations on `String.Pos.Raw` to the `String.Pos.Raw` namespace (#10735 ) This PR moves many operations involving `String.Pos.Raw` to a the `String.Pos.Raw` namespace with the eventual aim of freeing up the `String` namespace to contain operations using `String.ValidPos` (to be renamed to `String.Pos`) instead. This PR adds the `String.ValidPos.set` and `String.ValidPos.modify` functions. After this PR, `String.pos_lt_eq` is no longer a `simp` lemma. Add `String.Pos.Raw.lt_iff` as a `simp` lemma if your proofs break.	2025-10-18 12:12:55 +00:00
Markus Himmel	ca7a8e18b7	refactor: rename `String.split` to `String.splitToList` (#10822 ) This PR renames `String.split` to `String.splitToList`, because soon the name `String.split` will be used by a new implementation which is superior because it is polymorphic over the pattern kind and it returns an iterator of slices instead of a list of strings.	2025-10-18 12:12:54 +00:00
Sebastian Ullrich	721ffe5713	chore: CI: disable tree-less clone on nightly release	2025-10-18 13:32:04 +02:00
Leonardo de Moura	c76411d6c5	feat: compact notation for inspecting `grind` state (#10828 ) This PR implements a compact notation for inspecting the `grind` state in interactive mode. Within a `grind` tactic block, each tactic may optionally have a suffix of the form `\| filter?`. Examples: ```lean instantiate \| gen > 0 -- Displays terms in the `grind` state after executing `instantiate` with generation greater than zero ``` ```lean instantiate \| -- Displays the `grind` state after executing `instantiate` ``` Remark: If the user places the cursor one space before `\|`, the state before executing `instantiate` is displayed. This PR removes the code that was silently displaying the `grind` state after each tactic step, as it was too noisy. It also updates the notation for the `first` combinator in the `grind` tactic mode to avoid conflicts with the new syntax.	2025-10-17 19:54:23 +00:00
Joachim Breitner	c22100036c	fix: more pedantic checking of inaccessible patterns (#10796 ) This PR changes match compilation to reject some pattern matches that were previously accepted due to inaccessible patterns sometimes treated like accessible ones. Fixes #10794.	2025-10-17 17:02:54 +00:00
Sebastian Ullrich	5800ce17b3	chore: CI: upgrade all git checkouts to tree-less clones (#10814 )	2025-10-17 16:23:42 +00:00
Leonardo de Moura	78ab60d045	feat: `cases?` tactic for `grind` interactive mode (#10824 ) This PR implements the `cases?` tactic for the `grind` interactive mode. It provides a convenient way to select anchors. Users can filter the candidates using the filter language. Examples: <img width="1454" height="399" alt="image" src="https://github.com/user-attachments/assets/fc370c2e-97f9-4d68-93a6-f0ebf33499f8" /> <img width="1447" height="166" alt="image" src="https://github.com/user-attachments/assets/6c9c3707-79f7-4c63-8007-8d0aaedecc45" />	2025-10-17 15:44:19 +00:00
Sofia Rodrigues	f9adafe54d	feat: adds `acceptSelector` and modified selectors (#10667 ) This PR adds more selectors for TCP and Signals. It also fixes a problem with `Selectors` that they cannot be closures over a promise, otherwise it causes the waiter promise to never be dropped.	2025-10-17 14:53:46 +00:00
Sebastian Ullrich	69d8d63d58	feat: hint about inaccessible private declaration on dot notation failure (#10803 ) This PR improves the error message of generalized field notation if the issue is that the resolved declaration is not visible in the current context.	2025-10-17 09:31:56 +00:00
Sebastian Ullrich	dc7c184ee2	chore: CI: introduce `fast-ci` label	2025-10-17 08:45:41 +02:00
Sebastian Ullrich	e43ff50e76	chore: CI: revert macOS tests accidentally run on PRs	2025-10-17 08:45:41 +02:00
Leonardo de Moura	4ce7ad19ce	feat: `lia`, `linarith`, and `ac` actions (#10812 ) This PR implements `lia`, `linarith`, and `ac` actions for `grind` interactive mode.	2025-10-17 03:56:21 +00:00
Leonardo de Moura	2a70da50c1	feat: proper case-split anchor generation in `splitNext` for `grind?` and `finish?` (#10811 ) This PR implements proper case-split anchor generation in the `splitNext` action, which will be used to implement `grind?` and `finish?`.	2025-10-17 03:07:13 +00:00
Kim Morrison	effde06296	chore: add public modifiers in Lean.Elab.Tactic.Induction (#10810 )	2025-10-16 21:52:02 +00:00
Kim Morrison	127fe785a3	chore: add public modifiers in Lean.Elab.Tactic.Ext (#10809 ) This PR restores further definitions to `public`, after #10699.	2025-10-16 21:48:41 +00:00
Sebastian Ullrich	663df8f7e8	feat: `backward.privateInPublic` option (#10807 ) This PR introduces the `backward.privateInPublic` option to aid in porting projects to the module system by temporarily allowing access to private declarations from the public scope, even across modules. A warning will be generated by such accesses unless `backward.privateInPublic.warn` is disabled.	2025-10-16 20:51:45 +00:00
Sebastian Ullrich	428355cf02	chore: remove redundant imports in core (#10750 )	2025-10-16 20:27:46 +00:00
Sebastian Ullrich	83126883d9	chore: CI: overhaul check level logic (#10806 ) The logic was still wrong after two PRs so let's get rid of `check-level` as a matrix entry and trust in simple bools.	2025-10-16 20:27:02 +00:00
Sebastian Ullrich	5c7b003191	chore: lean.code-workspace: fix terminal cwd (#10802 )	2025-10-16 20:19:12 +00:00
Leonardo de Moura	8a1b6e0f71	feat: compress generated `grind` tactic sequences using `<;>` (#10808 ) This PR implements support for compressing auto-generated `grind` tactic sequences.	2025-10-16 18:14:33 +00:00
Leonardo de Moura	7087c4a039	feat: add `splitNext` `grind` action (#10801 ) This PR implements the `splitNext` action for `grind`.	2025-10-16 17:28:14 +00:00
Rob23oba	b7ea66d8d3	fix: consider underscores in `getHexNumSize` (#10719 ) This PR fixes `getHexNumSize` to consider underscores. Previously, only the amount of bytes was counted, making it output 9 for `1234_abcd` instead of the actual number of digits, which is 8.	2025-10-16 13:57:58 +00:00
Joachim Breitner	10d6232594	chore: remove test for #10766 (#10804 ) the tested situation (kernel runs into deep recursion but elaborator is happy) is not very stable and depends on, for example, stack size. This test is not worth that hassle.	2025-10-16 11:11:29 +00:00
Wojciech Różowski	5b35d6192c	feat: redefine HashSet.union and add lemmas (#10611 ) This PR adds adds union operation on `DHashMap`/`HashMap`/`HashSet` and their raw variants and provides lemmas about union operations. --------- Co-authored-by: Paul-Lez <paul.lezeau@gmail.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Markus Himmel <markus@himmel-villmar.de>	2025-10-16 08:43:01 +00:00
Joachim Breitner	8748031853	fix: only run `processInaccessibleAsCtor` if there is at least one constructor around (#10793 ) This PR fixes #10792.	2025-10-16 08:20:55 +00:00
Marc Huisinga	ac499323af	chore: add .vscode/settings.json to .gitignore (#10795 ) This PR adds `.vscode/settings.json` to our `.gitignore`, which allows Lean 4 developers to set local workspace settings. We already use the the workspace file for settings in core, so this shouldn't cause any problems.	2025-10-16 07:08:41 +00:00
Kim Morrison	def3c97dbf	chore: make `extCore` and `customEliminators` public for Batteries (#10799 ) This PR restores two declarations to `public`, that were made non-public in #10699, apparently breaking Batteries.	2025-10-16 05:01:23 +00:00
Kim Morrison	8db3969f87	chore: remove bad grind _=_ annotation on List.contains_iff_mem (#10800 )	2025-10-16 04:00:42 +00:00