chore: remove unneeded Batteries reference in repeat doc-string

this fixes a usability paper cut that just annoyed me. When editing a
larger simp proof, I usually want to see the goal state after the simp,
and this is what I see while the `simp` command is complete. But then,
when I start typing, and necessarily type incomplete lemma names, that
error makes `simp` do nothing again and I see the original goal state.
In fact, if a prefix of the simp theorem name I am typing is a valid
identifier, it jumps even more around.

With this PR, using `logException`, I still get the red squiggly lines
for the unknown identifer, but `simp` just ignores that argument and
still shows me the final goal. Much nicer.

I also demoted the message for `[-foo]` when `foo` isn’t `simp` to a
warning and gave it the correct `ref`.

See it in action here: (in the middle, when you suddenly see the
terminal,
I am switching lean versions.)


https://github.com/leanprover/lean4/assets/148037/8cb3c563-1354-4c2d-bcee-26dfa1005ae0

.github/workflows/ci.yml

@@ -20,8 +20,10 @@ jobs:
   configure:
     runs-on: ubuntu-latest
     outputs:
-      # Should we run only a quick CI? Yes on a pull request without the full-ci label
-      quick: ${{ steps.set-quick.outputs.quick }}
+      # 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.result }}
       # Should we make a nightly release? If so, this output contains the lean version string, else it is empty
@@ -38,167 +40,6 @@ jobs:
       RELEASE_TAG: ${{ steps.set-release.outputs.RELEASE_TAG }}
 
     steps:
-      - name: Run quick CI?
-        id: set-quick
-        # We do not use github.event.pull_request.labels.*.name here because
-        # re-running a run does not update that list, and we do want to be able to
-        # rerun the workflow run after settings the `full-ci` label.
-        run: |
-          if [ "${{ github.event_name }}" == 'pull_request' ]
-          then
-            echo "quick=$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels | any(.name == "full-ci") | not')" >> "$GITHUB_OUTPUT"
-          else
-            echo "quick=false" >> "$GITHUB_OUTPUT"
-          fi
-        env:
-          GH_TOKEN: ${{ github.token }}
-
-      - name: Configure build matrix
-        id: set-matrix
-        uses: actions/github-script@v7
-        with:
-          script: |
-            const quick = ${{ steps.set-quick.outputs.quick }};
-            console.log(`quick: ${quick}`);
-            // use large runners outside PRs where available (original repo)
-            // disabled for now as this mostly just speeds up the test suite which is not a bottleneck
-            // let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
-            let matrix = [
-              {
-                // portable release build: use channel with older glibc (2.27)
-                "name": "Linux LLVM",
-                "os": "ubuntu-latest",
-                "release": false,
-                "quick": false,
-                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
-                "binary-check": "ldd -v",
-                // foreign code may be linked against more recent glibc
-                // reverse-ffi needs to be updated to link to LLVM libraries
-                "CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
-                "CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
-              },
-              {
-                "name": "Linux release",
-                "os": "ubuntu-latest",
-                "release": true,
-                "quick": true,
-                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
-                "binary-check": "ldd -v",
-                // foreign code may be linked against more recent glibc
-                "CTEST_OPTIONS": "-E 'foreign'"
-              },
-              {
-                "name": "Linux",
-                "os": "ubuntu-latest",
-                "check-stage3": true,
-                "test-speedcenter": true,
-                "quick": false,
-              },
-              {
-                "name": "Linux Debug",
-                "os": "ubuntu-latest",
-                "quick": false,
-                "CMAKE_OPTIONS": "-DCMAKE_BUILD_TYPE=Debug",
-                // exclude seriously slow tests
-                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
-              },
-              // TODO: suddenly started failing in CI
-              /*{
-                "name": "Linux fsanitize",
-                "os": "ubuntu-latest",
-                "quick": false,
-                // turn off custom allocator & symbolic functions to make LSAN do its magic
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
-                // exclude seriously slow/problematic tests (laketests crash)
-                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
-              },*/
-              {
-                "name": "macOS",
-                "os": "macos-13",
-                "release": true,
-                "quick": false,
-                "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
-                "binary-check": "otool -L",
-                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
-              },
-              {
-                "name": "macOS aarch64",
-                "os": "macos-13",
-                "release": true,
-                "quick": false,
-                "cross": true,
-                "cross_target": "aarch64-apple-darwin",
-                "shell": "bash -euxo pipefail {0}",
-                "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-*",
-                "binary-check": "otool -L",
-                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
-              },
-              {
-                "name": "Windows",
-                "os": "windows-2022",
-                "release": true,
-                "quick": false,
-                "shell": "msys2 {0}",
-                "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
-                // for reasons unknown, interactivetests are flaky on Windows
-                "CTEST_OPTIONS": "--repeat until-pass:2",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
-                "binary-check": "ldd"
-              },
-              {
-                "name": "Linux aarch64",
-                "os": "ubuntu-latest",
-                "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
-                "release": true,
-                "quick": false,
-                "cross": true,
-                "cross_target": "aarch64-unknown-linux-gnu",
-                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
-              },
-              {
-                "name": "Linux 32bit",
-                "os": "ubuntu-latest",
-                // Use 32bit on stage0 and stage1 to keep oleans compatible
-                "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",
-                "cmultilib": true,
-                "release": true,
-                "quick": false,
-                "cross": true,
-                "shell": "bash -euxo pipefail {0}"
-              },
-              {
-                "name": "Web Assembly",
-                "os": "ubuntu-latest",
-                // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
-                "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32",
-                "wasm": true,
-                "cmultilib": true,
-                "release": true,
-                "quick": false,
-                "cross": true,
-                "shell": "bash -euxo pipefail {0}",
-                // Just a few selected tests because wasm is slow
-                "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean\""
-              }
-            ];
-            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
-            if (quick) {
-              return matrix.filter((job) => job.quick)
-            } else {
-              return matrix
-            }
-
       - name: Checkout
         uses: actions/checkout@v3
         # don't schedule nightlies on forks
@@ -249,6 +90,171 @@ jobs:
             echo "Tag ${TAG_NAME} did not match SemVer regex."
           fi
 
+      - name: Set check level
+        id: set-level
+        # We do not use github.event.pull_request.labels.*.name here because
+        # re-running a run does not update that list, and we do want to be able to
+        # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
+        run: |
+          check_level=0
+
+          if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" ]]; then
+            check_level=2
+          elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
+            check_level=1
+          else
+            labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }}) --jq '.labels'"
+            if echo "$labels" | grep -q "release-ci"; then
+              check_level=2
+            elif echo "$labels" | grep -q "merge-ci"; then
+              check_level=1
+            fi
+          fi
+
+          echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
+        env:
+          GH_TOKEN: ${{ github.token }}
+
+      - name: Configure build matrix
+        id: set-matrix
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const level = ${{ steps.set-level.outputs.check-level }};
+            console.log(`level: ${level}`);
+            // use large runners outside PRs where available (original repo)
+            // disabled for now as this mostly just speeds up the test suite which is not a bottleneck
+            // let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
+            let matrix = [
+              {
+                // portable release build: use channel with older glibc (2.27)
+                "name": "Linux LLVM",
+                "os": "ubuntu-latest",
+                "release": false,
+                "check-level": 2,
+                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
+                "binary-check": "ldd -v",
+                // foreign code may be linked against more recent glibc
+                // reverse-ffi needs to be updated to link to LLVM libraries
+                "CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
+                "CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
+              },
+              {
+                "name": "Linux release",
+                "os": "ubuntu-latest",
+                "release": true,
+                "check-level": 0,
+                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
+                "binary-check": "ldd -v",
+                // foreign code may be linked against more recent glibc
+                "CTEST_OPTIONS": "-E 'foreign'"
+              },
+              {
+                "name": "Linux",
+                "os": "ubuntu-latest",
+                "check-stage3": level >= 2,
+                "test-speedcenter": level >= 2,
+                "check-level": 1,
+              },
+              {
+                "name": "Linux Debug",
+                "os": "ubuntu-latest",
+                "check-level": 2,
+                "CMAKE_PRESET": "debug",
+                // exclude seriously slow tests
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
+              },
+              // TODO: suddenly started failing in CI
+              /*{
+                "name": "Linux fsanitize",
+                "os": "ubuntu-latest",
+                "check-level": 2,
+                // turn off custom allocator & symbolic functions to make LSAN do its magic
+                "CMAKE_PRESET": "sanitize",
+                // exclude seriously slow/problematic tests (laketests crash)
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
+              },*/
+              {
+                "name": "macOS",
+                "os": "macos-13",
+                "release": true,
+                "check-level": 2,
+                "shell": "bash -euxo pipefail {0}",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
+                "binary-check": "otool -L",
+                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
+              },
+              {
+                "name": "macOS aarch64",
+                "os": "macos-14",
+                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
+                "release": true,
+                "check-level": 1,
+                "shell": "bash -euxo pipefail {0}",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
+                "binary-check": "otool -L",
+                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
+              },
+              {
+                "name": "Windows",
+                "os": "windows-2022",
+                "release": true,
+                "check-level": 2,
+                "shell": "msys2 {0}",
+                "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
+                // for reasons unknown, interactivetests are flaky on Windows
+                "CTEST_OPTIONS": "--repeat until-pass:2",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
+                "binary-check": "ldd"
+              },
+              {
+                "name": "Linux aarch64",
+                "os": "ubuntu-latest",
+                "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
+                "release": true,
+                "check-level": 2,
+                "cross": true,
+                "cross_target": "aarch64-unknown-linux-gnu",
+                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
+              },
+              {
+                "name": "Linux 32bit",
+                "os": "ubuntu-latest",
+                // Use 32bit on stage0 and stage1 to keep oleans compatible
+                "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",
+                "cmultilib": true,
+                "release": true,
+                "check-level": 2,
+                "cross": true,
+                "shell": "bash -euxo pipefail {0}"
+              },
+              {
+                "name": "Web Assembly",
+                "os": "ubuntu-latest",
+                // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
+                "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32",
+                "wasm": true,
+                "cmultilib": true,
+                "release": true,
+                "check-level": 2,
+                "cross": true,
+                "shell": "bash -euxo pipefail {0}",
+                // Just a few selected tests because wasm is slow
+                "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean\""
+              }
+            ];
+            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
+            return matrix.filter((job) => level >= job["check-level"])
+
   build:
     needs: [configure]
     if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
@@ -327,6 +333,9 @@ jobs:
           # store in current directory, for easy uploading together with binary
           echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
         if: runner.os == 'Linux'
+      - name: Set up NPROC
+        run: |
+          echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
       - name: Build
         run: |
           mkdir build
@@ -357,8 +366,8 @@ jobs:
             OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }})
           fi
           # contortion to support empty OPTIONS with old macOS bash
