update scripts

Merge remote-tracking branch 'origin/master' into github_metrics
feat: show signature elaboration errors on body parse error (#4267 )
2026-03-21 04:14:07 +00:00 · 2024-06-01 03:12:29 +10:00 · 2024-05-24 23:11:36 +10:00 · 2024-05-24 10:07:07 +00:00 · 2024-05-24 08:18:49 +00:00 · 2024-05-24 05:15:15 +00:00
234 changed files with 1120 additions and 1229 deletions
--- a/.github/workflows/ci.yml
+++ b/.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,170 @@ 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",
+                "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 +332,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 +365,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 +395,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 +428,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
--- a/.github/workflows/restart-on-label.yml
+++ b/.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
--- a/CMakePresets.json
+++ b/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"
+    }
+  ]
+}
--- a/RELEASES.md
+++ b/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
 ---------
--- a/doc/make/index.md
+++ b/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`,
--- a/doc/make/msvc.md
+++ b/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.
--- a/doc/make/msys2.md
+++ b/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

--- a/doc/setup.md
+++ b/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

--- a/releases_drafts/README.md
+++ b/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.
--- a/releases_drafts/messagedata.md
+++ b/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
--- a/releases_drafts/wf.md
+++ b/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
--- a/script/github-issues-fro.py
+++ b/script/github-issues-fro.py
@@ -0,0 +1,180 @@
+#!/usr/bin/env python3
+
+import subprocess
+import sys
+import json
+from datetime import datetime, timedelta
+from urllib.parse import urlencode
+import argparse
+import calendar
+import time
+import statistics
+
+# Reminder: Ensure you have `gh` CLI installed and authorized before running this script.
+# Follow instructions from https://cli.github.com/ to set up `gh` and ensure it is authorized.
+
+LABELS = ["bug", "feature", "RFC", "new-user-papercuts", "Lake"]
+
+def get_items(query):
+    items = []
+    page = 1
+    base_url = 'https://api.github.com/search/issues'
+    retries = 0
+    max_retries = 5
+    while True:
+        params = {'q': query, 'per_page': 100, 'page': page}
+        url = f"{base_url}?{urlencode(params)}"
+        # print(f"Fetching page {page} from URL: {url}")
+        try:
+            result = subprocess.run(['gh', 'api', url], capture_output=True, text=True)
+            data = json.loads(result.stdout)
+            if 'items' in data:
+                items.extend(data['items'])
+            elif 'message' in data and 'rate limit' in data['message'].lower():
+                if retries < max_retries:
+                    wait_time = (2 ** retries) * 60  # Exponential backoff
+                    time.sleep(wait_time)
+                    retries += 1
+                    continue
+                else:
+                    print("Max retries exceeded. Exiting.")
+                    break
+            else:
+                print(f"Error fetching data: {data}")
+                break
+            if len(data['items']) < 100:
+                break
+            page += 1
+        except Exception as e:
+            print(f"Error fetching data: {e}")
+            print(result.stdout)  # Print the JSON output for debugging
+            break
+    return items
+
+def get_fro_team_members():
+    try:
+        result = subprocess.run(['gh', 'api', '-H', 'Accept: application/vnd.github.v3+json', '/orgs/leanprover/teams/fro/members'], capture_output=True, text=True)
+        members = json.loads(result.stdout)
+        return [member['login'] for member in members]
+    except Exception as e:
+        print(f"Error fetching team members: {e}")
+        return []
+
+def calculate_average_time_to_close(closed_items):
+    times_to_close = [(datetime.strptime(item['closed_at'], '%Y-%m-%dT%H:%M:%SZ') - datetime.strptime(item['created_at'], '%Y-%m-%dT%H:%M:%SZ')).days for item in closed_items]
+    average_time_to_close = sum(times_to_close) / len(times_to_close) if times_to_close else 0
+    return average_time_to_close
+
+def parse_dates(date_args):
+    if len(date_args) == 2:
+        start_date = date_args[0]
+        end_date = date_args[1]
+    elif len(date_args) == 1:
+        if len(date_args[0]) == 7:  # YYYY-MM format
+            year, month = map(int, date_args[0].split('-'))
+            start_date = f"{year}-{month:02d}-01"
+            end_date = f"{year}-{month:02d}-{calendar.monthrange(year, month)[1]}"
+        elif len(date_args[0]) == 4:  # YYYY format
+            year = int(date_args[0])
+            start_date = f"{year}-07-01"
+            end_date = f"{year+1}-06-30"
+        elif len(date_args[0]) == 6 and date_args[0][4] == 'Q':  # YYYYQn format
+            year = int(date_args[0][:4])
+            quarter = int(date_args[0][5])
+            if quarter == 1:
+                start_date = f"{year}-01-01"
+                end_date = f"{year}-03-31"
+            elif quarter == 2:
+                start_date = f"{year}-04-01"
+                end_date = f"{year}-06-30"
+            elif quarter == 3:
+                start_date = f"{year}-07-01"
+                end_date = f"{year}-09-30"
+            elif quarter == 4:
+                start_date = f"{year}-10-01"
+                end_date = f"{year}-12-31"
+            else:
+                raise ValueError("Invalid quarter format")
+        else:
+            raise ValueError("Invalid date format")
+    else:
+        raise ValueError("Invalid number of date arguments")
+
+    return start_date, end_date
+
+def split_date_range(start_date, end_date):
+    start = datetime.strptime(start_date, '%Y-%m-%d')
+    end = datetime.strptime(end_date, '%Y-%m-%d')
+    date_ranges = []
+
+    # Splitting into month-long windows to work around the GitHub search 1000 result limit.
+    while start <= end:
+        month_end = start + timedelta(days=calendar.monthrange(start.year, start.month)[1] - start.day)
+        month_end = min(month_end, end)
+        date_ranges.append((start.strftime('%Y-%m-%d'), month_end.strftime('%Y-%m-%d')))
+        start = month_end + timedelta(days=1)
+
+    return date_ranges
+
+def main():
+    parser = argparse.ArgumentParser(description="Fetch and count GitHub issues assigned to fro team members between two dates.")
+    parser.add_argument("dates", type=str, nargs='+', help="Start and end dates in YYYY-MM-DD, YYYY-MM, YYYY-Qn, or YYYY format")
+
+    args = parser.parse_args()
+    start_date, end_date = parse_dates(args.dates)
+
+    repo = "leanprover/lean4"
+
+    date_ranges = split_date_range(start_date, end_date)
+
+    fro_members = get_fro_team_members()
+    fro_members.append("unassigned")  # Add "unassigned" for issues with no assignee
+
+    label_headers = ", ".join([f"MTTR ({label})" for label in LABELS])
+    print(f"# username, open issues, new issues, closed issues, MTTR (all), {label_headers}")
+
+    for member in fro_members:
+        open_issues_count = 0
+        new_issues_count = 0
+        closed_issues_count = 0
+        total_time_to_close_issues = 0
+        closed_issues = []
+        label_times = {label: [] for label in LABELS}
+
+        for start, end in date_ranges:
+            if member == "unassigned":
+                open_issues_query1 = f'repo:{repo} is:issue no:assignee state:open created:<={end}'
+                open_issues_query2 = f'repo:{repo} is:issue no:assignee state:closed created:<={end} closed:>{end}'
+                new_issues_query = f'repo:{repo} is:issue no:assignee created:{start}..{end}'
+                closed_issues_query = f'repo:{repo} is:issue no:assignee closed:{start}..{end}'
+            else:
+                open_issues_query1 = f'repo:{repo} is:issue assignee:{member} state:open created:<={end}'
+                open_issues_query2 = f'repo:{repo} is:issue assignee:{member} state:closed created:<={end} closed:>{end}'
+                new_issues_query = f'repo:{repo} is:issue assignee:{member} created:{start}..{end}'
+                closed_issues_query = f'repo:{repo} is:issue assignee:{member} closed:{start}..{end}'
+
+            open_issues1 = get_items(open_issues_query1)
+            open_issues2 = get_items(open_issues_query2)
+            new_issues = get_items(new_issues_query)
+            closed_issues_period = get_items(closed_issues_query)
+
+            open_issues_count = len(open_issues1) + len(open_issues2)
+            new_issues_count += len(new_issues)
+            closed_issues_count += len(closed_issues_period)
+            closed_issues.extend(closed_issues_period)
+
+            for issue in closed_issues_period:
+                time_to_close = (datetime.strptime(issue['closed_at'], '%Y-%m-%dT%H:%M:%SZ') - datetime.strptime(issue['created_at'], '%Y-%m-%dT%H:%M:%SZ')).days
+                total_time_to_close_issues += time_to_close
+                for label in LABELS:
+                    if label in [l['name'] for l in issue['labels']]:
+                        label_times[label].append(time_to_close)
+
+        average_time_to_close_issues = total_time_to_close_issues / closed_issues_count if closed_issues_count else 0
+        label_averages = {label: (sum(times) / len(times)) if times else 0 for label, times in label_times.items()}
+
+        label_averages_str = ", ".join([f"{label_averages[label]:.2f}" for label in LABELS])
+        print(f"{member},{open_issues_count},{new_issues_count},{closed_issues_count},{average_time_to_close_issues:.2f},{label_averages_str}")
+
+if __name__ == "__main__":
+    main()
--- a/script/github-metrics.py
+++ b/script/github-metrics.py
@@ -0,0 +1,163 @@
+#!/usr/bin/env python3
+
+import subprocess
+import sys
+import json
+from datetime import datetime, timedelta
+from urllib.parse import urlencode
+import argparse
+import calendar
+import time
+
+# Reminder: Ensure you have `gh` CLI installed and authorized before running this script.
+# Follow instructions from https://cli.github.com/ to set up `gh` and ensure it is authorized.
+
+def get_items(query):
+    items = []
+    page = 1
+    base_url = 'https://api.github.com/search/issues'
+    retries = 0
+    max_retries = 5
+    while True:
+        params = {'q': query, 'per_page': 100, 'page': page}
+        url = f"{base_url}?{urlencode(params)}"
+        # print(f"Fetching page {page} from URL: {url}")
+        try:
+            result = subprocess.run(['gh', 'api', url], capture_output=True, text=True)
+            data = json.loads(result.stdout)
+            if 'items' in data:
+                items.extend(data['items'])
+            elif 'message' in data and 'rate limit' in data['message'].lower():
+                if retries < max_retries:
+                    wait_time = (2 ** retries) * 60  # Exponential backoff
+                    print(f"Rate limit exceeded. Retrying in {wait_time} seconds...")
+                    time.sleep(wait_time)
+                    retries += 1
+                    continue
+                else:
+                    print("Max retries exceeded. Exiting.")
+                    break
+            else:
+                print(f"Error fetching data: {data}")
+                break
+            if len(data['items']) < 100:
+                break
+            page += 1
+        except Exception as e:
+            print(f"Error fetching data: {e}")
+            print(result.stdout)  # Print the JSON output for debugging
+            break
+    return items
+
+def calculate_average_time_to_close(closed_items):
+    times_to_close = [(datetime.strptime(item['closed_at'], '%Y-%m-%dT%H:%M:%SZ') - datetime.strptime(item['created_at'], '%Y-%m-%dT%H:%M:%SZ')).days for item in closed_items]
+    average_time_to_close = sum(times_to_close) / len(times_to_close) if times_to_close else 0
+    return average_time_to_close
+
+def parse_dates(date_args):
+    if len(date_args) == 2:
+        start_date = date_args[0]
+        end_date = date_args[1]
+    elif len(date_args) == 1:
+        if len(date_args[0]) == 7:  # YYYY-MM format
+            year, month = map(int, date_args[0].split('-'))
+            start_date = f"{year}-{month:02d}-01"
+            end_date = f"{year}-{month:02d}-{calendar.monthrange(year, month)[1]}"
+        elif len(date_args[0]) == 4:  # YYYY format
+            year = int(date_args[0])
+            start_date = f"{year}-07-01"
+            end_date = f"{year+1}-06-30"
+        elif len(date_args[0]) == 6 and date_args[0][4] == 'Q':  # YYYYQn format
+            year = int(date_args[0][:4])
+            quarter = int(date_args[0][5])
+            if quarter == 1:
+                start_date = f"{year}-01-01"
+                end_date = f"{year}-03-31"
+            elif quarter == 2:
+                start_date = f"{year}-04-01"
+                end_date = f"{year}-06-30"
+            elif quarter == 3:
+                start_date = f"{year}-07-01"
+                end_date = f"{year}-09-30"
+            elif quarter == 4:
+                start_date = f"{year}-10-01"
+                end_date = f"{year}-12-31"
+            else:
+                raise ValueError("Invalid quarter format")
+        else:
+            raise ValueError("Invalid date format")
+    else:
+        raise ValueError("Invalid number of date arguments")
+
+    return start_date, end_date
+
+def split_date_range(start_date, end_date):
+    start = datetime.strptime(start_date, '%Y-%m-%d')
+    end = datetime.strptime(end_date, '%Y-%m-%d')
+    date_ranges = []
+
+    # Splitting into month-long windows to work around the GitHub search 1000 result limit.
+    while start <= end:
+        month_end = start + timedelta(days=calendar.monthrange(start.year, start.month)[1] - start.day)
+        month_end = min(month_end, end)
+        date_ranges.append((start.strftime('%Y-%m-%d'), month_end.strftime('%Y-%m-%d')))
+        start = month_end + timedelta(days=1)
+
+    return date_ranges
+
+def main():
+    parser = argparse.ArgumentParser(description="Fetch and count GitHub issues and pull requests between two dates.")
+    parser.add_argument("dates", type=str, nargs='+', help="Start and end dates in YYYY-MM-DD, YYYY-MM, YYYY-Qn, or YYYY format")
+
+    args = parser.parse_args()
+    start_date, end_date = parse_dates(args.dates)
+
+    repo = "leanprover/lean4"
+
+    date_ranges = split_date_range(start_date, end_date)
+
+    open_issues_count = 0
+    opened_issues_count = 0
+    closed_issues_count = 0
+    total_time_to_close_issues = 0
+    open_prs_count = 0
+    closed_but_not_merged_prs_count = 0
+    merged_prs_count = 0
+
+    for start, end in date_ranges:
+        open_issues_query1 = f'repo:{repo} is:issue state:open created:<={end}'
+        open_issues_query2 = f'repo:{repo} is:issue state:closed created:<={end} closed:>{end}'
+        opened_issues_query = f'repo:{repo} is:issue created:{start}..{end}'
+        closed_issues_query = f'repo:{repo} is:issue closed:{start}..{end}'
+
+        open_prs_query1 = f'repo:{repo} is:pr state:open created:<={end}'
+        open_prs_query2 = f'repo:{repo} is:pr state:closed created:<={end} closed:>{end}'
+        closed_but_not_merged_prs_query = f'repo:{repo} is:pr state:closed is:unmerged closed:{start}..{end}'
+        merged_prs_query = f'repo:{repo} is:pr is:merged closed:{start}..{end}'
+
+        open_issues1 = get_items(open_issues_query1)
+        open_issues2 = get_items(open_issues_query2)
+        opened_issues = get_items(opened_issues_query)
+        closed_issues = get_items(closed_issues_query)
+
+        open_prs1 = get_items(open_prs_query1)
+        open_prs2 = get_items(open_prs_query2)
+        closed_but_not_merged_prs = get_items(closed_but_not_merged_prs_query)
+        merged_prs = get_items(merged_prs_query)
+
+        open_issues_count = len(open_issues1) + len(open_issues2)
+        opened_issues_count += len(opened_issues)
+        closed_issues_count += len(closed_issues)
+        total_time_to_close_issues += sum((datetime.strptime(item['closed_at'], '%Y-%m-%dT%H:%M:%SZ') - datetime.strptime(item['created_at'], '%Y-%m-%dT%H:%M:%SZ')).days for item in closed_issues)
+
+        open_prs_count = len(open_prs1) + len(open_prs2)
+        closed_but_not_merged_prs_count += len(closed_but_not_merged_prs)
+        merged_prs_count += len(merged_prs)
+
+    average_time_to_close_issues = total_time_to_close_issues / closed_issues_count if closed_issues_count else 0
+
+    print("# open issues, opened issues, closed issues, average age of closed issues, open PRs, closed PRs, merged PRs")
+    print(f"{open_issues_count},{opened_issues_count},{closed_issues_count},{average_time_to_close_issues:.2f},{open_prs_count},{closed_but_not_merged_prs_count},{merged_prs_count}")
+
+if __name__ == "__main__":
+    main()
--- a/src/CMakeLists.txt
+++ b/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)
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/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
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -175,8 +175,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]
--- a/src/Init/Data/Bool.lean
+++ b/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 : α) :
--- a/src/Init/Data/Int/Order.lean
+++ 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)
--- a/src/Init/Data/Nat/Bitwise/Basic.lean
+++ b/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
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/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]
--- a/src/Lean/Attributes.lean
+++ b/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
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/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 }
--- a/src/Lean/Elab/Command.lean
+++ b/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
--- a/src/Lean/Elab/Declaration.lean
+++ b/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
--- a/src/Lean/Elab/DefView.lean
+++ b/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 :=
--- a/src/Lean/Elab/MutualDef.lean
+++ b/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
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/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

--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/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
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/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
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/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
--- a/src/Lean/Elab/Term.lean
+++ b/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
--- a/src/lake/Lake/Util/Family.lean
+++ b/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
--- a/src/lake/Lake/Util/Store.lean
+++ b/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
--- a/src/lake/Lake/Util/StoreInsts.lean
+++ b/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
--- a/stage0/src/runtime/alloc.cpp
+++ b/stage0/src/runtime/alloc.cpp
--- a/stage0/src/runtime/alloc.h
+++ b/stage0/src/runtime/alloc.h
--- a/stage0/src/runtime/io.cpp
+++ b/stage0/src/runtime/io.cpp
--- a/stage0/stdlib/Init/Data/BitVec/Lemmas.c
+++ b/stage0/stdlib/Init/Data/BitVec/Lemmas.c
--- a/stage0/stdlib/Init/Data/Nat/Bitwise/Basic.c
+++ b/stage0/stdlib/Init/Data/Nat/Bitwise/Basic.c
--- a/stage0/stdlib/Init/Data/String/Basic.c
+++ b/stage0/stdlib/Init/Data/String/Basic.c
--- a/stage0/stdlib/Init/Grind.c
+++ b/stage0/stdlib/Init/Grind.c
--- a/stage0/stdlib/Init/Grind/Cases.c
+++ b/stage0/stdlib/Init/Grind/Cases.c
--- a/stage0/stdlib/Init/Grind/Tactics.c
+++ b/stage0/stdlib/Init/Grind/Tactics.c
--- a/stage0/stdlib/Init/Prelude.c
+++ b/stage0/stdlib/Init/Prelude.c
--- a/stage0/stdlib/Init/System/IO.c
+++ b/stage0/stdlib/Init/System/IO.c
--- a/stage0/stdlib/Lean/AddDecl.c
+++ b/stage0/stdlib/Lean/AddDecl.c
--- a/stage0/stdlib/Lean/Attributes.c
+++ b/stage0/stdlib/Lean/Attributes.c
--- a/stage0/stdlib/Lean/Compiler/ExternAttr.c
+++ b/stage0/stdlib/Lean/Compiler/ExternAttr.c
--- a/stage0/stdlib/Lean/Compiler/InitAttr.c
+++ b/stage0/stdlib/Lean/Compiler/InitAttr.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Main.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Main.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/PrettyPrinter.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Simp/Main.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/Simp/SimpM.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/Simp/SimpM.c
--- a/stage0/stdlib/Lean/Compiler/LCNF/ToLCNF.c
+++ b/stage0/stdlib/Lean/Compiler/LCNF/ToLCNF.c
--- a/stage0/stdlib/Lean/Compiler/Specialize.c
+++ b/stage0/stdlib/Lean/Compiler/Specialize.c
--- a/stage0/stdlib/Lean/CoreM.c
+++ b/stage0/stdlib/Lean/CoreM.c
--- a/stage0/stdlib/Lean/Elab/App.c
+++ b/stage0/stdlib/Lean/Elab/App.c
--- a/stage0/stdlib/Lean/Elab/Arg.c
+++ b/stage0/stdlib/Lean/Elab/Arg.c
--- a/stage0/stdlib/Lean/Elab/Binders.c
+++ b/stage0/stdlib/Lean/Elab/Binders.c
--- a/stage0/stdlib/Lean/Elab/BuiltinCommand.c
+++ b/stage0/stdlib/Lean/Elab/BuiltinCommand.c
--- a/stage0/stdlib/Lean/Elab/BuiltinNotation.c
+++ b/stage0/stdlib/Lean/Elab/BuiltinNotation.c
--- a/stage0/stdlib/Lean/Elab/BuiltinTerm.c
+++ b/stage0/stdlib/Lean/Elab/BuiltinTerm.c
--- a/stage0/stdlib/Lean/Elab/Calc.c
+++ b/stage0/stdlib/Lean/Elab/Calc.c
--- a/stage0/stdlib/Lean/Elab/CheckTactic.c
+++ b/stage0/stdlib/Lean/Elab/CheckTactic.c
--- a/stage0/stdlib/Lean/Elab/Command.c
+++ b/stage0/stdlib/Lean/Elab/Command.c
--- a/stage0/stdlib/Lean/Elab/ComputedFields.c
+++ b/stage0/stdlib/Lean/Elab/ComputedFields.c
--- a/stage0/stdlib/Lean/Elab/DeclNameGen.c
+++ b/stage0/stdlib/Lean/Elab/DeclNameGen.c
--- a/stage0/stdlib/Lean/Elab/Declaration.c
+++ b/stage0/stdlib/Lean/Elab/Declaration.c
--- a/stage0/stdlib/Lean/Elab/DefView.c
+++ b/stage0/stdlib/Lean/Elab/DefView.c
--- a/stage0/stdlib/Lean/Elab/Deriving/Basic.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Basic.c
--- a/stage0/stdlib/Lean/Elab/Deriving/Inhabited.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Inhabited.c
--- a/stage0/stdlib/Lean/Elab/Deriving/Util.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/Util.c
--- a/stage0/stdlib/Lean/Elab/Do.c
+++ b/stage0/stdlib/Lean/Elab/Do.c
--- a/stage0/stdlib/Lean/Elab/ElabRules.c
+++ b/stage0/stdlib/Lean/Elab/ElabRules.c
--- a/stage0/stdlib/Lean/Elab/Exception.c
+++ b/stage0/stdlib/Lean/Elab/Exception.c
--- a/stage0/stdlib/Lean/Elab/Extra.c
+++ b/stage0/stdlib/Lean/Elab/Extra.c
--- a/stage0/stdlib/Lean/Elab/Frontend.c
+++ b/stage0/stdlib/Lean/Elab/Frontend.c
--- a/stage0/stdlib/Lean/Elab/GuardMsgs.c
+++ b/stage0/stdlib/Lean/Elab/GuardMsgs.c
--- a/stage0/stdlib/Lean/Elab/Import.c
+++ b/stage0/stdlib/Lean/Elab/Import.c
--- a/stage0/stdlib/Lean/Elab/Inductive.c
+++ b/stage0/stdlib/Lean/Elab/Inductive.c
--- a/stage0/stdlib/Lean/Elab/InfoTree/Main.c
+++ b/stage0/stdlib/Lean/Elab/InfoTree/Main.c
--- a/stage0/stdlib/Lean/Elab/InheritDoc.c
+++ b/stage0/stdlib/Lean/Elab/InheritDoc.c
--- a/stage0/stdlib/Lean/Elab/LetRec.c
+++ b/stage0/stdlib/Lean/Elab/LetRec.c
--- a/stage0/stdlib/Lean/Elab/Macro.c
+++ b/stage0/stdlib/Lean/Elab/Macro.c
--- a/stage0/stdlib/Lean/Elab/MacroRules.c
+++ b/stage0/stdlib/Lean/Elab/MacroRules.c
--- a/stage0/stdlib/Lean/Elab/Match.c
+++ b/stage0/stdlib/Lean/Elab/Match.c
--- a/stage0/stdlib/Lean/Elab/MutualDef.c
+++ b/stage0/stdlib/Lean/Elab/MutualDef.c
--- a/stage0/stdlib/Lean/Elab/PatternVar.c
+++ b/stage0/stdlib/Lean/Elab/PatternVar.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Basic.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Basic.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Main.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Main.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/MkInhabitant.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/MkInhabitant.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/BRecOn.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/BRecOn.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/FindRecArg.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/FindRecArg.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/IndPred.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/IndPred.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Fix.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Fix.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/GuessLex.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/GuessLex.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c
--- a/Show More
+++ b/Show More
Author	SHA1	Message	Date
Kim Morrison	f5b6070594	update scripts	2024-06-01 03:12:29 +10:00
Kim Morrison	bd00c5bca3	Merge remote-tracking branch 'origin/master' into github_metrics	2024-05-24 23:11:36 +10:00
Sebastian Ullrich	d3ee0be908	feat: show signature elaboration errors on body parse error (#4267 ) Fixes #3556 --------- Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>	2024-05-24 10:07:07 +00:00
Sebastian Ullrich	d1a96f6d8f	chore: CI: native-compile aarch64 macOS (#4265 )	2024-05-24 08:18:49 +00:00
Kim Morrison	b0c1112471	chore: better `omega` error message if no facts found (#4264 )	2024-05-24 05:15:15 +00:00
JovanGerb	e5e5a4d2e0	chore: fix the `MonadStore` type classes, with semiOutParam (#4205 ) The type class `MonadStore1` and friends have an outParam, which should not be an outParam, because there are multiple possible values for this parameter. At this function [fetchOrCreate](`1382e9fbc4/src/lake/Lake/Load/Main.lean (L196C49-L196C63)`), there are multiple stacked `StateT` monad transformers that each give a different instance to `MonadStore1`. It is an implementation detail of type class synthesis which instance is found. This particular type class synthesis fails when the unused instance `Lake.instMonadStore1OfMonadDStoreOfFamilyOut` is set to a lower priority, because then the synthesis order happens to go differently, so the wrong instance is found. Replacing the outParam with a semiOutParam solves this issue. Thus, we make a new type class `MonadStore1Of`, which is the same, but with a semiOutParam. This follows the design of `MonadState` and `MonadStateOf`. However, then it turns out that the instance cannot anymore be synthesised. There are two instances for `MonadStore1`: ``` instance [MonadDStore κ β m] : MonadStore1 k (β k) m instance [MonadDStore κ β m] [FamilyOut β k α] : MonadStore1 k α m ``` The first one is problematic during unification, especially when `β` should be instantiated as a constant function. We make the second one sufficient by adding an instance for the general type family: ``` /-- The general type family -/ instance (priority := low) : FamilyDef Fam a (Fam a) where family_key_eq_type := rfl ``` So then we can get rid of the first instance.	2024-05-24 02:09:07 +00:00
Kim Morrison	e5d6872065	average ages of all issues	2024-05-24 11:11:05 +10:00
Kim Morrison	45e05788ed	report average age	2024-05-24 11:04:02 +10:00
Kim Morrison	e22e2d5051	chore: script to collect github metrics	2024-05-24 10:51:01 +10:00
Sebastian Ullrich	e020f3d159	chore: CI: move some expensive checks from merge queue to releases (#4255 )	2024-05-23 20:45:44 +00:00
Sebastian Ullrich	811bad16e1	fix: ensure incremental commands and tactics are reached only on supported paths (#4259 ) Without this, it would not easy but perhaps be feasible to break incrementality when editing command prefixes such as `set_option ... in theorem` or also `theorem namesp.name ...` (which is a macro), especially if at some later point we support incrementality in input shifted by an edit. Explicit, sound support for these common cases will be brought back soon.	2024-05-23 17:57:42 +00:00
Sebastian Ullrich	67338bac23	chore: replace `registerBuiltinIncrementalTactic` with `@[builtin_incremental]`	2024-05-23 17:53:58 +02:00
Sebastian Ullrich	ba629545cc	chore: update stage0	2024-05-23 17:26:21 +02:00
Sebastian Ullrich	dfb496a271	fix: allow multiple `declareBuiltin` per declaration	2024-05-23 17:23:39 +02:00
Sebastian Ullrich	250994166c	feat: `[(builtin_)incremental]` elab attribute	2024-05-23 17:23:39 +02:00
Sebastian Ullrich	73a0c73c7c	chore: modernize build instructions (#4032 ) Use `cmake --preset`, adjust and document parallelism settings	2024-05-23 10:55:07 +00:00
meow-sister	258cc28dfc	fix: docstring in `Attributes.lean` (#4238 ) Changing document string in `Attributes.lean`, in order to consistent with code in `Lean.Parser.Attr`. --------- Co-authored-by: Kim Morrison <kim@tqft.net>	2024-05-23 10:13:43 +00:00
Sebastian Ullrich	f61a64d2ff	chore: reset `LEAN_VERSION_IS_RELEASE`	2024-05-23 12:28:24 +02:00
Kyle Miller	d984030c6a	chore: set up procedure for preparing release notes (#4247 ) We are switching to a new system for preparing release notes. * Release notes will be compiled when creating a release candidate from all the commits that are part of that release. * PRs can include suggestions for release notes in PR messages. Please use language such as "release notes" and "breaking changes" to call attention to the suggestions. Release notes are user-centric rather than developer-centric. * For more complicated release notes, these can be put into the `releases_drafts` folder. This solves an issue where PRs that include release notes can, when merged, have those notes appear under the wrong Lean version, since they might have been created before a release but not merged until after. It also solves merge conflicts due to multiple PRs updating the release notes.	2024-05-23 02:46:11 +00:00
FR	93758cc222	perf: faster `Nat.testBit` (#4188 ) `1 &&& n` is faster than `n &&& 1` for big `n`. ---	2024-05-23 01:34:40 +00:00
Alex Keizer	4fa3b3c4a0	feat: bitblasting theorems for signed comparisons (#4201 ) Prove theorems that relate `BitVec.slt` and `sle` to `carry`, so that these signed comparisons may be bitblasted in LeanSAT. This PR is stacked on top of #4200. For the diff without changes from that PR, see: https://github.com/opencompl/lean4/compare/opencompl:lean4:bitvec-toInt-iff-msb...bitvec-slt-blast --------- Co-authored-by: Kim Morrison <scott@tqft.net>	2024-05-23 01:24:04 +00:00