-          cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-          make -j4
+          cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
+          make -j$NPROC
           make install
       - name: Check Binaries
         run: ${{ matrix.binary-check }} lean-*/bin/* || true
@@ -387,32 +396,29 @@ jobs:
           build/stage1/bin/lean --stats src/Lean.lean
         if: ${{ !matrix.cross }}
       - name: Test
+        id: test
         run: |
-          cd build/stage1
           ulimit -c unlimited # coredumps
-          # exclude nonreproducible test
-          ctest -j4 --progress --output-junit test-results.xml --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
-        if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
+          ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
+        if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.check-level >= 1
       - name: Test Summary
         uses: test-summary/action@v2
         with:
           paths: build/stage1/test-results.xml
         # prefix `if` above with `always` so it's run even if tests failed
-        if: always() && (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
+        if: always() && steps.test.conclusion != 'skipped'
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
-        if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
+        if: (!matrix.cross) && steps.test.conclusion != 'skipped'
       - name: Build Stage 2
         run: |
-          cd build
           ulimit -c unlimited # coredumps
-          make -j4 stage2
+          make -C build -j$NPROC stage2
         if: matrix.test-speedcenter
       - name: Check Stage 3
         run: |
-          cd build
           ulimit -c unlimited # coredumps
-          make -j4 check-stage3
+          make -C build -j$NPROC stage3
         if: matrix.test-speedcenter
       - name: Test Speedcenter Benchmarks
         run: |
@@ -423,11 +429,10 @@ jobs:
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
-          cd build
           ulimit -c unlimited # coredumps
           # clean rebuild in case of Makefile changes
-          make update-stage0 && rm -rf ./stage* && make -j4
-        if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
+          make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
+        if: matrix.name == 'Linux' && needs.configure.outputs.check-level >= 1
       - name: CCache stats
         run: ccache -s
       - name: Show stacktrace for coredumps

.github/workflows/restart-on-label.yml

@@ -7,7 +7,7 @@ on:
 jobs:
   restart-on-label:
     runs-on: ubuntu-latest
-    if: contains(github.event.label.name, 'full-ci')
+    if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci')
     steps:
     - run: |
         # Finding latest CI workflow run on current pull request

CMakePresets.json

@@ -0,0 +1,83 @@
+{
+  "version": 2,
+  "cmakeMinimumRequired": {
+    "major": 3,
+    "minor": 10,
+    "patch": 0
+  },
+  "configurePresets": [
+    {
+      "name": "release",
+      "displayName": "Default development optimized build config",
+      "generator": "Unix Makefiles",
+      "binaryDir": "${sourceDir}/build/release"
+    },
+    {
+      "name": "debug",
+      "displayName": "Debug build config",
+      "cacheVariables": {
+        "CMAKE_BUILD_TYPE": "Debug"
+      },
+      "generator": "Unix Makefiles",
+      "binaryDir": "${sourceDir}/build/debug"
+    },
+    {
+      "name": "sanitize",
+      "displayName": "Sanitize build config",
+      "cacheVariables": {
+        "LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined",
+        "LEANC_EXTRA_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
+        "SMALL_ALLOCATOR": "OFF",
+        "BSYMBOLIC": "OFF"
+      },
+      "generator": "Unix Makefiles",
+      "binaryDir": "${sourceDir}/build/sanitize"
+    },
+    {
+      "name": "sandebug",
+      "inherits": ["debug", "sanitize"],
+      "displayName": "Sanitize+debug build config",
+      "binaryDir": "${sourceDir}/build/sandebug"
+    }
+  ],
+  "buildPresets": [
+    {
+      "name": "release",
+      "configurePreset": "release"
+    },
+    {
+      "name": "debug",
+      "configurePreset": "debug"
+    },
+    {
+      "name": "sanitize",
+      "configurePreset": "sanitize"
+    },
+    {
+      "name": "sandebug",
+      "configurePreset": "sandebug"
+    }
+  ],
+  "testPresets": [
+    {
+      "name": "release",
+      "configurePreset": "release",
+      "output": {"outputOnFailure": true, "shortProgress": true}
+    },
+    {
+      "name": "debug",
+      "configurePreset": "debug",
+      "inherits": "release"
+    },
+    {
+      "name": "sanitize",
+      "configurePreset": "sanitize",
+      "inherits": "release"
+    },
+    {
+      "name": "sandebug",
+      "configurePreset": "sandebug",
+      "inherits": "release"
+    }
+  ]
+}

RELEASES.md

@@ -1,626 +1,23 @@
 # Lean 4 releases
 
+This file contains release notes for each stable release.
+Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
+of each version.
+During development, drafts of future release notes appear in [`releases_drafts`](https://github.com/leanprover/lean4/tree/master/script).
+
 We intend to provide regular "minor version" releases of the Lean language at approximately monthly intervals.
 There is not yet a strong guarantee of backwards compatibility between versions,
 only an expectation that breaking changes will be documented in this file.
 
-This file contains work-in-progress notes for the upcoming release, as well as previous stable releases.
-Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
-of each version.
-
-v4.8.0
-v4.9.0 (development in progress)
+v4.9.0
 ---------
 
-* Functions defined by well-founded recursion are now marked as
-  `@[irreducible]`, which should prevent expensive and often unfruitful
-  unfolding of such definitions.
-
-  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
-  rewritten to explictly unfold the function definition (using `simp`,
-  `unfold`, `rw`), or the recursive function can be temporariliy made
-  semireducible (using `unseal f in` before the command) or the function
-  definition itself can be marked as `@[semireducible]` to get the previous
-  behavor.
-
-* The `MessageData.ofPPFormat` constructor has been removed.
-  Its functionality has been split into two:
-
-  - for lazy structured messages, please use `MessageData.lazy`;
-  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
-
-  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
-
-* The `MessageData.ofFormat` constructor has been turned into a function.
-  If you need to inspect `MessageData`,
-  you can pattern-match on `MessageData.ofFormatWithInfos`.
+Development in progress.
 
 v4.8.0
 ---------
 
-* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
-
-  The way Lean is built on Windows has changed (see PR [#3601](https://github.com/leanprover/lean4/pull/3601)). As a result, Lake now dynamically links executables with `supportInterpreter := true` on Windows to `libleanshared.dll` and `libInit_shared.dll`. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of `PATH`. Running the executable via `lake exe` will ensure these libraries are part of `PATH`.
-
-  In a related change, the signature of the `nativeFacets` Lake configuration options has changed from a static `Array` to a function `(shouldExport : Bool) → Array`. See its docstring or Lake's [README](src/lake/README.md) for further details on the changed option.
-
-* Lean now generates an error if the type of a theorem is **not** a proposition.
-
-* Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
-
-* Functional induction principles.
-
-  Derived from the definition of a (possibly mutually) recursive function, a **functional induction principle** is created that is tailored to proofs about that function.
-
-  For example from:
-  ```
-  def ackermann : Nat → Nat → Nat
-    | 0, m => m + 1
-    | n+1, 0 => ackermann n 1
-    | n+1, m+1 => ackermann n (ackermann (n + 1) m)
-  ```
-  we get
-  ```
-  ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-    (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
-    (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
-    (x x : Nat) : motive x x
-  ```
-
-  It can be used in the `induction` tactic using the `using` syntax:
-  ```
-  induction n, m using ackermann.induct
-  ```
-
-* The termination checker now recognizes more recursion patterns without an
-  explicit `termination_by`. In particular the idiom of counting up to an upper
-  bound, as in
-  ```
-  def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
-    if _ : i < arr.size then
-      Array.sum arr (i+1) (acc + arr[i])
-    else
-      acc
-  ```
-  is recognized without having to say `termination_by arr.size - i`.
-
-* Shorter instances names. There is a new algorithm for generating names for anonymous instances.
-  Across Std and Mathlib, the median ratio between lengths of new names and of old names is about 72%.
-  With the old algorithm, the longest name was 1660 characters, and now the longest name is 202 characters.
-  The new algorithm's 95th percentile name length is 67 characters, versus 278 for the old algorithm.
-  While the new algorithm produces names that are 1.2% less unique,
-  it avoids cross-project collisions by adding a module-based suffix
-  when it does not refer to declarations from the same "project" (modules that share the same root).
-  PR [#3089](https://github.com/leanprover/lean4/pull/3089).
-
-* Attribute `@[pp_using_anonymous_constructor]` to make structures pretty print like `⟨x, y, z⟩`
-  rather than `{a := x, b := y, c := z}`.
-  This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
-
-* Now structure instances pretty print with parent structures' fields inlined.
-  That is, if `B` extends `A`, then `{ toA := { x := 1 }, y := 2 }` now pretty prints as `{ x := 1, y := 2 }`.
-  Setting option `pp.structureInstances.flatten` to false turns this off.
-
-* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
-  to enable pretty printing function applications using generalized field notation (defaults to true).
-  Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
-
-* Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
-  When `pp.mvars` is false, expression metavariables pretty print as `?_` and universe metavariables pretty print as `_`.
-  When `pp.mvars.withType` is true, expression metavariables pretty print with a type ascription.
-  These can be set when using `#guard_msgs` to make tests not depend on the particular names of metavariables.
-  [#3798](https://github.com/leanprover/lean4/pull/3798) and
-  [#3978](https://github.com/leanprover/lean4/pull/3978).
-
-* Hovers for terms in `match` expressions in the Infoview now reliably show the correct term.
-
-* Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
-  for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
-  Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
-  rather than `Nat.zero` and `Nat.succ n`.
-  Added option `tactic.customEliminators` to control whether to use custom eliminators.
-  Added a hack for `rcases`/`rintro`/`obtain` to use the custom eliminator for `Nat`.
-  [#3629](https://github.com/leanprover/lean4/pull/3629),
-  [#3655](https://github.com/leanprover/lean4/pull/3655), and
-  [#3747](https://github.com/leanprover/lean4/pull/3747).
-
-* The `#guard_msgs` command now has options to change whitespace normalization and sensitivity to message ordering.
-  For example, `#guard_msgs (whitespace := lax) in cmd` collapses whitespace before checking messages,
-  and `#guard_msgs (ordering := sorted) in cmd` sorts the messages in lexicographic order before checking.
-  PR [#3883](https://github.com/leanprover/lean4/pull/3883).
-
-* The `#guard_msgs` command now supports showing a diff between the expected and actual outputs. This feature is currently
-  disabled by default, but can be enabled with `set_option guard_msgs.diff true`. Depending on user feedback, this option
-  may default to `true` in a future version of Lean.
-### Language features, tactics, and metaprograms
-
-* **Functional induction principles.**
-  [#3432](https://github.com/leanprover/lean4/pull/3432), [#3620](https://github.com/leanprover/lean4/pull/3620),
-  [#3754](https://github.com/leanprover/lean4/pull/3754), [#3762](https://github.com/leanprover/lean4/pull/3762),
-  [#3738](https://github.com/leanprover/lean4/pull/3738), [#3776](https://github.com/leanprover/lean4/pull/3776),
-  [#3898](https://github.com/leanprover/lean4/pull/3898).
-
-  Derived from the definition of a (possibly mutually) recursive function,
-  a **functional induction principle** is created that is tailored to proofs about that function.
-
-  For example from:
-  ```
-  def ackermann : Nat → Nat → Nat
-    | 0, m => m + 1
-    | n+1, 0 => ackermann n 1
-    | n+1, m+1 => ackermann n (ackermann (n + 1) m)
-  ```
-  we get
-  ```
-  ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-    (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
-    (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
-    (x x : Nat) : motive x x
-  ```
-
-  It can be used in the `induction` tactic using the `using` syntax:
-  ```
-  induction n, m using ackermann.induct
-  ```
-* The termination checker now recognizes more recursion patterns without an
-  explicit `termination_by`. In particular the idiom of counting up to an upper
-  bound, as in
-  ```
-  def Array.sum (arr : Array Nat) (i acc : Nat) : Nat :=
-    if _ : i < arr.size then
-      Array.sum arr (i+1) (acc + arr[i])
-    else
-      acc
-  ```
-  is recognized without having to say `termination_by arr.size - i`.
-  * [#3630](https://github.com/leanprover/lean4/pull/3630) makes `termination_by?` not use `sizeOf` when not needed
-  * [#3652](https://github.com/leanprover/lean4/pull/3652) improves the `termination_by` syntax.
-  * [#3658](https://github.com/leanprover/lean4/pull/3658) changes how termination arguments are elaborated.
-  * [#3665](https://github.com/leanprover/lean4/pull/3665) refactors GuessLex to allow inferring more complex termination arguments
-  * [#3666](https://github.com/leanprover/lean4/pull/3666) infers termination arguments such as `xs.size - i`
-* [#3629](https://github.com/leanprover/lean4/pull/3629),
-  [#3655](https://github.com/leanprover/lean4/pull/3655),
-  [#3747](https://github.com/leanprover/lean4/pull/3747):
-  Adds `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
-  for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
-  Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`
-  rather than `Nat.zero` and `Nat.succ n`.
-  Added option `tactic.customEliminators` to control whether to use custom eliminators.
-  Added a hack for `rcases`/`rintro`/`obtain` to use the custom eliminator for `Nat`.
-* **Shorter instances names.** There is a new algorithm for generating names for anonymous instances.
-  Across Std and Mathlib, the median ratio between lengths of new names and of old names is about 72%.
-  With the old algorithm, the longest name was 1660 characters, and now the longest name is 202 characters.
-  The new algorithm's 95th percentile name length is 67 characters, versus 278 for the old algorithm.
-  While the new algorithm produces names that are 1.2% less unique,
-  it avoids cross-project collisions by adding a module-based suffix
-  when it does not refer to declarations from the same "project" (modules that share the same root).
-  [#3089](https://github.com/leanprover/lean4/pull/3089)
-  and [#3934](https://github.com/leanprover/lean4/pull/3934).
-* [8d2adf](https://github.com/leanprover/lean4/commit/8d2adf521d2b7636347a5b01bfe473bf0fcfaf31)
-  Importing two different files containing proofs of the same theorem is no longer considered an error.
-  This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
-* [84b091](https://github.com/leanprover/lean4/commit/84b0919a116e9be12f933e764474f45d964ce85c)
-  Lean now generates an error if the type of a theorem is **not** a proposition.
-* **Definition transparency.** [47a343](https://github.com/leanprover/lean4/commit/47a34316fc03ce936fddd2d3dce44784c5bcdfa9). `@[reducible]`, `@[semireducible]`, and `@[irreducible]` are now scoped and able to be set for imported declarations.
-* `simp`/`dsimp`
-  * [#3607](https://github.com/leanprover/lean4/pull/3607) enables kernel projection reduction in `dsimp`
-  * [b24fbf](https://github.com/leanprover/lean4/commit/b24fbf44f3aaa112f5d799ef2a341772d1eb222d)
-    and [acdb00](https://github.com/leanprover/lean4/commit/acdb0054d5a0efa724cff596ac26852fad5724c4):
-    `dsimproc` command
-    to define defeq-preserving simplification procedures.
-  * [#3624](https://github.com/leanprover/lean4/pull/3624) makes `dsimp` normalize raw nat literals as `OfNat.ofNat` applications.
-  * [#3628](https://github.com/leanprover/lean4/pull/3628) makes `simp` correctly handle `OfScientific.ofScientific` literals.
-  * [#3654](https://github.com/leanprover/lean4/pull/3654) makes `dsimp?` report used simprocs.
-  * [dee074](https://github.com/leanprover/lean4/commit/dee074dcde03a37b7895a4901df2e4fa490c73c7) fixes equation theorem
-    handling in `simp` for non-recursive definitions.
-  * [#3819](https://github.com/leanprover/lean4/pull/3819) improved performance when simp encounters a loop.
-  * [#3821](https://github.com/leanprover/lean4/pull/3821) fixes discharger/cache interaction.
-  * [#3824](https://github.com/leanprover/lean4/pull/3824) keeps `simp` from breaking `Char` literals.
-  * [#3838](https://github.com/leanprover/lean4/pull/3838) allows `Nat` instances matching to be more lenient.
-  * [#3870](https://github.com/leanprover/lean4/pull/3870) documentation for `simp` configuration options.
-  * [#3972](https://github.com/leanprover/lean4/pull/3972) fixes simp caching.
-  * [#4044](https://github.com/leanprover/lean4/pull/4044) improves cache behavior for "well-behaved" dischargers.
-* `omega`
-  * [#3639](https://github.com/leanprover/lean4/pull/3639), [#3766](https://github.com/leanprover/lean4/pull/3766),
-    [#3853](https://github.com/leanprover/lean4/pull/3853), [#3875](https://github.com/leanprover/lean4/pull/3875):
-    introduces a term canonicalizer.
-  * [#3736](https://github.com/leanprover/lean4/pull/3736) improves handling of positivity for the modulo operator for `Int`.
-  * [#3828](https://github.com/leanprover/lean4/pull/3828) makes it work as a `simp` discharger.
-  * [#3847](https://github.com/leanprover/lean4/pull/3847) adds helpful error messages.
-* `rfl`
-  * [#3671](https://github.com/leanprover/lean4/pull/3671), [#3708](https://github.com/leanprover/lean4/pull/3708): upstreams the `@[refl]` attribute and the `rfl` tactic.
-  * [#3751](https://github.com/leanprover/lean4/pull/3751) makes `apply_rfl` not operate on `Eq` itself.
-  * [#4067](https://github.com/leanprover/lean4/pull/4067) improves error message when there are no goals.
-* [#3719](https://github.com/leanprover/lean4/pull/3719) upstreams the `rw?` tactic, with fixes and improvements in
-  [#3783](https://github.com/leanprover/lean4/pull/3783), [#3794](https://github.com/leanprover/lean4/pull/3794),
-  [#3911](https://github.com/leanprover/lean4/pull/3911).
-* `conv`
-  * [#3659](https://github.com/leanprover/lean4/pull/3659) adds a `conv` version of the `calc` tactic.
-  * [#3763](https://github.com/leanprover/lean4/pull/3763) makes `conv` clean up using `try with_reducible rfl` instead of `try rfl`.
-* `#guard_msgs`
-  * [#3617](https://github.com/leanprover/lean4/pull/3617) introduces whitespace protection using the `⏎` character.
-  * [#3883](https://github.com/leanprover/lean4/pull/3883):
-    The `#guard_msgs` command now has options to change whitespace normalization and sensitivity to message ordering.
-    For example, `#guard_msgs (whitespace := lax) in cmd` collapses whitespace before checking messages,
-    and `#guard_msgs (ordering := sorted) in cmd` sorts the messages in lexicographic order before checking.
-  * [#3931](https://github.com/leanprover/lean4/pull/3931) adds an unused variables ignore function for `#guard_msgs`.
-  * [#3912](https://github.com/leanprover/lean4/pull/3912) adds a diff between the expected and actual outputs. This feature is currently
-    disabled by default, but can be enabled with `set_option guard_msgs.diff true`.
-    Depending on user feedback, this option may default to `true` in a future version of Lean.
-* `do` **notation**
-  * [#3820](https://github.com/leanprover/lean4/pull/3820) makes it an error to lift `(<- ...)` out of a pure `if ... then ... else ...`
-* **Lazy discrimination trees**
-  * [#3610](https://github.com/leanprover/lean4/pull/3610) fixes a name collision for `LazyDiscrTree` that could lead to cache poisoning.
-  * [#3677](https://github.com/leanprover/lean4/pull/3677) simplifies and fixes `LazyDiscrTree` handling for `exact?`/`apply?`.
-  * [#3685](https://github.com/leanprover/lean4/pull/3685) moves general `exact?`/`apply?` functionality into `LazyDiscrTree`.
-  * [#3769](https://github.com/leanprover/lean4/pull/3769) has lemma selection improvements for `rw?` and `LazyDiscrTree`.
-  * [#3818](https://github.com/leanprover/lean4/pull/3818) improves ordering of matches.
-* [#3590](https://github.com/leanprover/lean4/pull/3590) adds `inductive.autoPromoteIndices` option to be able to disable auto promotion of indices in the `inductive` command.
-* **Miscellaneous bug fixes and improvements**
-  * [#3606](https://github.com/leanprover/lean4/pull/3606) preserves `cache` and `dischargeDepth` fields in `Lean.Meta.Simp.Result.mkEqSymm`.
-  * [#3633](https://github.com/leanprover/lean4/pull/3633) makes `elabTermEnsuringType` respect `errToSorry`, improving error recovery of the `have` tactic.
-  * [#3647](https://github.com/leanprover/lean4/pull/3647) enables `noncomputable unsafe` definitions, for deferring implementations until later.
-  * [#3672](https://github.com/leanprover/lean4/pull/3672) adjust namespaces of tactics.
-  * [#3725](https://github.com/leanprover/lean4/pull/3725) fixes `Ord` derive handler for indexed inductive types with unused alternatives.
-  * [#3893](https://github.com/leanprover/lean4/pull/3893) improves performance of derived `Ord` instances.
-  * [#3771](https://github.com/leanprover/lean4/pull/3771) changes error reporting for failing tactic macros. Improves `rfl` error message.
-  * [#3745](https://github.com/leanprover/lean4/pull/3745) fixes elaboration of generalized field notation if the object of the notation is an optional parameter.
-  * [#3799](https://github.com/leanprover/lean4/pull/3799) makes commands such as `universe`, `variable`, `namespace`, etc. require that their argument appear in a later column.
-    Commands that can optionally parse an `ident` or parse any number of `ident`s generally should require
-    that the `ident` use `colGt`. This keeps typos in commands from being interpreted as identifiers.
-  * [#3815](https://github.com/leanprover/lean4/pull/3815) lets the `split` tactic be used for writing code.
-  * [#3822](https://github.com/leanprover/lean4/pull/3822) adds missing info in `induction` tactic for `with` clauses of the form `| cstr a b c => ?_`.
-  * [#3806](https://github.com/leanprover/lean4/pull/3806) fixes `withSetOptionIn` combinator.
-  * [#3844](https://github.com/leanprover/lean4/pull/3844) removes unused `trace.Elab.syntax` option.
-  * [#3896](https://github.com/leanprover/lean4/pull/3896) improves hover and go-to-def for `attribute` command.
-  * [#3989](https://github.com/leanprover/lean4/pull/3989) makes linter options more discoverable.
-  * [#3916](https://github.com/leanprover/lean4/pull/3916) fixes go-to-def for syntax defined with `@[builtin_term_parser]`.
-  * [#3962](https://github.com/leanprover/lean4/pull/3962) fixes how `solveByElim` handles `symm` lemmas, making `exact?`/`apply?` usable again.
-  * [#3968](https://github.com/leanprover/lean4/pull/3968) improves the `@[deprecated]` attribute, adding `(since := "<date>")` field.
-  * [#3768](https://github.com/leanprover/lean4/pull/3768) makes `#print` command show structure fields.
-  * [#3974](https://github.com/leanprover/lean4/pull/3974) makes `exact?%` behave like `by exact?` rather than `by apply?`.
-  * [#3994](https://github.com/leanprover/lean4/pull/3994) makes elaboration of `he ▸ h` notation more predictable.
-  * [#3991](https://github.com/leanprover/lean4/pull/3991) adjusts transparency for `decreasing_trivial` macros.
-  * [#4092](https://github.com/leanprover/lean4/pull/4092) improves performance of `binop%` and `binrel%` expression tree elaborators.
-* **Docs:** [#3748](https://github.com/leanprover/lean4/pull/3748), [#3796](https://github.com/leanprover/lean4/pull/3796),
-[#3800](https://github.com/leanprover/lean4/pull/3800), [#3874](https://github.com/leanprover/lean4/pull/3874),
-[#3863](https://github.com/leanprover/lean4/pull/3863), [#3862](https://github.com/leanprover/lean4/pull/3862),
-[#3891](https://github.com/leanprover/lean4/pull/3891), [#3873](https://github.com/leanprover/lean4/pull/3873),
-[#3908](https://github.com/leanprover/lean4/pull/3908), [#3872](https://github.com/leanprover/lean4/pull/3872).
-
-### Language server and IDE extensions
-
-* [#3432](https://github.com/leanprover/lean4/pull/3432) enables `import` auto-completions.
-* [#3608](https://github.com/leanprover/lean4/pull/3608) fixes issue [leanprover/vscode-lean4#392](https://github.com/leanprover/vscode-lean4/issues/392).
-  Diagnostic ranges had an off-by-one error that would misplace goal states for example.
-* [#3014](https://github.com/leanprover/lean4/pull/3014) introduces snapshot trees, foundational work for incremental tactics and parallelism.
-  [#3849](https://github.com/leanprover/lean4/pull/3849) adds basic incrementality API.
-* [#3271](https://github.com/leanprover/lean4/pull/3271) adds support for server-to-client requests.
-* [#3656](https://github.com/leanprover/lean4/pull/3656) fixes jump to definition when there are conflicting names from different files.
-  Fixes issue [#1170](https://github.com/leanprover/lean4/issues/1170).
-* [#3691](https://github.com/leanprover/lean4/pull/3691), [#3925](https://github.com/leanprover/lean4/pull/3925),
-  [#3932](https://github.com/leanprover/lean4/pull/3932) keep semantic tokens synchronized (used for semantic highlighting), with performance improvements.
-* [#3247](https://github.com/leanprover/lean4/pull/3247) and [#3730](https://github.com/leanprover/lean4/pull/3730)
-  add diagnostics to run "Restart File" when a file dependency is saved.
-* [#3722](https://github.com/leanprover/lean4/pull/3722) uses the correct module names when displaying references.
-* [#3728](https://github.com/leanprover/lean4/pull/3728) makes errors in header reliably appear and makes the "Import out of date" warning be at "hint" severity.
-  [#3739](https://github.com/leanprover/lean4/pull/3739) simplifies the text of this warning.
-* [#3778](https://github.com/leanprover/lean4/pull/3778) fixes [#3462](https://github.com/leanprover/lean4/issues/3462),
-  where info nodes from before the cursor would be used for computing completions.
-* [#3985](https://github.com/leanprover/lean4/pull/3985) makes trace timings appear in Infoview.
-
-### Pretty printing
-
-* [#3797](https://github.com/leanprover/lean4/pull/3797) fixes the hovers over binders so that they show their types.
-* [#3640](https://github.com/leanprover/lean4/pull/3640) and [#3735](https://github.com/leanprover/lean4/pull/3735): Adds attribute `@[pp_using_anonymous_constructor]` to make structures pretty print as `⟨x, y, z⟩`
-  rather than as `{a := x, b := y, c := z}`.
-  This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
-* [#3749](https://github.com/leanprover/lean4/pull/3749)
-  Now structure instances pretty print with parent structures' fields inlined.
-  That is, if `B` extends `A`, then `{ toA := { x := 1 }, y := 2 }` now pretty prints as `{ x := 1, y := 2 }`.
-  Setting option `pp.structureInstances.flatten` to false turns this off.
-* [#3737](https://github.com/leanprover/lean4/pull/3737), [#3744](https://github.com/leanprover/lean4/pull/3744)
-  and [#3750](https://github.com/leanprover/lean4/pull/3750):
-  Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
-  to enable pretty printing function applications using generalized field notation (defaults to true).
-  Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
-  The notation is not used for theorems.
-* [#4071](https://github.com/leanprover/lean4/pull/4071) fixes interaction between app unexpanders and `pp.fieldNotation.generalized`
-* [#3625](https://github.com/leanprover/lean4/pull/3625) makes `delabConstWithSignature` (used by `#check`) have the ability to put arguments "after the colon"
-  to avoid printing inaccessible names.
-* [#3798](https://github.com/leanprover/lean4/pull/3798),
-  [#3978](https://github.com/leanprover/lean4/pull/3978),
-  [#3798](https://github.com/leanprover/lean4/pull/3980):
-  Adds options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
-  When `pp.mvars` is false, expression metavariables pretty print as `?_` and universe metavariables pretty print as `_`.
-  When `pp.mvars.withType` is true, expression metavariables pretty print with a type ascription.
-  These can be set when using `#guard_msgs` to make tests not depend on the particular names of metavariables.
-* [#3917](https://github.com/leanprover/lean4/pull/3917) makes binders hoverable and gives them docstrings.
-* [#4034](https://github.com/leanprover/lean4/pull/4034) makes hovers for RHS terms in `match` expressions in the Infoview reliably show the correct term.
-
-### Library
-
-* `Bool`/`Prop`
-  * [#3508](https://github.com/leanprover/lean4/pull/3508) improves `simp` confluence for `Bool` and `Prop` terms.
-  * Theorems: [#3604](https://github.com/leanprover/lean4/pull/3604)
-* `Nat`
-  * [#3579](https://github.com/leanprover/lean4/pull/3579) makes `Nat.succ_eq_add_one` be a simp lemma, now that `induction`/`cases` uses `n + 1` instead of `Nat.succ n`.
-  * [#3808](https://github.com/leanprover/lean4/pull/3808) replaces `Nat.succ` simp rules with simprocs.
-  * [#3876](https://github.com/leanprover/lean4/pull/3876) adds faster `Nat.repr` implementation in C.
-* `Int`
-  * Theorems: [#3890](https://github.com/leanprover/lean4/pull/3890)
-* `UInt`s
-  * [#3960](https://github.com/leanprover/lean4/pull/3960) improves performance of upcasting.
-* `Array` and `Subarray`
-  * [#3676](https://github.com/leanprover/lean4/pull/3676) removes `Array.eraseIdxAux`, `Array.eraseIdxSzAux`, and `Array.eraseIdx'`.
-  * [#3648](https://github.com/leanprover/lean4/pull/3648) simplifies `Array.findIdx?`.
-  * [#3851](https://github.com/leanprover/lean4/pull/3851) renames fields of `Subarray`.
-* `List`
-  * [#3785](https://github.com/leanprover/lean4/pull/3785) upstreams tail-recursive List operations and `@[csimp]` lemmas.
-* `BitVec`
-  * Theorems: [#3593](https://github.com/leanprover/lean4/pull/3593),
-  [#3593](https://github.com/leanprover/lean4/pull/3593), [#3597](https://github.com/leanprover/lean4/pull/3597),
-  [#3598](https://github.com/leanprover/lean4/pull/3598), [#3721](https://github.com/leanprover/lean4/pull/3721),
-  [#3729](https://github.com/leanprover/lean4/pull/3729), [#3880](https://github.com/leanprover/lean4/pull/3880),
-  [#4039](https://github.com/leanprover/lean4/pull/4039).
-  * [#3884](https://github.com/leanprover/lean4/pull/3884) protects `Std.BitVec`.
-* `String`
-  * [#3832](https://github.com/leanprover/lean4/pull/3832) fixes `String.splitOn`.
-  * [#3959](https://github.com/leanprover/lean4/pull/3959) adds `String.Pos.isValid`.
-  * [#3959](https://github.com/leanprover/lean4/pull/3959) UTF-8 string validation.
-  * [#3961](https://github.com/leanprover/lean4/pull/3961) adds a model implementation for UTF-8 encoding and decoding.
-* `IO`
-  * [#4097](https://github.com/leanprover/lean4/pull/4097) adds `IO.getTaskState` which returns whether a task is finished, actively running, or waiting on other Tasks to finish.
-
-* **Refactors**
-  * [#3605](https://github.com/leanprover/lean4/pull/3605) reduces imports for `Init.Data.Nat` and `Init.Data.Int`.
-  * [#3613](https://github.com/leanprover/lean4/pull/3613) reduces imports for `Init.Omega.Int`.
-  * [#3634](https://github.com/leanprover/lean4/pull/3634) upstreams `Std.Data.Nat`
-    and [#3635](https://github.com/leanprover/lean4/pull/3635) upstreams `Std.Data.Int`.
-  * [#3790](https://github.com/leanprover/lean4/pull/3790) reduces more imports for `omega`.
-  * [#3694](https://github.com/leanprover/lean4/pull/3694) extends `GetElem` interface with `getElem!` and `getElem?` to simplify containers like `RBMap`.
-  * [#3865](https://github.com/leanprover/lean4/pull/3865) renames `Option.toMonad` (see breaking changes below).
-  * [#3882](https://github.com/leanprover/lean4/pull/3882) unifies `lexOrd` with `compareLex`.
-* **Other fixes or improvements**
-  * [#3765](https://github.com/leanprover/lean4/pull/3765) makes `Quotient.sound` be a `theorem`.
-  * [#3645](https://github.com/leanprover/lean4/pull/3645) fixes `System.FilePath.parent` in the case of absolute paths.
-  * [#3660](https://github.com/leanprover/lean4/pull/3660) `ByteArray.toUInt64LE!` and `ByteArray.toUInt64BE!` were swapped.
-  * [#3881](https://github.com/leanprover/lean4/pull/3881), [#3887](https://github.com/leanprover/lean4/pull/3887) fix linearity issues in `HashMap.insertIfNew`, `HashSet.erase`, and `HashMap.erase`.
-    The `HashMap.insertIfNew` fix improves `import` performance.
-  * [#3830](https://github.com/leanprover/lean4/pull/3830) ensures linearity in `Parsec.many*Core`.
-  * [#3930](https://github.com/leanprover/lean4/pull/3930) adds `FS.Stream.isTty` field.
-  * [#3866](https://github.com/leanprover/lean4/pull/3866) deprecates `Option.toBool` in favor of `Option.isSome`.
-  * [#3975](https://github.com/leanprover/lean4/pull/3975) upstreams `Data.List.Init` and `Data.Array.Init` material from Std.
-  * [#3942](https://github.com/leanprover/lean4/pull/3942) adds instances that make `ac_rfl` work without Mathlib.
-  * [#4010](https://github.com/leanprover/lean4/pull/4010) changes `Fin.induction` to use structural induction.
-  * [02753f](https://github.com/leanprover/lean4/commit/02753f6e4c510c385efcbf71fa9a6bec50fce9ab)
-    fixes bug in `reduceLeDiff` simproc.
-  * [#4097](https://github.com/leanprover/lean4/pull/4097)
-    adds `IO.TaskState` and `IO.getTaskState` to get the task from the Lean runtime's task manager.
-* **Docs:** [#3615](https://github.com/leanprover/lean4/pull/3615), [#3664](https://github.com/leanprover/lean4/pull/3664),
-  [#3707](https://github.com/leanprover/lean4/pull/3707), [#3734](https://github.com/leanprover/lean4/pull/3734),
-  [#3868](https://github.com/leanprover/lean4/pull/3868), [#3861](https://github.com/leanprover/lean4/pull/3861),
-  [#3869](https://github.com/leanprover/lean4/pull/3869), [#3858](https://github.com/leanprover/lean4/pull/3858),
-  [#3856](https://github.com/leanprover/lean4/pull/3856), [#3857](https://github.com/leanprover/lean4/pull/3857),
-  [#3867](https://github.com/leanprover/lean4/pull/3867), [#3864](https://github.com/leanprover/lean4/pull/3864),
-  [#3860](https://github.com/leanprover/lean4/pull/3860), [#3859](https://github.com/leanprover/lean4/pull/3859),
-  [#3871](https://github.com/leanprover/lean4/pull/3871), [#3919](https://github.com/leanprover/lean4/pull/3919).
-
-### Lean internals
-
-* **Defeq and WHNF algorithms**
-  * [#3616](https://github.com/leanprover/lean4/pull/3616) gives better support for reducing `Nat.rec` expressions.
-  * [#3774](https://github.com/leanprover/lean4/pull/3774) add tracing for "non-easy" WHNF cases.
-  * [#3807](https://github.com/leanprover/lean4/pull/3807) fixes an `isDefEq` performance issue, now trying structure eta *after* lazy delta reduction.
-  * [#3816](https://github.com/leanprover/lean4/pull/3816) fixes `.yesWithDeltaI` behavior to prevent increasing transparency level when reducing projections.
-  * [#3837](https://github.com/leanprover/lean4/pull/3837) improves heuristic at `isDefEq`.
-  * [#3965](https://github.com/leanprover/lean4/pull/3965) improves `isDefEq` for constraints of the form `t.i =?= s.i`.
-  * [#3977](https://github.com/leanprover/lean4/pull/3977) improves `isDefEqProj`.
-  * [#3981](https://github.com/leanprover/lean4/pull/3981) adds universe constraint approximations to be able to solve `u =?= max u ?v` using `?v = u`.
-    These approximations are only applied when universe constraints cannot be postponed anymore.
-  * [#4004](https://github.com/leanprover/lean4/pull/4004) improves `isDefEqProj` during typeclass resolution.
-  * [#4012](https://github.com/leanprover/lean4/pull/4012) adds `backward.isDefEq.lazyProjDelta` and `backward.isDefEq.lazyWhnfCore` backwards compatibility flags.
-* **Kernel**
-  * [#3966](https://github.com/leanprover/lean4/pull/3966) removes dead code.
-  * [#4035](https://github.com/leanprover/lean4/pull/4035) fixes mismatch for `TheoremVal` between Lean and C++.
-* **Discrimination trees**
-  * [423fed](https://github.com/leanprover/lean4/commit/423fed79a9de75705f34b3e8648db7e076c688d7)
-    and [3218b2](https://github.com/leanprover/lean4/commit/3218b25974d33e92807af3ce42198911c256ff1d):
-    simplify handling of dependent/non-dependent pi types.
-* **Typeclass instance synthesis**
-  * [#3638](https://github.com/leanprover/lean4/pull/3638) eta-reduces synthesized instances
-  * [ce350f](https://github.com/leanprover/lean4/commit/ce350f348161e63fccde6c4a5fe1fd2070e7ce0f) fixes a linearity issue
-  * [917a31](https://github.com/leanprover/lean4/commit/917a31f694f0db44d6907cc2b1485459afe74d49)
-    improves performance by considering at most one answer for subgoals not containing metavariables.
-    [#4008](https://github.com/leanprover/lean4/pull/4008) adds `backward.synthInstance.canonInstances` backward compatibility flag.
-* **Definition processing**
-  * [#3661](https://github.com/leanprover/lean4/pull/3661), [#3767](https://github.com/leanprover/lean4/pull/3767) changes automatically generated equational theorems to be named
-    using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.eq_def` instead of `._unfold`. (See breaking changes below.)
-    [#3675](https://github.com/leanprover/lean4/pull/3675) adds a mechanism to reserve names.
-    [#3803](https://github.com/leanprover/lean4/pull/3803) fixes reserved name resolution inside namespaces and fixes handling of `match`er declarations and equation lemmas.
-  * [#3662](https://github.com/leanprover/lean4/pull/3662) causes auxiliary definitions nested inside theorems to become `def`s if they are not proofs.
-  * [#4006](https://github.com/leanprover/lean4/pull/4006) makes proposition fields of `structure`s be theorems.
-  * [#4018](https://github.com/leanprover/lean4/pull/4018) makes it an error for a theorem to be `extern`.
-  * [#4047](https://github.com/leanprover/lean4/pull/4047) improves performance making equations for well-founded recursive definitions.
-* **Refactors**
-  * [#3614](https://github.com/leanprover/lean4/pull/3614) avoids unfolding in `Lean.Meta.evalNat`.
-  * [#3621](https://github.com/leanprover/lean4/pull/3621) centralizes functionality for `Fix`/`GuessLex`/`FunInd` in the `ArgsPacker` module.
-  * [#3186](https://github.com/leanprover/lean4/pull/3186) rewrites the UnusedVariable linter to be more performant.
-  * [#3589](https://github.com/leanprover/lean4/pull/3589) removes coercion from `String` to `Name` (see breaking changes below).
-  * [#3237](https://github.com/leanprover/lean4/pull/3237) removes the `lines` field from `FileMap`.
-  * [#3951](https://github.com/leanprover/lean4/pull/3951) makes msg parameter to `throwTacticEx` optional.
-* **Diagnostics**
-  * [#4016](https://github.com/leanprover/lean4/pull/4016), [#4019](https://github.com/leanprover/lean4/pull/4019),
-    [#4020](https://github.com/leanprover/lean4/pull/4020), [#4030](https://github.com/leanprover/lean4/pull/4030),
-    [#4031](https://github.com/leanprover/lean4/pull/4031),
-    [c3714b](https://github.com/leanprover/lean4/commit/c3714bdc6d46845c0428735b283c5b48b23cbcf7),
-    [#4049](https://github.com/leanprover/lean4/pull/4049) adds `set_option diagnostics true` for diagnostic counters.
-    Tracks number of unfolded declarations, instances, reducible declarations, used instances, recursor reductions,
-    `isDefEq` heuristic applications, among others.
-    This option is suggested in exceptional situations, such as at deterministic timeout and maximum recursion depth.
-  * [283587](https://github.com/leanprover/lean4/commit/283587987ab2eb3b56fbc3a19d5f33ab9e04a2ef)
-    adds diagnostic information for `simp`.
-  * [#4043](https://github.com/leanprover/lean4/pull/4043) adds diagnostic information for congruence theorems.
-  * [#4048](https://github.com/leanprover/lean4/pull/4048) display diagnostic information
-    for `set_option diagnostics true in <tactic>` and `set_option diagnostics true in <term>`.
-* **Other features**
-  * [#3800](https://github.com/leanprover/lean4/pull/3800) adds environment extension to record which definitions use structural or well-founded recursion.
-  * [#3801](https://github.com/leanprover/lean4/pull/3801) `trace.profiler` can now export to Firefox Profiler.
-  * [#3918](https://github.com/leanprover/lean4/pull/3918), [#3953](https://github.com/leanprover/lean4/pull/3953) adds `@[builtin_doc]` attribute to make docs and location of a declaration available as a builtin.
-  * [#3939](https://github.com/leanprover/lean4/pull/3939) adds the `lean --json` CLI option to print messages as JSON.
-  * [#3075](https://github.com/leanprover/lean4/pull/3075) improves `test_extern` command.
-  * [#3970](https://github.com/leanprover/lean4/pull/3970) gives monadic generalization of `FindExpr`.
-* **Docs:** [#3743](https://github.com/leanprover/lean4/pull/3743), [#3921](https://github.com/leanprover/lean4/pull/3921),
-  [#3954](https://github.com/leanprover/lean4/pull/3954).
-* **Other fixes:** [#3622](https://github.com/leanprover/lean4/pull/3622),
-  [#3726](https://github.com/leanprover/lean4/pull/3726), [#3823](https://github.com/leanprover/lean4/pull/3823),
-  [#3897](https://github.com/leanprover/lean4/pull/3897), [#3964](https://github.com/leanprover/lean4/pull/3964),
-  [#3946](https://github.com/leanprover/lean4/pull/3946), [#4007](https://github.com/leanprover/lean4/pull/4007),
-  [#4026](https://github.com/leanprover/lean4/pull/4026).
-
-### Compiler, runtime, and FFI
-
-* [#3632](https://github.com/leanprover/lean4/pull/3632) makes it possible to allocate and free thread-local runtime resources for threads not started by Lean itself.
-* [#3627](https://github.com/leanprover/lean4/pull/3627) improves error message about compacting closures.
-* [#3692](https://github.com/leanprover/lean4/pull/3692) fixes deadlock in `IO.Promise.resolve`.
-* [#3753](https://github.com/leanprover/lean4/pull/3753) catches error code from `MoveFileEx` on Windows.
-* [#4028](https://github.com/leanprover/lean4/pull/4028) fixes a double `reset` bug in `ResetReuse` transformation.
-* [6e731b](https://github.com/leanprover/lean4/commit/6e731b4370000a8e7a5cfb675a7f3d7635d21f58)
-  removes `interpreter` copy constructor to avoid potential memory safety issues.
-
-### Lake
-
-* **TOML Lake configurations**. [#3298](https://github.com/leanprover/lean4/pull/3298), [#4104](https://github.com/leanprover/lean4/pull/4104).
-
-  Lake packages can now use TOML as a alternative configuration file format instead of Lean. If the default `lakefile.lean` is missing, Lake will also look for a `lakefile.toml`. The TOML version of the configuration supports a restricted set of the Lake configuration options, only including those which can easily mapped to a TOML data structure. The TOML syntax itself fully compiles with the TOML v1.0.0 specification.
-
-  As part of the introduction of this new feature, we have been helping maintainers of some major packages within the ecosystem switch to this format. For example, the following is Aesop's new `lakefile.toml`:
-
-
-  **[leanprover-community/aesop/lakefile.toml](https://raw.githubusercontent.com/leanprover-community/aesop/de11e0ecf372976e6d627c210573146153090d2d/lakefile.toml)**
-  ```toml
-  name = "aesop"
-  defaultTargets = ["Aesop"]
-  testRunner = "test"
-  precompileModules = false
-
-  [[require]]
-  name = "batteries"
-  git = "https://github.com/leanprover-community/batteries"
-  rev = "main"
-
-  [[lean_lib]]
-  name = "Aesop"
-
-  [[lean_lib]]
-  name = "AesopTest"
-  globs = ["AesopTest.+"]
-  leanOptions = {linter.unusedVariables = false}
-
-  [[lean_exe]]
-  name = "test"
-  srcDir = "scripts"
-  ```
-
-  To assist users who wish to transition their packages between configuration file formats, there is also a new `lake translate-config` command for migrating to/from TOML.
-
-  Running `lake translate-config toml` will produce a `lakefile.toml` version of a package's `lakefile.lean`. Any configuration options unsupported by the TOML format will be discarded during translation, but the original `lakefile.lean` will remain so that you can verify the translation looks good before deleting it.
-
-* **Build progress overhaul.** [#3835](https://github.com/leanprover/lean4/pull/3835), [#4115](https://github.com/leanprover/lean4/pull/4115), [#4127](https://github.com/leanprover/lean4/pull/4127), [#4220](https://github.com/leanprover/lean4/pull/4220), [#4232](https://github.com/leanprover/lean4/pull/4232), [#4236](https://github.com/leanprover/lean4/pull/4236).
-
-  Builds are now managed by a top-level Lake build monitor, this makes the output of Lake builds more standardized and enables producing prettier and more configurable progress reports.
-
-  As part of this change, job isolation has improved. Stray I/O and other build related errors in custom targets are now properly isolated and caught as part of their job. Import errors no longer cause Lake to abort the entire build and are instead localized to the build jobs of the modules in question.
-
-  Lake also now uses ANSI escape sequences to add color and produce progress lines that update in-place; this can be toggled on and off using `--ansi` / `--no-ansi`.
-
-
-  `--wfail` and `--iofail` options have been added that causes a build to fail if any of the jobs log a warning (`--wfail`) or produce any output or log information messages (`--iofail`). Unlike some other build systems, these options do **NOT** convert these logs into errors, and Lake does not abort jobs on such a log (i.e., dependent jobs will still continue unimpeded).
-
-* `lake test`. [#3779](https://github.com/leanprover/lean4/pull/3779).
-
-  Lake now has a built-in `test` command which will run a script or executable labelled `@[test_runner]` (in Lean) or defined as the `testRunner` (in TOML) in the root package.
-
-  Lake also provides a `lake check-test` command which will exit with code `0` if the package has a properly configured test runner or error with `1` otherwise.
-
-* `lake lean`. [#3793](https://github.com/leanprover/lean4/pull/3793).
-
-  The new command `lake lean <file> [-- <args...>]` functions like `lake env lean <file> <args...>`, except that it builds the imports of `file` before running `lean`. This makes it very useful for running test or example code that imports modules that are not guaranteed to have been built beforehand.
-
-* **Miscellaneous bug fixes and improvements**
-  * [#3609](https://github.com/leanprover/lean4/pull/3609) `LEAN_GITHASH` environment variable to override the detected Git hash for Lean when computing traces, useful for testing custom builds of Lean.
-  * [#3795](https://github.com/leanprover/lean4/pull/3795) improves relative package directory path normalization in the pre-rename check.
-  * [#3957](https://github.com/leanprover/lean4/pull/3957) fixes handling of packages that appear multiple times in a dependency tree.
-  * [#3999](https://github.com/leanprover/lean4/pull/3999) makes it an error for there to be a mismatch between a package name and what it is required as. Also adds a special message for the `std`-to-`batteries` rename.
-  * [#4033](https://github.com/leanprover/lean4/pull/4033) fixes quiet mode.
-* **Docs:** [#3704](https://github.com/leanprover/lean4/pull/3704).
-
-### DevOps
-
-* [#3536](https://github.com/leanprover/lean4/pull/3536) and [#3833](https://github.com/leanprover/lean4/pull/3833)
-  add a checklist for the release process.
-* [#3600](https://github.com/leanprover/lean4/pull/3600) runs nix-ci more uniformly.
-* [#3612](https://github.com/leanprover/lean4/pull/3612) avoids argument limits when building on Windows.
-* [#3682](https://github.com/leanprover/lean4/pull/3682) builds Lean's `.o` files in parallel to rest of core.
-* [#3601](https://github.com/leanprover/lean4/pull/3601)
-  changes the way Lean is built on Windows (see breaking changes below).
-  As a result, Lake now dynamically links executables with `supportInterpreter := true` on Windows
-  to `libleanshared.dll` and `libInit_shared.dll`. Therefore, such executables will not run
-  unless those shared libraries are co-located with the executables or part of `PATH`.
-  Running the executable via `lake exe` will ensure these libraries are part of `PATH`.
-
-  In a related change, the signature of the `nativeFacets` Lake configuration options has changed
-  from a static `Array` to a function `(shouldExport : Bool) → Array`.
-  See its docstring or Lake's [README](src/lake/README.md) for further details on the changed option.
-* [#3690](https://github.com/leanprover/lean4/pull/3690) marks "Build matrix complete" as canceled if the build is canceled.
-* [#3700](https://github.com/leanprover/lean4/pull/3700), [#3702](https://github.com/leanprover/lean4/pull/3702),
-  [#3701](https://github.com/leanprover/lean4/pull/3701), [#3834](https://github.com/leanprover/lean4/pull/3834),
-  [#3923](https://github.com/leanprover/lean4/pull/3923): fixes and improvements for std and mathlib CI.
-* [#3712](https://github.com/leanprover/lean4/pull/3712) fixes `nix build .` on macOS.
-* [#3717](https://github.com/leanprover/lean4/pull/3717) replaces `shell.nix` in devShell with `flake.nix`.
-* [#3715](https://github.com/leanprover/lean4/pull/3715) and [#3790](https://github.com/leanprover/lean4/pull/3790) add test result summaries.
-* [#3971](https://github.com/leanprover/lean4/pull/3971) prevents stage0 changes via the merge queue.
-* [#3979](https://github.com/leanprover/lean4/pull/3979) adds handling for `changes-stage0` label.
-* [#3952](https://github.com/leanprover/lean4/pull/3952) adds a script to summarize GitHub issues.
-* [18a699](https://github.com/leanprover/lean4/commit/18a69914da53dbe37c91bc2b9ce65e1dc01752b6)
-  fixes asan linking
-
-### Breaking changes
-
-* Due to the major Lake build refactor, code using the affected parts of the Lake API or relying on the previous output format of Lake builds is likely to have been broken. We have tried to minimize the breakages and, were possible, old definitions have been marked `@[deprecated]` with a reference to the new alternative.
-
-* Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
-```
-def fact : Nat → Nat
-  | 0 => 1
-  | n+1 => (n+1) * fact n
-
-theorem ex : fact 0 = 1 := by unfold fact; decide
-
-#check fact.eq_1
--- fact.eq_1 : fact 0 = 1
-
-#check fact.eq_2
--- fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n
-
-#check fact.def
-/-
-fact.def :
-  ∀ (x : Nat),
-    fact x =
-      match x with
-      | 0 => 1
-      | Nat.succ n => (n + 1) * fact n
--/
-```
-
-* The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`.
-
-* The `Subarray` fields `as`, `h₁` and `h₂` have been renamed to `array`, `start_le_stop`, and `stop_le_array_size`, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projections were added; these will be removed in a future release.
-
-* The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names.
-
-* `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
+Release candidate, release notes will be copied from branch `releases/v4.8.0` once completed.
 
 v4.7.0
 ---------

doc/make/index.md

@@ -1,3 +1,7 @@
+These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](doc/dev/index.md).
+
+We strongly suggest that new users instead follow the [Quickstart](doc/quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
+
 Requirements
 ------------
 
@@ -17,39 +21,27 @@ Platform-Specific Setup
 Generic Build Instructions
 --------------------------
 
-Setting up a basic release build:
+Setting up a basic parallelized release build:
 
 ```bash
-git clone https://github.com/leanprover/lean4 --recurse-submodules
+git clone https://github.com/leanprover/lean4
 cd lean4
-mkdir -p build/release
-cd build/release
-cmake ../..
-make
+cmake --preset release
+make -C build/release -j$(nproc)  # see below for macOS
 ```
-
-For regular development, we recommend running
-```bash
-git config submodule.recurse true
-```
-in the checkout so that `--recurse-submodules` doesn't have to be
-specified with `git pull/checkout/...`.
+You can replace `$(nproc)`, which is not available on macOS and some alternative shells, with the desired parallelism amount.
 
 The above commands will compile the Lean library and binaries into the
-`stage1` subfolder; see below for details. Add `-j N` for an
-appropriate `N` to `make` for a parallel build.
+`stage1` subfolder; see below for details.
 
-For example, on an AMD Ryzen 9 `make` takes 00:04:55, whereas `make -j 10`
-takes 00:01:38.  Your results may vary depending on the speed of your hard
-drive.
-
-You should not usually run `make install` after a successful build.
+You should not usually run `cmake --install` after a successful build.
 See [Dev setup using elan](../dev/index.md#dev-setup-using-elan) on how to properly set up your editor to use the correct stage depending on the source directory.
 
 Useful CMake Configuration Settings
 -----------------------------------
 
-Pass these along with the `cmake ../..` command.
+Pass these along with the `cmake --preset release` command.
+There are also two alternative presets that combine some of these options you can use instead of `release`: `debug` and `sandebug` (sanitize + debug).
 
 * `-D CMAKE_BUILD_TYPE=`\
   Select the build type. Valid values are `RELEASE` (default), `DEBUG`,

doc/make/msvc.md

@@ -1,39 +0,0 @@
-# Compiling Lean with Visual Studio
-
-WARNING: Compiling Lean with Visual Studio doesn't currently work.
-There's an ongoing effort to port Lean to Visual Studio.
-The instructions below are for VS 2017.
-
-In the meantime you can use [MSYS2](msys2.md) or [WSL](wsl.md).
-
-## Installing dependencies
-
-First, install `vcpkg` from https://github.com/Microsoft/vcpkg if you haven't
-done so already.
-Then, open a console in the directory you cloned `vcpkg` to, and type:
-`vcpkg install mpir` for the 32-bit library or
-`vcpkg install mpir:x64-windows` for the x64 one.
-
-In Visual Studio, use the "open folder" feature and open the Lean directory.
-Go to the `CMake->Change CMake Settings` menu. File `CMakeSettings.json` opens.
-In each of the targets, add the following snippet (i.e., after every
-`ctestCommandArgs`):
-
-```json
-    "variables": [
-      {
-        "name": "CMAKE_TOOLCHAIN_FILE",
-        "value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake"
-      }
-    ]
-```
-
-## Enable Intellisense
-
-In Visual Studio, press Ctrl+Q and type `CppProperties.json` and press Enter.
-Ensure `includePath` variables include `"${workspaceRoot}\\src"`.
-
-
-## Build Lean
-
-Press F7.

doc/make/msys2.md

@@ -38,10 +38,9 @@ cmake --version
 Then follow the [generic build instructions](index.md) in the MSYS2
 MinGW shell, using:
 ```
-cmake ../.. -G "Unix Makefiles"  -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
+cmake --preset release -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
 ```
-instead of `cmake ../..`. This ensures that cmake will call `sh` instead of `cmd.exe`
-for script tasks and it will use the clang compiler instead of gcc, which is required.
+instead of `cmake --preset release`. This will use the clang compiler instead of gcc, which is required with msys2.
 
 ## Install lean
 

doc/make/osx-10.9.md

@@ -1,4 +1,4 @@
-# Install Packages on OS X 10.9
+# Install Packages on OS X 14.5
 
 We assume that you are using [homebrew][homebrew] as a package manager.
 
@@ -22,7 +22,7 @@ brew install gcc
 ```
 To install clang++-3.5 via homebrew, please execute:
 ```bash
-brew install llvm --with-clang --with-asan
+brew install llvm
 ```
 To use compilers other than the default one (Apple's clang++), you
 need to use `-DCMAKE_CXX_COMPILER` option to specify the compiler

doc/setup.md

@@ -6,6 +6,7 @@ Platforms built & tested by our CI, available as binary releases via elan (see b
 
 * x86-64 Linux with glibc 2.27+
 * x86-64 macOS 10.15+
+* aarch64 (Apple Silicon) macOS 10.15+
 * x86-64 Windows 10+
 
 ### Tier 2
@@ -16,7 +17,6 @@ Releases may be silently broken due to the lack of automated testing.
 Issue reports and fixes are welcome.
 
 * aarch64 Linux with glibc 2.27+
-* aarch64 (Apple Silicon) macOS
 * x86 (32-bit) Linux
 * Emscripten Web Assembly
 

releases_drafts/README.md

@@ -0,0 +1,22 @@
+Draft release notes
+-------------------
+
+This folder contains drafts of release notes for inclusion in `RELEASES.md`.
+During the process to create a release candidate, we look through all the commits that make up the release
+to prepare the release notes, and in that process we take these drafts into account.
+
+Guidelines:
+- You should prefer adding release notes to commit messages over adding anything to this folder.
+  A release note should briefly explain the impact of a change from a user's point of view.
+  Please mark these parts out with words such as **release notes** and/or **breaking changes**.
+- It is not necessary to add anything to this folder. It is meant for larger features that span multiple PRs,
+  or for anything that would be helpful when preparing the release notes that might be missed
+  by someone reading through the change log.
+- If the PR that adds a feature simultaneously adds a draft release note, including the PR number is not required
+  since it can be obtained from the git history for the file.
+
+When release notes are prepared, all the draft release notes are deleted from this folder.
+For release candidates beyond the first one, you can either update `RELEASE.md` directly
+or continue to add drafts.
+
+When a release is finalized, we will copy the completed release notes from `RELEASE.md` to the `master` branch.

releases_drafts/messagedata.md

@@ -0,0 +1,13 @@
+* The `MessageData.ofPPFormat` constructor has been removed.
+  Its functionality has been split into two:
+
+  - for lazy structured messages, please use `MessageData.lazy`;
+  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
+
+  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
+
+* The `MessageData.ofFormat` constructor has been turned into a function.
+  If you need to inspect `MessageData`,
+  you can pattern-match on `MessageData.ofFormatWithInfos`.
+
+part of #3929

releases_drafts/wf.md

@@ -0,0 +1,12 @@
+Functions defined by well-founded recursion are now marked as
+`@[irreducible]`, which should prevent expensive and often unfruitful
+unfolding of such definitions.
+
+Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+rewritten to explictly unfold the function definition (using `simp`,
+`unfold`, `rw`), or the recursive function can be temporariliy made
+semireducible (using `unseal f in` before the command) or the function
+definition itself can be marked as `@[semireducible]` to get the previous
+behavor.
+
+#4061

src/CMakeLists.txt

@@ -11,7 +11,7 @@ project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 9)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
+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'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Init/Data/BitVec/Bitblast.lean

@@ -198,4 +198,41 @@ theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
 theorem ule_eq_carry (x y : BitVec w) : x.ule y = carry w y (~~~x) true := by
   simp [ule_eq_not_ult, ult_eq_not_carry]
 
+/-- If two bitvectors have the same `msb`, then signed and unsigned comparisons coincide -/
+theorem slt_eq_ult_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) :
+    x.slt y = x.ult y := by
+  simp only [BitVec.slt, toInt_eq_msb_cond, BitVec.ult, decide_eq_decide, h]
+  cases y.msb <;> simp
+
+/-- If two bitvectors have different `msb`s, then unsigned comparison is determined by this bit -/
+theorem ult_eq_msb_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
+    x.ult y = y.msb := by
+  simp only [BitVec.ult, msb_eq_decide, ne_eq, decide_eq_decide] at *
+  omega
+
+/-- If two bitvectors have different `msb`s, then signed and unsigned comparisons are opposites -/
+theorem slt_eq_not_ult_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
+    x.slt y = !x.ult y := by
+  simp only [BitVec.slt, toInt_eq_msb_cond, Bool.eq_not_of_ne h, ult_eq_msb_of_msb_neq h]
+  cases y.msb <;> (simp; omega)
+
+theorem slt_eq_ult (x y : BitVec w) :
+    x.slt y = (x.msb != y.msb).xor (x.ult y) := by
+  by_cases h : x.msb = y.msb
+  · simp [h, slt_eq_ult_of_msb_eq]
+  · have h' : x.msb != y.msb := by simp_all
+    simp [slt_eq_not_ult_of_msb_neq h, h']
+
+theorem slt_eq_not_carry (x y : BitVec w) :
+    x.slt y = (x.msb == y.msb).xor (carry w x (~~~y) true) := by
+  simp only [slt_eq_ult, bne, ult_eq_not_carry]
+  cases x.msb == y.msb <;> simp
+
+theorem sle_eq_not_slt (x y : BitVec w) : x.sle y = !y.slt x := by
+  simp only [BitVec.sle, BitVec.slt, ← decide_not, decide_eq_decide]; omega
+
+theorem sle_eq_carry (x y : BitVec w) :
+    x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true)) := by
+  rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -10,6 +10,7 @@ import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
+import Init.Data.Int.Bitwise.Lemmas
 
 namespace BitVec
 
@@ -141,6 +142,8 @@ theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b'
 @[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
   simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
 
+@[simp] theorem toFin_ofNat (x : Nat) : toFin x#w = Fin.ofNat' x (Nat.two_pow_pos w) := rfl
+
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
 -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
 theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
@@ -175,8 +178,7 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
     x.getLsb (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by
   rcases w with rfl | w
   · simp
-  · simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
-    Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
+  · simp only [getLsb, Nat.testBit_to_div_mod, Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
     rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
     · simp [Nat.div_eq_of_lt h, h]
     · simp only [h]
@@ -280,6 +282,9 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
   have p : 0 ≤ i % (2^n : Nat) := by omega
   simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
 
+@[simp] theorem ofInt_natCast (w n : Nat) :
+  BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl
+
 /-! ### zeroExtend and truncate -/
 
 @[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
@@ -462,6 +467,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   ext
   simp
 
+theorem or_assoc (x y z : BitVec w) :
+    x ||| y ||| z = x ||| (y ||| z) := by
+  ext i
+  simp [Bool.or_assoc]
+
 /-! ### and -/
 
 @[simp] theorem toNat_and (x y : BitVec v) :
@@ -488,6 +498,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   ext
   simp
 
+theorem and_assoc (x y z : BitVec w) :
+    x &&& y &&& z = x &&& (y &&& z) := by
+  ext i
+  simp [Bool.and_assoc]
+
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :
@@ -508,6 +523,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   ext
   simp
 
+theorem xor_assoc (x y z : BitVec w) :
+    x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by
+  ext i
+  simp [Bool.xor_assoc]
+
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@@ -642,6 +662,70 @@ theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
     getLsb (x >>> i) j = getLsb x (i+j) := by
   unfold getLsb ; simp
 
+/-! ### sshiftRight -/
+
+theorem sshiftRight_eq {x : BitVec n} {i : Nat} :
+    x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i) := by
+  apply BitVec.eq_of_toInt_eq
+  simp [BitVec.sshiftRight]
+
+/-- if the msb is false, the arithmetic shift right equals logical shift right -/
+theorem sshiftRight_eq_of_msb_false {x : BitVec w} {s : Nat} (h : x.msb = false) :
+    (x.sshiftRight s) = x >>> s := by
+  apply BitVec.eq_of_toNat_eq
+  rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond]
+  have hxbound : 2 * x.toNat < 2 ^ w := (BitVec.msb_eq_false_iff_two_mul_lt x).mp h
+  simp only [hxbound, ↓reduceIte, Int.natCast_shiftRight, Int.ofNat_eq_coe, ofInt_natCast,
+    toNat_ofNat, toNat_ushiftRight]
+  replace hxbound : x.toNat >>> s < 2 ^ w := by
+    rw [Nat.shiftRight_eq_div_pow]
+    exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) x.isLt
+  apply Nat.mod_eq_of_lt hxbound
+
+/--
+If the msb is `true`, the arithmetic shift right equals negating,
+then logical shifting right, then negating again.
+The double negation preserves the lower bits that have been shifted,
+and the outer negation ensures that the high bits are '1'. -/
+theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
+    (x.sshiftRight s) = ~~~((~~~x) >>> s) := by
+  apply BitVec.eq_of_toNat_eq
+  rcases w with rfl | w
+  · simp
+  · rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond]
+    have hxbound : (2 * x.toNat ≥ 2 ^ (w + 1)) := (BitVec.msb_eq_true_iff_two_mul_ge x).mp h
+    replace hxbound : ¬ (2 * x.toNat < 2 ^ (w + 1)) := by omega
+    simp only [hxbound, ↓reduceIte, toNat_ofInt, toNat_not, toNat_ushiftRight]
+    rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (by omega),
+        Nat.pred_eq_sub_one, Int.negSucc_shiftRight,
+        Int.emod_negSucc, Int.natAbs_ofNat, Nat.succ_eq_add_one,
+        Int.subNatNat_of_le (by omega), Int.toNat_ofNat, Nat.mod_eq_of_lt,
+        Nat.sub_right_comm]
+    omega
+    · rw [Nat.shiftRight_eq_div_pow]
+      apply Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (by omega)
+
+theorem getLsb_sshiftRight (x : BitVec w) (s i : Nat) :
+    getLsb (x.sshiftRight s) i =
+      (!decide (w ≤ i) && if s + i < w then x.getLsb (s + i) else x.msb) := by
+  rcases hmsb : x.msb with rfl | rfl
+  · simp only [sshiftRight_eq_of_msb_false hmsb, getLsb_ushiftRight, Bool.if_false_right]
+    by_cases hi : i ≥ w
+    · simp only [hi, decide_True, Bool.not_true, Bool.false_and]
+      apply getLsb_ge
+      omega
+    · simp only [hi, decide_False, Bool.not_false, Bool.true_and, Bool.iff_and_self,
+        decide_eq_true_eq]
+      intros hlsb
+      apply BitVec.lt_of_getLsb _ _ hlsb
+  · by_cases hi : i ≥ w
+    · simp [hi]
+    · simp only [sshiftRight_eq_of_msb_true hmsb, getLsb_not, getLsb_ushiftRight, Bool.not_and,
+        Bool.not_not, hi, decide_False, Bool.not_false, Bool.if_true_right, Bool.true_and,
+        Bool.and_iff_right_iff_imp, Bool.or_eq_true, Bool.not_eq_true', decide_eq_false_iff_not,
+        Nat.not_lt, decide_eq_true_eq]
+      omega
+
 /-! ### append -/
 
 theorem append_def (x : BitVec v) (y : BitVec w) :
@@ -925,6 +1009,10 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : x#n - y#n = .ofNat n (x + (2^n - y % 2
 @[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
   simp [Neg.neg, BitVec.neg]
 
+@[simp] theorem toFin_neg (x : BitVec n) :
+    (-x).toFin = Fin.ofNat' (2^n - x.toNat) (Nat.two_pow_pos _) :=
+  rfl
+
 theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
   apply eq_of_toNat_eq
   simp
@@ -1070,8 +1158,126 @@ theorem rotateLeft_eq_rotateLeftAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w)
     x.rotateLeft r = x.rotateLeftAux r := by
   simp only [rotateLeft, Nat.mod_eq_of_lt hr]
 
+
+/--
+Accessing bits in `x.rotateLeft r` the range `[0, r)` is equal to
+accessing bits `x` in the range `[w - r, w)`.
+
+Proof by example:
+Let x := <6 5 4 3 2 1 0> : BitVec 7.
+x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
+
+(x.rotateLeft 2).getLsb ⟨i, i < 2⟩
+= <3 2 1 0 | 6 5>.getLsb ⟨i, i < 2⟩
+= <6 5>[i]
+= <6 5 | 4 3 2 1 0>[i + len(<4 3 2 1 0>)]
+= <6 5 | 4 3 2 1 0>[i + 7 - 2]
+-/
+theorem getLsb_rotateLeftAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
+    (x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i) := by
+  rw [rotateLeftAux, getLsb_or, getLsb_ushiftRight]
+  suffices (x <<< r).getLsb i = false by
+    simp; omega
+  simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
+    Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
+  omega
+
+/--
+Accessing bits in `x.rotateLeft r` the range `[r, w)` is equal to
+accessing bits `x` in the range `[0, w - r)`.
+
+Proof by example:
+Let x := <6 5 4 3 2 1 0> : BitVec 7.
+x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>
+
+(x.rotateLeft 2).getLsb ⟨i, i ≥ 2⟩
+= <3 2 1 0 | 6 5>.getLsb ⟨i, i ≥ 2⟩
+= <3 2 1 0>[i - 2]
+= <6 5 | 3 2 1 0>[i - 2]
+
+Intuitively, grab the full width (7), then move the marker `|` by `r` to the right `(-2)`
+Then, access the bit at `i` from the right `(+i)`.
+ -/
+theorem getLsb_rotateLeftAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
+    (x.rotateLeftAux r).getLsb i = (decide (i < w) && x.getLsb (i - r)) := by
+  rw [rotateLeftAux, getLsb_or]
+  suffices (x >>> (w - r)).getLsb i = false by
+    have hiltr : decide (i < r) = false := by
+      simp [hi]
+    simp [getLsb_shiftLeft, Bool.or_false, hi, hiltr, this]
+  simp only [getLsb_ushiftRight]
+  apply getLsb_ge
+  omega
+
+/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
+theorem getLsb_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
+    (x.rotateLeft r).getLsb i =
+      cond (i < r)
+      (x.getLsb (w - r + i))
+      (decide (i < w) && x.getLsb (i - r)) := by
+  · rw [rotateLeft_eq_rotateLeftAux_of_lt hr]
+    by_cases h : i < r
+    · simp [h, getLsb_rotateLeftAux_of_le h]
+    · simp [h, getLsb_rotateLeftAux_of_geq <| Nat.ge_of_not_lt h]
+
+@[simp]
+theorem getLsb_rotateLeft {x : BitVec w} {r i : Nat}  :
+    (x.rotateLeft r).getLsb i =
+      cond (i < r % w)
+      (x.getLsb (w - (r % w) + i))
+      (decide (i < w) && x.getLsb (i - (r % w))) := by
+  rcases w with ⟨rfl, w⟩
+  · simp
+  · rw [← rotateLeft_mod_eq_rotateLeft, getLsb_rotateLeft_of_le (Nat.mod_lt _ (by omega))]
+
 /-! ## Rotate Right -/
 
+/--
+Accessing bits in `x.rotateRight r` the range `[0, w-r)` is equal to
+accessing bits `x` in the range `[r, w)`.
+
+Proof by example:
+Let x := <6 5 4 3 2 1 0> : BitVec 7.
+x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>
+
+(x.rotateLeft 2).getLsb ⟨i, i ≤ 7 - 2⟩
+= <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩
+= <6 5 4 3 2>.getLsb i
+= <6 5 4 3 2 | 1 0>[i + 2]
+-/
+theorem getLsb_rotateRightAux_of_le {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
+    (x.rotateRightAux r).getLsb i = x.getLsb (r + i) := by
+  rw [rotateRightAux, getLsb_or, getLsb_ushiftRight]
+  suffices (x <<< (w - r)).getLsb i = false by
+    simp only [this, Bool.or_false]
+  simp only [getLsb_shiftLeft, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
+    Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
+  omega
+
+/--
+Accessing bits in `x.rotateRight r` the range `[w-r, w)` is equal to
+accessing bits `x` in the range `[0, r)`.
+
+Proof by example:
+Let x := <6 5 4 3 2 1 0> : BitVec 7.
+x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>
+
+(x.rotateLeft 2).getLsb ⟨i, i ≥ 7 - 2⟩
+= <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩
+= <1 0>.getLsb (i - len(<6 5 4 3 2>)
+= <6 5 4 3 2 | 1 0> (i - len<6 4 4 3 2>)
+ -/
+theorem getLsb_rotateRightAux_of_geq {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ w - r) :
+    (x.rotateRightAux r).getLsb i = (decide (i < w) && x.getLsb (i - (w - r))) := by
+  rw [rotateRightAux, getLsb_or]
+  suffices (x >>> r).getLsb i = false by
+    simp only [this, getLsb_shiftLeft, Bool.false_or]
+    by_cases hiw : i < w
+    <;> simp [hiw, hi]
+  simp only [getLsb_ushiftRight]
+  apply getLsb_ge
+  omega
+
 /-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
 smaller than the bitwidth. -/
 theorem rotateRight_eq_rotateRightAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :
@@ -1084,4 +1290,25 @@ theorem rotateRight_mod_eq_rotateRight {x : BitVec w} {r : Nat} :
     x.rotateRight (r % w) = x.rotateRight r := by
   simp only [rotateRight, Nat.mod_mod]
 
+/-- When `r < w`, we give a formula for `(x.rotateRight r).getLsb i`. -/
+theorem getLsb_rotateRight_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
+    (x.rotateRight r).getLsb i =
+      cond (i < w - r)
+      (x.getLsb (r + i))
+      (decide (i < w) && x.getLsb (i - (w - r))) := by
+  · rw [rotateRight_eq_rotateRightAux_of_lt hr]
+    by_cases h : i < w - r
+    · simp [h, getLsb_rotateRightAux_of_le h]
+    · simp [h, getLsb_rotateRightAux_of_geq <| Nat.le_of_not_lt h]
+
+@[simp]
+theorem getLsb_rotateRight {x : BitVec w} {r i : Nat} :
+    (x.rotateRight r).getLsb i =
+      cond (i < w - (r % w))
+      (x.getLsb ((r % w) + i))
+      (decide (i < w) && x.getLsb (i - (w - (r % w)))) := by
+  rcases w with ⟨rfl, w⟩
+  · simp
+  · rw [← rotateRight_mod_eq_rotateRight, getLsb_rotateRight_of_le (Nat.mod_lt _ (by omega))]
+
 end BitVec

src/Init/Data/Bool.lean

@@ -227,6 +227,8 @@ instance : Std.Associative (· != ·) := ⟨bne_assoc⟩
 @[simp] theorem bne_left_inj  : ∀ (x y z : Bool), (x != y) = (x != z) ↔ y = z := by decide
 @[simp] theorem bne_right_inj : ∀ (x y z : Bool), (x != z) = (y != z) ↔ x = y := by decide
 
+theorem eq_not_of_ne : ∀ {x y : Bool}, x ≠ y → x = !y := by decide
+
 /-! ### coercision related normal forms -/
 
 theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :

src/Init/Data/Fin/Fold.lean

@@ -6,6 +6,8 @@ Authors: François G. Dorais
 prelude
 import Init.Data.Nat.Linear
 
+namespace Fin
+
 /-- Folds over `Fin n` from the left: `foldl 3 f x = f (f (f x 0) 1) 2`. -/
 @[inline] def foldl (n) (f : α → Fin n → α) (init : α) : α := loop init 0 where
   /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
@@ -20,3 +22,5 @@ import Init.Data.Nat.Linear
   loop : {i // i ≤ n} → α → α
   | ⟨0, _⟩, x => x
   | ⟨i+1, h⟩, x => loop ⟨i, Nat.le_of_lt h⟩ (f ⟨i, h⟩ x)
+
+end Fin

src/Init/Data/Int/Bitwise/Lemmas.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2023 Siddharth Bhat. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddharth Bhat, Jeremy Avigad
+-/
+prelude
+import Init.Data.Nat.Bitwise.Lemmas
+import Init.Data.Int.Bitwise
+
+namespace Int
+
+theorem shiftRight_eq (n : Int) (s : Nat) : n >>> s = Int.shiftRight n s := rfl
+@[simp]
+theorem natCast_shiftRight (n s : Nat) : (n : Int) >>> s = n >>> s := rfl
+
+@[simp]
+theorem negSucc_shiftRight (m n : Nat) :
+    -[m+1] >>> n = -[m >>>n +1] := rfl
+
+theorem shiftRight_add (i : Int) (m n : Nat) :
+    i >>> (m + n) = i >>> m >>> n := by
+  simp only [shiftRight_eq, Int.shiftRight]
+  cases i <;> simp [Nat.shiftRight_add]
+
+theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
+    m >>> n = m / ((2 ^ n) : Nat) := by
+  simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow]
+  split
+  · simp
+  · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]
+    rfl
+
+@[simp]
+theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
+  simp [Int.shiftRight_eq_div_pow]
+
+end Int

src/Init/Data/Int/DivModLemmas.lean

@@ -420,6 +420,9 @@ theorem negSucc_emod (m : Nat) {b : Int} (bpos : 0 < b) : -[m+1] % b = b - 1 - m
   match b, eq_succ_of_zero_lt bpos with
   | _, ⟨n, rfl⟩ => rfl
 
+theorem emod_negSucc (m : Nat) (n : Int) :
+  (Int.negSucc m) % n = Int.subNatNat (Int.natAbs n) (Nat.succ (m % Int.natAbs n)) := rfl
+
 theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl
 
 theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b

src/Init/Data/Int/Order.lean

@@ -813,6 +813,20 @@ protected theorem sub_lt_sub_right {a b : Int} (h : a < b) (c : Int) : a - c < b
 protected theorem sub_lt_sub {a b c d : Int} (hab : a < b) (hcd : c < d) : a - d < b - c :=
   Int.add_lt_add hab (Int.neg_lt_neg hcd)
 
+protected theorem lt_of_sub_lt_sub_left {a b c : Int} (h : c - a < c - b) : b < a :=
+  Int.lt_of_neg_lt_neg <| Int.lt_of_add_lt_add_left h
+
+protected theorem lt_of_sub_lt_sub_right {a b c : Int} (h : a - c < b - c) : a < b :=
+  Int.lt_of_add_lt_add_right h
+
+@[simp] protected theorem sub_lt_sub_left_iff (a b c : Int) :
+    c - a < c - b ↔ b < a :=
+  ⟨Int.lt_of_sub_lt_sub_left, (Int.sub_lt_sub_left · c)⟩
+
+@[simp] protected theorem sub_lt_sub_right_iff (a b c : Int) :
+    a - c < b - c ↔ a < b :=
+  ⟨Int.lt_of_sub_lt_sub_right, (Int.sub_lt_sub_right · c)⟩
+
 protected theorem sub_lt_sub_of_le_of_lt {a b c d : Int}
   (hab : a ≤ b) (hcd : c < d) : a - d < b - c :=
   Int.add_lt_add_of_le_of_lt hab (Int.neg_lt_neg hcd)

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -78,6 +78,8 @@ of a number.
 -/
 
 /-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/
-def testBit (m n : Nat) : Bool := (m >>> n) &&& 1 != 0
+def testBit (m n : Nat) : Bool :=
+  -- `1 &&& n` is faster than `n &&& 1` for big `n`.
+  1 &&& (m >>> n) != 0
 
 end Nat

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -60,6 +60,13 @@ noncomputable def div2Induction {motive : Nat → Sort u}
   unfold bitwise
   simp
 
+@[simp] theorem one_and_eq_mod_two (n : Nat) : 1 &&& n = n % 2 := by
+  if n0 : n = 0 then
+    subst n0; decide
+  else
+    simp only [HAnd.hAnd, AndOp.and, land]
+    cases mod_two_eq_zero_or_one n with | _ h => simp [bitwise, n0, h]
+
 @[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
   if xz : x = 0 then
     simp [xz, zero_and]
@@ -74,7 +81,7 @@ noncomputable def div2Induction {motive : Nat → Sort u}
 /-! ### testBit -/
 
 @[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
-  simp only [testBit, zero_shiftRight, zero_and, bne_self_eq_false]
+  simp only [testBit, zero_shiftRight, and_zero, bne_self_eq_false]
 
 @[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
   cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]

src/Init/Data/Option/Lemmas.lean

@@ -101,7 +101,7 @@ theorem ball_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x)
 @[simp] theorem bind_none (x : Option α) : x.bind (fun _ => none (α := β)) = none := by
   cases x <;> rfl
 
-@[simp] theorem bind_eq_some : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by
+theorem bind_eq_some : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b := by
   cases x <;> simp
 
 @[simp] theorem bind_eq_none {o : Option α} {f : α → Option β} :
@@ -119,7 +119,7 @@ theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ)
     (x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl
 
 theorem join_eq_some : x.join = some a ↔ x = some (some a) := by
-  simp
+  simp [bind_eq_some]
 
 theorem join_ne_none : x.join ≠ none ↔ ∃ z, x = some (some z) := by
   simp only [ne_none_iff_exists', join_eq_some, iff_self]

src/Init/Tactics.lean

@@ -835,7 +835,8 @@ syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic
 /--
 `repeat tac` repeatedly applies `tac` to the main goal until it fails.
 That is, if `tac` produces multiple subgoals, only subgoals up to the first failure will be visited.
-The `Batteries` library provides `repeat'` which repeats separately in each subgoal.
+
+See also the tactic `repeat'` which repeats separately in each subgoal.
 -/
 syntax "repeat " tacticSeq : tactic
 macro_rules

src/Lean/Attributes.lean

@@ -67,13 +67,11 @@ def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do
   Helper methods for decoding the parameters of builtin attributes that are defined before `Lean.Parser`.
   We have the following ones:
   ```
-  @[builtin_attr_parser] def simple     := leading_parser ident >> optional ident >> optional priorityParser
-  /- We can't use `simple` for `class`, `instance`, `export` and `macro` because they are  keywords. -/
-  @[builtin_attr_parser] def «class»    := leading_parser "class"
-  @[builtin_attr_parser] def «instance» := leading_parser "instance" >> optional priorityParser
+  @[builtin_attr_parser] def simple     := leading_parser ident >> optional (ppSpace >> (priorityParser <|> ident))
   @[builtin_attr_parser] def «macro»    := leading_parser "macro " >> ident
+  @[builtin_attr_parser] def «export»   := leading_parser "export " >> ident
   ```
-  Note that we need the parsers for `class`, `instance`, and `macros` because they are keywords.
+  Note that we need the parsers for `class`, `instance`, `export` and `macros` because they are keywords.
 -/
 
 def Attribute.Builtin.ensureNoArgs (stx : Syntax) : AttrM Unit := do

src/Lean/Compiler/ConstFolding.lean

@@ -193,12 +193,13 @@ def foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr := do
   else
     return mkUInt32Lit 0
 
-def foldToNat (_ : Bool) (a : Expr) : Option Expr := do
+def foldToNat (size : Nat) (_ : Bool) (a : Expr) : Option Expr := do
   let n ← getNumLit a
-  return mkRawNatLit n
+  return mkRawNatLit (n % size)
+
 
 def uintFoldToNatFns : List (Name × UnFoldFn) :=
-  numScalarTypes.foldl (fun r info => (info.toNatFn, foldToNat) :: r) []
+  numScalarTypes.foldl (fun r info => (info.toNatFn, foldToNat info.size) :: r) []
 
 def unFoldFns : List (Name × UnFoldFn) :=
   [(``Nat.succ, foldNatSucc),

src/Lean/Compiler/InitAttr.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.AddDecl
+import Lean.MonadEnv
 import Lean.Elab.InfoTree.Main
 
 namespace Lean
@@ -139,7 +140,7 @@ def setBuiltinInitAttr (env : Environment) (declName : Name) (initFnName : Name
   builtinInitAttr.setParam env declName initFnName
 
 def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do
-  let name := `_regBuiltin ++ forDecl
+  let name ← mkAuxName (`_regBuiltin ++ forDecl) 1
   let type := mkApp (mkConst `IO) (mkConst `Unit)
   let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,
                                      safety := DefinitionSafety.safe }

src/Lean/Elab/Command.lean

@@ -296,11 +296,29 @@ private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArr
   }
   return InfoTree.context ctx tree
 
+/--
+Disables incremental command reuse *and* reporting for `act` if `cond` is true by setting
+`Context.snap?` to `none`.
+-/
+def withoutCommandIncrementality (cond : Bool) (act : CommandElabM α) : CommandElabM α := do
+  let opts ← getOptions
+  withReader (fun ctx => { ctx with snap? := ctx.snap?.filter fun snap => Id.run do
+    if let some old := snap.old? then
+      if cond && opts.getBool `trace.Elab.reuse then
+        dbg_trace "reuse stopped: guard failed at {old.stx}"
+    return !cond
+  }) act
+
 private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Unit
   | []                => withInfoTreeContext (mkInfoTree := mkInfoTree `no_elab stx) <| throwError "unexpected syntax{indentD stx}"
   | (elabFn::elabFns) =>
     catchInternalId unsupportedSyntaxExceptionId
-      (withInfoTreeContext (mkInfoTree := mkInfoTree elabFn.declName stx) <| elabFn.value stx)
+      (do
+        -- prevent unsupported commands from accidentally accessing `Context.snap?` (e.g. by nested
+        -- supported commands)
+        withoutCommandIncrementality (!(← isIncrementalElab elabFn.declName)) do
+        withInfoTreeContext (mkInfoTree := mkInfoTree elabFn.declName stx) do
+         elabFn.value stx)
       (fun _ => do set s; elabCommandUsing s stx elabFns)
 
 /-- Elaborate `x` with `stx` on the macro stack -/
@@ -327,7 +345,10 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
       if k == nullKind then
         -- list of commands => elaborate in order
         -- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
-        args.forM elabCommand
+        -- TODO: support incrementality at least for some cases such as expansions of
+        -- `set_option in` or `def a.b`
+        withoutCommandIncrementality true do
+          args.forM elabCommand
       else withTraceNode `Elab.command (fun _ => return stx) (tag :=
         -- special case: show actual declaration kind for `declaration` commands
         (if stx.isOfKind ``Parser.Command.declaration then stx[1] else stx).getKind.toString) do

src/Lean/Elab/Declaration.lean

@@ -188,7 +188,7 @@ def elabClassInductive (modifiers : Modifiers) (stx : Syntax) : CommandElabM Uni
   let v ← classInductiveSyntaxToView modifiers stx
   elabInductiveViews #[v]
 
-@[builtin_command_elab declaration]
+@[builtin_command_elab declaration, builtin_incremental]
 def elabDeclaration : CommandElab := fun stx => do
   match (← liftMacroM <| expandDeclNamespace? stx) with
   | some (ns, newStx) => do
@@ -198,22 +198,24 @@ def elabDeclaration : CommandElab := fun stx => do
   | none => do
     let decl     := stx[1]
     let declKind := decl.getKind
-    if declKind == ``Lean.Parser.Command.«axiom» then
-      let modifiers ← elabModifiers stx[0]
-      elabAxiom modifiers decl
-    else if declKind == ``Lean.Parser.Command.«inductive» then
-      let modifiers ← elabModifiers stx[0]
-      elabInductive modifiers decl
-    else if declKind == ``Lean.Parser.Command.classInductive then
-      let modifiers ← elabModifiers stx[0]
-      elabClassInductive modifiers decl
-    else if declKind == ``Lean.Parser.Command.«structure» then
-      let modifiers ← elabModifiers stx[0]
-      elabStructure modifiers decl
-    else if isDefLike decl then
+    if isDefLike decl then
+      -- only case implementing incrementality currently
       elabMutualDef #[stx]
-    else
-      throwError "unexpected declaration"
+    else withoutCommandIncrementality true do
+      if declKind == ``Lean.Parser.Command.«axiom» then
+        let modifiers ← elabModifiers stx[0]
+        elabAxiom modifiers decl
+      else if declKind == ``Lean.Parser.Command.«inductive» then
+        let modifiers ← elabModifiers stx[0]
+        elabInductive modifiers decl
+      else if declKind == ``Lean.Parser.Command.classInductive then
+        let modifiers ← elabModifiers stx[0]
+        elabClassInductive modifiers decl
+      else if declKind == ``Lean.Parser.Command.«structure» then
+        let modifiers ← elabModifiers stx[0]
+        elabStructure modifiers decl
+      else
+        throwError "unexpected declaration"
 
 /-- Return true if all elements of the mutual-block are inductive declarations. -/
 private def isMutualInductive (stx : Syntax) : Bool :=
@@ -322,14 +324,16 @@ def expandMutualPreamble : Macro := fun stx =>
     let endCmd    ← `(end)
     return mkNullNode (#[secCmd] ++ preamble ++ #[newMutual] ++ #[endCmd])
 
-@[builtin_command_elab «mutual»]
+@[builtin_command_elab «mutual», builtin_incremental]
 def elabMutual : CommandElab := fun stx => do
-  if isMutualInductive stx then
-    elabMutualInductive stx[1].getArgs
-  else if isMutualDef stx then
+  if isMutualDef stx then
+    -- only case implementing incrementality currently
     elabMutualDef stx[1].getArgs
-  else
-    throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
+  else withoutCommandIncrementality true do
+    if isMutualInductive stx then
+      elabMutualInductive stx[1].getArgs
+    else
+      throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
 
 /- leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "]" >> many1 ident -/
 @[builtin_command_elab «attribute»] def elabAttr : CommandElab := fun stx => do

src/Lean/Elab/DefView.lean

@@ -84,10 +84,10 @@ instance : Language.ToSnapshotTree HeaderProcessedSnapshot where
 /-- State before elaboration of a mutual definition. -/
 structure DefParsed where
   /--
-  Input substring uniquely identifying header elaboration result given the same `Environment`.
-  If missing, results should never be reused.
+  Unstructured syntax object comprising the full "header" of the definition from the modifiers
+  (incl. docstring) up to the value, used for determining header elaboration reuse.
   -/
-  headerSubstr? : Option Substring
+  fullHeaderRef : Syntax
   /-- Elaboration result, unless fatal exception occurred. -/
   headerProcessedSnap : SnapshotTask (Option HeaderProcessedSnapshot)
 deriving Nonempty
@@ -106,6 +106,11 @@ end Snapshots
 structure DefView where
   kind          : DefKind
   ref           : Syntax
+  /--
+  An unstructured syntax object that comprises the "header" of the definition, i.e. everything up
+  to the value. Used as a more specific ref for header elaboration.
+  -/
+  headerRef     : Syntax
   modifiers     : Modifiers
   declId        : Syntax
   binders       : Syntax
@@ -132,20 +137,20 @@ def mkDefViewOfAbbrev (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let (binders, type) := expandOptDeclSig stx[2]
   let modifiers       := modifiers.addAttribute { name := `inline }
   let modifiers       := modifiers.addAttribute { name := `reducible }
-  { ref := stx, kind := DefKind.abbrev, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.abbrev, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3] }
 
 def mkDefViewOfDef (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "def " >> declId >> optDeclSig >> declVal >> optDefDeriving
   let (binders, type) := expandOptDeclSig stx[2]
   let deriving? := if stx[4].isNone then none else some stx[4][1].getSepArgs
-  { ref := stx, kind := DefKind.def, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.def, modifiers,
     declId := stx[1], binders, type? := type, value := stx[3], deriving? }
 
 def mkDefViewOfTheorem (modifiers : Modifiers) (stx : Syntax) : DefView :=
   -- leading_parser "theorem " >> declId >> declSig >> declVal
   let (binders, type) := expandDeclSig stx[2]
-  { ref := stx, kind := DefKind.theorem, modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.theorem, modifiers,
     declId := stx[1], binders, type? := some type, value := stx[3] }
 
 def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
@@ -166,7 +171,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
       trace[Elab.instance.mkInstanceName] "generated {(← getCurrNamespace) ++ id}"
       pure <| mkNode ``Parser.Command.declId #[mkIdentFrom stx id, mkNullNode]
   return {
-    ref := stx, kind := DefKind.def, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:5], kind := DefKind.def, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[5]
   }
 
@@ -179,7 +184,7 @@ def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefV
       let val ← if modifiers.isUnsafe then `(default_or_ofNonempty% unsafe) else `(default_or_ofNonempty%)
       `(Parser.Command.declValSimple| := $val)
   return {
-    ref := stx, kind := DefKind.opaque, modifiers := modifiers,
+    ref := stx, headerRef := mkNullNode stx.getArgs[:3], kind := DefKind.opaque, modifiers := modifiers,
     declId := stx[1], binders := binders, type? := some type, value := val
   }
 
@@ -188,7 +193,7 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
   let (binders, type) := expandOptDeclSig stx[1]
   let id              := mkIdentFrom stx `_example
   let declId          := mkNode ``Parser.Command.declId #[id, mkNullNode]
-  { ref := stx, kind := DefKind.example, modifiers := modifiers,
+  { ref := stx, headerRef := mkNullNode stx.getArgs[:2], kind := DefKind.example, modifiers := modifiers,
     declId := declId, binders := binders, type? := type, value := stx[2] }
 
 def isDefLike (stx : Syntax) : Bool :=

src/Lean/Elab/Deriving/DecEq.lean

@@ -182,7 +182,8 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
       fun x y =>
         if h : x.toCtorIdx = y.toCtorIdx then
           -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct.
-          isTrue (by first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
+          -- Temporarily avoiding tactic `have` for bootstrapping
+          isTrue (by first | refine_lift have aux := congrArg $ofNatIdent h; ?_; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
         else
           isFalse fun h => by subst h; contradiction
   )

src/Lean/Elab/Do.lean

@@ -688,27 +688,15 @@ def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) :=
   -- leading_parser "let " >> optional "mut " >> letDecl
   getLetDeclVars doLet[2]
 
-def getHaveIdLhsVar (optIdent : Syntax) : Var :=
-  if optIdent.getKind == hygieneInfoKind then
-    HygieneInfo.mkIdent optIdent[0] `this
-  else
-    optIdent
-
-def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) := do
-  -- doHave := leading_parser "have " >> Term.haveDecl
-  -- haveDecl := leading_parser haveIdDecl <|> letPatDecl <|> haveEqnsDecl
-  let arg := doHave[1][0]
-  if arg.getKind == ``Parser.Term.haveIdDecl then
-    -- haveIdDecl := leading_parser atomic (haveIdLhs >> " := ") >> termParser
-    -- haveIdLhs := (binderIdent <|> hygieneInfo) >> many letIdBinder >> optType
-    return #[getHaveIdLhsVar arg[0]]
-  else if arg.getKind == ``Parser.Term.letPatDecl then
-    getLetPatDeclVars arg
-  else if arg.getKind == ``Parser.Term.haveEqnsDecl then
-    -- haveEqnsDecl := leading_parser haveIdLhs >> matchAlts
-    return #[getHaveIdLhsVar arg[0]]
-  else
-    throwError "unexpected kind of have declaration"
+def getDoHaveVars : Syntax → TermElabM (Array Var)
+  -- NOTE: `hygieneInfo` case should come first as `id` will match anything else
+  | `(doElem| have $info:hygieneInfo $_params* $[$_:typeSpec]? := $_val)
+  | `(doElem| have $info:hygieneInfo $_params* $[$_:typeSpec]? $_eqns:matchAlts) =>
+    return #[HygieneInfo.mkIdent info `this]
+  | `(doElem| have $id $_params* $[$_:typeSpec]? := $_val)
+  | `(doElem| have $id $_params* $[$_:typeSpec]? $_eqns:matchAlts) => return #[id]
+  | `(doElem| have $pat:letPatDecl) => getLetPatDeclVars pat
+  | _ => throwError "unexpected kind of have declaration"
 
 def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var) := do
   -- letRecDecls is an array of `(group (optional attributes >> letDecl))`

src/Lean/Elab/MacroArgUtil.lean

@@ -56,13 +56,11 @@ where
           return ⟨Syntax.mkAntiquotNode kind term⟩
         | some (.category cat) =>
           return ⟨Syntax.mkAntiquotNode cat term (isPseudoKind := true)⟩
-        | none =>
+        | some (.alias _) =>
           let id := id.getId.eraseMacroScopes
-          if (← Parser.isParserAlias id) then
-            let kind := (← Parser.getSyntaxKindOfParserAlias? id).getD Name.anonymous
-            return ⟨Syntax.mkAntiquotNode kind term⟩
-          else
-            throwError "unknown parser declaration/category/alias '{id}'"
+          let kind := (← Parser.getSyntaxKindOfParserAlias? id).getD Name.anonymous
+          return ⟨Syntax.mkAntiquotNode kind term⟩
+        | _ => throwError "unknown parser declaration/category/alias '{id}'"
     | stx, term => do
       -- can't match against `` `(stx| ($stxs*)) `` as `*` is interpreted as the `stx` operator
       if stx.raw.isOfKind ``Parser.Syntax.paren then

src/Lean/Elab/MutualDef.lean

@@ -131,7 +131,7 @@ private def elabHeaders (views : Array DefView)
     (bodyPromises : Array (IO.Promise (Option BodyProcessedSnapshot)))
     (tacPromises : Array (IO.Promise Tactic.TacticParsedSnapshot)) :
     TermElabM (Array DefViewElabHeader) := do
-  let expandedDeclIds ← views.mapM fun view => withRef view.ref do
+  let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do
     Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
   withAutoBoundImplicitForbiddenPred (fun n => expandedDeclIds.any (·.shortName == n)) do
     let mut headers := #[]
@@ -181,9 +181,13 @@ private def elabHeaders (views : Array DefView)
           reuseBody := false
 
       let header ← withRestoreOrSaveFull reusableResult? fun save => do
-        withRef view.ref do
-        addDeclarationRanges declName view.ref
+        withRef view.headerRef do
+        addDeclarationRanges declName view.ref  -- NOTE: this should be the full `ref`
         applyAttributesAt declName view.modifiers.attrs .beforeElaboration
+        -- do not hide header errors on partial body syntax as these two elaboration parts are
+        -- sufficiently independent
+        withTheReader Core.Context ({ · with suppressElabErrors :=
+          view.headerRef.hasMissing && !Command.showPartialSyntaxErrors.get (← getOptions) }) do
         withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
           elabBindersEx view.binders.getArgs fun xs => do
             let refForElabFunType := view.value
@@ -961,40 +965,41 @@ end Term
 namespace Command
 
 def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
+  let opts ← getOptions
   withAlwaysResolvedPromises ds.size fun headerPromises => do
-    let substr? := (mkNullNode ds).getSubstring?
     let snap? := (← read).snap?
     let mut views := #[]
     let mut defs := #[]
+    let mut reusedAllHeaders := true
     for h : i in [0:ds.size], headerPromise in headerPromises do
       let d := ds[i]
       let modifiers ← elabModifiers d[0]
       if ds.size > 1 && modifiers.isNonrec then
         throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
       let mut view ← mkDefView modifiers d[1]
+      let fullHeaderRef := mkNullNode #[d[0], view.headerRef]
       if let some snap := snap? then
-        -- overapproximation: includes previous bodies as well
-        let headerSubstr? := return { (← substr?) with stopPos := (← view.value.getPos?) }
         view := { view with headerSnap? := some {
           old? := do
-            -- transitioning from `Context.snap?` to `DefView.snap?` invariant: if the elaboration
-            -- context and state are unchanged, and the substring from the beginning of the first
-            -- header to the beginning of the current body is unchanged, then the elaboration result for
-            -- this header (which includes state from elaboration of previous headers!) should be
-            -- unchanged.
+            -- transitioning from `Context.snap?` to `DefView.headerSnap?` invariant: if the
+            -- elaboration context and state are unchanged, and the syntax of this as well as all
+            -- previous headers is unchanged, then the elaboration result for this header (which
+            -- includes state from elaboration of previous headers!) should be unchanged.
+            guard reusedAllHeaders
             let old ← snap.old?
             -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick
             let old ← old.val.get.toTyped? DefsParsedSnapshot
             let oldParsed ← old.defs[i]?
-            guard <| (← headerSubstr?).sameAs (← oldParsed.headerSubstr?)
+            guard <| fullHeaderRef.structRangeEqWithTraceReuse opts oldParsed.fullHeaderRef
             -- no syntax guard to store, we already did the necessary checks
             return ⟨.missing, oldParsed.headerProcessedSnap⟩
           new := headerPromise
         } }
         defs := defs.push {
-          headerSubstr?
+          fullHeaderRef
           headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result }
         }
+        reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome)
       views := views.push view
     if let some snap := snap? then
       -- no non-fatal diagnostics at this point

src/Lean/Elab/Quotation.lean

@@ -223,9 +223,12 @@ def getQuotKind (stx : Syntax) : TermElabM SyntaxNodeKind := do
   | ``Parser.Tactic.quot => addNamedQuotInfo stx `tactic
   | ``Parser.Tactic.quotSeq => addNamedQuotInfo stx `tactic.seq
   | .str kind "quot" => addNamedQuotInfo stx kind
-  | ``dynamicQuot => match ← elabParserName stx[1] with
+  | ``dynamicQuot =>
+    let id := stx[1]
+    match (← elabParserName id) with
     | .parser n _ => return n
     | .category c => return c
+    | .alias _    => return (← Parser.getSyntaxKindOfParserAlias? id.getId.eraseMacroScopes).get!
   | k => throwError "unexpected quotation kind {k}"
 
 def mkSyntaxQuotation (stx : Syntax) (kind : Name) : TermElabM Syntax := do

src/Lean/Elab/Syntax.lean

@@ -80,7 +80,7 @@ def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do
   markAsTrailingParser (prec?.getD 0)
   return true
 
-def elabParserName? (stx : Syntax.Ident) : TermElabM (Option Parser.ParserName) := do
+def elabParserName? (stx : Syntax.Ident) : TermElabM (Option Parser.ParserResolution) := do
   match ← Parser.resolveParserName stx with
   | [n@(.category cat)] =>
     addCategoryInfo stx cat
@@ -88,10 +88,12 @@ def elabParserName? (stx : Syntax.Ident) : TermElabM (Option Parser.ParserName)
   | [n@(.parser parser _)] =>
     addTermInfo' stx (Lean.mkConst parser)
     return n
+  | [n@(.alias _)] =>
+    return n
   | _::_::_ => throwErrorAt stx "ambiguous parser {stx}"
   | [] => return none
 
-def elabParserName (stx : Syntax.Ident) : TermElabM Parser.ParserName := do
+def elabParserName (stx : Syntax.Ident) : TermElabM Parser.ParserResolution := do
   match ← elabParserName? stx with
   | some n => return n
   | none => throwErrorAt stx "unknown parser {stx}"
@@ -194,12 +196,6 @@ where
   processNullaryOrCat (stx : Syntax) := do
     let ident := stx[0]
     let id := ident.getId.eraseMacroScopes
-    -- run when parser is neither a decl nor a cat
-    let default := do
-      if (← Parser.isParserAlias id) then
-        ensureNoPrec stx
-        return (← processAlias ident #[])
-      throwError "unknown parser declaration/category/alias '{id}'"
     match (← elabParserName? ident) with
     | some (.parser c (isDescr := true)) =>
       ensureNoPrec stx
@@ -209,14 +205,18 @@ where
     | some (.parser c (isDescr := false)) =>
       if (← Parser.getParserAliasInfo id).declName == c then
         -- prefer parser alias over base declaration because it has more metadata, #2249
-        return (← default)
+        ensureNoPrec stx
+        return (← processAlias ident #[])
       ensureNoPrec stx
       -- as usual, we assume that people using `Parser` know what they are doing
       let stackSz := 1
       return (← `(ParserDescr.parser $(quote c)), stackSz)
     | some (.category _) =>
       processParserCategory stx
-    | none => default
+    | some (.alias _) =>
+      ensureNoPrec stx
+      processAlias ident #[]
+    | none => throwError "unknown parser declaration/category/alias '{id}'"
 
   processSepBy (stx : Syntax) := do
     let p ← ensureUnaryOutput <$> withNestedParser do process stx[1]

src/Lean/Elab/Tactic/Basic.lean

@@ -152,7 +152,10 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := do
     | .node _ k _    =>
       if k == nullKind then
         -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
-        stx.getArgs.forM evalTactic
+        -- We could support incrementality here by allocating `n` new snapshot bundles but the
+        -- practical value is not clear
+        Term.withoutTacticIncrementality true do
+          stx.getArgs.forM evalTactic
       else withTraceNode `Elab.step (fun _ => return stx) (tag := stx.getKind.toString) do
         let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind
         let macros  := macroAttribute.getEntries (← getEnv) stx.getKind
@@ -206,7 +209,11 @@ where
       | []              => throwExs failures
       | evalFn::evalFns => do
         try
-          withReader ({ · with elaborator := evalFn.declName }) <| withTacticInfoContext stx <| evalFn.value stx
+          -- prevent unsupported tactics from accidentally accessing `Term.Context.tacSnap?`
+          Term.withoutTacticIncrementality (!(← isIncrementalElab evalFn.declName)) do
+          withReader ({ · with elaborator := evalFn.declName }) do
+          withTacticInfoContext stx do
+            evalFn.value stx
         catch ex => handleEx s failures ex (eval s evalFns)
 
 def throwNoGoalsToBeSolved : TacticM α :=
@@ -438,12 +445,6 @@ def getNameOfIdent' (id : Syntax) : Name :=
 def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α :=
   withRef (mkNullNode #[arrow, body]) x
 
--- TODO: attribute(s)
-builtin_initialize builtinIncrementalTactics : IO.Ref NameSet ← IO.mkRef {}
-
-def registerBuiltinIncrementalTactic (kind : Name) : IO Unit := do
-  builtinIncrementalTactics.modify fun s => s.insert kind
-
 builtin_initialize registerTraceClass `Elab.tactic
 builtin_initialize registerTraceClass `Elab.tactic.backtrack
 

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -91,14 +91,9 @@ where
                 range? := stxs |>.getRange?
                 task := next.result }]
             let state ← withRestoreOrSaveFull reusableResult? fun save => do
-              -- allow nested reuse for allowlisted tactics
+              -- set up nested reuse; `evalTactic` will check for `isIncrementalElab`
               withTheReader Term.Context ({ · with
-                  tacSnap? :=
-                    guard ((← builtinIncrementalTactics.get).contains tac.getKind) *>
-                    some {
-                      old? := oldInner?
-                      new := inner
-                    } }) do
+                  tacSnap? := some { old? := oldInner?, new := inner } }) do
                 evalTactic tac
               save
             finished.resolve { state? := state }
@@ -186,20 +181,20 @@ def addCheckpoints (stx : Syntax) : TacticM Syntax := do
   output := output ++ currentCheckpointBlock
   return stx.setArgs output
 
-builtin_initialize registerBuiltinIncrementalTactic ``tacticSeq1Indented
-@[builtin_tactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic :=
+@[builtin_tactic tacticSeq1Indented, builtin_incremental]
+def evalTacticSeq1Indented : Tactic :=
   Term.withNarrowedArgTacticReuse (argIdx := 0) evalSepTactics
 
-builtin_initialize registerBuiltinIncrementalTactic ``tacticSeqBracketed
-@[builtin_tactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => do
+@[builtin_tactic tacticSeqBracketed, builtin_incremental]
+def evalTacticSeqBracketed : Tactic := fun stx => do
   let initInfo ← mkInitialTacticInfo stx[0]
   withRef stx[2] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `{`
     withInfoContext (pure ()) initInfo
     Term.withNarrowedArgTacticReuse (argIdx := 1) evalSepTactics stx
 
-builtin_initialize registerBuiltinIncrementalTactic ``cdot
-@[builtin_tactic Lean.cdot] def evalTacticCDot : Tactic := fun stx => do
+@[builtin_tactic Lean.cdot, builtin_incremental]
+def evalTacticCDot : Tactic := fun stx => do
   -- adjusted copy of `evalTacticSeqBracketed`; we used to use the macro
   -- ``| `(tactic| $cdot:cdotTk $tacs) => `(tactic| {%$cdot ($tacs) }%$cdot)``
   -- but the token antiquotation does not copy trailing whitespace, leading to
@@ -281,8 +276,8 @@ private def getOptRotation (stx : Syntax) : Nat :=
     throwError "failed on all goals"
   setGoals mvarIdsNew.toList
 
-builtin_initialize registerBuiltinIncrementalTactic ``tacticSeq
-@[builtin_tactic tacticSeq] def evalTacticSeq : Tactic :=
+@[builtin_tactic tacticSeq, builtin_incremental]
+def evalTacticSeq : Tactic :=
   Term.withNarrowedArgTacticReuse (argIdx := 0) evalTactic
 
 partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
@@ -503,8 +498,8 @@ where
     .group <| .nest 2 <|
     .ofFormat .line ++ .joinSep items sep
 
-builtin_initialize registerBuiltinIncrementalTactic ``case
-@[builtin_tactic «case»] def evalCase : Tactic
+@[builtin_tactic «case», builtin_incremental]
+def evalCase : Tactic
   | stx@`(tactic| case $[$tag $hs*]|* =>%$arr $tac:tacticSeq1Indented) =>
     for tag in tag, hs in hs do
       let (g, gs) ← getCaseGoals tag
@@ -576,7 +571,7 @@ where
   match stx with
   | `(tactic| replace $decl:haveDecl) =>
     withMainContext do
-      let vars ← Elab.Term.Do.getDoHaveVars <| mkNullNode #[.missing, decl]
+      let vars ← Elab.Term.Do.getDoHaveVars (← `(doElem| have $decl:haveDecl))
       let origLCtx ← getLCtx
       evalTactic $ ← `(tactic| have $decl:haveDecl)
       let mut toClear := #[]

src/Lean/Elab/Tactic/Induction.lean

@@ -636,8 +636,8 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
   else
     return exprs
 
-builtin_initialize registerBuiltinIncrementalTactic ``Lean.Parser.Tactic.induction
-@[builtin_tactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx =>
+@[builtin_tactic Lean.Parser.Tactic.induction, builtin_incremental]
+def evalInduction : Tactic := fun stx =>
   match expandInduction? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
@@ -708,8 +708,8 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Id
     else
       return (args.map (·.expr), #[])
 
-builtin_initialize registerBuiltinIncrementalTactic ``Lean.Parser.Tactic.cases
-@[builtin_tactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx =>
+@[builtin_tactic Lean.Parser.Tactic.cases, builtin_incremental]
+def evalCases : Tactic := fun stx =>
   match expandCases? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -532,7 +532,9 @@ Helpful error message when omega cannot find a solution
 def formatErrorMessage (p : Problem) : OmegaM MessageData := do
   if p.possible then
     if p.isEmpty then
-      return m!"it is false"
+      return m!"No usable constraints found. You may need to unfold definitions so `omega` can see \
+      linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, \
+      division, and modular remainder by constants."
     else
       let as ← atoms
       let mask ← mentioned p.constraints

src/Lean/Elab/Tactic/Simp.lean

@@ -153,6 +153,7 @@ inductive ResolveSimpIdResult where
   Elaborate extra simp theorems provided to `simp`. `stx` is of the form `"[" simpTheorem,* "]"`
   If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`),
   this option only makes sense for `simp_all` or `*` is used.
+  Try to recover from errors as much as possible so that users keep seeing the current goal.
 -/
 def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
   if stx.isNone then
@@ -171,56 +172,58 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
       let mut simprocs  := simprocs
       let mut starArg   := false
       for arg in stx[1].getSepArgs do
-        if arg.getKind == ``Lean.Parser.Tactic.simpErase then
-          let fvar ← if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none
-          if let some fvar := fvar then
-            -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
-            thms := thms.eraseCore (.fvar fvar.fvarId!)
+        try -- like withLogging, but compatible with do-notation
+          if arg.getKind == ``Lean.Parser.Tactic.simpErase then
+            let fvar? ← if eraseLocal || starArg then Term.isLocalIdent? arg[1] else pure none
+            if let some fvar := fvar? then
+              -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
+              thms := thms.eraseCore (.fvar fvar.fvarId!)
+            else
+              let id := arg[1]
+              if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
+                if (← Simp.isSimproc declName) then
+                  simprocs := simprocs.erase declName
+                else if ctx.config.autoUnfold then
+                  thms := thms.eraseCore (.decl declName)
+                else
+                  thms ← withRef id <| thms.erase (.decl declName)
+              else
+                -- If `id` could not be resolved, we should check whether it is a builtin simproc.
+                -- before returning error.
+                let name := id.getId.eraseMacroScopes
+                if (← Simp.isBuiltinSimproc name) then
+                  simprocs := simprocs.erase name
+                else
+                  withRef id <| throwUnknownConstant name
+          else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
+            let post :=
+              if arg[0].isNone then
+                true
+              else
+                arg[0][0].getKind == ``Parser.Tactic.simpPost
+            let inv  := !arg[1].isNone
+            let term := arg[2]
+            match (← resolveSimpIdTheorem? term) with
+            | .expr e  =>
+              let name ← mkFreshId
+              thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
+            | .simproc declName =>
+              simprocs ← simprocs.add declName post
+            | .ext (some ext₁) (some ext₂) _ =>
+              thmsArray := thmsArray.push (← ext₁.getTheorems)
+              simprocs  := simprocs.push (← ext₂.getSimprocs)
+            | .ext (some ext₁) none _ =>
+              thmsArray := thmsArray.push (← ext₁.getTheorems)
+            | .ext none (some ext₂) _ =>
+              simprocs  := simprocs.push (← ext₂.getSimprocs)
+            | .none    =>
+              let name ← mkFreshId
+              thms ← addSimpTheorem thms (.stx name arg) term post inv
+          else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
+            starArg := true
           else
-            let id := arg[1]
-            if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
-              if (← Simp.isSimproc declName) then
-                simprocs := simprocs.erase declName
-              else if ctx.config.autoUnfold then
-                thms := thms.eraseCore (.decl declName)
-              else
-                thms ← thms.erase (.decl declName)
-            else
-              -- If `id` could not be resolved, we should check whether it is a builtin simproc.
-              -- before returning error.
-              let name := id.getId.eraseMacroScopes
-              if (← Simp.isBuiltinSimproc name) then
-                simprocs := simprocs.erase name
-              else
-                throwUnknownConstant name
-        else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
-          let post :=
-            if arg[0].isNone then
-              true
-            else
-              arg[0][0].getKind == ``Parser.Tactic.simpPost
-          let inv  := !arg[1].isNone
-          let term := arg[2]
-          match (← resolveSimpIdTheorem? term) with
-          | .expr e  =>
-            let name ← mkFreshId
-            thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
-          | .simproc declName =>
-            simprocs ← simprocs.add declName post
-          | .ext (some ext₁) (some ext₂) _ =>
-            thmsArray := thmsArray.push (← ext₁.getTheorems)
-            simprocs  := simprocs.push (← ext₂.getSimprocs)
-          | .ext (some ext₁) none _ =>
-            thmsArray := thmsArray.push (← ext₁.getTheorems)
-          | .ext none (some ext₂) _ =>
-            simprocs  := simprocs.push (← ext₂.getSimprocs)
-          | .none    =>
-            let name ← mkFreshId
-            thms ← addSimpTheorem thms (.stx name arg) term post inv
-        else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
-          starArg := true
-        else
-          throwUnsupportedSyntax
+            throwUnsupportedSyntax
+        catch ex => logException ex
       return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
 where
   isSimproc? (e : Expr) : MetaM (Option Name) := do
@@ -336,7 +339,9 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
     | .decl declName post inv => -- global definitions in the environment
-      if env.contains declName && (inv || !simpOnlyBuiltins.contains declName) then
+      if env.contains declName
+         && (inv || !simpOnlyBuiltins.contains declName)
+         && !Match.isMatchEqnTheorem env declName then
         let decl : Term ← `($(mkIdent (← unresolveNameGlobal declName)):ident)
         let arg ← match post, inv with
           | true,  true  => `(Parser.Tactic.simpLemma| ← $decl:term)

src/Lean/Elab/Term.lean

@@ -1882,6 +1882,33 @@ builtin_initialize
   registerTraceClass `Elab.debug
   registerTraceClass `Elab.reuse
 
+builtin_initialize incrementalAttr : TagAttribute ←
+  registerTagAttribute `incremental "Marks an elaborator (tactic or command, currently) as \
+supporting incremental elaboration. For unmarked elaborators, the corresponding snapshot bundle \
+field in the elaboration context is unset so as to prevent accidental, incorrect reuse."
+
+builtin_initialize builtinIncrementalElabs : IO.Ref NameSet ← IO.mkRef {}
+
+def addBuiltinIncrementalElab (decl : Name) : IO Unit := do
+  builtinIncrementalElabs.modify fun s => s.insert decl
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name            := `builtin_incremental
+    descr           := s!"(builtin) {incrementalAttr.attr.descr}"
+    applicationTime := .afterCompilation
+    add             := fun decl stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless kind == AttributeKind.global do
+        throwError "invalid attribute 'builtin_incremental', must be global"
+      declareBuiltin decl <| mkApp (mkConst ``addBuiltinIncrementalElab) (toExpr decl)
+  }
+
+/-- Checks whether a declaration is annotated with `[builtin_incremental]` or `[incremental]`. -/
+def isIncrementalElab [Monad m] [MonadEnv m] [MonadLiftT IO m] (decl : Name) : m Bool :=
+  (return (← builtinIncrementalElabs.get (m := IO)).contains decl) <||>
+  (return incrementalAttr.hasTag (← getEnv) decl)
+
 export Term (TermElabM)
 
 end Lean.Elab

src/Lean/Elab/Util.lean

@@ -209,6 +209,9 @@ def logException [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [
       let name ← id.getName
       logError m!"internal exception: {name}"
 
+/--
+If `x` throws an exception, catch it and turn it into a log message (using `logException`).
+-/
 def withLogging [Monad m] [MonadLog m] [MonadExcept Exception m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m]
     (x : m Unit) : m Unit := do
   try x catch ex => logException ex

src/Lean/Message.lean

@@ -57,23 +57,33 @@ inductive MessageData where
   This constructor is inspected in various hacks. -/
   | ofFormatWithInfos : FormatWithInfos → MessageData
   | ofGoal            : MVarId → MessageData
+  /-- A widget instance.
+
+  In `ofWidget wi alt`,
+  the nested message `alt` should approximate the contents of the widget
+  without itself using `ofWidget wi _`.
+  This is used as fallback in environments that cannot display user widgets.
+  `alt` may nest any structured message,
+  for example `ofGoal` to approximate a tactic state widget,
+  and, if necessary, even other widget instances
+  (for which approximations are computed recursively). -/
+  | ofWidget          : Widget.WidgetInstance → MessageData → MessageData
   /-- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/
   | withContext       : MessageDataContext → MessageData → MessageData
   | withNamingContext : NamingContext → MessageData → MessageData
   /-- Lifted `Format.nest` -/
-  |  nest              : Nat → MessageData → MessageData
+  | nest              : Nat → MessageData → MessageData
   /-- Lifted `Format.group` -/
-  |  group             : MessageData → MessageData
+  | group             : MessageData → MessageData
   /-- Lifted `Format.compose` -/
-  |  compose           : MessageData → MessageData → MessageData
+  | compose           : MessageData → MessageData → MessageData
   /-- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
     Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
   | tagged            : Name → MessageData → MessageData
   | trace (data : TraceData) (msg : MessageData) (children : Array MessageData)
   /-- A lazy message.
   The provided thunk will not be run until it is about to be displayed.
-  This can save computation in cases where the message may never be seen,
-  e.g. when nested inside a collapsed trace.
+  This can save computation in cases where the message may never be seen.
 
   The `Dynamic` value is expected to be a `MessageData`,
   which is a workaround for the positivity restriction.
@@ -160,6 +170,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
   | _, _,            ofFormatWithInfos fmt    => return fmt.1
   | _,    none,      ofGoal mvarId            => return "goal " ++ format (mkMVar mvarId)
   | nCtx, some ctx,  ofGoal mvarId            => ppGoal (mkPPContext nCtx ctx) mvarId
+  | nCtx, ctx,       ofWidget _ d             => formatAux nCtx ctx d
   | nCtx, _,         withContext ctx d        => formatAux nCtx ctx d
   | _,    ctx,       withNamingContext nCtx d => formatAux nCtx ctx d
   | nCtx, ctx,       tagged _ d               => formatAux nCtx ctx d

src/Lean/Meta/Match/MatchEqsExt.lean

@@ -19,14 +19,18 @@ def MatchEqns.size (e : MatchEqns) : Nat :=
 
 structure MatchEqnsExtState where
   map : PHashMap Name MatchEqns := {}
+  eqns : PHashSet Name := {}
   deriving Inhabited
 
 /- We generate the equations and splitter on demand, and do not save them on .olean files. -/
 builtin_initialize matchEqnsExt : EnvExtension MatchEqnsExtState ←
   registerEnvExtension (pure {})
 
-def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit :=
-  modifyEnv fun env => matchEqnsExt.modifyState env fun s => { s with map := s.map.insert matchDeclName matchEqns }
+def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit := do
+  modifyEnv fun env => matchEqnsExt.modifyState env fun { map, eqns } => {
+    eqns := matchEqns.eqnNames.foldl (init := eqns) fun eqns eqn => eqns.insert eqn
+    map := map.insert matchDeclName matchEqns
+  }
 
 /-
   Forward definition. We want to use `getEquationsFor` in the simplifier,
@@ -34,4 +38,10 @@ def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Uni
 @[extern "lean_get_match_equations_for"]
 opaque getEquationsFor (matchDeclName : Name) : MetaM MatchEqns
 
+/--
+Returns `true` if `declName` is the name of a `match` equational theorem.
+-/
+def isMatchEqnTheorem (env : Environment) (declName : Name) : Bool :=
+  matchEqnsExt.getState env |>.eqns.contains declName
+
 end Lean.Meta.Match

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -221,13 +221,14 @@ partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpThe
   else
     d
 
-def SimpTheorems.erase [Monad m] [MonadError m] (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
+def SimpTheorems.erase [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
+    (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
   unless d.isLemma thmId ||
     match thmId with
     | .decl declName .. => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
     | _ => false
   do
-    throwError "'{thmId.key}' does not have [simp] attribute"
+    logWarning m!"'{thmId.key}' does not have [simp] attribute"
   return d.eraseCore thmId
 
 private partial def isPerm : Expr → Expr → MetaM Bool

src/Lean/Parser/Command.lean

@@ -94,8 +94,41 @@ def declSig          := leading_parser
 /-- `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` -/
 def optDeclSig       := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
+/-- Right-hand side of a `:=` in a declaration, a term. -/
+def declBody : Parser :=
+  /-
+  We want to make sure that bodies starting with `by` in fact create a single `by` node instead of
+  accidentally parsing some remnants after it as well. This can especially happen when starting to
+  type comments inside tactic blocks where
+  ```
+  by
+    sleep 2000
+    unfold f
+    -starting comment here
+  ```
+  is parsed as
+  ```
+  (by
+    sleep 2000
+    unfold f
+    ) - (starting comment here)
+  ```
+  where the new nesting will discard incrementality data. By using `byTactic`'s precedence, the
+  stray `-` will be flagged as an unexpected token and will not disturb the syntax tree up to it. We
+  do not call `byTactic` directly to avoid differences in pretty printing or behavior or error
+  reporting between the two branches.
+  -/
+  lookahead (setExpected [] "by") >> termParser leadPrec <|>
+  termParser
+
+-- As the pretty printer ignores `lookahead`, we need a custom parenthesizer to choose the correct
+-- precedence
+open PrettyPrinter in
+@[combinator_parenthesizer declBody] def declBody.parenthesizer : Parenthesizer :=
+  Parenthesizer.categoryParser.parenthesizer `term 0
+
 def declValSimple    := leading_parser
-  " :=" >> ppHardLineUnlessUngrouped >> termParser >> Termination.suffix >> optional Term.whereDecls
+  " :=" >> ppHardLineUnlessUngrouped >> declBody >> Termination.suffix >> optional Term.whereDecls
 def declValEqns      := leading_parser
   Term.matchAltsWhereDecls
 def whereStructField := leading_parser

src/Lean/Parser/Extension.lean

@@ -615,15 +615,30 @@ def withOpenDeclFn (p : ParserFn) : ParserFn := fun c s =>
 
 @[inline] def withOpenDecl : Parser → Parser := withFn withOpenDeclFn
 
-inductive ParserName
+/--
+Helper environment extension that gives us access to built-in aliases in pure parser functions.
+-/
+builtin_initialize aliasExtension : EnvExtension (NameMap ParserAliasValue) ←
+  registerEnvExtension parserAliasesRef.get
+
+/-- Result of resolving a parser name. -/
+inductive ParserResolution where
+  /-- Reference to a category. -/
   | category (cat : Name)
+  /--
+  Reference to a parser declaration in the environment.  A `(Trailing)ParserDescr` if `isDescr` is
+  true.
+  -/
   | parser (decl : Name) (isDescr : Bool)
-  -- TODO(gabriel): add parser aliases (this is blocked on doing IO in parsers)
-  deriving Repr
+  /--
+  Reference to a parser alias. Note that as aliases are built-in, a corresponding declaration may
+  not be in the environment (yet).
+  -/
+  | alias (p : ParserAliasValue)
 
 /-- Resolve the given parser name and return a list of candidates. -/
 def resolveParserNameCore (env : Environment) (currNamespace : Name)
-    (openDecls : List OpenDecl) (ident : Ident) : List ParserName := Id.run do
+    (openDecls : List OpenDecl) (ident : Ident) : List ParserResolution := Id.run do
   let ⟨.ident (val := val) (preresolved := pre) ..⟩ := ident | return []
 
   let rec isParser (name : Name) : Option Bool :=
@@ -643,16 +658,24 @@ def resolveParserNameCore (env : Environment) (currNamespace : Name)
   if isParserCategory env erased then
     return [.category erased]
 
-  ResolveName.resolveGlobalName env currNamespace openDecls val |>.filterMap fun
-      | (name, []) => (isParser name).map fun isDescr => .parser name isDescr
-      | _ => none
+  let resolved ← ResolveName.resolveGlobalName env currNamespace openDecls val |>.filterMap fun
+    | (name, []) => (isParser name).map fun isDescr => .parser name isDescr
+    | _ => none
+  unless resolved.isEmpty do
+    return resolved
+
+  -- Aliases are considered global declarations and so should be tried after scope-aware resolution
+  if let some alias := aliasExtension.getState env |>.find? erased then
+    return [.alias alias]
+
+  return []
 
 /-- Resolve the given parser name and return a list of candidates. -/
-def ParserContext.resolveParserName (ctx : ParserContext) (id : Ident) : List ParserName :=
+def ParserContext.resolveParserName (ctx : ParserContext) (id : Ident) : List ParserResolution :=
   Parser.resolveParserNameCore ctx.env ctx.currNamespace ctx.openDecls id
 
 /-- Resolve the given parser name and return a list of candidates. -/
-def resolveParserName (id : Ident) : CoreM (List ParserName) :=
+def resolveParserName (id : Ident) : CoreM (List ParserResolution) :=
   return resolveParserNameCore (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
 
 def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do
@@ -661,23 +684,27 @@ def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do
     return s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small")
   let parserName@(.ident ..) := stack.get! (stack.size - offset - 1)
     | s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier")
-  match ctx.resolveParserName ⟨parserName⟩ with
-  | [.category cat] =>
-    categoryParserFn cat ctx s
-  | [.parser parserName _] =>
-    let iniSz := s.stackSize
-    let s := adaptUncacheableContextFn (fun ctx =>
-      if !internal.parseQuotWithCurrentStage.get ctx.options then
-        -- static quotations such as `(e) do not use the interpreter unless the above option is set,
-        -- so for consistency neither should dynamic quotations using this function
-        { ctx with options := ctx.options.setBool `interpreter.prefer_native true }
-      else ctx) (evalParserConst parserName) ctx s
-    if !s.hasError && s.stackSize != iniSz + 1 then
-      s.mkUnexpectedError "expected parser to return exactly one syntax object"
-    else
-      s
-  | _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}"
-  | [] => s.mkUnexpectedError s!"unknown parser {parserName}"
+  let iniSz := s.stackSize
+  let s ← match ctx.resolveParserName ⟨parserName⟩ with
+    | [.category cat] =>
+      categoryParserFn cat ctx s
+    | [.parser parserName _] =>
+      adaptUncacheableContextFn (fun ctx =>
+        if !internal.parseQuotWithCurrentStage.get ctx.options then
+          -- static quotations such as `(e) do not use the interpreter unless the above option is set,
+          -- so for consistency neither should dynamic quotations using this function
+          { ctx with options := ctx.options.setBool `interpreter.prefer_native true }
+        else ctx) (evalParserConst parserName) ctx s
+    | [.alias alias] =>
+      match alias with
+      | .const p => p.fn ctx s
+      | _ =>
+        return s.mkUnexpectedError s!"parser alias {parserName}, must not take parameters"
+    | _::_::_ => return s.mkUnexpectedError s!"ambiguous parser name {parserName}"
+    | [] => return s.mkUnexpectedError s!"unknown parser {parserName}"
+  if !s.hasError && s.stackSize != iniSz + 1 then
+    return s.mkUnexpectedError "expected parser to return exactly one syntax object"
+  s
 
 def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser where
   fn := adaptCacheableContextFn ({ · with prec }) (parserOfStackFn offset)

src/Lean/Parser/Term.lean

@@ -542,8 +542,11 @@ It is often used when building macros.
 @[builtin_term_parser] def «let_tmp» := leading_parser:leadPrec
   withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser
 
+def haveId := leading_parser (withAnonymousAntiquot := false)
+  (ppSpace >> binderIdent) <|> hygieneInfo
 /- like `let_fun` but with optional name -/
-def haveIdLhs    := ((ppSpace >> binderIdent) <|> hygieneInfo) >> many (ppSpace >> letIdBinder) >> optType
+def haveIdLhs    :=
+  haveId >> many (ppSpace >> letIdBinder) >> optType
 def haveIdDecl   := leading_parser (withAnonymousAntiquot := false)
   atomic (haveIdLhs >> " := ") >> termParser
 def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false)
@@ -786,7 +789,7 @@ def isIdent (stx : Syntax) : Bool :=
   checkStackTop isIdent "expected preceding identifier" >>
   checkNoWsBefore "no space before '.{'" >> ".{" >>
   sepBy1 levelParser ", " >> "}"
-/-- `x@e` or `x:h@e` matches the pattern `e` and binds its value to the identifier `x`.
+/-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
 If present, the identifier `h` is bound to a proof of `x = e`. -/
 @[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser
   checkStackTop isIdent "expected preceding identifier" >>

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -28,15 +28,25 @@ inductive MsgEmbed where
   | expr : CodeWithInfos → MsgEmbed
   /-- An interactive goal display. -/
   | goal : InteractiveGoal → MsgEmbed
-  /-- Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow
-  the user to expand sub-traces interactively. -/
+  /-- A widget instance.
+
+  `alt` is a fallback rendering of the widget
+  that can be shown in standard, non-interactive LSP diagnostics,
+  as well as when user widgets are not supported by the client. -/
+  | widget (wi : Widget.WidgetInstance) (alt : TaggedText MsgEmbed)
+  /-- Some messages (in particular, traces) are too costly to print eagerly.
+  Instead, we allow the user to expand sub-traces interactively. -/
   | trace (indent : Nat) (cls : Name) (msg : TaggedText MsgEmbed) (collapsed : Bool)
       (children : StrictOrLazy (Array (TaggedText MsgEmbed)) (WithRpcRef LazyTraceChildren))
   deriving Inhabited, RpcEncodable
 
-/-- The `message` field is the text of a message possibly containing interactive *embeds* of type
-`MsgEmbed`. We maintain the invariant that embeds are stored in `.tag`s with empty `.text` subtrees,
-i.e. `.tag embed (.text "")`, because a `MsgEmbed` display involve more than just text. -/
+/-- The `message` field is the text of a message
+possibly containing interactive *embeds* of type `MsgEmbed`.
+We maintain the invariant that embeds are stored in `.tag`s with empty `.text` subtrees,
+i.e., `.tag embed (.text "")`.
+
+Client-side display algorithms render tags in a custom way,
+ignoring the nested text. -/
 abbrev InteractiveDiagnostic := Lsp.DiagnosticWith (TaggedText MsgEmbed)
 
 deriving instance RpcEncodable for Lsp.DiagnosticWith
@@ -44,14 +54,15 @@ deriving instance RpcEncodable for Lsp.DiagnosticWith
 namespace InteractiveDiagnostic
 open MsgEmbed
 
-def toDiagnostic (diag : InteractiveDiagnostic) : Lsp.Diagnostic :=
+partial def toDiagnostic (diag : InteractiveDiagnostic) : Lsp.Diagnostic :=
   { diag with message := prettyTt diag.message }
 where
   prettyTt (tt : TaggedText MsgEmbed) : String :=
     let tt : TaggedText MsgEmbed := tt.rewrite fun
-      | .expr tt,  _ => .text tt.stripTags
-      | .goal g,   _ => .text (toString g.pretty)
-      | .trace .., _ => .text "(trace)"
+      | .expr tt,      _ => .text tt.stripTags
+      | .goal g,       _ => .text (toString g.pretty)
+      | .widget _ alt, _ => .text $ prettyTt alt
+      | .trace ..,     _ => .text "(trace)"
     tt.stripTags
 
 /-- Compares interactive diagnostics modulo `TaggedText` tags and traces. -/
@@ -88,6 +99,8 @@ private inductive EmbedFmt
   /-- Nested text is ignored. -/
   | goal (ctx : Elab.ContextInfo) (lctx : LocalContext) (g : MVarId)
   /-- Nested text is ignored. -/
+  | widget (wi : WidgetInstance) (alt : Format)
+  /-- Nested text is ignored. -/
   | trace (cls : Name) (msg : Format) (collapsed : Bool)
     (children : StrictOrLazy (Array Format) (Array MessageData))
   /-- Nested tags are ignored, show nested text as-is. -/
@@ -128,20 +141,23 @@ where
   }
 
   go (nCtx : NamingContext) : Option MessageDataContext → MessageData → MsgFmtM Format
-  | none,      ofFormatWithInfos ⟨fmt, _⟩ => withIgnoreTags fmt
-  | some ctx,  ofFormatWithInfos ⟨fmt, infos⟩ => do
+  | none,     ofFormatWithInfos ⟨fmt, _⟩ => withIgnoreTags fmt
+  | some ctx, ofFormatWithInfos ⟨fmt, infos⟩ => do
     let t ← pushEmbed <| EmbedFmt.code (mkContextInfo nCtx ctx) infos
     return Format.tag t fmt
-  | none,      ofGoal mvarId            => pure $ "goal " ++ format (mkMVar mvarId)
-  | some ctx,  ofGoal mvarId            =>
-    return .tag (← pushEmbed (.goal (mkContextInfo nCtx ctx) ctx.lctx mvarId)) "\n"
-  | _,         withContext ctx d        => go nCtx ctx d
-  | ctx,       withNamingContext nCtx d => go nCtx ctx d
-  | ctx,       tagged _ d               => go nCtx ctx d
-  | ctx,       nest n d                 => Format.nest n <$> go nCtx ctx d
-  | ctx,       compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
-  | ctx,       group d                  => Format.group <$> go nCtx ctx d
-  | ctx,       .trace data header children => do
+  | none,     ofGoal mvarId            => pure $ "goal " ++ format (mkMVar mvarId)
+  | some ctx, ofGoal mvarId            =>
+    return .tag (← pushEmbed (.goal (mkContextInfo nCtx ctx) ctx.lctx mvarId)) default
+  | ctx,       ofWidget wi d            => do
+    let t ← pushEmbed <| EmbedFmt.widget wi (← go nCtx ctx d)
+    return Format.tag t default
+  | _,        withContext ctx d        => go nCtx ctx d
+  | ctx,      withNamingContext nCtx d => go nCtx ctx d
+  | ctx,      tagged _ d               => go nCtx ctx d
+  | ctx,      nest n d                 => Format.nest n <$> go nCtx ctx d
+  | ctx,      compose d₁ d₂            => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
+  | ctx,      group d                  => Format.group <$> go nCtx ctx d
+  | ctx,      .trace data header children => do
     let mut header := (← go nCtx ctx header).nest 4
     if data.startTime != 0 then
       header := f!"[{data.stopTime - data.startTime}] {header}"
@@ -159,7 +175,7 @@ where
       else
         pure (.strict (← children.mapM (go nCtx ctx)))
     let e := .trace data.cls header data.collapsed nodes
-    return .tag (← pushEmbed e) ".\n"
+    return .tag (← pushEmbed e) default
   | ctx?,     ofLazy f _          => do
     let dyn ← f (ctx?.map (mkPPContext nCtx))
     let some msg := dyn.get? MessageData
@@ -188,6 +204,8 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
         | .goal ctx lctx g =>
           ctx.runMetaM lctx do
             return .tag (.goal (← goalToInteractive g)) default
+        | .widget wi alt =>
+          return .tag (.widget wi (← fmtToTT alt col)) default
         | .trace cls msg collapsed children => do
           let col := col + tt.stripTags.length - 2
           let children ←

src/Lean/Widget/Types.lean

@@ -26,5 +26,6 @@ structure WidgetInstance where
   so must be stored as a computation
   with access to the RPC object store. -/
   props : StateM Server.RpcObjectStore Json
+  deriving Server.RpcEncodable
 
 end Lean.Widget

src/Lean/Widget/UserWidget.lean

@@ -214,17 +214,28 @@ def addPanelWidgetLocal [Monad m] [MonadEnv m] (wi : WidgetInstance) : m Unit :=
 def erasePanelWidget [Monad m] [MonadEnv m] (h : UInt64) : m Unit := do
   modifyEnv fun env => panelWidgetsExt.modifyState env fun st => st.erase h
 
-/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.
+/-- Construct a widget instance by finding a widget module
+in the current environment.
+
 `hash` must be `hash (toModule c).javascript`
-where `c` is some global constant annotated with `@[widget_module]`. -/
-def savePanelWidgetInfo (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) :
-    CoreM Unit := do
+where `c` is some global constant annotated with `@[widget_module]`,
+or the name of a builtin widget module. -/
+def WidgetInstance.ofHash (hash : UInt64) (props : StateM Server.RpcObjectStore Json) :
+    CoreM WidgetInstance := do
   let env ← getEnv
   let builtins ← builtinModulesRef.get
   let some id :=
     (builtins.find? hash |>.map (·.1)) <|> (moduleRegistry.getState env |>.find? hash |>.map (·.1))
     | throwError s!"No widget module with hash {hash} registered"
-  pushInfoLeaf <| .ofUserWidgetInfo { id, javascriptHash := hash, props, stx }
+  return { id, javascriptHash := hash, props }
+
+/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.
+
+`hash` must be as in `WidgetInstance.ofHash`. -/
+def savePanelWidgetInfo (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) :
+    CoreM Unit := do
+  let wi ← WidgetInstance.ofHash hash props
+  pushInfoLeaf <| .ofUserWidgetInfo { wi with stx }
 
 /-! ## `show_panel_widgets` command -/
 
@@ -372,8 +383,6 @@ opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadEr
 
 /-! ## Retrieving panel widget instances -/
 
-deriving instance Server.RpcEncodable for WidgetInstance
-
 /-- Retrieve all the `UserWidgetInfo`s that intersect a given line. -/
 def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverLine : Nat) : List UserWidgetInfo :=
   t.deepestNodes fun

src/lake/Lake/Build/Actions.lean

@@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
 import Lake.Util.Proc
 import Lake.Util.NativeLib
-import Lake.Build.Job
+import Lake.Util.IO
 
 /-! # Common Build Actions
 Low level actions to build common Lean artifacts via the Lean toolchain.
@@ -22,7 +22,7 @@ def compileLeanModule
   (leanPath : SearchPath := []) (rootDir : FilePath := ".")
   (dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
   (leanArgs : Array String := #[]) (lean : FilePath := "lean")
-: JobM Unit := do
+: LogIO Unit := do
   let mut args := leanArgs ++
     #[leanFile.toString, "-R", rootDir.toString]
   if let some oleanFile := oleanFile? then
@@ -70,7 +70,7 @@ def compileLeanModule
 def compileO
   (oFile srcFile : FilePath)
   (moreArgs : Array String := #[]) (compiler : FilePath := "cc")
-: JobM Unit := do
+: LogIO Unit := do
   createParentDirs oFile
   proc {
     cmd := compiler.toString
@@ -80,7 +80,7 @@ def compileO
 def compileStaticLib
   (libFile : FilePath) (oFiles : Array FilePath)
   (ar : FilePath := "ar")
-: JobM Unit := do
+: LogIO Unit := do
   createParentDirs libFile
   proc {
     cmd := ar.toString
@@ -90,7 +90,7 @@ def compileStaticLib
 def compileSharedLib
   (libFile : FilePath) (linkArgs : Array String)
   (linker : FilePath := "cc")
-: JobM Unit := do
+: LogIO Unit := do
   createParentDirs libFile
   proc {
     cmd := linker.toString
@@ -100,7 +100,7 @@ def compileSharedLib
 def compileExe
   (binFile : FilePath) (linkFiles : Array FilePath)
   (linkArgs : Array String := #[]) (linker : FilePath := "cc")
-: JobM Unit := do
+: LogIO Unit := do
   createParentDirs binFile
   proc {
     cmd := linker.toString

src/lake/Lake/Build/Basic.lean

@@ -95,3 +95,13 @@ abbrev MonadBuild (m : Type → Type u) :=
 
 /-- The internal core monad of Lake builds.  Not intended for user use. -/
 abbrev CoreBuildM := BuildT LogIO
+
+/--
+Logs a build step with `message`.
+
+**Deprecated:**  Build steps are now managed by a top-level build monitor.
+As a result, this no longer functions the way it used to. It now just logs the
+`message` via `logVerbose`.
+-/
+@[deprecated, inline] def logStep [Monad m] [MonadLog m] (message : String) : m Unit := do
+  logVerbose message

src/lake/Lake/Build/Fetch.lean

@@ -25,6 +25,19 @@ abbrev RecBuildM :=
 
 instance : MonadLift LogIO RecBuildM := ⟨ELogT.takeAndRun⟩
 
+/--
+Run a `JobM` action in `RecBuildM` (and thus `FetchM`).
+
+Generally, this should not be done, and instead a job action
+should be run asynchronously in a Job (e.g., via `Job.async`).
+-/
+@[inline] def RecBuildM.runJobM (x : JobM α) : RecBuildM α := fun _ ctx log store => do
+  match (← x ctx {log}) with
+  | .ok a s => return (.ok a s.log, store)
+  | .error e s => return (.error e s.log, store)
+
+instance : MonadLift JobM RecBuildM := ⟨RecBuildM.runJobM⟩
+
 /-- Run a recursive build. -/
 @[inline] def RecBuildM.run
   (stack : CallStack BuildKey) (store : BuildStore) (build : RecBuildM α)
@@ -55,6 +68,12 @@ abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m
 /-- The top-level monad for Lake build functions. -/
 abbrev FetchM := IndexT RecBuildM
 
+/-- Ensures that `JobM` lifts into `FetchM`. -/
+example : MonadLiftT JobM FetchM := inferInstance
+
+/-- Ensures that `SpawnM` lifts into `FetchM`. -/
+example : MonadLiftT SpawnM FetchM := inferInstance
+
 /-- The top-level monad for Lake build functions. **Renamed `FetchM`.** -/
 @[deprecated FetchM] abbrev IndexBuildM := FetchM
 

src/lake/Lake/Build/Job.lean

@@ -66,7 +66,13 @@ abbrev JobResult α := EResult Log.Pos JobState α
 /-- The `Task` of a Lake job. -/
 abbrev JobTask α := BaseIOTask (JobResult α)
 
-/-- The monad of asynchronous Lake jobs. Lifts into `FetchM`. -/
+/--
+The monad of asynchronous Lake jobs.
+
+While this can be lifted into `FetchM`, job action should generally
+be wrapped into an asynchronous job (e.g., via `Job.async`) instead of being
+run directly in `FetchM`.
+-/
 abbrev JobM := BuildT <| EStateT Log.Pos JobState BaseIO
 
 instance [Pure m] : MonadLift LakeM (BuildT m) where
@@ -94,16 +100,6 @@ abbrev SpawnM := BuildT BaseIO
 /-- The monad used to spawn asynchronous Lake build jobs. **Replaced by `SpawnM`.** -/
 @[deprecated SpawnM] abbrev SchedulerM := SpawnM
 
-/--
-Logs a build step with `message`.
-
-**Deprecated:**  Build steps are now managed by a top-level build monitor.
-As a result, this no longer functions the way it used to. It now just logs the
-`message` via `logVerbose`.
--/
-@[deprecated] def logStep (message : String) : JobM Unit := do
-  logVerbose message
-
 /-- A Lake job. -/
 structure Job (α : Type u)  where
   task : JobTask α

src/lake/Lake/Build/Package.lean

@@ -71,7 +71,7 @@ def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.asy
     download url self.buildArchiveFile
   unless upToDate && (← self.buildDir.pathExists) do
     updateAction .fetch
-    logVerbose s!"unpacking {self.name}/{tag}/{self.buildArchive}"
+    logVerbose s!"unpacking {self.name}:{tag}:{self.buildArchive}"
     untar self.buildArchiveFile self.buildDir
   return (true, .nil)
 

src/lake/Lake/Build/Trace.lean

@@ -3,18 +3,16 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Util.IO
 
 open System
+
 namespace Lake
 
 --------------------------------------------------------------------------------
 /-! # Utilities -/
 --------------------------------------------------------------------------------
 
-/-- Creates any missing parent directories of `path`. -/
-@[inline] def createParentDirs (path : FilePath) : IO Unit := do
-  if let some dir := path.parent then IO.FS.createDirAll dir
-
 class CheckExists.{u} (i : Type u) where
   /-- Check whether there already exists an artifact for the given target info. -/
   checkExists : i → BaseIO Bool

src/lake/Lake/CLI/Actions.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lake.Build.Run
 import Lake.Build.Targets
+import Lake.CLI.Build
 
 namespace Lake
 
@@ -18,24 +19,69 @@ def exe (name : Name) (args  : Array String := #[]) (buildConfig : BuildConfig :
   let exeFile ← ws.runBuild exe.fetch buildConfig
   env exeFile.toString args
 
-def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do
+def Package.pack (pkg : Package) (file : FilePath := pkg.buildArchiveFile) : LogIO Unit := do
+  logInfo s!"packing {file}"
+  tar pkg.buildDir file
+
+def Package.unpack (pkg : Package) (file : FilePath := pkg.buildArchiveFile) : LogIO Unit := do
+  logInfo s!"unpacking {file}"
+  untar file pkg.buildDir
+
+def Package.uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do
+  pkg.pack
+  logInfo s!"uploading {tag}:{pkg.buildArchive}"
   let mut args :=
     #["release", "upload", tag, pkg.buildArchiveFile.toString, "--clobber"]
   if let some repo := pkg.releaseRepo? then
     args := args.append #["-R", repo]
-  logInfo s!"packing {pkg.buildArchive}"
-  tar pkg.buildDir pkg.buildArchiveFile
-  logInfo s!"uploading {tag}/{pkg.buildArchive}"
   proc {cmd := "gh", args}
 
-def Package.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT IO UInt32 := do
+def Package.resolveDriver
+  (pkg : Package) (kind : String) (driver : String)
+: LakeT IO (Package × String) := do
   let pkgName := pkg.name.toString (escape := false)
-  if pkg.testRunner.isAnonymous then
-    error s!"{pkgName}: no test runner script or executable"
-  else if let some script := pkg.scripts.find? pkg.testRunner then
-    script.run args
-  else if let some exe := pkg.findLeanExe? pkg.testRunner then
-    let exeFile ← runBuild exe.fetch buildConfig
-    env exeFile.toString args.toArray
+  if driver.isEmpty then
+    error s!"{pkgName}: no {kind} driver configured"
   else
-    error s!"{pkgName}: invalid test runner: unknown script or executable `{pkg.testRunner}`"
+    match driver.split (· == '/') with
+    | [pkg, driver] =>
+      let some pkg ← findPackage? pkg.toName
+        | error s!"{pkgName}: unknown {kind} driver package '{pkg}'"
+      return (pkg, driver)
+    | [driver] =>
+      return (pkg, driver)
+    | _ =>
+      error s!"{pkgName}: invalid {kind} driver '{driver}' (too many '/')"
+
+def Package.test (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT IO UInt32 := do
+  let cfgArgs := pkg.testDriverArgs
+  let (pkg, driver) ← pkg.resolveDriver "test" pkg.testDriver
+  let pkgName := pkg.name.toString (escape := false)
+  if let some script := pkg.scripts.find? driver.toName then
+    script.run (cfgArgs.toList ++ args)
+  else if let some exe := pkg.findLeanExe? driver.toName  then
+    let exeFile ← runBuild exe.fetch buildConfig
+    env exeFile.toString (cfgArgs ++ args.toArray)
+  else if let some lib := pkg.findLeanLib? driver.toName then
+    unless cfgArgs.isEmpty ∧ args.isEmpty do
+      error s!"{pkgName}: arguments cannot be passed to a library test driver"
+    match resolveLibTarget (← getWorkspace) lib with
+    | .ok specs =>
+      runBuild (buildSpecs specs) {buildConfig with out := .stdout}
+      return 0
+    | .error e =>
+      error s!"{pkgName}: invalid test driver: {e}"
+  else
+    error s!"{pkgName}: invalid test driver: unknown script, executable, or library '{driver}'"
+
+def Package.lint (pkg : Package) (args : List String := []) (buildConfig : BuildConfig := {}) : LakeT IO UInt32 := do
+  let cfgArgs := pkg.lintDriverArgs
+  let (pkg, driver) ← pkg.resolveDriver "lint" pkg.lintDriver
+  if let some script := pkg.scripts.find? driver.toName then
+    script.run (cfgArgs.data ++ args)
+  else if let some exe := pkg.findLeanExe? driver.toName  then
+    let exeFile ← runBuild exe.fetch buildConfig
+    env exeFile.toString (cfgArgs ++ args.toArray)
+  else
+    let pkgName := pkg.name.toString (escape := false)
+    error s!"{pkgName}: invalid lint driver: unknown script or executable '{driver}'"

src/lake/Lake/CLI/Build.lean

@@ -15,15 +15,18 @@ structure BuildSpec where
   getBuildJob : BuildData info.key → BuildJob Unit
 
 @[inline] def BuildData.toBuildJob
-[FamilyOut BuildData k (BuildJob α)] (data : BuildData k) : BuildJob Unit :=
+  [FamilyOut BuildData k (BuildJob α)] (data : BuildData k)
+: BuildJob Unit :=
   discard <| ofFamily data
 
-@[inline] def mkBuildSpec (info : BuildInfo)
-[FamilyOut BuildData info.key (BuildJob α)] : BuildSpec :=
+@[inline] def mkBuildSpec
+  (info : BuildInfo) [FamilyOut BuildData info.key (BuildJob α)]
+: BuildSpec :=
   {info, getBuildJob := BuildData.toBuildJob}
 
-@[inline] def mkConfigBuildSpec (facetType : String)
-(info : BuildInfo) (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
+@[inline] def mkConfigBuildSpec
+  (facetType : String) (info : BuildInfo)
+  (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
 : Except CliError BuildSpec := do
   let some getJob := config.getJob?
     | throw <| CliError.nonCliFacet facetType facet
@@ -47,7 +50,9 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package
     | none => throw <| CliError.unknownPackage spec
 
 open Module in
-def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError BuildSpec :=
+def resolveModuleTarget
+  (ws : Workspace) (mod : Module) (facet : Name := .anonymous)
+: Except CliError BuildSpec :=
   if facet.isAnonymous then
     return mkBuildSpec <| mod.facet leanArtsFacet
   else if let some config := ws.findModuleFacetConfig? facet then do
@@ -55,7 +60,9 @@ def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except
   else
     throw <| CliError.unknownFacet "module" facet
 
-def resolveLibTarget (ws : Workspace) (lib : LeanLib) (facet : Name) : Except CliError (Array BuildSpec) :=
+def resolveLibTarget
+  (ws : Workspace) (lib : LeanLib) (facet : Name := .anonymous)
+: Except CliError (Array BuildSpec) :=
   if facet.isAnonymous then
     lib.defaultFacets.mapM (resolveFacet ·)
   else

src/lake/Lake/CLI/Help.lean

@@ -18,11 +18,16 @@ COMMANDS:
   init <name> <temp>    create a Lean package in the current directory
   build <targets>...    build targets
   exe <exe> <args>...   build an exe and run it in Lake's environment
-  test                  run the workspace's test script or executable
+  test                  test the package using the configured test driver
+  check-test            check if there is a properly configured test driver
+  lint                  lint the package using the configured lint driver
+  check-lint            check if there is a properly configured lint driver
   clean                 remove build outputs
   env <cmd> <args>...   execute a command in Lake's environment
   lean <file>           elaborate a Lean file in Lake's context
   update                update dependencies and save them to the manifest
+  pack                  pack build artifacts into an archive for distribution
+  unpack                unpack build artifacts from an distributed archive
   upload <tag>          upload build artifacts to a GitHub release
   script                manage and run workspace scripts
   scripts               shorthand for `lake script list`
@@ -142,13 +147,84 @@ of the same package, the version materialized is undefined.
 A bare `lake update` will upgrade all dependencies."
 
 def helpTest :=
-"Run the workspace's test script or executable
+"Test the workspace's root package using its configured test driver
 
 USAGE:
   lake test [-- <args>...]
 
-Looks for a script or executable tagged `@[test_runner]` in the workspace's
-root package and executes it with `args`. "
+A test driver can be configured by either setting the 'testDriver'
+package configuration option or by tagging a script, executable, or library
+`@[test_driver]`. A definition in a dependency can be used as a test driver
+by using the `<pkg>/<name>` syntax for the 'testDriver' configuration option.
+
+A script test driver will be run with the  package configuration's
+`testDriverArgs` plus the CLI `args`. An executable test driver will be
+built and then run like a script. A library test driver will just be built.
+"
+
+def helpCheckTest :=
+"Check if there is a properly configured test driver
+
+USAGE:
+  lake check-test
+
+Exits with code 0 if the workspace's root package has a properly
+configured lint driver. Errors (with code 1) otherwise.
+
+Does NOT verify that the configured test driver actually exists in the
+package or its dependencies. It merely verifies that one is specified.
+"
+
+def helpLint :=
+"Lint the workspace's root package using its configured lint driver
+
+USAGE:
+  lake lint [-- <args>...]
+
+A lint driver can be configured by either setting the `lintDriver` package
+configuration option by tagging a script or executable `@[lint_driver]`.
+A definition in dependency can be used as a test driver by using the
+`<pkg>/<name>` syntax for the 'testDriver' configuration option.
+
+A script lint driver will be run with the  package configuration's
+`lintDriverArgs` plus the CLI `args`. An executable lint driver will be
+built and then run like a script.
+"
+
+def helpCheckLint :=
+"Check if there is a properly configured lint driver
+
+USAGE:
+  lake check-lint
+
+Exits with code 0 if the workspace's root package has a properly
+configured lint driver. Errors (with code 1) otherwise.
+
+Does NOT verify that the configured lint driver actually exists in the
+package or its dependencies. It merely verifies that one is specified.
+"
+
+def helpPack :=
+"Pack build artifacts into a archive for distribution
+
+USAGE:
+  lake pack [<file.tgz>]
+
+Packs the root package's `buildDir` into a gzip tar archive using `tar`.
+If a path for the archive is not specified, creates a archive in the package's
+Lake directory (`.lake`) named according to its `buildArchive` setting.
+
+Does NOT build any artifacts. It just packs the existing ones."
+
+def helpUnpack :=
+"Unpack build artifacts from a distributed archive
+
+USAGE:
+  lake unpack [<file.tgz>]
+
+Unpack build artifacts from the gzip tar archive `file.tgz` into the root
+package's `buildDir`. If a path for the archive is not specified, uses the
+the package's `buildArchive` in its Lake directory (`.lake`)."
 
 def helpUpload :=
 "Upload build artifacts to a GitHub release
@@ -300,8 +376,13 @@ def help : (cmd : String) → String
 | "init"                => helpInit
 | "build"               => helpBuild
 | "update" | "upgrade"  => helpUpdate
+| "pack"                => helpPack
+| "unpack"              => helpUnpack
 | "upload"              => helpUpload
 | "test"                => helpTest
+| "check-test"          => helpCheckTest
+| "lint"                => helpLint
+| "check-lint"          => helpCheckLint
 | "clean"               => helpClean
 | "script"              => helpScriptCli
 | "scripts"             => helpScriptList

src/lake/Lake/CLI/Main.lean

@@ -326,13 +326,28 @@ protected def update : CliM PUnit := do
   let toUpdate := (← getArgs).foldl (·.insert <| stringToLegalOrSimpleName ·) {}
   updateManifest config toUpdate
 
+protected def pack : CliM PUnit := do
+  processOptions lakeOption
+  let file? ← takeArg?
+  noArgsRem do
+  let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions))
+  let file := (FilePath.mk <$> file?).getD ws.root.buildArchiveFile
+  ws.root.pack file
+
+protected def unpack : CliM PUnit := do
+  processOptions lakeOption
+  let file? ← takeArg?
+  noArgsRem do
+  let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions))
+  let file := (FilePath.mk <$> file?).getD ws.root.buildArchiveFile
+  ws.root.unpack file
+
 protected def upload : CliM PUnit := do
   processOptions lakeOption
   let tag ← takeArg "release tag"
-  let opts ← getThe LakeOptions
-  let config ← mkLoadConfig opts
-  let ws ← loadWorkspace config
-  uploadRelease ws.root tag
+  noArgsRem do
+  let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions))
+  ws.root.uploadRelease tag
 
 protected def setupFile : CliM PUnit := do
   processOptions lakeOption
@@ -346,16 +361,28 @@ protected def setupFile : CliM PUnit := do
 protected def test : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
-  let config ← mkLoadConfig opts
-  let ws ← loadWorkspace config
+  let ws ← loadWorkspace (← mkLoadConfig opts)
   noArgsRem do
   let x := ws.root.test opts.subArgs (mkBuildConfig opts)
   exit <| ← x.run (mkLakeContext ws)
 
 protected def checkTest : CliM PUnit := do
   processOptions lakeOption
-  let ws ← loadWorkspace ( ← mkLoadConfig (← getThe LakeOptions))
-  noArgsRem do exit <| if ws.root.testRunner.isAnonymous then 1 else 0
+  let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
+  noArgsRem do exit <| if pkg.testDriver.isEmpty then 1 else 0
+
+protected def lint : CliM PUnit := do
+  processOptions lakeOption
+  let opts ← getThe LakeOptions
+  let ws ← loadWorkspace (← mkLoadConfig opts)
+  noArgsRem do
+  let x := ws.root.lint opts.subArgs (mkBuildConfig opts)
+  exit <| ← x.run (mkLakeContext ws)
+
+protected def checkLint : CliM PUnit := do
+  processOptions lakeOption
+  let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
+  noArgsRem do exit <| if pkg.lintDriver.isEmpty then 1 else 0
 
 protected def clean : CliM PUnit := do
   processOptions lakeOption
@@ -440,8 +467,7 @@ protected def translateConfig : CliM PUnit := do
   let lang ← parseLangSpec (← takeArg "configuration language")
   let outFile? := (← takeArg?).map FilePath.mk
   noArgsRem do
-  Lean.searchPathRef.set cfg.lakeEnv.leanSearchPath
-  let (pkg, _) ← loadPackage "[root]" cfg
+  let pkg ← loadPackage cfg
   let outFile := outFile?.getD <| pkg.configFile.withExtension lang.fileExtension
   if (← outFile.pathExists) then
     throw (.outputConfigExists outFile)
@@ -464,10 +490,14 @@ def lakeCli : (cmd : String) → CliM PUnit
 | "build"               => lake.build
 | "update" | "upgrade"  => lake.update
 | "resolve-deps"        => lake.resolveDeps
+| "pack"                => lake.pack
+| "unpack"              => lake.unpack
 | "upload"              => lake.upload
 | "setup-file"          => lake.setupFile
 | "test"                => lake.test
 | "check-test"          => lake.checkTest
+| "lint"                => lake.lint
+| "check-lint"          => lake.checkLint
 | "clean"               => lake.clean
 | "script"              => lake.script
 | "scripts"             => lake.script.list

src/lake/Lake/CLI/Translate/Lean.lean

@@ -89,8 +89,10 @@ def LeanConfig.addDeclFields (cfg : LeanConfig) (fs : Array DeclField) : Array D
 @[inline] def mkDeclValWhere? (fields : Array DeclField) : Option (TSyntax ``declValWhere) :=
   if fields.isEmpty then none else Unhygienic.run `(declValWhere|where $fields*)
 
-def PackageConfig.mkSyntax (cfg : PackageConfig) : PackageDecl := Unhygienic.run do
-  let declVal? := mkDeclValWhere? <|Array.empty
+def PackageConfig.mkSyntax (cfg : PackageConfig)
+  (testDriver := cfg.testDriver) (lintDriver := cfg.lintDriver)
+  : PackageDecl := Unhygienic.run do
+  let declVal? := mkDeclValWhere? <| Array.empty
     |> addDeclFieldD `precompileModules cfg.precompileModules false
     |> addDeclFieldD `moreGlobalServerArgs cfg.moreGlobalServerArgs #[]
     |> addDeclFieldD `srcDir cfg.srcDir "."
@@ -102,6 +104,10 @@ def PackageConfig.mkSyntax (cfg : PackageConfig) : PackageDecl := Unhygienic.run
     |> addDeclField? `releaseRepo (cfg.releaseRepo <|> cfg.releaseRepo?)
     |> addDeclFieldD `buildArchive (cfg.buildArchive?.getD cfg.buildArchive) (defaultBuildArchive cfg.name)
     |> addDeclFieldD `preferReleaseBuild cfg.preferReleaseBuild false
+    |> addDeclFieldD `testDriver testDriver ""
+    |> addDeclFieldD `testDriverArgs cfg.testDriverArgs #[]
+    |> addDeclFieldD `lintDriver lintDriver ""
+    |> addDeclFieldD `lintDriverArgs cfg.lintDriverArgs #[]
     |> cfg.toWorkspaceConfig.addDeclFields
     |> cfg.toLeanConfig.addDeclFields
   `(packageDecl|package $(mkIdent cfg.name) $[$declVal?]?)
@@ -145,7 +151,7 @@ protected def LeanLibConfig.mkSyntax
   `(leanLibDecl|$[$attrs?:attributes]? lean_lib $(mkIdent cfg.name) $[$declVal?]?)
 
 protected def LeanExeConfig.mkSyntax
-  (cfg : LeanExeConfig) (defaultTarget := false) (testRunner := false)
+  (cfg : LeanExeConfig) (defaultTarget := false)
 : LeanExeDecl := Unhygienic.run do
   let declVal? := mkDeclValWhere? <| Array.empty
     |> addDeclFieldD `srcDir cfg.srcDir "."
@@ -153,11 +159,7 @@ protected def LeanExeConfig.mkSyntax
     |> addDeclFieldD `exeName cfg.exeName (cfg.name.toStringWithSep "-" (escape := false))
     |> addDeclFieldD `supportInterpreter cfg.supportInterpreter false
     |> cfg.toLeanConfig.addDeclFields
-  let attrs? ← id do
-    let mut attrs := #[]
-    if testRunner then attrs := attrs.push <| ← `(Term.attrInstance|test_runner)
-    if defaultTarget then attrs := attrs.push <| ← `(Term.attrInstance|default_target)
-    if attrs.isEmpty then pure none else some <$> `(Term.attributes|@[$attrs,*])
+    let attrs? ← if defaultTarget then some <$> `(Term.attributes|@[default_target]) else pure none
   `(leanExeDecl|$[$attrs?:attributes]? lean_exe $(mkIdent cfg.name) $[$declVal?]?)
 
 protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic.run do
@@ -175,14 +177,13 @@ protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic
 
 /-- Create a Lean module that encodes the declarative configuration of the package. -/
 def Package.mkLeanConfig (pkg : Package) : TSyntax ``module := Unhygienic.run do
-  let testRunner := pkg.testRunner
   let defaultTargets := pkg.defaultTargets.foldl NameSet.insert NameSet.empty
-  let pkgConfig := pkg.config.mkSyntax
+  let pkgConfig := pkg.config.mkSyntax pkg.testDriver pkg.lintDriver
   let requires := pkg.depConfigs.map (·.mkSyntax)
   let leanLibs := pkg.leanLibConfigs.toArray.map fun cfg =>
     cfg.mkSyntax (defaultTargets.contains cfg.name)
   let leanExes := pkg.leanExeConfigs.toArray.map fun cfg =>
-    cfg.mkSyntax (defaultTargets.contains cfg.name) (cfg.name == testRunner)
+    cfg.mkSyntax (defaultTargets.contains cfg.name)
   `(module|
   import $(mkIdent `Lake)
   open $(mkIdent `System) $(mkIdent `Lake) $(mkIdent `DSL)

src/lake/Lake/CLI/Translate/Toml.lean

@@ -122,7 +122,10 @@ instance : ToToml Dependency := ⟨(toToml ·.toToml)⟩
 /-- Create a TOML table that encodes the declarative configuration of the package. -/
 def Package.mkTomlConfig (pkg : Package) (t : Table := {}) : Table :=
   pkg.config.toToml t
-  |>.insertD `testRunner pkg.testRunner .anonymous
+  |>.smartInsert `testDriver pkg.testDriver
+  |>.smartInsert `testDriverArgs pkg.testDriverArgs
+  |>.smartInsert `lintDriver pkg.lintDriver
+  |>.smartInsert `lintDriverArgs pkg.lintDriverArgs
   |>.smartInsert `defaultTargets pkg.defaultTargets
   |>.smartInsert `require pkg.depConfigs
   |>.smartInsert `lean_lib pkg.leanLibConfigs.toArray

src/lake/Lake/Config/Package.lean

@@ -154,6 +154,44 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   -/
   preferReleaseBuild : Bool := false
 
+  /--
+  The name of the script, executable, or library by `lake test` when
+  this package is the workspace root. To point to a definition in another
+  package, use the syntax `<pkg>/<def>`.
+
+  A script driver will be run by `lake test` with the arguments
+  configured in `testDriverArgs`  followed by any specified on the CLI
+  (e.g., via  `lake lint -- <args>...`). An executable driver will be built
+  and then run like a script. A library will just be built.
+  -/
+  testDriver : String := ""
+
+  /--
+  Arguments to pass to the package's test driver.
+  These arguments will come before those passed on the command line via
+  `lake test -- <args>...`.
+  -/
+  testDriverArgs : Array String := #[]
+
+  /--
+  The name of the script or executable used by `lake lint` when this package
+  is the workspace root. To point to a definition in another package, use the
+  syntax `<pkg>/<def>`.
+
+  A script driver will be run by `lake lint` with the arguments
+  configured in `lintDriverArgs` followed by any specified on the CLI
+  (e.g., via  `lake lint -- <args>...`). An executable driver will be built
+  and then run like a script.
+  -/
+  lintDriver : String := ""
+
+  /--
+  Arguments to pass to the package's linter.
+  These arguments will come before those passed on the command line via
+  `lake lint -- <args>...`.
+  -/
+  lintDriverArgs : Array String := #[]
+
 deriving Inhabited
 
 --------------------------------------------------------------------------------
@@ -203,8 +241,11 @@ structure Package where
   defaultScripts : Array Script := #[]
   /-- Post-`lake update` hooks for the package. -/
   postUpdateHooks : Array (OpaquePostUpdateHook config.name) := #[]
-  /-- Name of the package's test runner script or executable (if any). -/
-  testRunner : Name := .anonymous
+  /-- The driver used for `lake test` when this package is the workspace root. -/
+  testDriver : String := config.testDriver
+  /-- The driver used for `lake lint` when this package is the workspace root. -/
+  lintDriver : String := config.lintDriver
+
 
 instance : Nonempty Package :=
   have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance
@@ -287,6 +328,14 @@ namespace Package
 @[inline] def buildDir (self : Package) : FilePath :=
   self.dir / self.config.buildDir
 
+/-- The package's `testDriverArgs` configuration. -/
+@[inline] def testDriverArgs (self : Package) : Array String :=
+  self.config.testDriverArgs
+
+/-- The package's `lintDriverArgs` configuration. -/
+@[inline] def lintDriverArgs (self : Package) : Array String :=
+  self.config.lintDriverArgs
+
 /-- The package's `extraDepTargets` configuration. -/
 @[inline] def extraDepTargets (self : Package) : Array Name :=
   self.config.extraDepTargets

src/lake/Lake/DSL/Attributes.lean

@@ -1,68 +1,22 @@
 /-
-Copyright (c) 2021 Mac Malone. All rights reserved.
+Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Util.OrderedTagAttribute
+import Lake.DSL.AttributesCore
 
 open Lean
+
 namespace Lake
 
-initialize packageAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `package "mark a definition as a Lake package configuration"
-
-initialize packageDepAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency"
-
-initialize postUpdateAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook"
-
-initialize scriptAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `script "mark a definition as a Lake script"
-
-initialize defaultScriptAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `default_script "mark a Lake script as the package's default"
-    fun name => do
-      unless (← getEnv <&> (scriptAttr.hasTag · name)) do
-        throwError "attribute `default_script` can only be used on a `script`"
-
-initialize leanLibAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration"
-
-initialize leanExeAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration"
-
-initialize externLibAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target"
-
-initialize targetAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `target "mark a definition as a custom Lake target"
-
-initialize defaultTargetAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `default_target "mark a Lake target as the package's default"
-    fun name => do
-      let valid ← getEnv <&> fun env =>
-        leanLibAttr.hasTag env name ||
-        leanExeAttr.hasTag env name ||
-        externLibAttr.hasTag env name ||
-        targetAttr.hasTag env name
-      unless valid do
-        throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
-
-initialize testRunnerAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `test_runner "mark a Lake script or executable as the package's test runner"
-    fun name => do
-      let valid ← getEnv <&> fun env =>
-        scriptAttr.hasTag env name ||
-        leanExeAttr.hasTag env name
-      unless valid do
-        throwError "attribute `test_runner` can only be used on a `script` or `lean_exe`"
-
-initialize moduleFacetAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet"
-
-initialize packageFacetAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `package_facet "mark a definition as a Lake package facet"
-
-initialize libraryFacetAttr : OrderedTagAttribute ←
-  registerOrderedTagAttribute `library_facet "mark a definition as a Lake library facet"
+initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `test_runner
+    descr           := testDriverAttr.attr.descr
+    add             := fun decl stx attrKind => do
+      logWarningAt stx "@[test_runner] has been deprecated, use @[test_driver] instead"
+      testDriverAttr.attr.add decl stx attrKind
+    applicationTime := testDriverAttr.attr.applicationTime
+    erase           := fun decl => testDriverAttr.attr.erase decl
+ }

src/lake/Lake/DSL/AttributesCore.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.OrderedTagAttribute
+
+open Lean
+namespace Lake
+
+initialize packageAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `package "mark a definition as a Lake package configuration"
+
+initialize packageDepAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency"
+
+initialize postUpdateAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook"
+
+initialize scriptAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `script "mark a definition as a Lake script"
+
+initialize defaultScriptAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `default_script "mark a Lake script as the package's default"
+    fun name => do
+      unless (← getEnv <&> (scriptAttr.hasTag · name)) do
+        throwError "attribute `default_script` can only be used on a `script`"
+
+initialize leanLibAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `lean_lib "mark a definition as a Lake Lean library target configuration"
+
+initialize leanExeAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `lean_exe "mark a definition as a Lake Lean executable target configuration"
+
+initialize externLibAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target"
+
+initialize targetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `target "mark a definition as a custom Lake target"
+
+initialize defaultTargetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `default_target "mark a Lake target as the package's default"
+    fun name => do
+      let valid ← getEnv <&> fun env =>
+        leanLibAttr.hasTag env name ||
+        leanExeAttr.hasTag env name ||
+        externLibAttr.hasTag env name ||
+        targetAttr.hasTag env name
+      unless valid do
+        throwError "attribute `default_target` can only be used on a target (e.g., `lean_lib`, `lean_exe`)"
+
+initialize testDriverAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `test_driver "mark a Lake script, executable, or library as package's test driver"
+    fun name => do
+      let valid ← getEnv <&> fun env =>
+        scriptAttr.hasTag env name ||
+        leanExeAttr.hasTag env name ||
+        leanLibAttr.hasTag env name
+      unless valid do
+        throwError "attribute `test_driver` can only be used on a `script`, `lean_exe`, or `lean_lib`"
+
+initialize lintDriverAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `lint_driver "mark a Lake script or executable as package's linter"
+    fun name => do
+      let valid ← getEnv <&> fun env =>
+        scriptAttr.hasTag env name ||
+        leanExeAttr.hasTag env name
+      unless valid do
+        throwError "attribute `lint_driver` can only be used on a `script` or `lean_exe`"
+
+initialize moduleFacetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `module_facet "mark a definition as a Lake module facet"
+
+initialize packageFacetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `package_facet "mark a definition as a Lake package facet"
+
+initialize libraryFacetAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `library_facet "mark a definition as a Lake library facet"

src/lake/Lake/Load/Elab.lean

@@ -133,7 +133,8 @@ where
     |>.insert ``externLibAttr
     |>.insert ``targetAttr
     |>.insert ``defaultTargetAttr
-    |>.insert ``testRunnerAttr
+    |>.insert ``testDriverAttr
+    |>.insert ``lintDriverAttr
     |>.insert ``moduleFacetAttr
     |>.insert ``packageFacetAttr
     |>.insert ``libraryFacetAttr

src/lake/Lake/Load/Main.lean

@@ -53,7 +53,7 @@ def configFileExists (cfgFile : FilePath) : BaseIO Bool :=
     leanFile.pathExists <||> tomlFile.pathExists
 
 /-- Loads a Lake package configuration (either Lean or TOML). -/
-def loadPackage
+def loadPackageCore
   (name : String) (cfg : LoadConfig)
 : LogIO (Package × Option Environment) := do
   if let some ext := cfg.relConfigFile.extension then
@@ -88,7 +88,7 @@ def loadDepPackage
   (dep : MaterializedDep) (leanOpts : Options) (reconfigure : Bool)
 : StateT Workspace LogIO Package := fun ws => do
   let name := dep.name.toString (escape := false)
-  let (pkg, env?) ← loadPackage name {
+  let (pkg, env?) ← loadPackageCore name {
     lakeEnv := ws.lakeEnv
     wsDir := ws.dir
     relPkgDir := dep.relPkgDir
@@ -110,7 +110,7 @@ Does not resolve dependencies.
 -/
 def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   Lean.searchPathRef.set config.lakeEnv.leanSearchPath
-  let (root, env?) ← loadPackage "[root]" config
+  let (root, env?) ← loadPackageCore "[root]" config
   let ws : Workspace := {
     root, lakeEnv := config.lakeEnv
     moduleFacetConfigs := initModuleFacetConfigs
@@ -122,6 +122,11 @@ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   else
     return ws
 
+/-- Loads a Lake package as a single independent object (without dependencies). -/
+def loadPackage (config : LoadConfig) : LogIO Package := do
+  Lean.searchPathRef.set config.lakeEnv.leanSearchPath
+  (·.1) <$> loadPackageCore "[root]" config
+
 /-- Recursively visits a package dependency graph, avoiding cycles. -/
 private def resolveDepsAcyclic
   [Monad m] [MonadError m]
@@ -208,7 +213,7 @@ def Workspace.updateAndMaterialize
           if depPkg.name ≠ dep.name then
             if dep.name = .mkSimple "std" then
               let rev :=
-                match dep.manifestEntry with
+                match dep.manifestEntry.src with
                 | .git (inputRev? := some rev) .. => s!" @ {repr rev}"
                 | _ => ""
               logError (stdMismatchError depPkg.name.toString rev)
@@ -285,7 +290,7 @@ def Workspace.materializeDeps
               s!"manifest out of date: {what} of dependency '{dep.name}' changed; " ++
               s!"use `lake update {dep.name}` to update it"
           if let .some entry := pkgEntries.find? dep.name then
-          match dep.src, entry with
+          match dep.src, entry.src with
           | .git (url := url) (rev := rev) .., .git (url := url') (inputRev? := rev')  .. =>
             if url ≠ url' then warnOutOfDate "git url"
             if rev ≠ rev' then warnOutOfDate "git revision"

src/lake/Lake/Load/Manifest.lean

@@ -6,6 +6,8 @@ Authors: Mac Malone, Gabriel Ebner
 import Lake.Util.Log
 import Lake.Util.Name
 import Lake.Util.FilePath
+import Lake.Util.JsonObject
+import Lake.Util.Version
 import Lake.Load.Config
 import Lake.Config.Workspace
 
@@ -18,139 +20,145 @@ to create, modify, serialize, and deserialize it.
 
 namespace Lake
 
-/-- Current version of the manifest format. -/
-def Manifest.version : Nat := 7
+/--
+The current version of the manifest format.
 
-/-- An entry for a package stored in the manifest. -/
+Three-part semantic versions were introduced in `v1.0.0`.
+Major version increments indicate breaking changes
+(e.g., new required fields and semantic changes to existing fields).
+Minor version increments (after `0.x`) indicate backwards-compatible extensions
+(e.g., adding optional fields, removing fields).
+
+Lake supports reading manifests with versions that have `-` suffixes.
+When checking for version compatibility, Lake expects a manifest with version
+`x.y.z-foo` to have all the features of the official manifest version `x.y.z`.
+That is, Lake ignores the `-` suffix.
+
+**VERSION HISTORY**
+
+**v0.x.0** (versioned by a natural number)
+- `1`: First version
+- `2`: Adds optional `inputRev` package entry field
+- `3`: Changes entry to inductive (with `path`/`git`)
+- `4`: Adds required `packagesDir` manifest field
+- `5`: Adds optional `inherited` package entry field (and removed `opts`)
+- `6`: Adds optional package root `name` manifest field
+- `7`: `type` refactor, custom to/fromJson
+
+**v1.x.x** (versioned by a string)
+- `"1.0.0"`: Switches to a semantic versioning scheme
+-/
+@[inline] def Manifest.version : LeanVer := v!"1.0.0"
+
+/-- Manifest version `0.6.0` package entry. For backwards compatibility. -/
 inductive PackageEntryV6
 | path (name : Name) (opts : NameMap String) (inherited : Bool) (dir : FilePath)
 | git (name : Name) (opts : NameMap String) (inherited : Bool) (url : String) (rev : String)
     (inputRev? : Option String) (subDir? : Option FilePath)
 deriving FromJson, ToJson, Inhabited
 
-/-- An entry for a package stored in the manifest. -/
-inductive PackageEntry
+/--
+The package source for an entry in the manifest.
+Describes exactly how Lake should materialize the package.
+-/
+inductive PackageEntrySrc
   /--
   A local filesystem package. `dir` is relative to the package directory
   of the package containing the manifest.
   -/
   | path
-    (name : Name)
-    (inherited : Bool)
-    (configFile : FilePath)
-    (manifestFile? : Option FilePath)
     (dir : FilePath)
   /-- A remote Git package. -/
   | git
-    (name : Name)
-    (inherited : Bool)
-    (configFile : FilePath)
-    (manifestFile? : Option FilePath)
     (url : String)
     (rev : String)
     (inputRev? : Option String)
     (subDir? : Option FilePath)
   deriving Inhabited
 
+/-- An entry for a package stored in the manifest. -/
+structure PackageEntry where
+  name : Name
+  inherited : Bool
+  configFile : FilePath := defaultConfigFile
+  manifestFile? : Option FilePath := none
+  src : PackageEntrySrc
+  deriving Inhabited
+
 namespace PackageEntry
 
-protected def toJson : PackageEntry → Json
-| .path name inherited configFile manifestFile? dir => Json.mkObj [
-  ("type", "path"),
-  ("inherited", toJson inherited),
-  ("name", toJson name),
-  ("configFile" , toJson configFile),
-  ("manifestFile", toJson manifestFile?),
-  ("inherited", toJson inherited),
-  ("dir", toJson dir)
-]
-| .git name inherited configFile manifestFile? url rev inputRev? subDir? => Json.mkObj [
-  ("type", "git"),
-  ("inherited", toJson inherited),
-  ("name", toJson name),
-  ("configFile" , toJson configFile),
-  ("manifestFile", toJson manifestFile?),
-  ("url", toJson url),
-  ("rev", toJson rev),
-  ("inputRev", toJson inputRev?),
-  ("subDir", toJson subDir?)
-]
+protected def toJson (entry : PackageEntry) : Json :=
+  let fields := [
+    ("name", toJson entry.name),
+    ("configFile" , toJson entry.configFile),
+    ("manifestFile", toJson entry.manifestFile?),
+    ("inherited", toJson entry.inherited),
+  ]
+  let fields :=
+    match entry.src with
+    | .path  dir =>
+      ("type", "path") :: fields.append [
+        ("dir", toJson dir),
+      ]
+    | .git url rev inputRev? subDir? =>
+      ("type", "git") :: fields.append [
+        ("url", toJson url),
+        ("rev", toJson rev),
+        ("inputRev", toJson inputRev?),
+        ("subDir", toJson subDir?),
+      ]
+  Json.mkObj fields
 
 instance : ToJson PackageEntry := ⟨PackageEntry.toJson⟩
 
 protected def fromJson? (json : Json) : Except String PackageEntry := do
-  let obj ← json.getObj?
-  let type ← get obj "type"
-  let name ← get obj "name"
-  let inherited ← get obj "inherited"
-  let configFile ← getD obj "configFile" defaultConfigFile
-  let manifestFile ← getD obj "manifestFile" defaultManifestFile
-  match type with
-  | "path"=>
-    let dir ← get obj "dir"
-    return .path name inherited configFile manifestFile dir
-  | "git" =>
-    let url ← get obj "url"
-    let rev ← get obj "rev"
-    let inputRev? ← get? obj "inputRev"
-    let subDir? ← get? obj "subDir"
-    return .git name inherited configFile manifestFile url rev inputRev? subDir?
-  | _ =>
-    throw s!"unknown package entry type '{type}'"
-where
-  get {α} [FromJson α] obj prop : Except String α :=
-    match obj.find compare prop with
-    | none => throw s!"package entry missing required property '{prop}'"
-    | some val => fromJson? val |>.mapError (s!"in package entry property '{prop}': {·}")
-  get? {α} [FromJson α] obj prop : Except String (Option α) :=
-    match obj.find compare prop with
-    | none => pure none
-    | some val => fromJson? val |>.mapError (s!"in package entry property '{prop}': {·}")
-  getD {α} [FromJson α] obj prop (default : α) : Except String α :=
-    (Option.getD · default) <$> get? obj prop
+  let obj ← JsonObject.fromJson? json |>.mapError (s!"package entry: {·}")
+  let name ← obj.get "name" |>.mapError (s!"package entry: {·}")
+  try
+    let type ← obj.get "type"
+    let inherited ← obj.get "inherited"
+    let configFile ← obj.getD "configFile" defaultConfigFile
+    let manifestFile ← obj.getD "manifestFile" defaultManifestFile
+    let src : PackageEntrySrc ← id do
+      match type with
+      | "path" =>
+        let dir ← obj.get "dir"
+        return .path dir
+      | "git" =>
+        let url ← obj.get "url"
+        let rev ← obj.get "rev"
+        let inputRev? ← obj.get? "inputRev"
+        let subDir? ← obj.get? "subDir"
+        return .git url rev inputRev? subDir?
+      | _ =>
+        throw s!"unknown package entry type '{type}'"
+    return {
+      name, inherited,
+      configFile, manifestFile? := manifestFile, src
+      : PackageEntry
+    }
+  catch e =>
+    throw s!"package entry '{name}': {e}"
 
 instance : FromJson PackageEntry := ⟨PackageEntry.fromJson?⟩
 
-@[inline] protected def name : PackageEntry → Name
-| .path (name := name) .. | .git (name := name) .. => name
+@[inline] def setInherited (entry : PackageEntry) : PackageEntry :=
+  {entry with inherited := true}
 
-@[inline] protected def inherited : PackageEntry → Bool
-| .path (inherited := inherited) .. | .git (inherited := inherited) .. => inherited
+@[inline] def setConfigFile (path : FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with configFile := path}
 
-def setInherited : PackageEntry → PackageEntry
-| .path name _ configFile manifestFile? dir =>
-  .path name true configFile manifestFile? dir
-| .git name _ configFile manifestFile? url rev inputRev? subDir? =>
-  .git name true configFile manifestFile? url rev inputRev? subDir?
+@[inline] def setManifestFile (path? : Option FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with manifestFile? := path?}
 
-@[inline] protected def configFile : PackageEntry → FilePath
-| .path (configFile := configFile) .. | .git (configFile := configFile) .. => configFile
-
-@[inline] protected def manifestFile? : PackageEntry →  Option FilePath
-| .path (manifestFile? := manifestFile?) .. | .git (manifestFile? := manifestFile?) .. => manifestFile?
-
-def setConfigFile (path : FilePath) : PackageEntry → PackageEntry
-| .path name inherited _ manifestFile? dir =>
-  .path name inherited path manifestFile? dir
-| .git name inherited _ manifestFile? url rev inputRev? subDir? =>
-  .git name inherited path manifestFile? url rev inputRev? subDir?
-
-def setManifestFile (path? : Option FilePath) : PackageEntry → PackageEntry
-| .path name inherited configFile _ dir =>
-  .path name inherited configFile path? dir
-| .git name inherited configFile _ url rev inputRev? subDir? =>
-  .git name inherited configFile path? url rev inputRev? subDir?
-
-def inDirectory (pkgDir : FilePath) : PackageEntry → PackageEntry
-| .path name inherited configFile manifestFile? dir =>
-  .path name inherited configFile manifestFile? (pkgDir / dir)
-| entry => entry
+@[inline] def inDirectory (pkgDir : FilePath) (entry : PackageEntry) : PackageEntry :=
+  {entry with src := match entry.src with | .path dir => .path (pkgDir / dir) | s => s}
 
 def ofV6 : PackageEntryV6 → PackageEntry
 | .path name _opts inherited dir =>
-  .path name inherited defaultConfigFile none dir
+  {name, inherited, src := .path dir}
 | .git name _opts inherited url rev inputRev? subDir? =>
-  .git name inherited defaultConfigFile none url rev inputRev? subDir?
+  {name, inherited, src := .git url rev inputRev? subDir?}
 
 end PackageEntry
 
@@ -169,50 +177,38 @@ def addPackage (entry : PackageEntry) (self : Manifest) : Manifest :=
 
 protected def toJson (self : Manifest) : Json :=
   Json.mkObj [
-    ("version", version),
+    ("version", toJson version),
     ("name", toJson self.name),
     ("lakeDir", toJson self.lakeDir),
     ("packagesDir", toJson self.packagesDir?),
-    ("packages", toJson self.packages)
+    ("packages", toJson self.packages),
   ]
 
 instance : ToJson Manifest := ⟨Manifest.toJson⟩
 
 protected def fromJson? (json : Json) : Except String Manifest := do
-  let .ok obj := json.getObj?
-    | throw "manifest not a JSON object"
-  let ver : Json ← get obj "version"
-  let .ok ver := ver.getNat?
-    | throw s!"unknown manifest version '{ver}'"
-  if ver < 5 then
+  let obj ← JsonObject.fromJson? json
+  let ver : SemVerCore ←
+    match (← obj.get "version" : Json) with
+    | (n : Nat) => pure {minor := n}
+    | (s : String) => LeanVer.parse s
+    | ver => throw s!"unknown manifest version format '{ver}'; \
+      you may need to update your 'lean-toolchain'"
+  if ver.major > 1 then
+    throw s!"manifest version '{ver}' is of a higher major version than this \
+      Lake's '{Manifest.version}'; you may need to update your 'lean-toolchain'"
+  else if ver < v!"0.5.0" then
     throw s!"incompatible manifest version '{ver}'"
-  else if ver ≤ 6 then
-    let name ← getD obj "name" Name.anonymous
-    let lakeDir ← getD obj "lakeDir" defaultLakeDir
-    let packagesDir? ← get? obj "packagesDir"
-    let pkgs : Array PackageEntryV6 ← getD obj "packages" #[]
-    return {name, lakeDir, packagesDir?, packages := pkgs.map PackageEntry.ofV6}
-  else if ver = 7 then
-    let name ← getD obj "name" Name.anonymous
-    let lakeDir ← get obj "lakeDir"
-    let packagesDir ← get obj "packagesDir"
-    let packages : Array PackageEntry ← getD obj "packages" #[]
-    return {name, lakeDir, packagesDir? := packagesDir, packages}
   else
-    throw <|
-      s!"manifest version `{ver}` is higher than this Lake's '{Manifest.version}'; " ++
-      "you may need to update your `lean-toolchain`"
-where
-  get {α} [FromJson α] obj prop : Except String α :=
-    match obj.find compare prop with
-    | none => throw s!"manifest missing required property '{prop}'"
-    | some val => fromJson? val |>.mapError (s!"in manifest property '{prop}': {·}")
-  get? {α} [FromJson α] obj prop : Except String (Option α) :=
-    match obj.find compare prop with
-    | none => pure none
-    | some val => fromJson? val |>.mapError (s!"in manifest property '{prop}': {·}")
-  getD {α} [FromJson α] obj prop (default : α) : Except String α :=
-    (Option.getD · default) <$> get? obj prop
+    let name ← obj.getD "name" Name.anonymous
+    let lakeDir ← obj.getD "lakeDir" defaultLakeDir
+    let packagesDir? ← obj.get? "packagesDir"
+    let packages ←
+      if ver < v!"0.7.0" then
+        (·.map PackageEntry.ofV6) <$> obj.getD "packages" #[]
+      else
+        obj.getD "packages" #[]
+    return {name, lakeDir, packagesDir?, packages}
 
 instance : FromJson Manifest := ⟨Manifest.fromJson?⟩
 

src/lake/Lake/Load/Materialize.lean

@@ -113,7 +113,7 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
     return {
       relPkgDir
       remoteUrl? := none
-      manifestEntry := .path dep.name inherited defaultConfigFile none relPkgDir
+      manifestEntry := mkEntry <| .path relPkgDir
       configDep := dep
     }
   | .git url inputRev? subDir? => do
@@ -127,9 +127,11 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
     return {
       relPkgDir
       remoteUrl? := Git.filterUrl? url
-      manifestEntry := .git dep.name inherited defaultConfigFile none url rev inputRev? subDir?
+      manifestEntry := mkEntry <| .git url rev inputRev? subDir?
       configDep := dep
     }
+where
+  mkEntry src : PackageEntry := {name := dep.name, inherited, src}
 
 /--
 Materializes a manifest package entry, cloning and/or checking it out as necessary.
@@ -137,7 +139,7 @@ Materializes a manifest package entry, cloning and/or checking it out as necessa
 def PackageEntry.materialize (manifestEntry : PackageEntry)
 (configDep : Dependency) (wsDir relPkgsDir : FilePath) (pkgUrlMap : NameMap String)
 : LogIO MaterializedDep :=
-  match manifestEntry with
+  match manifestEntry.src with
   | .path (dir := relPkgDir) .. =>
     return {
       relPkgDir
@@ -145,8 +147,8 @@ def PackageEntry.materialize (manifestEntry : PackageEntry)
       manifestEntry
       configDep
     }
-  | .git name (url := url) (rev := rev) (subDir? := subDir?) .. => do
-    let sname := name.toString (escape := false)
+  | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
+    let sname := manifestEntry.name.toString (escape := false)
     let relGitDir := relPkgsDir / sname
     let gitDir := wsDir / relGitDir
     let repo := GitRepo.mk gitDir
@@ -161,10 +163,10 @@ def PackageEntry.materialize (manifestEntry : PackageEntry)
         if (← repo.hasDiff) then
           logWarning s!"{sname}: repository '{repo.dir}' has local changes"
       else
-        let url := pkgUrlMap.find? name |>.getD url
+        let url := pkgUrlMap.find? manifestEntry.name |>.getD url
         updateGitRepo sname repo url rev
     else
-      let url := pkgUrlMap.find? name |>.getD url
+      let url := pkgUrlMap.find? manifestEntry.name |>.getD url
       cloneGitPkg sname repo url rev
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
     return {

src/lake/Lake/Load/Package.lean

@@ -109,14 +109,28 @@ def Package.loadFromEnv
     | .error e => error e
   let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name =>
     evalConstCheck env opts Dependency ``Dependency name
-  let testRunners := testRunnerAttr.getAllEntries env
-  let testRunner ←
-    if testRunners.size > 1 then
-      error s!"{self.name}: only one script or executable can be tagged `@[test_runner]`"
-    else if h : testRunners.size > 0 then
-      pure (testRunners[0]'h)
+  let testDrivers := testDriverAttr.getAllEntries env
+  let testDriver ←
+    if testDrivers.size > 1 then
+      error s!"{self.name}: only one script, executable, or library can be tagged @[test_driver]"
+    else if h : testDrivers.size > 0 then
+      if self.config.testDriver.isEmpty then
+        pure (testDrivers[0]'h |>.toString)
+      else
+        error s!"{self.name}: cannot both set testDriver and use @[test_driver]"
     else
-      pure .anonymous
+      pure self.config.testDriver
+  let lintDrivers := lintDriverAttr.getAllEntries env
+  let lintDriver ←
+    if lintDrivers.size > 1 then
+      error s!"{self.name}: only one script or executable can be tagged @[linter]"
+    else if h : lintDrivers.size > 0 then
+      if self.config.lintDriver.isEmpty then
+        pure (lintDrivers[0]'h |>.toString)
+      else
+        error s!"{self.name}: cannot both set linter and use @[linter]"
+    else
+      pure self.config.lintDriver
 
   -- Deprecation warnings
   unless self.config.manifestFile.isNone do
@@ -127,8 +141,8 @@ def Package.loadFromEnv
   -- Fill in the Package
   return {self with
     depConfigs, leanLibConfigs, leanExeConfigs, externLibConfigs
-    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts, testRunner
-    postUpdateHooks
+    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts
+    testDriver, lintDriver,  postUpdateHooks
   }
 
 /--

src/lake/Lake/Load/Toml.lean

@@ -175,12 +175,19 @@ protected def PackageConfig.decodeToml (t : Table) (ref := Syntax.missing) : Exc
   let releaseRepo ← t.tryDecode? `releaseRepo
   let buildArchive? ← t.tryDecode? `buildArchive
   let preferReleaseBuild ← t.tryDecodeD `preferReleaseBuild false
+  let testRunner ← t.tryDecodeD `testRunner ""
+  let testDriver ← t.tryDecodeD `testDriver ""
+  let testDriver := if ¬testRunner.isEmpty ∧ testDriver.isEmpty then testRunner else testDriver
+  let testDriverArgs ← t.tryDecodeD `testDriverArgs #[]
+  let lintDriver ← t.tryDecodeD `lintDriver ""
+  let lintDriverArgs ← t.tryDecodeD `lintDriverArgs #[]
   let toLeanConfig ← tryDecode <| LeanConfig.decodeToml t
   let toWorkspaceConfig ← tryDecode <| WorkspaceConfig.decodeToml t
   return {
     name, precompileModules, moreGlobalServerArgs,
     srcDir, buildDir, leanLibDir, nativeLibDir, binDir, irDir,
     releaseRepo, buildArchive?, preferReleaseBuild
+    testDriver, testDriverArgs, lintDriver, lintDriverArgs
     toLeanConfig, toWorkspaceConfig
   }
 
@@ -259,12 +266,11 @@ def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do
       let leanLibConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_lib #[]
       let leanExeConfigs ← mkRBArray (·.name) <$> table.tryDecodeD `lean_exe #[]
       let defaultTargets ← table.tryDecodeD `defaultTargets #[]
-      let testRunner ← table.tryDecodeD `testRunner .anonymous
       let depConfigs ← table.tryDecodeD `require #[]
       return {
         dir, relDir, relConfigFile
         config, depConfigs, leanLibConfigs, leanExeConfigs
-        defaultTargets, testRunner
+        defaultTargets
       }
     if errs.isEmpty then
       return pkg

src/lake/Lake/Toml/Encode.lean

@@ -43,8 +43,6 @@ namespace Toml.Table
 @[inline] nonrec def insert [enc : ToToml α] (k : Name) (v : α) (t : Table) : Table :=
   t.insert k (enc.toToml v)
 
-instance (priority := low) [ToToml α] : SmartInsert α := ⟨Table.insert⟩
-
 /-- If the value is not `none`, inserts the encoded value into the table. -/
 @[inline] nonrec def insertSome [enc : ToToml α] (k : Name) (v? : Option α) (t : Table) : Table :=
   t.insertSome k (v?.map enc.toToml)
@@ -61,6 +59,9 @@ instance : SmartInsert Table where
 instance [ToToml (Array α)] : SmartInsert (Array α) where
   smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
 
+instance : SmartInsert String  where
+  smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
+
 /-- Insert a value into the table if `p` is `true`. -/
 @[inline] nonrec def insertIf [enc : ToToml α] (p : Bool) (k : Name) (v : α) (t : Table) : Table :=
   t.insertIf p k (enc.toToml v)

src/lake/Lake/Util/Family.lean

@@ -147,6 +147,10 @@ attribute [simp] FamilyOut.family_key_eq_type
 instance [FamilyDef Fam a β] : FamilyOut Fam a β where
   family_key_eq_type := FamilyDef.family_key_eq_type
 
+/-- The constant type family -/
+instance : FamilyDef (fun _ => β) a β where
+  family_key_eq_type := rfl
+
 /-- Cast a datum from its individual type to its general family. -/
 @[macro_inline] def toFamily [FamilyOut Fam a β] (b : β) : Fam a :=
   cast FamilyOut.family_key_eq_type.symm b

src/lake/Lake/Util/IO.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+
+/-- Creates any missing parent directories of `path`. -/
+@[inline] def createParentDirs (path : System.FilePath) : IO Unit := do
+  if let some dir := path.parent then IO.FS.createDirAll dir

src/lake/Lake/Util/JsonObject.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Data.Json
+
+open Lean
+
+/-! # JSON Object
+Defines a convenient wrapper type for JSON object data that makes
+indexing fields more convenient.
+-/
+
+namespace Lake
+
+/-- A JSON object (`Json.obj` data). -/
+abbrev JsonObject :=
+  RBNode String (fun _ => Json)
+
+namespace JsonObject
+
+@[inline] protected def toJson (obj : JsonObject) : Json :=
+  .obj obj
+
+instance : ToJson JsonObject := ⟨JsonObject.toJson⟩
+
+@[inline] protected def fromJson? (json : Json) : Except String JsonObject :=
+  json.getObj?
+
+instance : FromJson JsonObject := ⟨JsonObject.fromJson?⟩
+
+@[inline] nonrec def erase (obj : JsonObject) (prop : String) : JsonObject :=
+  obj.erase compare prop
+
+@[inline] def getJson? (obj : JsonObject) (prop : String) : Option Json :=
+  obj.find compare prop
+
+@[inline] def get [FromJson α] (obj : JsonObject) (prop : String) : Except String α :=
+  match obj.getJson? prop with
+  | none => throw s!"property not found: {prop}"
+  | some val => fromJson? val |>.mapError (s!"{prop}: {·}")
+
+@[inline] def get? [FromJson α] (obj : JsonObject) (prop : String) : Except String (Option α) :=
+  match obj.getJson? prop with
+  | none => pure none
+  | some val => fromJson? val |>.mapError (s!"{prop}: {·}")
+
+@[inline] def getD  [FromJson α] (obj : JsonObject) (prop : String) (default : α) : Except String α :=
+  (Option.getD · default) <$> obj.get? prop

src/lake/Lake/Util/Store.lean

@@ -6,18 +6,29 @@ Authors: Mac Malone
 namespace Lake
 
 /-- A monad equipped with a dependently typed key-value store for a particular key. -/
+class MonadStore1Of {κ : Type u} (k : κ) (α : semiOutParam $ Type v) (m : Type v → Type w) where
+  fetch? : m (Option α)
+  store : α → m PUnit
+
+export MonadStore1Of (store)
+
+/-- Similar to `MonadStore1Of`, but `α` is an `outParam` for convenience. -/
 class MonadStore1 {κ : Type u} (k : κ) (α : outParam $ Type v) (m : Type v → Type w) where
   fetch? : m (Option α)
   store : α → m PUnit
 
-export MonadStore1 (fetch? store)
+export MonadStore1 (fetch?)
+
+instance [MonadStore1Of k α m] : MonadStore1 k α m where
+  fetch? := MonadStore1Of.fetch? k
+  store := MonadStore1Of.store k
 
 /-- A monad equipped with a dependently typed key-object store. -/
-class MonadDStore (κ : Type u) (β : outParam $ κ → Type v) (m : Type v → Type w) where
+class MonadDStore (κ : Type u) (β : semiOutParam $ κ → Type v) (m : Type v → Type w) where
   fetch? : (key : κ) → m (Option (β key))
   store : (key : κ) → β key → m PUnit
 
-instance [MonadDStore κ β m] : MonadStore1 k (β k) m where
+instance [MonadDStore κ β m] : MonadStore1Of k (β k) m where
   fetch? := MonadDStore.fetch? k
   store o := MonadDStore.store k o
 
@@ -29,7 +40,7 @@ instance [MonadLift m n] [MonadDStore κ β m] : MonadDStore κ β n where
   store k a := liftM (m := m) <| store k a
 
 @[inline] def fetchOrCreate [Monad m]
-(key : κ) [MonadStore1 key α m] (create : m α) : m α := do
+(key : κ) [MonadStore1Of key α m] (create : m α) : m α := do
   if let some val ← fetch? key then
     return val
   else

src/lake/Lake/Util/StoreInsts.lean

@@ -13,7 +13,7 @@ namespace Lake
 
 instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where
   fetch? k := return (← get).find? k
-  store k a :=  modify (·.insert k a)
+  store k a := modify (·.insert k a)
 
 instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
   fetch? k := return (← get).find? k
@@ -21,11 +21,11 @@ instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where
 
 instance [Monad m] : MonadStore κ α (StateT (RBArray κ α cmp) m) where
   fetch? k := return (← get).find? k
-  store k a :=  modify (·.insert k a)
+  store k a := modify (·.insert k a)
 
 instance [Monad m] : MonadStore Name α (StateT (NameMap α) m) :=
   inferInstanceAs (MonadStore _ _ (StateT (RBMap ..) _))
 
-@[inline] instance [MonadDStore κ β m] [t : FamilyOut β k α] : MonadStore1 k α m where
+@[inline] instance [MonadDStore κ β m] [t : FamilyOut β k α] : MonadStore1Of k α m where
   fetch? := cast (by rw [t.family_key_eq_type]) <| fetch? (m := m) k
   store a := store k <| cast t.family_key_eq_type.symm a

src/lake/Lake/Util/Version.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2024 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lean.Elab.Eval
+
+/-! # Version
+
+This module contains useful definitions for manipulating versions.
+It also defines a `v!"<ver>"` syntax for version literals.
+-/
+
+open Lean
+
+namespace Lake
+
+/-- The major-minor-patch triple of a [SemVer](https://semver.org/). -/
+structure SemVerCore where
+  major : Nat := 0
+  minor : Nat := 0
+  patch : Nat := 0
+  deriving Inhabited, Repr, DecidableEq, Ord
+
+instance : LT SemVerCore := ltOfOrd
+instance : LE SemVerCore := leOfOrd
+instance : Min SemVerCore := minOfLe
+instance : Max SemVerCore := maxOfLe
+
+def SemVerCore.parse (ver : String) : Except String SemVerCore := do
+  try
+    match ver.split (· == '.') with
+    | [major, minor, patch] =>
+        let parseNat (v : String) (what : String) := do
+          let some v := v.toNat?
+            | throw s!"expect numeral {what} version, got '{v}'"
+          return v
+        return {
+          major := ← parseNat major "major"
+          minor := ← parseNat minor "minor"
+          patch := ← parseNat patch "patch"
+        }
+    | ps => throw s!"incorrect number of components: got {ps.length}, expected 3"
+  catch e =>
+    throw s!"invalid version core: {e}"
+
+protected def SemVerCore.toString (ver : SemVerCore) : String :=
+  s!"{ver.major}.{ver.minor}.{ver.patch}"
+
+instance : ToString SemVerCore := ⟨SemVerCore.toString⟩
+instance : ToJson SemVerCore := ⟨(·.toString)⟩
+instance : FromJson SemVerCore := ⟨(do SemVerCore.parse <| ← fromJson? ·)⟩
+
+instance : ToExpr SemVerCore where
+  toExpr ver := mkAppN (mkConst ``SemVerCore.mk)
+    #[toExpr ver.major, toExpr ver.minor, toExpr ver.patch]
+  toTypeExpr := mkConst ``SemVerCore
+
+/--
+A Lean-style semantic version.
+A major-minor-patch triple with an optional arbitrary `-` suffix.
+-/
+structure LeanVer extends SemVerCore where
+  specialDescr : String := ""
+  deriving Inhabited, Repr, DecidableEq
+
+instance : Coe LeanVer SemVerCore := ⟨LeanVer.toSemVerCore⟩
+
+@[inline] protected def LeanVer.ofSemVerCore (ver : SemVerCore) : LeanVer :=
+  {toSemVerCore := ver, specialDescr := ""}
+
+instance : Coe SemVerCore LeanVer := ⟨LeanVer.ofSemVerCore⟩
+
+protected def LeanVer.compare (a b : LeanVer) : Ordering :=
+  match compare a.toSemVerCore b.toSemVerCore with
+  | .eq =>
+    match a.specialDescr, b.specialDescr with
+    | "", "" => .eq
+    |  _, "" => .lt
+    | "",  _ => .gt
+    | a, b => compare a b
+  | ord => ord
+
+instance : Ord LeanVer := ⟨LeanVer.compare⟩
+
+instance : LT LeanVer := ltOfOrd
+instance : LE LeanVer := leOfOrd
+instance : Min LeanVer := minOfLe
+instance : Max LeanVer := maxOfLe
+
+def LeanVer.parse (ver : String) : Except String LeanVer := do
+  let sepPos := ver.find (· == '-')
+  if h : ver.atEnd sepPos then
+    SemVerCore.parse ver
+  else
+    let core ← SemVerCore.parse <| ver.extract 0 sepPos
+    let specialDescr := ver.extract (ver.next' sepPos h) ver.endPos
+    if specialDescr.isEmpty then
+      throw "invalid Lean version: '-' suffix cannot be empty"
+    return {toSemVerCore := core, specialDescr}
+
+protected def LeanVer.toString (ver : LeanVer) : String :=
+  if ver.specialDescr.isEmpty then
+    ver.toSemVerCore.toString
+  else
+    s!"{ver.toSemVerCore}-{ver.specialDescr}"
+
+instance : ToString LeanVer := ⟨LeanVer.toString⟩
+instance : ToJson LeanVer := ⟨(·.toString)⟩
+instance : FromJson LeanVer := ⟨(do LeanVer.parse <| ← fromJson? ·)⟩
+
+instance : ToExpr LeanVer where
+  toExpr ver := mkAppN (mkConst ``LeanVer.mk)
+    #[toExpr ver.toSemVerCore, toExpr ver.specialDescr]
+  toTypeExpr := mkConst ``LeanVer
+
+/-! ## Version Literals
+
+Defines the `v!"<ver>"` syntax for version literals.
+The elaborator attempts to synthesize an instance of `ToVersion` for the
+expected type and then applies it to the string literal.
+-/
+
+open Elab Term Meta
+
+/-- Parses a version from a string. -/
+class DecodeVersion (α : Type u) where
+  decodeVersion : String → Except String α
+
+export DecodeVersion (decodeVersion)
+
+instance : DecodeVersion SemVerCore := ⟨SemVerCore.parse⟩
+instance : DecodeVersion LeanVer := ⟨LeanVer.parse⟩
+
+private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr :=
+  Functor.map toExpr x
+
+/-- A Lake version literal. -/
+scoped syntax:max (name := verLit) "v!" noWs interpolatedStr(term) : term
+
+@[term_elab verLit] def elabVerLit : TermElab := fun stx expectedType? => do
+  let `(v!$v) := stx | throwUnsupportedSyntax
+  tryPostponeIfNoneOrMVar expectedType?
+  let some expectedType := expectedType?
+    | throwError "expected type is not known"
+  let ofVerT? ← mkAppM ``Except #[mkConst ``String, expectedType]
+  let ofVerE ← elabTermEnsuringType (← ``(decodeVersion s!$v)) ofVerT?
+  let resT ← mkAppM ``Except #[mkConst ``String, mkConst ``Expr]
+  let resE ← mkAppM ``toResultExpr #[ofVerE]
+  match (← unsafe evalExpr (Except String Expr) resT resE) with
+  | .ok ver => return ver
+  | .error e => throwError e

src/lake/README.md

@@ -15,6 +15,7 @@ Each `lakefile.lean` includes a `package` declaration (akin to `main`) which def
 * [Package Configuration Options](#package-configuration-options)
   + [Layout](#layout)
   + [Build & Run](#build--run)
+  + [Test & Lint](#test--lint)
   + [Cloud Releases](#cloud-releases)
 * [Defining Build Targets](#defining-build-targets)
   + [Lean Libraries](#lean-libraries)
@@ -164,8 +165,10 @@ Lake provides a large assortment of configuration options for packages.
 
 ### Layout
 
+These options control the top-level directory layout of the package and its build directory. Further paths specified by libraries, executables, and targets within the package are relative to these directories.
+
 * `packagesDir`: The directory to which Lake should download remote dependencies. Defaults to `.lake/packages`.
-* `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory. (This will be passed to `lean` as the `-R` option.)
+* `srcDir`: The directory containing the package's Lean source files. Defaults to the package's directory.
 * `buildDir`: The directory to which Lake should output the package's build results. Defaults to `build`.
 * `leanLibDir`: The build subdirectory to which Lake should output the package's binary Lean libraries (e.g., `.olean`, `.ilean` files). Defaults to `lib`.
 * `nativeLibDir`: The build subdirectory to which Lake should output the package's native libraries (e.g., `.a`, `.so`, `.dll` files). Defaults to `lib`.
@@ -174,6 +177,8 @@ Lake provides a large assortment of configuration options for packages.
 
 ### Build & Run
 
+These options configure how code is built and run in the package. Libraries, executables, and other targets within a package can further add to parts of this configuration.
+
 * `platformIndependent`: Asserts whether Lake should assume Lean modules are platform-independent. That is, whether lake should include the platform and platform-dependent elements in a module's trace. See the docstring of `Lake.LeanConfig.platformIndependent` for more details. Defaults to `none`.
 * `precompileModules`:  Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`.
 * `moreServerOptions`: An `Array` of additional options to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`.
@@ -188,8 +193,21 @@ Lake provides a large assortment of configuration options for packages.
 * `weakLinkArgs`: An `Array` of additional arguments to pass to `leanc` when linking (e.g., binary executables or shared libraries) Unlike `moreLinkArgs`, these arguments do not affect the trace of the build result, so they can be changed without triggering a rebuild. They come *before* `moreLinkArgs`.
 * `extraDepTargets`: An `Array` of [target](#custom-targets) names that the package should always build before anything else.
 
+### Test & Lint
+
+The CLI commands `lake test` and `lake lint` use definitions configured by the workspace's root package to perform testing and linting (this referred to as the test or lint *driver*). In Lean configuration files, these can be specified by applying the `@[test_driver]` or `@[lint_driver]` to a `script`, `lean_exe`, or `lean_lb`. They can also be configured (in Lean or TOML format) via the following options on the package.
+
+* `testDriver`: The name of the script, executable, or library to drive `lake test`.
+* `testDriverArgs`: An `Array` of arguments to pass to the package's test driver.
+* `lintDriver`: The name of the script or executable used by `lake lint`. Libraries cannot be lint drivers.
+* `lintDriverArgs`: An `Array` of arguments to pass to the package's lint driver.
+
+You can specify definition from a dependency as a package's test or lint driver by using the syntax `<pkg>/<name>`. An executable driver will be built and then run, a script driver will just be run, and a library driver will just be built. A script or executable driver is run with any arguments configured by package (e.g., via `testDriverArgs`) followed by any specified on the CLI (e.g., via `lake lint -- <args>...`).
+
 ### Cloud Releases
 
+These options define a cloud release for the package. See the section on [GitHub Release Builds](#github-release-builds) for more information.
+
 * `releaseRepo`: The URL of the GitHub repository to upload and download releases of this package.  If `none` (the default), for downloads, Lake uses the URL the package was download from (if it is a dependency) and for uploads, uses `gh`'s default.
 * `buildArchive`: The name of the build archive for the GitHub cloud release.
 Defaults to `{(pkg-)name}-{System.Platform.target}.tar.gz`.

src/lake/examples/deps/bar/lake-manifest.expected.json

@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"type": "path",

src/lake/examples/hello/test.sh

@@ -1,4 +1,5 @@
-set -ex
+#!/usr/bin/env bash
+set -euxo pipefail
 
 LAKE=${LAKE:-../../.lake/build/bin/lake}
 
@@ -15,6 +16,16 @@ $LAKE -q build hello 2>&1 | diff - /dev/null
 # Related: https://github.com/leanprover/lean4/issues/2549
 test -f lake-manifest.json
 
+# Test pack/unpack
+$LAKE pack .lake/build.tgz 2>&1 | grep --color "packing"
+rm -rf .lake/build
+$LAKE unpack .lake/build.tgz 2>&1 | grep --color "unpacking"
+.lake/build/bin/hello
+$LAKE pack 2>&1 | grep --color "packing"
+rm -rf .lake/build
+$LAKE unpack 2>&1 | grep --color "unpacking"
+.lake/build/bin/hello
+
 ./clean.sh
 
 $LAKE -f lakefile.toml exe hello

src/lake/tests/driver/dep-invalid.lean

@@ -0,0 +1,6 @@
+import Lake
+open Lake DSL
+
+package test where
+  testDriver := "dep/driver/foo"
+  lintDriver := "dep/driver/foo"

src/lake/tests/driver/dep-invalid.toml

@@ -0,0 +1,3 @@
+name = "test"
+testDriver = "dep/driver/foo"
+lintDriver = "dep/driver/foo"

src/lake/tests/driver/dep-unknown.lean

@@ -0,0 +1,6 @@
+import Lake
+open Lake DSL
+
+package test where
+  testDriver := "dep/driver"
+  lintDriver := "dep/driver"

src/lake/tests/driver/dep-unknown.toml

@@ -0,0 +1,3 @@
+name = "test"
+testDriver = "dep/driver"
+lintDriver = "dep/driver"

src/lake/tests/driver/dep.lean

@@ -0,0 +1,8 @@
+import Lake
+open Lake DSL
+
+package test where
+  testDriver := "dep/driver"
+  lintDriver := "dep/driver"
+
+require dep from "dep"

src/lake/tests/driver/dep.toml

@@ -0,0 +1,7 @@
+name = "test"
+testDriver = "dep/driver"
+lintDriver = "dep/driver"
+
+[[require]]
+name = "dep"
+path = "dep"

src/lake/tests/driver/dep/lakefile.lean

@@ -0,0 +1,9 @@
+import Lake
+open System Lake DSL
+
+package dep
+
+@[test_driver, lint_driver]
+script driver args do
+  IO.println s!"dep: {args}"
+  return 0

src/lake/tests/driver/exe.lean

@@ -0,0 +1,7 @@
+import Lake
+open System Lake DSL
+
+package test
+
+@[test_driver, lint_driver]
+lean_exe driver

src/lake/tests/driver/exe.toml

@@ -0,0 +1,6 @@
+name = "test"
+testDriver = "driver"
+lintDriver = "driver"
+
+[[lean_exe]]
+name = "driver"

src/lake/tests/driver/lib.lean

@@ -0,0 +1,7 @@
+import Lake
+open Lake DSL
+
+package test
+
+@[test_driver]
+lean_lib Test

src/lake/tests/driver/lib.toml

@@ -0,0 +1,5 @@
+name = "test"
+testDriver = "Test"
+
+[[lean_lib]]
+name = "Test"

src/lake/tests/driver/runner.lean

@@ -4,4 +4,4 @@ open System Lake DSL
 package test
 
 @[test_runner]
-lean_exe test
+lean_exe driver