chore: CI: update github-script

.github/ISSUE_TEMPLATE/bug_report.md

@@ -9,15 +9,9 @@ assignees: ''
 
 ### Prerequisites
 
-Please put an X between the brackets as you perform the following steps:
-
-* [ ] Check that your issue is not already filed:
-      https://github.com/leanprover/lean4/issues
-* [ ] Reduce the issue to a minimal, self-contained, reproducible test case.
-      Avoid dependencies to Mathlib or Batteries.
-* [ ] Test your test case against the latest nightly release, for example on
-      https://live.lean-lang.org/#project=lean-nightly
-      (You can also use the settings there to switch to “Lean nightly”)
+* [ ] Put an X between the brackets on this line if you have done all of the following:
+    * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
+    * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
 
 ### Description
 
@@ -25,7 +19,7 @@ Please put an X between the brackets as you perform the following steps:
 
 ### Context
 
-[Broader context that the issue occurred in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
+[Broader context that the issue occured in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
 
 ### Steps to Reproduce
 
@@ -39,8 +33,8 @@ Please put an X between the brackets as you perform the following steps:
 
 ### Versions
 
-[Output of `#version` or `#eval Lean.versionString`]
-[OS version, if not using live.lean-lang.org.]
+[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
+[OS version]
 
 ### Additional Information
 

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,21 +1,13 @@
-# Read this section before submitting
+# Read and remove this section before submitting
 
 * Ensure your PR follows the [External Contribution Guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md).
 * Please make sure the PR has excellent documentation and tests. If we label it `missing documentation` or `missing tests` then it needs fixing!
-* Include the link to your `RFC` or `bug` issue in the description.
+* Add the link to your `RFC` or `bug` issue below.
 * If the issue does not already have approval from a developer, submit the PR as draft.
-* The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
-* For `feat/fix` PRs, the first paragraph starting with "This PR" must be present and will become a
-  changelog entry unless the PR is labeled with `no-changelog`. If the PR does not have this label,
-  it must instead be categorized with one of the `changelog-*` labels (which will be done by a
-  reviewer for external PRs).
-* A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line.
-* If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR.
-* You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
-* Remove this section, up to and including the `---` before submitting.
+* Remove this section before submitting.
 
----
+You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
 
-This PR <short changelog summary for feat/fix, see above>.
+# Summary
 
-Closes <`RFC` or `bug` issue number fixed by this PR, if any>
+Link to `RFC` or `bug` issue:

.github/dependabot.yml

@@ -1,8 +0,0 @@
-version: 2
-updates:
-  - package-ecosystem: "github-actions"
-    directory: "/"
-    schedule:
-      interval: "monthly"
-    commit-message:
-      prefix: "chore: CI"

.github/workflows/actionlint.yml

@@ -1,22 +0,0 @@
-name: Actionlint
-on:
-  push:
-    branches:
-      - 'master'
-    paths:
-      - '.github/**'
-  pull_request:
-    paths:
-      - '.github/**'
-  merge_group:
-
-jobs:
-  actionlint:
-    runs-on: ubuntu-latest
-    steps:
-    - name: Checkout
-      uses: actions/checkout@v4
-    - name: actionlint
-      uses: raven-actions/actionlint@v2
-      with:
-        pyflakes: false # we do not use python scripts

.github/workflows/changelog.yml

@@ -0,0 +1,33 @@
+name: add PR to changelog
+
+on:
+  # needs read/write GH token, do *not* execute arbitrary code from PR
+  pull_request_target:
+    types: [closed]
+
+jobs:
+  update-changelog:
+    if: |
+      github.event.pull_request.merged == true &&
+      contains(github.event.pull_request.labels.*.name, 'changelog') &&
+      github.base_ref == 'master'
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          # needs sufficiently elevated token to override branch protection rules
+          token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
+      - name: Update changelog
+        run: |
+          set -euxo pipefail
+          escaped_link=$(sed -e 's/[\/&]/\\&/g' <<'EOF'
+          [${{ github.event.pull_request.title}}](${{ github.event.pull_request.html_url }})
+          EOF
+          )
+          # insert link below first dashes line (https://stackoverflow.com/a/9453461/161659)
+          sed -i "0,/^---*/s/^---*/\0\n\n* $escaped_link./" RELEASES.md
+          # commit as github-actions bot (https://github.com/orgs/community/discussions/26560#discussioncomment-3252339)
+          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
+          git config user.name "github-actions[bot]"
+          git commit -i RELEASES.md -m "doc: update changelog"
+          git push

.github/workflows/check-prelude.yml

@@ -1,29 +0,0 @@
-name: Check for modules that should use `prelude`
-
-on: [pull_request]
-
-jobs:
-  check-prelude:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v4
-        with:
-          # the default is to use a virtual merge commit between the PR and master: just use the PR
-          ref: ${{ github.event.pull_request.head.sha }}
-          sparse-checkout: |
-            src/Lean
-            src/Std
-            src/lake/Lake
-      - name: Check Prelude
-        run: |
-          failed_files=""
-          while IFS= read -r -d '' file; do
-            if ! grep -q "^prelude$" "$file"; then
-              failed_files="$failed_files$file\n"
-            fi
-          done < <(find src/Lean src/Std src/lake/Lake -name '*.lean' -print0)
-          if [ -n "$failed_files" ]; then
-            echo -e "The following files should use 'prelude':\n$failed_files"
-            exit 1
-          fi

.github/workflows/check-stage0.yml

@@ -1,57 +0,0 @@
-name: Check for stage0 changes
-
-on:
-  merge_group:
-  pull_request:
-
-jobs:
-  check-stage0-on-queue:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v4
-      with:
-        ref: ${{ github.event.pull_request.head.sha }}
-        filter: blob:none
-        fetch-depth: 0
-
-    - name: Find base commit
-      if: github.event_name == 'pull_request'
-      run: echo "BASE=$(git merge-base origin/${{ github.base_ref }} HEAD)" >> "$GITHUB_ENV"
-
-    - name: Identify stage0 changes
-      run: |
-        git diff "${BASE:-HEAD^}..HEAD" --name-only -- stage0 |
-          grep -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in' \
-          > "$RUNNER_TEMP/stage0" || true
-        if test -s "$RUNNER_TEMP/stage0"
-        then
-          echo "CHANGES=yes" >> "$GITHUB_ENV"
-        else
-          echo "CHANGES=no" >> "$GITHUB_ENV"
-        fi
-      shell: bash
-
-    - if: github.event_name == 'pull_request'
-      name: Set label
-      uses: actions/github-script@v7
-      with:
-        script: |
-          const { owner, repo, number: issue_number  } = context.issue;
-          if (process.env.CHANGES == 'yes') {
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['changes-stage0'] }).catch(() => {});
-          } else {
-            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'changes-stage0' }).catch(() => {});
-          }
-
-    - if: env.CHANGES == 'yes'
-      name: Report changes
-      run: |
-        echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY"
-        # shellcheck disable=SC2129
-        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
-        cat  "$RUNNER_TEMP/stage0"  >> "$GITHUB_STEP_SUMMARY"
-        echo '```'                  >> "$GITHUB_STEP_SUMMARY"
-
-    - if: github.event_name == 'merge_group' && env.CHANGES == 'yes'
-      name: Fail when on the merge queue
-      run: exit 1

.github/workflows/ci.yml

@@ -9,17 +9,6 @@ on:
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
-  # for manual re-release of a nightly
-  workflow_dispatch:
-    inputs:
-      action:
-        description: 'Action'
-        required: true
-        default: 'release nightly'
-        type: choice
-        options:
-        - release nightly
-
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}-${{ github.event_name }}
@@ -31,10 +20,8 @@ jobs:
   configure:
     runs-on: ubuntu-latest
     outputs:
-      # 0: PRs without special label
-      # 1: PRs with `merge-ci` label, merge queue checks, master commits
-      # 2: PRs with `release-ci` label, releases (incl. nightlies)
-      check-level: ${{ steps.set-level.outputs.check-level }}
+      # Should we run only a quick CI? Yes on a pull request without the full-ci label
+      quick: ${{ steps.set-quick.outputs.quick }}
       # 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
@@ -51,12 +38,161 @@ jobs:
       RELEASE_TAG: ${{ steps.set-release.outputs.RELEASE_TAG }}
 
     steps:
+      - name: Run quick CI?
+        id: set-quick
+        env:
+          quick: ${{
+            github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
+           }}
+        run: |
+          echo "quick=${{env.quick}}" >> $GITHUB_OUTPUT
+
+      - 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}`)
+            let matrix = [
+              {
+                // portable release build: use channel with older glibc (2.27)
+                "name": "Linux LLVM",
+                "os": "ubuntu-latest",
+                "release": false,
+                "quick": false,
+                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"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-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"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'"
+              },
+              {
+                "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-latest",
+                "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-latest",
+                "release": true,
+                "quick": false,
+                "cross": true,
+                "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": "EXTRA_FLAGS=--target=aarch64-apple-darwin ../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,
+                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{ localSystem.config = \\\"aarch64-unknown-linux-gnu\\\"; }}\" --run \"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": "EXTRA_FLAGS=--target=aarch64-unknown-linux-gnu ../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@v4
+        uses: actions/checkout@v3
         # don't schedule nightlies on forks
-        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
       - name: Set Nightly
-        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
         id: set-nightly
         run: |
           if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
@@ -64,8 +200,8 @@ jobs:
             git fetch nightly --tags
             LEAN_VERSION_STRING="nightly-$(date -u +%F)"
             # do nothing if commit already has a different tag
-            if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
-              echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
+            if [[ $(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo $LEAN_VERSION_STRING) == $LEAN_VERSION_STRING ]]; then
+              echo "nightly=$LEAN_VERSION_STRING" >> $GITHUB_OUTPUT
             fi
           fi
 
@@ -73,7 +209,7 @@ jobs:
         if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4'
         id: set-release
         run: |
-          TAG_NAME="${GITHUB_REF##*/}"
+          TAG_NAME=${GITHUB_REF##*/}
 
           # From https://github.com/fsaintjacques/semver-tool/blob/master/src/semver
 
@@ -90,179 +226,15 @@ jobs:
 
           if [[ ${TAG_NAME} =~ ${SEMVER_REGEX} ]]; then
             echo "Tag ${TAG_NAME} matches SemVer regex, with groups ${BASH_REMATCH[1]} ${BASH_REMATCH[2]} ${BASH_REMATCH[3]} ${BASH_REMATCH[4]}"
-            {
-              echo "LEAN_VERSION_MAJOR=${BASH_REMATCH[1]}"
-              echo "LEAN_VERSION_MINOR=${BASH_REMATCH[2]}"
-              echo "LEAN_VERSION_PATCH=${BASH_REMATCH[3]}"
-              echo "LEAN_SPECIAL_VERSION_DESC=${BASH_REMATCH[4]##-}"
-              echo "RELEASE_TAG=$TAG_NAME"
-            } >> "$GITHUB_OUTPUT"
+            echo "LEAN_VERSION_MAJOR=${BASH_REMATCH[1]}" >> $GITHUB_OUTPUT
+            echo "LEAN_VERSION_MINOR=${BASH_REMATCH[2]}" >> $GITHUB_OUTPUT
+            echo "LEAN_VERSION_PATCH=${BASH_REMATCH[3]}" >> $GITHUB_OUTPUT
+            echo "LEAN_SPECIAL_VERSION_DESC=${BASH_REMATCH[4]##-}" >> $GITHUB_OUTPUT
+            echo "RELEASE_TAG=$TAG_NAME" >> $GITHUB_OUTPUT
           else
             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 where available (original repo)
-            let large = ${{ github.repository == 'leanprover/lean4' }};
-            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": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "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": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "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|bv_bitblast_stress'"
-              },
-              // TODO: suddenly started failing in CI
-              /*{
-                "name": "Linux fsanitize",
-                "os": "ubuntu-latest",
-                "check-level": 2,
-                // turn off custom allocator & symbolic functions to make LSAN do its magic
-                "CMAKE_PRESET": "sanitize",
-                // exclude seriously slow/problematic tests (laketests crash)
-                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
-              },*/
-              {
-                "name": "macOS",
-                "os": "macos-13",
-                "release": true,
-                "check-level": 2,
-                "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
-                "binary-check": "otool -L",
-                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
-              },
-              {
-                "name": "macOS aarch64",
-                "os": "macos-14",
-                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
-                "release": true,
-                "check-level": 0,
-                "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\"",
-                // 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": "nscloud-ubuntu-22.04-arm64-4x8",
-                "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
-                "release": true,
-                "check-level": 2,
-                "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
-                "llvm-url": "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*"
-              },
-              {
-                "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 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
-                "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 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
-                "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|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.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'
@@ -274,7 +246,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
+        shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }}
     name: ${{ matrix.name }}
     env:
       # must be inside workspace
@@ -289,76 +261,65 @@ jobs:
       CXX: c++
       MACOSX_DEPLOYMENT_TARGET: 10.15
     steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: true
+          # the default is to use a virtual merge commit between the PR and master: just use the PR
+          ref: ${{ github.event.pull_request.head.sha }}
       - name: Install Nix
-        uses: DeterminateSystems/nix-installer-action@main
-        if: runner.os == 'Linux' && !matrix.cmultilib
+        uses: cachix/install-nix-action@v18
+        with:
+          install_url: https://releases.nixos.org/nix/nix-2.12.0/install
+        if: matrix.os == 'ubuntu-latest' && !matrix.cmultilib
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
           msystem: clang64
-          # `:` means do not prefix with msystem
-          pacboy: "make: python: cmake clang ccache gmp libuv git: zip: unzip: diffutils: binutils: tree: zstd tar:"
-        if: runner.os == 'Windows'
+          # `:p` means prefix with appropriate msystem prefix
+          pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
+        if: matrix.os == 'windows-2022'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd coreutils gmp libuv
-        if: runner.os == 'macOS'
-      - name: Checkout
-        uses: actions/checkout@v4
-        with:
-          # the default is to use a virtual merge commit between the PR and master: just use the PR
-          ref: ${{ github.event.pull_request.head.sha }}
-      # Do check out some CI-relevant files from virtual merge commit to accommodate CI changes on
-      # master (as the workflow files themselves are always taken from the merge)
-      # (needs to be after "Install *" to use the right shell)
-      - name: CI Merge Checkout
-        run: |
-          git fetch --depth=1 origin ${{ github.sha }}
-          git checkout FETCH_HEAD flake.nix flake.lock
-        if: github.event_name == 'pull_request'
-      # (needs to be after "Checkout" so files don't get overridden)
+          brew install ccache tree zstd coreutils gmp
+        if: matrix.os == 'macos-latest'
       - name: Setup emsdk
-        uses: mymindstorm/setup-emsdk@v14
+        uses: mymindstorm/setup-emsdk@v12
         with:
           version: 3.1.44
           actions-cache-folder: emsdk
         if: matrix.wasm
       - name: Install 32bit c libs
         run: |
-          sudo dpkg --add-architecture i386
           sudo apt-get update
-          sudo apt-get install -y gcc-multilib g++-multilib ccache libuv1-dev:i386
+          sudo apt-get install -y gcc-multilib g++-multilib ccache
         if: matrix.cmultilib
       - name: Cache
-        uses: actions/cache@v4
+        uses: actions/cache@v3
         with:
           path: .ccache
-          key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-build-v3
-          save-always: true
-      # open nix-shell once for initial setup
       - name: Setup
         run: |
-          ccache --zero-stats
-        if: runner.os == 'Linux'
-      - name: Set up NPROC
+          # open nix-shell once for initial setup
+          true
+        if: matrix.os == 'ubuntu-latest'
+      - name: Set up core dumps
         run: |
-          echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
+          mkdir -p $PWD/coredumps
+          # store in current directory, for easy uploading together with binary
+          echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
+        if: matrix.os == 'ubuntu-latest'
       - name: Build
         run: |
           mkdir build
           cd build
-          # arguments passed to `cmake`
+          ulimit -c unlimited # coredumps
           # this also enables githash embedding into stage 1 library
           OPTIONS=(-DCHECK_OLEAN_VERSION=ON)
-          OPTIONS+=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
-          if [[ -n '${{ matrix.cross_target }}' ]]; then
-            # used by `prepare-llvm`
-            export EXTRA_FLAGS=--target=${{ matrix.cross_target }}
-            OPTIONS+=(-DLEAN_PLATFORM_TARGET=${{ matrix.cross_target }})
-          fi
           if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
             wget -q ${{ matrix.llvm-url }}
             PREPARE="$(${{ matrix.prepare-llvm }})"
@@ -375,19 +336,11 @@ jobs:
             OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }})
           fi
           # contortion to support empty OPTIONS with old macOS bash
-          cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-          time make -j$NPROC
-      - name: Install
-        run: |
-          make -C build install
+          cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
+          make -j4
+          make install
       - name: Check Binaries
         run: ${{ matrix.binary-check }} lean-*/bin/* || true
-      - name: Count binary symbols
-        run: |
-          for f in lean-*/bin/*; do
-            echo "$f: $(nm $f | grep " T " | wc -l) exported symbols"
-          done
-        if: matrix.name == 'Windows'
       - name: List Install Tree
         run: |
           # omit contents of Init/, ...
@@ -403,7 +356,7 @@ jobs:
           else
             ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
           fi
-      - uses: actions/upload-artifact@v4
+      - uses: actions/upload-artifact@v3
         if: matrix.release
         with:
           name: build-${{ matrix.name }}
@@ -413,72 +366,78 @@ jobs:
           build/stage1/bin/lean --stats src/Lean.lean
         if: ${{ !matrix.cross }}
       - name: Test
-        id: test
         run: |
-          time 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() && steps.test.conclusion != 'skipped'
+          cd build/stage1
+          ulimit -c unlimited # coredumps
+          # exclude nonreproducible test
+          ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
+        if: (matrix.wasm || !matrix.cross) && !needs.configure.outputs.quick
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
-        if: (!matrix.cross) && steps.test.conclusion != 'skipped'
+        if: ${{ !matrix.cross && !needs.configure.outputs.quick }}
       - name: Build Stage 2
         run: |
-          make -C build -j$NPROC stage2
+          cd build
+          ulimit -c unlimited # coredumps
+          make -j4 stage2
         if: matrix.test-speedcenter
       - name: Check Stage 3
         run: |
-          make -C build -j$NPROC check-stage3
+          cd build
+          ulimit -c unlimited # coredumps
+          make -j4 check-stage3
         if: matrix.test-speedcenter
       - name: Test Speedcenter Benchmarks
         run: |
-          # Necessary for some timing metrics but does not work on Namespace runners
-          # and we just want to test that the benchmarks run at all here
-          #echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
+          echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
           export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
           cd tests/bench
           nix shell .#temci -c temci exec --config speedcenter.yaml --included_blocks fast --runs 1
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
-          # clean rebuild in case of Makefile changes
-          make -C build update-stage0 && rm -rf build/stage* && make -C build -j$NPROC
-        if: matrix.name == 'Linux' && needs.configure.outputs.check-level >= 1
+          cd build
+          ulimit -c unlimited # coredumps
+          make update-stage0 && make -j4
+        if: matrix.name == 'Linux' && !needs.configure.outputs.quick
       - name: CCache stats
         run: ccache -s
+      - name: Show stacktrace for coredumps
+        if: ${{ failure() }} && matrix.os == 'ubuntu-latest'
+        run: |
+          for c in coredumps/*; do
+            progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
+            echo bt | $GDB/bin/gdb -q $progbin $c || true
+          done
+      - name: Upload coredumps
+        uses: actions/upload-artifact@v3
+        if: ${{ failure() }} && matrix.os == 'ubuntu-latest'
+        with:
+          name: coredumps-${{ matrix.name }}
+          path: |
+            ./coredumps
+            ./build/stage0/bin/lean
+            ./build/stage0/lib/lean/libleanshared.so
+            ./build/stage1/bin/lean
+            ./build/stage1/lib/lean/libleanshared.so
+            ./build/stage2/bin/lean
+            ./build/stage2/lib/lean/libleanshared.so
 
   # This job collects results from all the matrix jobs
-  # This can be made the "required" job, instead of listing each
+  # This can be made the “required” job, instead of listing each
   # matrix job separately
   all-done:
     name: Build matrix complete
     runs-on: ubuntu-latest
     needs: build
-    # mark as merely cancelled not failed if builds are cancelled
-    if: ${{ !cancelled() }}
+    if: ${{ always() }}
     steps:
-    - if: ${{ contains(needs.*.result, 'failure') && github.repository == 'leanprover/lean4' && github.ref_name == 'master' }}
-      uses: zulip/github-actions-zulip/send-message@v1
-      with:
-        api-key: ${{ secrets.ZULIP_BOT_KEY }}
-        email: "github-actions-bot@lean-fro.zulipchat.com"
-        organization-url: "https://lean-fro.zulipchat.com"
-        to: "infrastructure"
-        topic: "Github actions"
-        type: "stream"
-        content: |
-          A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
-    - if: contains(needs.*.result, 'failure')
+    - if: contains(needs.*.result, 'failure') ||  contains(needs.*.result, 'cancelled')
       uses: actions/github-script@v7
       with:
         script: |
             core.setFailed('Some jobs failed')
 
-
   # This job creates releases from tags
   # (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.)
   # We do not attempt to automatically construct a changelog here:
@@ -488,22 +447,16 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v4
+      - uses: actions/download-artifact@v3
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@v2
+        uses: softprops/action-gh-release@v1
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
-          prerelease: ${{ !startsWith(github.ref, 'refs/tags/v') || contains(github.ref, '-rc') }}
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      - name: Update release.lean-lang.org
-        run: |
-          gh workflow -R leanprover/release-index run update-index.yml
-        env:
-          GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
 
   # This job creates nightly releases during the cron job.
   # It is responsible for creating the tag, and automatically generating a changelog.
@@ -513,30 +466,30 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: actions/checkout@v3
         with:
           # needed for tagging
           fetch-depth: 0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v4
+      - uses: actions/download-artifact@v3
         with:
           path: artifacts
       - name: Prepare Nightly Release
         run: |
           git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
           git fetch nightly --tags
-          git tag "${{ needs.configure.outputs.nightly }}"
-          git push nightly "${{ needs.configure.outputs.nightly }}"
+          git tag ${{ needs.configure.outputs.nightly }}
+          git push nightly ${{ needs.configure.outputs.nightly }}
           git push -f origin refs/tags/${{ needs.configure.outputs.nightly }}:refs/heads/nightly
-          last_tag="$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[-0-9]*" | head -n 1)"
+          last_tag=$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[-0-9]*" | head -n 1)
           echo -e "*Changes since ${last_tag}:*\n\n" > diff.md
-          git show "$last_tag":RELEASES.md > old.md
+          git show $last_tag:RELEASES.md > old.md
           #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
           diff --changed-group-format='%>' --unchanged-group-format='' old.md RELEASES.md >> diff.md || true
           echo -e "\n*Full commit log*\n" >> diff.md
-          git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
+          git log --oneline $last_tag..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@v2
+        uses: softprops/action-gh-release@v1
         with:
           body_path: diff.md
           prerelease: true
@@ -546,13 +499,3 @@ jobs:
           repository: ${{ github.repository_owner }}/lean4-nightly
         env:
           GITHUB_TOKEN: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - name: Update release.lean-lang.org
-        run: |
-          gh workflow -R leanprover/release-index run update-index.yml
-        env:
-          GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
-      - name: Update toolchain on mathlib4's nightly-testing branch
-        run: |
-          gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
-        env:
-          GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

.github/workflows/copyright-header.yml

@@ -1,20 +0,0 @@
-name: Check for copyright header
-
-on: [pull_request]
-
-jobs:
-  check-lean-files:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v4
-
-    - name: Verify .lean files start with a copyright header.
-      run: |
-        FILES=$(find ./src -type d \( -path "./src/lake/examples" -o -path "./src/lake/tests" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
-        if [ -n "$FILES" ]; then
-          echo "Found .lean files which do not have a copyright header:"
-          echo "$FILES"
-          exit 1
-        else
-          echo "All copyright headers present."
-        fi

.github/workflows/jira.yml

@@ -1,34 +0,0 @@
-name: Jira sync
-
-on:
-  issues:
-    types: [closed]
-
-jobs:
-  jira-sync:
-    runs-on: ubuntu-latest
-
-    steps:
-      - name: Move Jira issue to Done
-        env:
-          JIRA_API_TOKEN: ${{ secrets.JIRA_API_TOKEN }}
-          JIRA_USERNAME: ${{ secrets.JIRA_USERNAME }}
-          JIRA_BASE_URL: ${{ secrets.JIRA_BASE_URL }}
-        run: |
-          issue_number=${{ github.event.issue.number }}
-
-          jira_issue_key=$(curl -s -u "${JIRA_USERNAME}:${JIRA_API_TOKEN}" \
-            -X GET -H "Content-Type: application/json" \
-            "${JIRA_BASE_URL}/rest/api/2/search?jql=summary~\"${issue_number}\"" | \
-            jq -r '.issues[0].key')
-
-          if [ -z "$jira_issue_key" ]; then
-            exit
-          fi
-
-          curl -s -u "${JIRA_USERNAME}:${JIRA_API_TOKEN}" \
-            -X POST -H "Content-Type: application/json" \
-            --data "{\"transition\": {\"id\": \"41\"}}" \
-            "${JIRA_BASE_URL}/rest/api/2/issue/${jira_issue_key}/transitions"
-
-          echo "Moved Jira issue ${jira_issue_key} to Done"

.github/workflows/labels-from-comments.yml

@@ -1,8 +1,6 @@
-# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
-# `release-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
-# If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
-# from that set are removed automatically at the same time.
-# Similarly, if any `changelog-XXX` label is added, other `changelog-YYY` labels are removed.
+# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, or `WIP` labels,
+# by commenting on the PR or issue.
+# Other labels from this set are removed automatically at the same time.
 
 name: Label PR based on Comment
 
@@ -12,7 +10,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'changelog-'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP'))
     runs-on: ubuntu-latest
 
     steps:
@@ -21,14 +19,12 @@ jobs:
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |
-          const { owner, repo, number: issue_number } = context.issue;
+          const { owner, repo, number: issue_number  } = context.issue;
           const commentLines = context.payload.comment.body.split('\r\n');
 
           const awaitingReview = commentLines.includes('awaiting-review');
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
-          const releaseCI = commentLines.includes('release-ci');
-          const changelogMatch = commentLines.find(line => line.startsWith('changelog-'));
 
           if (awaitingReview || awaitingAuthor || wip) {
             await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
@@ -45,23 +41,3 @@ jobs:
           if (wip) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['WIP'] });
           }
-
-          if (releaseCI) {
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
-          }
-
-          if (changelogMatch) {
-            const changelogLabel = changelogMatch.trim();
-            const { data: existingLabels } = await github.rest.issues.listLabelsOnIssue({ owner, repo, issue_number });
-            const changelogLabels = existingLabels.filter(label => label.name.startsWith('changelog-'));
-
-            // Remove all other changelog labels
-            for (const label of changelogLabels) {
-              if (label.name !== changelogLabel) {
-                await github.rest.issues.removeLabel({ owner, repo, issue_number, name: label.name }).catch(() => {});
-              }
-            }
-
-            // Add the new changelog label
-            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: [changelogLabel] });
-          }

.github/workflows/nix-ci.yml

@@ -13,130 +13,101 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  # see ci.yml
-  configure:
-    runs-on: ubuntu-latest
-    outputs:
-      matrix: ${{ steps.set-matrix.outputs.result }}
-    steps:
-      - name: Configure build matrix
-        id: set-matrix
-        uses: actions/github-script@v7
-        with:
-          script: |
-            let large = ${{ github.repository == 'leanprover/lean4' }};
-            let matrix = [
-              {
-                "name": "Nix Linux",
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x8" : "ubuntu-latest",
-              }
-            ];
-            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            return matrix;
-
   Build:
-    needs: [configure]
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        shell: nix run .#ciShell -- bash -euxo pipefail {0}
+        shell: nix -v --experimental-features "nix-command flakes" run .#ciShell -- bash -euxo pipefail {0}
     strategy:
       matrix:
-        include: ${{fromJson(needs.configure.outputs.matrix)}}
+        include:
+          - name: Nix Linux
+            os: ubuntu-latest
+          #- name: Nix macOS
+          #  os: macos-latest
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}
     env:
-      NIX_BUILD_ARGS: --print-build-logs --fallback
+      NIX_BUILD_ARGS: -v --print-build-logs --fallback
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: actions/checkout@v3
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
+      - name: Install Nix
+        uses: cachix/install-nix-action@v18
+        with:
+          # https://github.com/NixOS/nix/issues/6572
+          install_url: https://releases.nixos.org/nix/nix-2.7.0/install
+          extra_nix_config: |
+            extra-sandbox-paths = /nix/var/cache/ccache
+            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org
       - name: Set Up Nix Cache
-        uses: actions/cache@v4
+        uses: actions/cache@v3
         with:
           path: nix-store-cache
           key: ${{ matrix.name }}-nix-store-cache-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-nix-store-cache
-          save-always: true
       - name: Further Set Up Nix Cache
         shell: bash -euxo pipefail {0}
         run: |
           # Nix seems to mutate the cache, so make a copy
           cp -r nix-store-cache nix-store-cache-copy || true
-      - name: Install Nix
-        uses: DeterminateSystems/nix-installer-action@main
-        with:
-          extra-conf: |
-            extra-sandbox-paths = /nix/var/cache/ccache?
-            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
       - name: Prepare CCache Cache
+        shell: bash -euxo pipefail {0}
         run: |
           sudo mkdir -m0770 -p /nix/var/cache/ccache
           sudo chown -R $USER /nix/var/cache/ccache
       - name: Setup CCache Cache
-        uses: actions/cache@v4
+        uses: actions/cache@v3
         with:
           path: /nix/var/cache/ccache
           key: ${{ matrix.name }}-nix-ccache-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-nix-ccache
-          save-always: true
       - name: Further Set Up CCache Cache
+        shell: bash -euxo pipefail {0}
         run: |
           sudo chown -R root:nixbld /nix/var/cache
           sudo chmod -R 770 /nix/var/cache
+      - name: Install Cachix
+        uses: cachix/cachix-action@v12
+        with:
+          name: lean4
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+          skipPush: true  # we push specific outputs only
       - name: Build
         run: |
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build --keep-failed $NIX_BUILD_ARGS .#test -o push-test || (ln -s /tmp/nix-build-*/build/source/src/build ./push-test; false)
-      - name: Test Summary
-        uses: test-summary/action@v2
-        with:
-          paths: push-test/test-results.xml
-        if: always()
-        continue-on-error: true
+          nix build $NIX_BUILD_ARGS .#test -o push-test
       - name: Build manual
         run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
-          # https://github.com/netlify/cli/issues/1809
-          cp -r --dereference ./result ./dist
         if: matrix.name == 'Nix Linux'
+      - name: Push to Cachix
+        run: |
+          [ -z "${{ secrets.CACHIX_AUTH_TOKEN }}" ] || cachix push -j4 lean4 ./push-* || true
       - name: Rebuild Nix Store Cache
         run: |
           rm -rf nix-store-cache || true
           nix copy ./push-* --to file://$PWD/nix-store-cache?compression=none
-      - id: deploy-info
-        name: Compute Deployment Metadata
-        run: |
-          set -e
-          python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
-          echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
-      - name: Publish manual to Netlify
-        uses: nwtgck/actions-netlify@v3.0
-        id: publish-manual
+      - name: Publish manual
+        uses: peaceiris/actions-gh-pages@v3
         with:
-          publish-dir: ./dist
-          production-branch: master
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          deploy-message: |
-            ${{ github.event_name == 'pull_request' && format('pr#{0}: {1}', github.event.number, github.event.pull_request.title) || format('ref/{0}: {1}', github.ref_name, steps.deploy-info.outputs.message) }}
-          alias: ${{ steps.deploy-info.outputs.alias }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          github-deployment-environment: "lean-lang.org/lean4/doc"
-          fails-without-credentials: false
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "b8e805d2-7e9b-4f80-91fb-a84d72fc4a68"
+          github_token: ${{ secrets.GITHUB_TOKEN }}
+          publish_dir: ./result
+          destination_dir: ./doc
+        if: matrix.name == 'Nix Linux' && github.ref == 'refs/heads/master' && github.event_name == 'push'
       - name: Fixup CCache Cache
         run: |
           sudo chown -R $USER /nix/var/cache
+      - name: CCache stats
+        run: CCACHE_DIR=/nix/var/cache/ccache nix run .#nixpkgs.ccache -- -s

.github/workflows/pr-body.yml

@@ -1,25 +0,0 @@
-name: Check PR body for changelog convention
-
-on:
-  merge_group:
-  pull_request:
-    types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
-
-jobs:
-  check-pr-body:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check PR body
-        if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
-        with:
-          script: |
-            const { title, body, labels, draft } = context.payload.pull_request;
-            if (!draft && /^(feat|fix):/.test(title) && !labels.some(label => label.name == "changelog-no")) {
-              if (!labels.some(label => label.name.startsWith("changelog-"))) {
-                core.setFailed('feat/fix PR must have a `changelog-*` label');
-              }
-              if (!/^This PR [^<]/.test(body)) {
-                core.setFailed('feat/fix PR must have changelog summary starting with "This PR ..." as first line.');
-              }
-            }

.github/workflows/pr-release.yml

@@ -6,10 +6,6 @@
 # Instead we use `workflow_run`, which essentially allows us to escalate privileges
 # (but only runs the CI as described in the `master` branch, not in the PR branch).
 
-# The main specification/documentation for this workflow is at
-# https://leanprover-community.github.io/contribute/tags_and_branches.html
-# Keep that in sync!
-
 name: PR release
 
 on:
@@ -20,47 +16,50 @@ on:
 jobs:
   on-success:
     runs-on: ubuntu-latest
-    if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
+    if: github.event.workflow_run.conclusion == 'success' && github.repository == 'leanprover/lean4'
     steps:
       - name: Retrieve information about the original workflow
         uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
-        # This action is deprecated and archived, but it seems hard to find a better solution for getting the PR number
-        # see https://github.com/orgs/community/discussions/25220 for some discussion
         id: workflow-info
         with:
           token: ${{ secrets.GITHUB_TOKEN }}
           sourceRunId: ${{ github.event.workflow_run.id }}
+      - name: Checkout
+        # Only proceed if the previous workflow had a pull request number.
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: actions/checkout@v3
+        with:
+          token: ${{ secrets.PR_RELEASES_TOKEN }}
+          # Since `workflow_run` runs on master, we need to specify which commit to check out,
+          # so that we tag the PR.
+          # It's important that we use `sourceHeadSha` here, not `targetCommitSha`
+          # as we *don't* want the synthetic merge with master.
+          ref: ${{ steps.workflow-info.outputs.sourceHeadSha }}
+          # We need a full checkout, so that we can push the PR commits to the `lean4-pr-releases` repo.
+          fetch-depth: 0
 
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v7 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v2 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
           name: build-.*
           name_is_regexp: true
-
-      - name: Push tag
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          git init --bare lean4.git
-          git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
-          git -C lean4.git fetch -n origin master
-          git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-          git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-          git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
-          git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
-      - name: Delete existing release if present
+      - name: Prepare release
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
+          git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           # Try to delete any existing release for the current PR.
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
+          git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+          git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@v2
+        uses: softprops/action-gh-release@v1
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -73,103 +72,66 @@ jobs:
           # The token used here must have `workflow` privileges.
           GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
-      - name: Report release status
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v7
-        with:
-          script: |
-            await github.rest.repos.createCommitStatus({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
-              state: "success",
-              context: "PR toolchain",
-              description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}",
-            });
-
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v7
+        uses: actions-ecosystem/action-add-labels@v1
         with:
-          script: |
-            await github.rest.issues.addLabels({
-              issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }},
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              labels: ['toolchain-available']
-            })
+          number: ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          labels: toolchain-available
 
       # Next, determine the most recent nightly release in this PR's history.
-      - name: Find most recent nightly in feature branch
+      - name: Find most recent nightly
         id: most-recent-nightly-tag
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
-          git -C lean4.git remote add nightly https://github.com/leanprover/lean4-nightly.git
-          git -C lean4.git fetch nightly '+refs/tags/nightly-*:refs/tags/nightly-*'
-          git -C lean4.git tag --merged "${{ steps.workflow-info.outputs.sourceHeadSha }}" --list "nightly-*" \
-            | sort -rV | head -n 1 | sed "s/^nightly-*/MOST_RECENT_NIGHTLY=/" | tee -a "$GITHUB_ENV"
+          echo "MOST_RECENT_NIGHTLY=$(script/most-recent-nightly-tag.sh)" >> $GITHUB_ENV
 
       - name: 'Setup jq'
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: dcarbone/install-jq-action@v3.0.1
+        uses: dcarbone/install-jq-action@v1.0.1
 
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: ready
         run: |
-          echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY"
-          NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}")
-          echo "SHA of most recent nightly release: $NIGHTLY_SHA"
-          MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
+          echo "Most recent nightly: $MOST_RECENT_NIGHTLY"
+          NIGHTLY_SHA=$(git rev-parse nightly-$MOST_RECENT_NIGHTLY^{commit})
+          echo "SHA of most recent nightly: $NIGHTLY_SHA"
+          MERGE_BASE_SHA=$(git merge-base origin/master HEAD)
           echo "SHA of merge-base: $MERGE_BASE_SHA"
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
-            echo "The merge base of this PR coincides with the nightly release"
+            echo "Most recent nightly tag agrees with the merge base."
 
-            BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
-            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+            REMOTE_BRANCHES=$(git ls-remote -h https://github.com/leanprover-community/mathlib4.git nightly-testing-$MOST_RECENT_NIGHTLY)
 
-            if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
-              echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+            if [[ -n "$REMOTE_BRANCHES" ]]; then
+              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
               MESSAGE=""
-
-              if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
-                echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              else
-                echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-                MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
-              fi
             else
-              echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
+              echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
+              MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-$MOST_RECENT_NIGHTLY' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow."
             fi
 
           else
             echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
-            git -C lean4.git log -10 origin/master
+            git log -10
 
-            git -C lean4.git fetch origin nightly-with-mathlib
-            NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
-            MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
+            MESSAGE="- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch."
           fi
 
           if [[ -n "$MESSAGE" ]]; then
 
             echo "Checking existing messages"
 
-            # The code for updating comments is duplicated in mathlib's
-            # scripts/lean-pr-testing-comments.sh
-            # so keep in sync
-
             # Use GitHub API to check if a comment already exists
-            existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+            existing_comment=$(curl -L -s -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
                                     -H "Accept: application/vnd.github.v3+json" \
                                     "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-bot"))')"
-            existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
-            existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
+                                    | jq '.[] | select(.body | startswith("- ❗ Mathlib") or startswith("- ✅ Mathlib") or startswith("- ❌ Mathlib") or startswith("- 💥 Mathlib") or startswith("- 🟡 Mathlib"))')
+            existing_comment_id=$(echo "$existing_comment" | jq -r .id)
+            existing_comment_body=$(echo "$existing_comment" | jq -r .body)
 
             if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then
               MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))"
@@ -177,23 +139,22 @@ jobs:
               echo "Posting message to the comments: $MESSAGE"
 
               # Append new result to the existing comment or post a new comment
-              # It's essential we use the MATHLIB4_COMMENT_BOT token here, so that Mathlib CI can subsequently edit the comment.
+              # It's essential we use the MATHLIB4_BOT token here, so that Mathlib CI can subsequently edit the comment.
               if [ -z "$existing_comment_id" ]; then
-                INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
                 # Post new comment with a bullet point
                 echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X POST \
-                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
-                  -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
+                  -d "$(jq --null-input --arg val "$MESSAGE" '{"body": $val}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
               else
                 # Append new result to the existing comment
                 echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X PATCH \
-                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
@@ -201,146 +162,60 @@ jobs:
             else
               echo "The message already exists in the comment body."
             fi
-            echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
+            echo "::set-output name=mathlib_ready::false"
           else
-            echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
+            echo "::set-output name=mathlib_ready::true"
           fi
 
-      - name: Report mathlib base
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
-        uses: actions/github-script@v7
-        with:
-          script: |
-            const description =
-              process.env.MOST_RECENT_NIGHTLY ?
-              "nightly-" + process.env.MOST_RECENT_NIGHTLY :
-              "not branched off nightly";
-            await github.rest.repos.createCommitStatus({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
-              state: "success",
-              context: "PR branched off:",
-              description: description,
-            });
-
-      # We next automatically create a Batteries branch using this toolchain.
-      # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
-      # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
-      - name: Cleanup workspace
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        run: |
-          sudo rm -rf ./*
-
-      # Checkout the Batteries repository with all branches
-      - name: Checkout Batteries repository
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v4
-        with:
-          repository: leanprover-community/batteries
-          token: ${{ secrets.MATHLIB4_BOT }}
-          ref: nightly-testing
-          fetch-depth: 0 # This ensures we check out all tags and branches.
-
-      - name: Check if tag exists
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_batteries_tag
-        run: |
-          git config user.name "leanprover-community-mathlib4-bot"
-          git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
-
-          if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
-            BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
-          else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
-            BASE=nightly-testing
-          fi
-
-          echo "Using base branch: $BASE"
-
-          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
-          echo "Branch exists: $EXISTS"
-          if [ "$EXISTS" = "0" ]; then
-            echo "Branch does not exist, creating it."
-            git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
-            git add lean-toolchain
-            git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          else
-            echo "Branch already exists, pushing an empty commit."
-            git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
-            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
-            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
-          fi
-
-      - name: Push changes
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        run: |
-          git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-
-
       # We next automatically create a Mathlib branch using this toolchain.
       # Mathlib CI will be responsible for reporting back success or failure
       # to the PR comments asynchronously.
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
-          sudo rm -rf ./*
+          sudo rm -rf *
 
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v4
+        uses: actions/checkout@v3
         with:
           repository: leanprover-community/mathlib4
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
 
-      - name: install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
-
-      - name: Check if tag exists
+      - name: Check if branch exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_mathlib_tag
+        id: check_branch
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
 
-          if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
-            BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
+          if git branch -r | grep -q "nightly-testing-${MOST_RECENT_NIGHTLY}"; then
+            BASE=nightly-testing-${MOST_RECENT_NIGHTLY}
           else
             echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
-          echo "Using base tag: $BASE"
+          echo "Using base branch: $BASE"
 
-          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
+          git checkout $BASE
+
+          EXISTS=$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)
           echo "Branch exists: $EXISTS"
           if [ "$EXISTS" = "0" ]; then
             echo "Branch does not exist, creating it."
-            git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
+            git checkout -b lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
             git add lean-toolchain
-            sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean
-            lake update batteries
-            git add lakefile.lean lake-manifest.json
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
-            echo "Branch already exists, merging $BASE and bumping Batteries."
-            git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The Mathlib `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
-            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
-            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            lake update batteries
-            git add lake-manifest.json
+            echo "Branch already exists, pushing an empty commit."
+            git checkout lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
+            # The Mathlib `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
+            git merge $BASE --strategy-option ours --no-commit --allow-unrelated-histories
             git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 

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

@@ -1,35 +0,0 @@
-name: Restart by label
-on:
-  pull_request_target:
-    types:
-      - unlabeled
-      - labeled
-jobs:
-  restart-on-label:
-    runs-on: ubuntu-latest
-    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
-        # (unfortunately cannot search by PR number, only base branch,
-        # and that is't even unique given PRs from forks, but the risk
-        # of confusion is low and the danger is mild)
-        echo "Trying to find a run with branch $head_ref and commit $head_sha"
-        run_id="$(gh run list -e pull_request -b "$head_ref" -c "$head_sha" \
-          --workflow 'CI' --limit 1 --json databaseId --jq '.[0].databaseId')"
-        echo "Run id: ${run_id}"
-        gh run view "$run_id"
-        echo "Cancelling (just in case)"
-        gh run cancel "$run_id" || echo "(failed)"
-        echo "Waiting for 30s"
-        sleep 30
-        gh run view "$run_id"
-        echo "Rerunning"
-        gh run rerun "$run_id"
-        gh run view "$run_id"
-      shell: bash
-      env:
-        head_ref: ${{ github.head_ref }}
-        head_sha: ${{ github.event.pull_request.head.sha }}
-        GH_TOKEN: ${{ github.token }}
-        GH_REPO: ${{ github.repository }}

.github/workflows/stale.yml

@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v9
+      - uses: actions/stale@v8
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

.github/workflows/update-stage0.yml

@@ -1,78 +0,0 @@
-name: Update stage0
-
-# This action will update stage0 on master as soon as
-# src/stdlib_flags.h and stage0/src/stdlib_flags.h
-# are out of sync there, or when manually triggered.
-# The update bypasses the merge queue to be quick.
-# Also see <doc/dev/bootstrap.md>.
-
-on:
-  push:
-    branches:
-      - 'master'
-  workflow_dispatch:
-
-concurrency:
-  group: stage0
-  cancel-in-progress: true
-
-jobs:
-  update-stage0:
-    runs-on: ubuntu-latest
-    steps:
-    # This action should push to an otherwise protected branch, so it
-    # uses a deploy key with write permissions, as suggested at
-    # https://stackoverflow.com/a/76135647/946226
-    - uses: actions/checkout@v4
-      with:
-        ssh-key: ${{secrets.STAGE0_SSH_KEY}}
-    - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
-    - name: Check if automatic update is needed
-      if: github.event_name == 'push'
-      run: |
-        if diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h
-        then
-          echo "src/stdlib_flags.h and stage0/src/stdlib_flags.h agree, nothing to do"
-          echo "should_update_stage0=no" >> "$GITHUB_ENV"
-        fi
-    - name: Setup git user
-      if: env.should_update_stage0 == 'yes'
-      run: |
-          git config --global user.name "Lean stage0 autoupdater"
-          git config --global user.email "<>"
-    # Would be nice, but does not work yet:
-    # https://github.com/DeterminateSystems/magic-nix-cache/issues/39
-    # This action does not run that often and building runs in a few minutes, so ok for now
-    #- if: env.should_update_stage0 == 'yes'
-    #  uses: DeterminateSystems/magic-nix-cache-action@v2
-    - if: env.should_update_stage0 == 'yes'
-      name: Restore Build Cache
-      uses: actions/cache/restore@v4
-      with:
-        path: nix-store-cache
-        key: Nix Linux-nix-store-cache-${{ github.sha }}
-        # fall back to (latest) previous cache
-        restore-keys: |
-          Nix Linux-nix-store-cache
-    - if: env.should_update_stage0 == 'yes'
-      name: Further Set Up Nix Cache
-      shell: bash -euxo pipefail {0}
-      run: |
-        # Nix seems to mutate the cache, so make a copy
-        cp -r nix-store-cache nix-store-cache-copy || true
-    - if: env.should_update_stage0 == 'yes'
-      name: Install Nix
-      uses: DeterminateSystems/nix-installer-action@main
-      with:
-        extra-conf: |
-          substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
-    - if: env.should_update_stage0 == 'yes'
-      run: nix run .#update-stage0-commit
-    - if: env.should_update_stage0 == 'yes'
-      run: git show --stat
-    - if: env.should_update_stage0 == 'yes' && github.event_name == 'push'
-      name: Sanity check # to avoid loops
-      run: |
-        diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h || exit 1
-    - if: env.should_update_stage0 == 'yes'
-      run: git push origin

.gitignore

@@ -4,10 +4,8 @@
 *.lock
 .lake
 lake-manifest.json
-/build
-/src/lakefile.toml
-/tests/lakefile.toml
-/lakefile.toml
+build
+!/src/lake/Lake/Build
 GPATH
 GRTAGS
 GSYMS

CMakeLists.txt

@@ -30,35 +30,6 @@ if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
     set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
 endif()
 
-# Don't do anything with cadical on wasm
-if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  # On CI Linux, we source cadical from Nix instead; see flake.nix
-  find_program(CADICAL cadical)
-  if(NOT CADICAL)
-    set(CADICAL_CXX c++)
-    find_program(CCACHE ccache)
-    if(CCACHE)
-      set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
-    endif()
-    # missing stdio locking API on Windows
-    if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-      string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
-    endif()
-    ExternalProject_add(cadical
-      PREFIX cadical
-      GIT_REPOSITORY https://github.com/arminbiere/cadical
-      GIT_TAG rel-1.9.5
-      CONFIGURE_COMMAND ""
-      # https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
-      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}
-      BUILD_IN_SOURCE ON
-      INSTALL_COMMAND "")
-    set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
-    set(EXTRA_DEPENDS "cadical")
-  endif()
-  list(APPEND CL_ARGS -DCADICAL=${CADICAL})
-endif()
-
 ExternalProject_add(stage0
   SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
   SOURCE_SUBDIR src
@@ -107,10 +78,6 @@ add_custom_target(update-stage0
   COMMAND $(MAKE) -C stage1 update-stage0
   DEPENDS stage1)
 
-add_custom_target(update-stage0-commit
-  COMMAND $(MAKE) -C stage1 update-stage0-commit
-  DEPENDS stage1)
-
 add_custom_target(test
   COMMAND $(MAKE) -C stage1 test
   DEPENDS stage1)

CMakePresets.json

@@ -1,83 +0,0 @@
-{
-  "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"
-    }
-  ]
-}

CODEOWNERS

@@ -4,43 +4,18 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @kim-em
-/RELEASES.md @kim-em
+/.github/ @Kha @semorrison
+/RELEASES.md @semorrison
+/src/ @leodemoura @Kha
+/src/Init/IO.lean @joehendrix
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
 /src/Lean/Compiler/ @leodemoura
 /src/Lean/Data/Lsp/ @mhuisi
-/src/Lean/Elab/Deriving/ @kim-em
-/src/Lean/Elab/Tactic/ @kim-em
-/src/Lean/Language/ @Kha
+/src/Lean/Elab/Deriving/ @semorrison
+/src/Lean/Elab/Tactic/ @semorrison
 /src/Lean/Meta/Tactic/ @leodemoura
-/src/Lean/PrettyPrinter/ @kmill
+/src/Lean/Parser/ @Kha
+/src/Lean/PrettyPrinter/ @Kha
 /src/Lean/Server/ @mhuisi
-/src/Lean/Widget/ @Vtec234
-/src/Init/Data/ @kim-em
-/src/Init/Data/Array/Lemmas.lean @digama0
-/src/Init/Data/List/Lemmas.lean @digama0
-/src/Init/Data/List/BasicAux.lean @digama0
-/src/Init/Data/Array/Subarray.lean @david-christiansen
-/src/Lean/Elab/Tactic/RCases.lean @digama0
-/src/Init/RCases.lean @digama0
-/src/Lean/Elab/Tactic/Ext.lean @digama0
-/src/Init/Ext.lean @digama0
-/src/Lean/Elab/Tactic/Simpa.lean @digama0
-/src/Lean/Elab/Tactic/NormCast.lean @digama0
-/src/Lean/Meta/Tactic/NormCast.lean @digama0
-/src/Lean/Meta/Tactic/TryThis.lean @digama0
-/src/Lean/Elab/Tactic/SimpTrace.lean @digama0
-/src/Lean/Elab/Tactic/NoMatch.lean @digama0
-/src/Lean/Elab/Tactic/ShowTerm.lean @digama0
-/src/Lean/Elab/Tactic/Repeat.lean @digama0
-/src/Lean/Meta/Tactic/Repeat.lean @digama0
-/src/Lean/Meta/CoeAttr.lean @digama0
-/src/Lean/Elab/GuardMsgs.lean @digama0
-/src/Lean/Elab/Tactic/Guard.lean @digama0
-/src/Init/Guard.lean @digama0
-/src/Lean/Server/CodeActions/ @digama0
-/src/Std/ @TwoFX
-/src/Std/Tactic/BVDecide/ @hargoniX
-/src/Lean/Elab/Tactic/BVDecide/ @hargoniX
-/src/Std/Sat/ @hargoniX
+/src/runtime/io.cpp @joehendrix

CONTRIBUTING.md

@@ -63,20 +63,6 @@ Because the change will be squashed, there is no need to polish the commit messa
 Reviews and Feedback:
 ----
 
-The lean4 repo is managed by the Lean FRO's *triage team* that aims to provide initial feedback on new bug reports, PRs, and RFCs weekly.
-This feedback generally consists of prioritizing the ticket using one of the following categories:
-* label `P-high`: We will work on this issue
-* label `P-medium`: We may work on this issue if we find the time
-* label `P-low`: We are not planning to work on this issue
-* *closed*: This issue is already fixed, it is not an issue, or is not sufficiently compatible with our roadmap for the project and we will not work on it nor accept external contributions on it
-
-For *bug reports*, the listed priority reflects our commitment to fixing the issue.
-It is generally indicative but not necessarily identical to the priority an external contribution addressing this bug would receive.
-For *PRs* and *RFCs*, the priority reflects our commitment to reviewing them and getting them to an acceptable state.
-Accepted RFCs are marked with the label `RFC accepted` and afterwards assigned a new "implementation" priority as with bug reports.
-
-General guidelines for interacting with reviews and feedback:
-
 **Be Patient**: Given the limited number of full-time maintainers and the volume of PRs, reviews may take some time.
 
 **Engage Constructively**: Always approach feedback positively and constructively. Remember, reviews are about ensuring the best quality for the project, not personal criticism.

LICENSES

@@ -1341,33 +1341,3 @@ whether future versions of the GNU Lesser General Public License shall
 apply, that proxy's public statement of acceptance of any version is
 permanent authorization for you to choose that version for the
 Library.
-==============================================================================
-CaDiCaL is under the MIT License:
-==============================================================================
-MIT License
-
-Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria
-Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria
-Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria
-Copyright (c) 2022-2024 Katalin Fazekas, Vienna University of Technology, Austria
-Copyright (c) 2021-2024 Armin Biere, University of Freiburg, Germany
-Copyright (c) 2021-2024 Mathias Fleury, University of Freiburg, Germany
-Copyright (c) 2023-2024 Florian Pollitt, University of Freiburg, Germany
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to deal
-in the Software without restriction, including without limitation the rights
-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all
-copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-SOFTWARE.

README.md

@@ -1,8 +1,13 @@
 This is the repository for **Lean 4**.
 
+We provide [nightly releases](https://github.com/leanprover/lean4-nightly/releases)
+and have just begun regular [stable point releases](https://github.com/leanprover/lean4/releases).
+
 # About
 
-- [Quickstart](https://lean-lang.org/lean4/doc/quickstart.html)
+- [Quickstart](https://github.com/leanprover/lean4/blob/master/doc/quickstart.md)
+- [Walkthrough installation video](https://www.youtube.com/watch?v=yZo6k48L0VY)
+- [Quick tour video](https://youtu.be/zyXtbb_eYbY)
 - [Homepage](https://lean-lang.org)
 - [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
 - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
@@ -22,4 +27,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
 
 # Building from Source
 
-See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).
+See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html).

default.nix

@@ -0,0 +1,9 @@
+# used for `nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix`
+{ nix = (import ./shell.nix {}).nix; } //
+(import (
+  fetchTarball {
+    url = "https://github.com/edolstra/flake-compat/archive/c75e76f80c57784a6734356315b306140646ee84.tar.gz";
+    sha256 = "071aal00zp2m9knnhddgr2wqzlx6i6qa1263lv1y7bdn2w20h10h"; }
+) {
+  src =  ./.;
+}).defaultNix

doc/BoolExpr.lean

@@ -1,4 +1,4 @@
-open Batteries
+open Std
 open Lean
 
 inductive BoolExpr where

doc/SUMMARY.md

@@ -4,6 +4,7 @@
 - [Tour of Lean](./tour.md)
 - [Setting Up Lean](./quickstart.md)
   - [Extended Setup Notes](./setup.md)
+  - [Nix Setup](./setup/nix.md)
 - [Theorem Proving in Lean](./tpil.md)
 - [Functional Programming in Lean](fplean.md)
 - [Examples](./examples.md)
@@ -85,10 +86,10 @@
   - [macOS Setup](./make/osx-10.9.md)
   - [Windows MSYS2 Setup](./make/msys2.md)
   - [Windows with WSL](./make/wsl.md)
+  - [Nix Setup (*Experimental*)](./make/nix.md)
 - [Bootstrapping](./dev/bootstrap.md)
 - [Testing](./dev/testing.md)
 - [Debugging](./dev/debugging.md)
 - [Commit Convention](./dev/commit_convention.md)
-- [Release checklist](./dev/release_checklist.md)
 - [Building This Manual](./dev/mdbook.md)
 - [Foreign Function Interface](./dev/ffi.md)

doc/char.md

@@ -1,11 +1 @@
 # Characters
-
-A value of type `Char`, also known as a character, is a [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value). It is represented using an unsigned 32-bit integer and is statically guaranteed to be a valid Unicode scalar value.
-
-Syntactically, character literals are enclosed in single quotes.
-```lean
-#eval 'a' -- 'a'
-#eval '∀' -- '∀'
-```
-
-Characters are ordered and can be decidably compared using the relational operators `=`, `<`, `≤`, `>`, `≥`.

doc/declarations.md

@@ -483,43 +483,7 @@ def baz : Char → Nat
 | _   => 3
 ```
 
-The case where patterns are matched against an argument whose type is an inductive family is known as *dependent pattern matching*. This is more complicated, because the type of the function being defined can impose constraints on the patterns that are matched. In this case, the equation compiler will detect inconsistent cases and rule them out.
-
-```lean
-universe u
-
-inductive Vector (α : Type u) : Nat → Type u
-  | nil  : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
-
-namespace Vector
-
-def head : Vector α (n+1) → α
-  | cons h t => h
-
-def tail : Vector α (n+1) → Vector α n
-  | cons h t => t
-
-def map (f : α → β → γ) : Vector α n → Vector β n → Vector γ n
-  | nil, nil => nil
-  | cons a va, cons b vb => cons (f a b) (map f va vb)
-
-end Vector
-```
-
-.. _recursive_functions:
-
-Recursive functions
-===================
-
-Lean must ensure that a recursive function terminates, for which there are two strategies: _structural recursion_, in which all recursive calls are made on smaller parts of the input data, and _well-founded recursion_, in which recursive calls are justified by showing that arguments to recursive calls are smaller according to some other measure.
-
-Structural recursion
---------------------
-
-If the definition of a function contains recursive calls, Lean first tries to interpret the definition as a structural recursion. In order for that to succeed, the recursive arguments must be subterms of the corresponding arguments on the left-hand side.
-
-The function is then defined using a *course of values* recursion, using automatically generated functions ``below`` and ``brec`` in the namespace corresponding to the inductive type of the recursive argument. In this case the defining equations hold definitionally, possibly with additional case splits.
+If any of the terms ``tᵢ`` in the template above contain a recursive call to ``foo``, the equation compiler tries to interpret the definition as a structural recursion. In order for that to succeed, the recursive arguments must be subterms of the corresponding arguments on the left-hand side. The function is then defined using a *course of values* recursion, using automatically generated functions ``below`` and ``brec`` in the namespace corresponding to the inductive type of the recursive argument. In this case the defining equations hold definitionally, possibly with additional case splits.
 
 ```lean
 namespace Hide
@@ -540,12 +504,7 @@ example : append [(1 : Nat), 2, 3] [4, 5] = [1, 2, 3, 4, 5] => rfl
 end Hide
 ```
 
-Well-founded recursion
----------------------
-
-If structural recursion fails, the equation compiler falls back on well-founded recursion. It tries to infer an instance of ``SizeOf`` for the type of each argument, and then tries to find a permutation of the arguments such that each recursive call is decreasing under the lexicographic order with respect to ``sizeOf`` measures.  Lean uses information in the local context, so you can often provide the relevant proof manually using ``have`` in the body of the definition.
-
-In the case of well-founded recursion, the equation used to declare the function holds only propositionally, but not definitionally, and can be accessed using ``unfold``, ``simp`` and ``rewrite`` with the function name (for example ``unfold foo`` or ``simp [foo]``, where ``foo`` is the function defined with well-founded recursion).
+If structural recursion fails, the equation compiler falls back on well-founded recursion. It tries to infer an instance of ``SizeOf`` for the type of each argument, and then show that each recursive call is decreasing under the lexicographic order of the arguments with respect to ``sizeOf`` measure. If it fails, the error message provides information as to the goal that Lean tried to prove. Lean uses information in the local context, so you can often provide the relevant proof manually using ``have`` in the body of the definition. In this case of well-founded recursion, the defining equations hold only propositionally, and can be accessed using ``simp`` and ``rewrite`` with the name ``foo``.
 
 ```lean
 namespace Hide
@@ -569,53 +528,9 @@ by rw [div]; rfl
 end Hide
 ```
 
-If Lean cannot find a permutation of the arguments for which all recursive calls are decreasing, it will print a table that contains, for every recursive call, which arguments Lean could prove to be decreasing. For example, a function with three recursive calls and four parameters might cause the following message to be printed
-
-```
-example.lean:37:0-43:31: error: Could not find a decreasing measure.
-The arguments relate at each recursive call as follows:
-(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-           x1 x2 x3 x4
-1) 39:6-27  =  =  _  =
-2) 40:6-25  =  ?  _  <
-3) 41:6-25  <  _  _  _
-Please use `termination_by` to specify a decreasing measure.
-```
-
-This table should be read as follows:
-
- * In the first recursive call, in line 39, arguments 1, 2 and 4 are equal to the function's parameters.
- * The second recursive call, in line 40, has an equal first argument, a smaller fourth argument, and nothing could be inferred for the second argument.
- * The third recursive call, in line 41, has a decreasing first argument.
- * No other proofs were attempted, either because the parameter has a type without a non-trivial ``WellFounded`` instance (parameter 3), or because it is already clear that no decreasing measure can be found.
-
-
-Lean will print the termination argument it found if ``set_option showInferredTerminationBy true`` is set.
-
-If Lean does not find the termination argument, or if you want to be explicit, you can append a `termination_by` clause to the function definition, after the function's body, but before the `where` clause if present. It is of the form
-```
-termination_by e
-```
-where ``e`` is an expression that depends on the parameters of the function and should be decreasing at each recursive call. The type of `e` should be an instance of the class ``WellFoundedRelation``, which determines how to compare two values of that type.
-
-If ``f`` has parameters “after the ``:``” (for example when defining functions via patterns using `|`), then these can be brought into scope using the syntax
-```
-termination_by a₁ … aₙ => e
-```
-
-By default, Lean uses the tactic ``decreasing_tactic`` when proving that an argument is decreasing; see its documentation for how to globally extend it. You can also choose to use a different tactic for a given function definition with the clause
-```
-decreasing_by <tac>
-```
-which should come after ``termination_by`, if present.
-
-
 Note that recursive definitions can in general require nested recursions, that is, recursion on different arguments of ``foo`` in the template above. The equation compiler handles this by abstracting later arguments, and recursively defining higher-order functions to meet the specification.
 
-Mutual recursion
-----------------
-
-The equation compiler also allows mutual recursive definitions, with a syntax similar to that of [Mutual and Nested Inductive Definitions](#mutual-and-nested-inductive-definitions). Mutual definitions are always compiled using well-founded recursion, and so once again the defining equations hold only propositionally.
+The equation compiler also allows mutual recursive definitions, with a syntax similar to that of [Mutual and Nested Inductive Definitions](#mutual-and-nested-inductive-definitions). They are compiled using well-founded recursion, and so once again the defining equations hold only propositionally.
 
 ```lean
 mutual
@@ -672,31 +587,29 @@ def num_consts_lst : List Term → Nat
 end
 ```
 
-In a set of mutually recursive function, either all or no functions must have an explicit termination argument (``termination_by``). A change of the default termination tactic (``decreasing_by``) only affects the proofs about the recursive calls of that function, not the other functions in the group.
+The case where patterns are matched against an argument whose type is an inductive family is known as *dependent pattern matching*. This is more complicated, because the type of the function being defined can impose constraints on the patterns that are matched. In this case, the equation compiler will detect inconsistent cases and rule them out.
 
-```
-mutual
-theorem even_of_odd_succ : ∀ n, Odd (n + 1) → Even n
-| _, odd_succ n h => h
-termination_by n h => h
-decreasing_by decreasing_tactic
+```lean
+universe u
 
-theorem odd_of_even_succ : ∀ n, Even (n + 1) → Odd n
-| _, even_succ n h => h
-termination_by n h => h
-end
-```
+inductive Vector (α : Type u) : Nat → Type u
+| nil  : Vector α 0
+| cons : α → Vector α n → Vector α (n+1)
 
-Another way to express mutual recursion is using local function definitions in ``where`` or ``let rec`` clauses: these can be mutually recursive with each other and their containing function:
+namespace Vector
 
-```
-theorem even_of_odd_succ : ∀ n, Odd (n + 1) → Even n
-  | _, odd_succ n h => h
-termination_by n h => h
-  where
-    theorem odd_of_even_succ : ∀ n, Even (n + 1) → Odd n
-      | _, even_succ n h => h
-    termination_by n h => h
+def head {α : Type} : Vector α (n+1) → α
+| cons h t => h
+
+def tail {α : Type} : Vector α (n+1) → Vector α n
+| cons h t => t
+
+def map {α β γ : Type} (f : α → β → γ) :
+  ∀ {n}, Vector α n → Vector β n → Vector γ n
+| 0,   nil,       nil       => nil
+| n+1, cons a va, cons b vb => cons (f a b) (map f va vb)
+
+end Vector
 ```
 
 .. _match_expressions:

doc/dev/bootstrap.md

@@ -65,59 +65,26 @@ You now have a Lean binary and library that include your changes, though their
 own compilation was not influenced by them, that you can use to test your
 changes on test programs whose compilation *will* be influenced by the changes.
 
-## Updating stage0
-
 Finally, when we want to use new language features in the library, we need to
-update the archived C source code of the stage 0 compiler in `stage0/src`.
+update the stage 0 compiler, which can be done via `make -C stageN update-stage0`.
+`make update-stage0` without `-C` defaults to stage1.
 
-The github repository will automatically update stage0 on `master` once
-`src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
-
-If you have write access to the lean4 repository, you can also manually
-trigger that process, for example to be able to use new features in the compiler itself.
-You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
-or using Github CLI with
+Updates to `stage0` should be their own commits in the Git history. In
+other words, before running `make update-stage0`, please commit your
+work. Then, commit the updated `stage0` compiler code with the commit message:
 ```
-gh workflow run update-stage0.yml
+chore: update stage0
 ```
 
-Leaving stage0 updates to the CI automation is preferable, but should you need
-to do it locally, you can use `make update-stage0-commit` in `build/release` to
-update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
-update from another stage. This command will automatically stage the updated files
-and introduce a commit,so make sure to commit your work before that.
-
-If you rebased the branch (either onto a newer version of `master`, or fixing
-up some commits prior to the stage0 update, recreate the stage0 update commits.
-The script `script/rebase-stage0.sh` can be used for that.
-
-The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
-from entering `master` through the (squashing!) merge queue, and label such PRs
-with the `changes-stage0` label. Such PRs should have a cleaned up history,
-with separate stage0 update commits; then coordinate with the admins to merge
-your PR using rebase merge, bypassing the merge queue.
-
-
 ## Further Bootstrapping Complications
 
 As written above, changes in meta code in the current stage usually will only
 affect later stages. This is an issue in two specific cases.
 
-* For the special case of *quotations*, it is desirable to have changes in builtin parsers affect them immediately: when the changes in the parser become active in the next stage, builtin macros implemented via quotations should generate syntax trees compatible with the new parser, and quotation patterns in builtin macros and elaborators should be able to match syntax created by the new parser and macros.
-  Since quotations capture the syntax tree structure during execution of the current stage and turn it into code for the next stage, we need to run the current stage's builtin parsers in quotations via the interpreter for this to work.
-  Caveats:
-  * We activate this behavior by default when building stage 1 by setting `-Dinternal.parseQuotWithCurrentStage=true`.
-    We force-disable it inside `macro/macro_rules/elab/elab_rules` via `suppressInsideQuot` as they are guaranteed not to run in the next stage and may need to be run in the current one, so the stage 0 parser is the correct one to use for them.
-    It may be necessary to extend this disabling to functions that contain quotations and are (exclusively) used by one of the mentioned commands. A function using quotations should never be used by both builtin and non-builtin macros/elaborators. Example: https://github.com/leanprover/lean4/blob/f70b7e5722da6101572869d87832494e2f8534b7/src/Lean/Elab/Tactic/Config.lean#L118-L122
-  * The parser needs to be reachable via an `import` statement, otherwise the version of the previous stage will silently be used.
-  * Only the parser code (`Parser.fn`) is affected; all metadata such as leading tokens is taken from the previous stage.
-
-  For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422R13
-
 * For *non-builtin* meta code such as `notation`s or `macro`s in
   `Notation.lean`, we expect changes to affect the current file and all later
   files of the same stage immediately, just like outside the stdlib. To ensure
-  this, we build stage 1 using `-Dinterpreter.prefer_native=false` -
+  this, we need to build the stage using `-Dinterpreter.prefer_native=false` -
   otherwise, when executing a macro, the interpreter would notice that there is
   already a native symbol available for this function and run it instead of the
   new IR, but the symbol is from the previous stage!
@@ -135,11 +102,26 @@ affect later stages. This is an issue in two specific cases.
   further stages (e.g. after an `update-stage0`) will then need to be compiled
   with the flag set to `false` again since they will expect the new signature.
 
-  When enabling `prefer_native`, we usually want to *disable* `parseQuotWithCurrentStage` as it would otherwise make quotations use the interpreter after all.
-  However, there is a specific case where we want to set both options to `true`: when we make changes to a non-builtin parser like `simp` that has a builtin elaborator, we cannot have the new parser be active outside of quotations in stage 1 as the builtin elaborator from stage 0 would not understand them; on the other hand, we need quotations in e.g. the builtin `simp` elaborator to produce the new syntax in the next stage.
-  As this issue usually affects only tactics, enabling `debug.byAsSorry` instead of `prefer_native` can be a simpler solution.
+  For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
 
-  For a `prefer_native` example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
+* For the special case of *quotations*, it is desirable to have changes in
+  built-in parsers affect them immediately: when the changes in the parser
+  become active in the next stage, macros implemented via quotations should
+  generate syntax trees compatible with the new parser, and quotation patterns
+  in macro and elaborators should be able to match syntax created by the new
+  parser and macros. Since quotations capture the syntax tree structure during
+  execution of the current stage and turn it into code for the next stage, we
+  need to run the current stage's built-in parsers in quotation via the
+  interpreter for this to work. Caveats:
+  * Since interpreting full parsers is not nearly as cheap and we rarely change
+    built-in syntax, this needs to be opted in using `-Dinternal.parseQuotWithCurrentStage=true`.
+  * The parser needs to be reachable via an `import` statement, otherwise the
+    version of the previous stage will silently be used.
+  * Only the parser code (`Parser.fn`) is affected; all metadata such as leading
+    tokens is taken from the previous stage.
+
+  For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422
+  (from before the flag defaulted to `false`).
 
 To modify either of these flags both for building and editing the stdlib, adjust
 the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset

doc/dev/debugging.md

@@ -5,7 +5,7 @@ Some notes on how to debug Lean, which may also be applicable to debugging Lean
 
 ## Tracing
 
-In `CoreM` and derived monads, we use `trace[traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`.
+In `CoreM` and derived monads, we use `trace![traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`.
 New trace classes have to be registered using `registerTraceClass` first.
 
 Notable trace classes:
@@ -22,9 +22,7 @@ Notable trace classes:
 
 In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
 Note that if the return value is not actually used, the trace code is silently dropped as well.
-
-By default, such stderr output is buffered and shown as messages after a command has been elaborated, which is necessary to ensure deterministic ordering of messages under parallelism.
-If Lean aborts the process before it can finish the command or takes too long to do that, using `-DstderrAsMessages=false` avoids this buffering and shows `dbg_trace` output (but not `trace`s or other diagnostics) immediately.
+In the language server, stderr output is buffered and shown as messages after a command has been elaborated, unless the option `server.stderrAsMessages` is deactivated.
 
 ## Debuggers
 

doc/dev/ffi.md

@@ -53,59 +53,10 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
 * A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
-  Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
+  Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
   Example: the runtime value of `u : Unit` is always `lean_box(0)`.
 
-#### Inductive types
-
-For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
-
-The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
-
-* Non-scalar fields stored as `lean_object *`
-* Fields of type `USize`
-* Other scalar fields, in decreasing order by size
-
-Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
-
-* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
-* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
-* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
-
-For example, a structure such as
-```lean
-structure S where
-  ptr_1 : Array Nat
-  usize_1 : USize
-  sc64_1 : UInt64
-  ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
-  sc64_2 : Float -- `Float` is 64 bit
-  sc8_1 : Bool
-  sc16_1 : UInt16
-  sc8_2 : UInt8
-  sc64_3 : UInt64
-  usize_2 : USize
-  ptr_3 : Char -- trivial wrapper around `UInt32`
-  sc32_1 : UInt32
-  sc16_2 : UInt16
-```
-would get re-sorted into the following memory order:
-
-* `S.ptr_1` - `lean_ctor_get(val, 0)`
-* `S.ptr_2` - `lean_ctor_get(val, 1)`
-* `S.ptr_3` - `lean_ctor_get(val, 2)`
-* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
-* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
-* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
-* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
-* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
-* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
-* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
-* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
-* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
-* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
-
 ### Borrowing
 
 By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.
@@ -160,15 +111,6 @@ if (lean_io_result_is_ok(res)) {
 lean_io_mark_end_initialization();
 ```
 
-In addition, any other thread not spawned by the Lean runtime itself must be initialized for Lean use by calling
-```c
-void lean_initialize_thread();
-```
-and should be finalized in order to free all thread-local resources by calling
-```c
-void lean_finalize_thread();
-```
-
 ## `@[extern]` in the Interpreter
 
 The interpreter can run Lean declarations for which symbols are available in loaded shared libraries, which includes `@[extern]` declarations.
@@ -179,4 +121,4 @@ Thus to e.g. run `#eval` on such a declaration, you need to
 Note that it is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each `@[extern]` declaration.
 Thus it is not possible to interpret an `@[extern]` declaration in the same file.
 
-See [`tests/compiler/foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) for an example.
+See `tests/compiler/foreign` for an example.

doc/dev/index.md

@@ -74,9 +74,3 @@ Lean's build process uses [`ccache`](https://ccache.dev/) if it is
 installed to speed up recompilation of the generated C code. Without
 `ccache`, you'll likely spend more time than necessary waiting on
 rebuilds - it's a good idea to make sure it's installed.
-
-### `prelude`
-Unlike most Lean projects, all submodules of the `Lean` module begin with the
-`prelude` keyword. This disables the automated import of `Init`, meaning that
-developers need to figure out their own subset of `Init` to import. This is done
-such that changing files in `Init` doesn't force a full rebuild of `Lean`.

doc/dev/release_checklist.md

@@ -1,262 +0,0 @@
-# Releasing a stable version
-
-This checklist walks you through releasing a stable version.
-See below for the checklist for release candidates.
-
-We'll use `v4.6.0` as the intended release version as a running example.
-
-- One week before the planned release, ensure that
-  (1) someone has written the release notes and
-  (2) someone has written the first draft of the release blog post.
-  If there is any material in `./releases_drafts/` on the `releases/v4.6.0` branch, then the release notes are not done.
-  (See the section "Writing the release notes".)
-- `git checkout releases/v4.6.0`
-  (This branch should already exist, from the release candidates.)
-- `git pull`
-- In `src/CMakeLists.txt`, verify you see
-  - `set(LEAN_VERSION_MINOR 6)` (for whichever `6` is appropriate)
-  - `set(LEAN_VERSION_IS_RELEASE 1)`
-  - (both of these should already be in place from the release candidates)
-- `git tag v4.6.0`
-- `git push $REMOTE v4.6.0`, where `$REMOTE` is the upstream Lean repository (e.g., `origin`, `upstream`)
-- Now wait, while CI runs.
-  - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`,
-    looking for the `v4.6.0` tag.
-  - This step can take up to an hour.
-  - If you are intending to cut the next release candidate on the same day,
-    you may want to start on the release candidate checklist now.
-- Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
-  - Edit the release notes on Github to select the "Set as the latest release".
-  - Follow the instructions in creating a release candidate for the "GitHub release notes" step,
-    now that we have a written `RELEASES.md` section.
-    Do a quick sanity check.
-- Next, we will move a curated list of downstream repos to the latest stable release.
-  - For each of the repositories listed below:
-    - Make a PR to `master`/`main` changing the toolchain to `v4.6.0`
-      - Update the toolchain file
-      - In the Lakefile, if there are dependencies on specific version tags of dependencies that you've already pushed as part of this process, update them to the new tag.
-        If they depend on `main` or `master`, don't change this; you've just updated the dependency, so it will work and be saved in the manifest
-      - Run `lake update`
-      - The PR title should be "chore: bump toolchain to v4.6.0".
-    - Merge the PR once CI completes.
-    - Create the tag `v4.6.0` from `master`/`main` and push it.
-    - Merge the tag `v4.6.0` into the `stable` branch and push it.
-  - We do this for the repositories:
-    - [lean4checker](https://github.com/leanprover/lean4checker)
-      - No dependencies
-      - Toolchain bump PR
-      - Create and push the tag
-      - Merge the tag into `stable`
-    - [Batteries](https://github.com/leanprover-community/batteries)
-      - No dependencies
-      - Toolchain bump PR
-      - Create and push the tag
-      - Merge the tag into `stable`
-    - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
-      - Dependencies: `Batteries`
-      - Note on versions and branches:
-        - `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
-          which does not refer to the toolchain being used.
-        - Make a new release in this sequence after merging the toolchain bump PR.
-        - `ProofWidgets` does not maintain a `stable` branch.
-      - Toolchain bump PR
-      - Create and push the tag, following the version convention of the repository
-    - [Aesop](https://github.com/leanprover-community/aesop)
-      - Dependencies: `Batteries`
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - Merge the tag into `stable`
-    - [doc-gen4](https://github.com/leanprover/doc-gen4)
-      - Dependencies: exist, but they're not part of the release workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
-    - [Verso](https://github.com/leanprover/verso)
-      - Dependencies: exist, but they're not part of the release workflow
-      - The `SubVerso` dependency should be compatible with _every_ Lean release simultaneously, rather than following this workflow
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
-    - [import-graph](https://github.com/leanprover-community/import-graph)
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - There is no `stable` branch; skip this step
-    - [Mathlib](https://github.com/leanprover-community/mathlib4)
-      - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph`
-      - Toolchain bump PR notes:
-        - In addition to updating the `lean-toolchain` and `lakefile.lean`,
-          in `.github/workflows/lean4checker.yml` update the line
-          `git checkout v4.6.0` to the appropriate tag. 
-        - Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
-        - Create and push the tag
-        - Create a new branch from the tag, push it, and open a pull request against `stable`.
-          Coordinate with a Mathlib maintainer to get this merged.
-    - [REPL](https://github.com/leanprover-community/repl)
-      - Dependencies: `Mathlib` (for test code)
-      - Note that there are two copies of `lean-toolchain`/`lakefile.lean`:
-        in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
-      - Toolchain bump PR including updated Lake manifest
-      - Create and push the tag
-      - Merge the tag into `stable`
-- The `v4.6.0` section of `RELEASES.md` is out of sync between
-  `releases/v4.6.0` and `master`. This should be reconciled:
-  - Replace the `v4.6.0` section on `master` with the `v4.6.0` section on `releases/v4.6.0`
-    and commit this to `master`.
-- Merge the release announcement PR for the Lean website - it will be deployed automatically
-- Finally, make an announcement!
-  This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.6.0`.
-  Please see previous announcements for suggested language.
-  You will want a few bullet points for main topics from the release notes.
-  Link to the blog post from the Zulip announcement.
-- Make sure that whoever is handling social media knows the release is out.
-
-## Optimistic(?) time estimates:
-- Initial checks and push the tag: 30 minutes.
-- Waiting for the release: 60 minutes.
-- Fixing release notes: 10 minutes.
-- Bumping toolchains in downstream repositories, up to creating the Mathlib PR: 30 minutes.
-- Waiting for Mathlib CI and bors: 120 minutes.
-- Finalizing Mathlib tags and stable branch, and updating REPL: 15 minutes.
-- Posting announcement and/or blog post: 20 minutes.
-
-# Creating a release candidate.
-
-This checklist walks you through creating the first release candidate for a version of Lean.
-
-We'll use `v4.7.0-rc1` as the intended release version in this example.
-
-- Decide which nightly release you want to turn into a release candidate.
-  We will use `nightly-2024-02-29` in this example.
-- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly.
-  - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
-    in their `lean-toolchain`.
-  - The steps required to reach that state are beyond the scope of this checklist, but see below!
-- Create the release branch from this nightly tag:
-    ```
-    git remote add nightly https://github.com/leanprover/lean4-nightly.git
-    git fetch nightly tag nightly-2024-02-29
-    git checkout nightly-2024-02-29
-    git checkout -b releases/v4.7.0
-    ```
-- In `RELEASES.md` replace `Development in progress` in the `v4.7.0` section with `Release notes to be written.`
-- We will rely on automatically generated release notes for release candidates,
-  and the written release notes will be used for stable versions only.
-  It is essential to choose the nightly that will become the release candidate as early as possible, to avoid confusion.
-- In `src/CMakeLists.txt`,
-  - verify that you see `set(LEAN_VERSION_MINOR 7)` (for whichever `7` is appropriate); this should already have been updated when the development cycle began.
-  - `set(LEAN_VERSION_IS_RELEASE 1)` (this should be a change; on `master` and nightly releases it is always `0`).
-  - Commit your changes to `src/CMakeLists.txt`, and push.
-- `git tag v4.7.0-rc1`
-- `git push origin v4.7.0-rc1`
-- Ping the FRO Zulip that release notes need to be written. The release notes do not block completing the rest of this checklist.
-- Now wait, while CI runs.
-  - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
-  - This step can take up to an hour.
-- (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
-  - Verify that the release is marked as a prerelease (this should have been done automatically by the CI release job).
-  - In the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
-    This will add a list of all the commits since the last stable version.
-    - Delete "update stage0" commits, and anything with a completely inscrutable commit message.
-- Next, we will move a curated list of downstream repos to the release candidate.
-  - This assumes that for each repository either:
-    * There is already a *reviewed* branch `bump/v4.7.0` containing the required adaptations.
-      The preparation of this branch is beyond the scope of this document.
-    * The repository does not need any changes to move to the new version.
-  - For each of the target repositories:
-    - If the repository does not need any changes (i.e. `bump/v4.7.0` does not exist) then create
-      a new PR updating `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1` and running `lake update`.
-    - Otherwise:
-      - Checkout the `bump/v4.7.0` branch.
-      - Verify that the `lean-toolchain` is set to the nightly from which the release candidate was created.
-      - `git merge origin/master`
-      - Change the `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`
-      - In `lakefile.lean`, change any dependencies which were using `nightly-testing` or `bump/v4.7.0` branches
-        back to `master` or `main`, and run `lake update` for those dependencies.
-      - Run `lake build` to ensure that dependencies are found (but it's okay to stop it after a moment).
-      - `git commit`
-      - `git push`
-      - Open a PR from `bump/v4.7.0` to `master`, and either merge it yourself after CI, if appropriate,
-        or notify the maintainers that it is ready to go.
-    - Once the PR has been merged, tag `master` with `v4.7.0-rc1` and push this tag.
-  - We do this for the same list of repositories as for stable releases, see above.
-    As above, there are dependencies between these, and so the process above is iterative.
-    It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
-    It is essential for Mathlib CI that you then create the next `bump/v4.8.0` branch
-    for the next development cycle.
-    Set the `lean-toolchain` file on this branch to same `nightly` you used for this release.
-  - For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
-    `nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
-    (create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
-- Make an announcement!
-  This should go in https://leanprover.zulipchat.com/#narrow/stream/113486-announce, with topic `v4.7.0-rc1`.
-  Please see previous announcements for suggested language.
-  You will want a few bullet points for main topics from the release notes.
-  Please also make sure that whoever is handling social media knows the release is out.
-- Begin the next development cycle (i.e. for `v4.8.0`) on the Lean repository, by making a PR that:
-  - Updates `src/CMakeLists.txt` to say `set(LEAN_VERSION_MINOR 8)`
-  - Replaces the "release notes will be copied" text in the `v4.6.0` section of `RELEASES.md` with the
-    finalized release notes from the `releases/v4.6.0` branch.
-  - Replaces the "development in progress" in the `v4.7.0` section of `RELEASES.md` with
-    ```
-    Release candidate, release notes will be copied from the branch `releases/v4.7.0` once completed.
-    ```
-    and inserts the following section before that section:
-    ```
-    v4.8.0
-    ----------
-    Development in progress.
-    ```
-  - Removes all the entries from the `./releases_drafts/` folder.
-  - Titled "chore: begin development cycle for v4.8.0"
-
-
-## Time estimates:
-Slightly longer than the corresponding steps for a stable release.
-Similar process, but more things go wrong.
-In particular, updating the downstream repositories is significantly more work
-(because we need to merge existing `bump/v4.7.0` branches, not just update a toolchain).
-
-# Preparing `bump/v4.7.0` branches
-
-While not part of the release process per se,
-this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
-
-Please read https://leanprover-community.github.io/contribute/tags_and_branches.html
-
-* Each repo has an unreviewed `nightly-testing` branch that
-  receives commits automatically from `master`, and
-  has its toolchain updated automatically for every nightly.
-  (Note: the aesop branch is not automated, and is updated on an as needed basis.)
-  As a consequence this branch is often broken.
-  A bot posts in the (private!) "Mathlib reviewers" stream on Zulip about the status of these branches.
-* We fix the breakages by committing directly to `nightly-testing`: there is no PR process.
-  * This can either be done by the person managing this process directly,
-    or by soliciting assistance from authors of files, or generally helpful people on Zulip!
-* Each repo has a `bump/v4.7.0` which accumulates reviewed changes adapting to new versions.
-* Once `nightly-testing` is working on a given nightly, say `nightly-2024-02-15`, we will create a PR to `bump/v4.7.0`.
-* For Mathlib, there is a script in `scripts/create-adaptation-pr.sh` that automates this process.
-* For Batteries and Aesop it is currently manual.
-* For all of these repositories, the process is the same:
-  * Make sure `bump/v4.7.0` is up to date with `master` (by merging `master`, no PR necessary)
-  * Create from `bump/v4.7.0` a `bump/nightly-2024-02-15` branch.
-  * In that branch, `git merge nightly-testing` to bring across changes from `nightly-testing`.
-  * Sanity check changes, commit, and make a PR to `bump/v4.7.0` from the `bump/nightly-2024-02-15` branch.
-  * Solicit review, merge the PR into `bump/v4.7.0`.
-* It is always okay to merge in the following directions:
-  `master` -> `bump/v4.7.0` -> `bump/nightly-2024-02-15` -> `nightly-testing`.
-  Please remember to push any merges you make to intermediate steps!
-
-# Writing the release notes
-
-We are currently trying a system where release notes are compiled all at once from someone looking through the commit history.
-The exact steps are a work in progress.
-Here is the general idea:
-
-* The work is done right on the `releases/v4.6.0` branch sometime after it is created but before the stable release is made.
-  The release notes for `v4.6.0` will later be copied to `master` when we begin a new development cycle.
-* There can be material for release notes entries in commit messages.
-* There can also be pre-written entries in `./releases_drafts`, which should be all incorporated in the release notes and then deleted from the branch.
-  See `./releases_drafts/README.md` for more information.
-* The release notes should be written from a downstream expert user's point of view.
-
-This section will be updated when the next release notes are written (for `v4.10.0`).

doc/dev/testing.md

@@ -5,6 +5,7 @@ After [building Lean](../make/index.md) you can run all the tests using
 cd build/release
 make test ARGS=-j4
 ```
+
 Change the 4 to the maximum number of parallel tests you want to
 allow. The best choice is the number of CPU cores on your machine as
 the tests are mostly CPU bound.  You can find the number of processors
@@ -16,12 +17,6 @@ adding the `-C stageN` argument. The default when run as above is stage 1.  The
 Lean tests will automatically use that stage's corresponding Lean
 executables
 
-Running `make test` will not pick up new test files; run
-```bash
-cmake build/release/stage1
-```
-to update the list of tests.
-
 You can also use `ctest` directly if you are in the right folder.  So
 to run stage1 tests with a 300 second timeout run this:
 
@@ -29,9 +24,6 @@ to run stage1 tests with a 300 second timeout run this:
 cd build/release/stage1
 ctest -j 4 --output-on-failure --timeout 300
 ```
-Useful `ctest` flags are `-R <name of test>` to run a single test, and
-`--rerun-failed` to run all tests that failed during the last run.
-You can also pass `ctest` flags via `make test ARGS="--rerun-failed"`.
 
 To get verbose output from ctest pass the `--verbose` command line
 option. Test output is normally suppressed and only summary
@@ -41,17 +33,17 @@ information is displayed. This option will show all test output.
 
 All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
 
-- [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/): contains tests that come equipped with a
-  .lean.expected.out file. The driver script [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/test_single.sh) runs
+- `tests/lean`: contains tests that come equipped with a
+  .lean.expected.out file. The driver script `test_single.sh` runs
   each test and checks the actual output (*.produced.out) with the
   checked in expected output.
 
-- [`tests/lean/run`](https://github.com/leanprover/lean4/tree/master/tests/lean/run/): contains tests that are run through the lean
+- `tests/lean/run`: contains tests that are run through the lean
   command line one file at a time. These tests only look for error
   codes and do not check the expected output even though output is
   produced, it is ignored.
 
-- [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a
+- `tests/lean/interactive`: are designed to test server requests at a
   given position in the input file. Each .lean file contains comments
   that indicate how to simulate a client request at that position.
   using a `--^` point to the line position. Example:
@@ -61,7 +53,7 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     Bla.
       --^ textDocument/completion
     ```
-    In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
+    In this example, the test driver `test_single.sh` will simulate an
     auto-completion request at `Bla.`. The expected output is stored in
     a .lean.expected.out in the json format that is part of the
     [Language Server
@@ -78,21 +70,21 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     --^ collectDiagnostics
     ```
 
-- [`tests/lean/server`](https://github.com/leanprover/lean4/tree/master/tests/lean/server/): Tests more of the Lean `--server` protocol.
+- `tests/lean/server`: Tests more of the Lean `--server` protocol.
   There are just a few of them, and it uses .log files containing
   JSON.
 
-- [`tests/compiler`](https://github.com/leanprover/lean4/tree/master/tests/compiler/): contains tests that will run the Lean compiler and
+- `tests/compiler`: contains tests that will run the Lean compiler and
   build an executable that is executed and the output is compared to
   the .lean.expected.out file. This test also contains a subfolder
-  [`foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) which shows how to extend Lean using C++.
+  `foreign` which shows how to extend Lean using C++.
 
-- [`tests/lean/trust0`](https://github.com/leanprover/lean4/tree/master/tests/lean/trust0): tests that run Lean in a mode that Lean doesn't
+- `tests/lean/trust0`: tests that run Lean in a mode that Lean doesn't
   even trust the .olean files (i.e., trust 0).
 
-- [`tests/bench`](https://github.com/leanprover/lean4/tree/master/tests/bench/): contains performance tests.
+- `tests/bench`: contains performance tests.
 
-- [`tests/plugin`](https://github.com/leanprover/lean4/tree/master/tests/plugin/): tests that compiled Lean code can be loaded into
+- `tests/plugin`: tests that compiled Lean code can be loaded into
   `lean` via the `--plugin` command line option.
 
 ## Writing Good Tests
@@ -103,7 +95,7 @@ Every test file should contain:
   and, if not 100% clear, why that is the desirable behavior
 
 At the time of writing, most tests do not follow these new guidelines yet.
-For an example of a conforming test, see [`tests/lean/1971.lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/1971.lean).
+For an example of a conforming test, see `tests/lean/1971.lean`.
 
 ## Fixing Tests
 
@@ -119,7 +111,7 @@ First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by
 sudo apt-get install meld
 ```
 
-Now, suppose `bad_class.lean` test is broken. We can see the problem by going to [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean) directory and
+Now, suppose `bad_class.lean` test is broken. We can see the problem by going to `tests/lean` directory and
 executing
 
 ```
@@ -132,3 +124,8 @@ outputs. `meld` can also be used to repair the problems.
 
 In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
 To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.
+When using the Nix setup, add `--keep-failed` to the `nix build` call and then call
+```sh
+tests/lean/copy-produced <build-dir>/source/tests/lean
+```
+instead where `<build-dir>` is the path printed out by `nix build`.

doc/examples/Certora2022/ex8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by x y => (x, y)
+termination_by ack x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if _ : i < a.size then
+     if i < a.size then
         a[i] + go (i+1)
      else
         0
-  termination_by a.size - i
   go 0
+termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

doc/examples/ICERM2022/ctor.lean

@@ -4,42 +4,43 @@ open Lean Meta
 
 def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
   /- Set `MetaM` context using `mvarId` -/
-  mvarId.withContext do
+  withMVarContext mvarId do 
     /- Fail if the metavariable is already assigned. -/
-    mvarId.checkNotAssigned `ctor
+    checkNotAssigned mvarId `ctor
     /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← mvarId.getType'
+    let target ← getMVarType' mvarId
     let .const declName us := target.getAppFn
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     let .inductInfo { ctors, .. } ← getConstInfo declName
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     if idx = 0 then
-      throwTacticEx `ctor mvarId "invalid index, it must be > 0"
+      throwTacticEx `ctor mvarId "invalid index, it must be > 0"  
     else if h : idx - 1 < ctors.length then
-      mvarId.apply (.const ctors[idx - 1] us)
+      apply mvarId (.const ctors[idx - 1] us)
     else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} constructors"
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"  
 
 open Elab Tactic
 
-elab "ctor" idx:num : tactic =>
+elab "ctor" idx:num : tactic => 
   liftMetaTactic (ctor · idx.getNat)
 
-example (p : Prop) : p := by
+example (p : Prop) : p := by 
   ctor 1 -- Error
 
-example (h : q) : p ∨ q := by
+example (h : q) : p ∨ q := by 
   ctor 0 -- Error
   exact h
 
-example (h : q) : p ∨ q := by
+example (h : q) : p ∨ q := by 
   ctor 3 -- Error
   exact h
 
-example (h : q) : p ∨ q := by
+example (h : q) : p ∨ q := by 
   ctor 2
   exact h
 
-example (h : q) : p ∨ q := by
+example (h : q) : p ∨ q := by 
   ctor 1
-  exact h -- Error
+  exact h -- Error 
+

doc/examples/ICERM2022/meta.lean

@@ -5,15 +5,15 @@ open Lean Meta
 def ex1 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   IO.println s!"{declName} : {← ppExpr info.type}"
-  if let some val := info.value? then
+  if let some val := info.value? then 
     IO.println s!"{declName} : {← ppExpr val}"
-
+    
 #eval ex1 ``Nat
 
 def ex2 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   trace[Meta.debug] "{declName} : {info.type}"
-  if let some val := info.value? then
+  if let some val := info.value? then 
     trace[Meta.debug] "{declName} : {val}"
 
 #eval ex2 ``Add.add
@@ -30,9 +30,9 @@ def ex3 (declName : Name) : MetaM Unit := do
       trace[Meta.debug] "{x} : {← inferType x}"
 
 def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
-  if a < b then
+  if a < b then 
     a
-  else
+  else 
     b
 
 set_option trace.Meta.debug true in
@@ -40,7 +40,7 @@ set_option trace.Meta.debug true in
 
 def ex4 : MetaM Unit := do
   let nat := mkConst ``Nat
-  withLocalDeclD `a nat fun a =>
+  withLocalDeclD `a nat fun a => 
   withLocalDeclD `b nat fun b => do
     let e ← mkAppM ``HAdd.hAdd #[a, b]
     trace[Meta.debug] "{e} : {← inferType e}"
@@ -66,17 +66,15 @@ open Elab Term
 
 def ex5 : TermElabM Unit := do
   let nat := Lean.mkConst ``Nat
-  withLocalDeclD `a nat fun a => do
+  withLocalDeclD `a nat fun a => do 
   withLocalDeclD `b nat fun b => do
     let ab ← mkAppM ``HAdd.hAdd #[a, b]
-    let abStx ← exprToSyntax ab
-    let aStx ← exprToSyntax a
-    let stx ← `(fun x => if x < 10 then $abStx + x else x + $aStx)
+    let stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
     let e ← elabTerm stx none
     trace[Meta.debug] "{e} : {← inferType e}"
     let e := mkApp e (mkNatLit 5)
     let e ← whnf e
     trace[Meta.debug] "{e}"
-
+       
 set_option trace.Meta.debug true in
 #eval ex5

doc/examples/NFM2022/nfm8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by x y => (x, y)
+termination_by ack x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if _ : i < a.size then
+     if i < a.size then
         a[i] + go (i+1)
      else
         0
-  termination_by a.size - i
   go 0
+termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

doc/examples/bintree.lean

@@ -277,13 +277,14 @@ theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
     . by_cases' key < k
       cases h; apply ihr; assumption
 
-theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
+theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
         : (b.insert k v).find? k' = b.find? k' := by
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    intros le
-    exact Nat.lt_of_le_of_ne le ne
+    split <;> (try simp) <;> split <;> (try simp)
+    have_eq k k'
+    contradiction
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h
     specialize ihl bl

doc/examples/compiler/.gitignore

@@ -1 +0,0 @@
-build

doc/examples/deBruijn.lean

@@ -149,7 +149,7 @@ We now define the constant folding optimization that traverses a term if replace
 /-!
 The correctness of the `Term.constFold` is proved using induction, case-analysis, and the term simplifier.
 We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
-use hypotheses such as `a = b` as rewriting/simplifications rules.
+use hypotheses such as `a = b` as rewriting/simplications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
 The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in

doc/examples/interp.lean

@@ -12,17 +12,17 @@ Remark: this example is based on an example found in the Idris manual.
 Vectors
 --------
 
-A `Vec` is a list of size `n` whose elements belong to a type `α`.
+A `Vector` is a list of size `n` whose elements belong to a type `α`.
 -/
 
-inductive Vec (α : Type u) : Nat → Type u
-  | nil : Vec α 0
-  | cons : α → Vec α n → Vec α (n+1)
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
 
 /-!
-We can overload the `List.cons` notation `::` and use it to create `Vec`s.
+We can overload the `List.cons` notation `::` and use it to create `Vector`s.
 -/
-infix:67 " :: " => Vec.cons
+infix:67 " :: " => Vector.cons
 
 /-!
 Now, we define the types of our simple functional language.
@@ -50,11 +50,11 @@ the builtin instance for `Add Int` as the solution.
 /-!
 Expressions are indexed by the types of the local variables, and the type of the expression itself.
 -/
-inductive HasType : Fin n → Vec Ty n → Ty → Type where
+inductive HasType : Fin n → Vector Ty n → Ty → Type where
   | stop : HasType 0 (ty :: ctx) ty
   | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
 
-inductive Expr : Vec Ty n → Ty → Type where
+inductive Expr : Vector Ty n → Ty → Type where
   | var   : HasType i ctx ty → Expr ctx ty
   | val   : Int → Expr ctx Ty.int
   | lam   : Expr (a :: ctx) ty → Expr ctx (Ty.fn a ty)
@@ -102,8 +102,8 @@ indexed over the types in scope. Since an environment is just another form of li
 to the vector of local variable types, we overload again the notation `::` so that we can use the usual list syntax.
 Given a proof that a variable is defined in the context, we can then produce a value from the environment.
 -/
-inductive Env : Vec Ty n → Type where
-  | nil  : Env Vec.nil
+inductive Env : Vector Ty n → Type where
+  | nil  : Env Vector.nil
   | cons : Ty.interp a → Env ctx → Env (a :: ctx)
 
 infix:67 " :: " => Env.cons
@@ -149,4 +149,4 @@ def fact : Expr ctx (Ty.fn Ty.int Ty.int) :=
            (op (·*·) (delay fun _ => app fact (op (·-·) (var stop) (val 1))) (var stop)))
   decreasing_by sorry
 
-#eval! fact.interp Env.nil 10
+#eval fact.interp Env.nil 10

doc/examples/palindromes.lean

@@ -82,7 +82,7 @@ theorem List.palindrome_ind (motive : List α → Prop)
     have ih := palindrome_ind motive h₁ h₂ h₃ (a₂::as').dropLast
     have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (by simp)] = a₁::a₂::as' := by simp
     this ▸ h₃ _ _ _ ih
-termination_by as.length
+termination_by _ as => as.length
 
 /-!
 We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds.

doc/examples/phoas.lean

@@ -225,7 +225,7 @@ We now define the constant folding optimization that traverses a term if replace
 /-!
 The correctness of the `constFold` is proved using induction, case-analysis, and the term simplifier.
 We prove all cases but the one for `plus` using `simp [*]`. This tactic instructs the term simplifier to
-use hypotheses such as `a = b` as rewriting/simplifications rules.
+use hypotheses such as `a = b` as rewriting/simplications rules.
 We use the `split` to break the nested `match` expression in the `plus` case into two cases.
 The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
 The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in

doc/examples/tc.lean

@@ -29,7 +29,7 @@ inductive HasType : Expr → Ty → Prop
 
 /-!
 We can easily show that if `e` has type `t₁` and type `t₂`, then `t₁` and `t₂` must be equal
-by using the `cases` tactic. This tactic creates a new subgoal for every constructor,
+by using the the `cases` tactic. This tactic creates a new subgoal for every constructor,
 and automatically discharges unreachable cases. The tactic combinator `tac₁ <;> tac₂` applies
 `tac₂` to each subgoal produced by `tac₁`. Then, the tactic `rfl` is used to close all produced
 goals using reflexivity.
@@ -82,7 +82,9 @@ theorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .un
 /-!
 Now, we prove that if `Expr.typeCheck e` returns `Maybe.unknown`, then forall `ty`, `HasType e ty` does not hold.
 The notation `e.typeCheck` is sugar for `Expr.typeCheck e`. Lean can infer this because we explicitly said that `e` has type `Expr`.
-The proof is by induction on `e` and case analysis. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
+The proof is by induction on `e` and case analysis. The tactic `rename_i` is used to to rename "inaccessible" variables.
+We say a variable is inaccessible if it is introduced by a tactic (e.g., `cases`) or has been shadowed by another variable introduced
+by the user. Note that the tactic `simp [typeCheck]` is applied to all goal generated by the `induction` tactic, and closes
 the cases corresponding to the constructors `Expr.nat` and `Expr.bool`.
 -/
 theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := by

doc/examples/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../tests/common.sh
 
-exec_check_raw lean -Dlinter.all=false "$f"
+exec_check lean -j 0 -Dlinter.all=false "$f"

doc/examples/widgets.lean

@@ -4,97 +4,76 @@ open Lean Widget
 /-!
 # The user-widgets system
 
-Proving and programming are inherently interactive tasks.
-Lots of mathematical objects and data structures are visual in nature.
-*User widgets* let you associate custom interactive UIs
-with sections of a Lean document.
-User widgets are rendered in the Lean infoview.
+Proving and programming are inherently interactive tasks. Lots of mathematical objects and data
+structures are visual in nature. *User widgets* let you associate custom interactive UIs with
+sections of a Lean document. User widgets are rendered in the Lean infoview.
 
 ![Rubik's cube](../images/widgets_rubiks.png)
 
 ## Trying it out
 
-To try it out, type in the following code and place your cursor over the `#widget` command.
-You can also [view this manual entry in the online editor](https://live.lean-lang.org/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fleanprover%2Flean4%2Fmaster%2Fdoc%2Fexamples%2Fwidgets.lean).
+To try it out, simply type in the following code and place your cursor over the `#widget` command.
 -/
 
-@[widget_module]
-def helloWidget : Widget.Module where
+@[widget]
+def helloWidget : UserWidgetDefinition where
+  name := "Hello"
   javascript := "
     import * as React from 'react';
     export default function(props) {
       const name = props.name || 'world'
-      return React.createElement('p', {}, 'Hello ' + name + '!')
+      return React.createElement('p', {}, name + '!')
     }"
 
-#widget helloWidget
+#widget helloWidget .null
 
 /-!
 If you want to dive into a full sample right away, check out
-[`Rubiks`](https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/Rubiks.lean).
-This sample uses higher-level widget components from the ProofWidgets library.
-
+[`RubiksCube`](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/).
 Below, we'll explain the system piece by piece.
 
 ⚠️ WARNING: All of the user widget APIs are **unstable** and subject to breaking changes.
 
-## Widget modules and instances
+## Widget sources and instances
 
-A [widget module](https://leanprover-community.github.io/mathlib4_docs/Lean/Widget/UserWidget.html#Lean.Widget.Module)
-is a valid JavaScript [ESModule](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
-that can execute in the Lean infoview.
-Most widget modules export a [React component](https://reactjs.org/docs/components-and-props.html)
-as the piece of user interface to be rendered.
-To access React, the module can use `import * as React from 'react'`.
-Our first example of a widget module is `helloWidget` above.
-Widget modules must be registered with the `@[widget_module]` attribute.
+A *widget source* is a valid JavaScript [ESModule](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
+which exports a [React component](https://reactjs.org/docs/components-and-props.html). To access
+React, the module must use `import * as React from 'react'`. Our first example of a widget source
+is of course the value of `helloWidget.javascript`.
 
-A [widget instance](https://leanprover-community.github.io/mathlib4_docs/Lean/Widget/Types.html#Lean.Widget.WidgetInstance)
-is then the identifier of a widget module (e.g. `` `helloWidget ``)
-bundled with a value for its props.
-This value is passed as the argument to the React component.
-In our first invocation of `#widget`, we set it to `.null`.
-Try out what happens when you type in:
+We can register a widget source with the `@[widget]` attribute, giving it a friendlier name
+in the `name` field. This is bundled together in a `UserWidgetDefinition`.
+
+A *widget instance* is then the identifier of a `UserWidgetDefinition` (so `` `helloWidget ``,
+not `"Hello"`) associated with a range of positions in the Lean source code. Widget instances
+are stored in the *infotree* in the same manner as other information about the source file
+such as the type of every expression. In our example, the `#widget` command stores a widget instance
+with the entire line as its range. We can think of a widget instance as an instruction for the
+infoview: "when the user places their cursor here, please render the following widget".
+
+Every widget instance also contains a `props : Json` value. This value is passed as an argument
+to the React component. In our first invocation of `#widget`, we set it to `.null`. Try out what
+happens when you type in:
 -/
 
-structure HelloWidgetProps where
-  name? : Option String := none
-  deriving Server.RpcEncodable
-
-#widget helloWidget with { name? := "<your name here>" : HelloWidgetProps }
+#widget helloWidget (Json.mkObj [("name", "<your name here>")])
 
 /-!
-Under the hood, widget instances are associated with a range of positions in the source file.
-Widget instances are stored in the *infotree*
-in the same manner as other information about the source file
-such as the type of every expression.
-In our example, the `#widget` command stores a widget instance
-with the entire line as its range.
-One can think of the infotree entry as an instruction for the infoview:
-"when the user places their cursor here, please render the following widget".
--/
+💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case
+is the web-based infoview in VSCode.
 
-/-!
 ## Querying the Lean server
 
-💡 NOTE: The RPC system presented below does not depend on JavaScript.
-However, the primary use case is the web-based infoview in VSCode.
+Besides enabling us to create cool client-side visualizations, user widgets come with the ability
+to communicate with the Lean server. Thanks to this, they have the same metaprogramming capabilities
+as custom elaborators or the tactic framework. To see this in action, let's implement a `#check`
+command as a web input form. This example assumes some familiarity with React.
 
-Besides enabling us to create cool client-side visualizations,
-user widgets have the ability to communicate with the Lean server.
-Thanks to this, they have the same metaprogramming capabilities
-as custom elaborators or the tactic framework.
-To see this in action, let's implement a `#check` command as a web input form.
-This example assumes some familiarity with React.
-
-The first thing we'll need is to create an *RPC method*.
-Meaning "Remote Procedure Call",this is a Lean function callable from widget code
-(possibly remotely over the internet).
+The first thing we'll need is to create an *RPC method*. Meaning "Remote Procedure Call", this
+is basically a Lean function callable from widget code (possibly remotely over the internet).
 Our method will take in the `name : Name` of a constant in the environment and return its type.
-By convention, we represent the input data as a `structure`.
-Since it will be sent over from JavaScript,
-we need `FromJson` and `ToJson` instance.
-We'll see why the position field is needed later.
+By convention, we represent the input data as a `structure`. Since it will be sent over from JavaScript,
+we need `FromJson` and `ToJson`. We'll see below why the position field is needed.
 -/
 
 structure GetTypeParams where
@@ -105,33 +84,25 @@ structure GetTypeParams where
   deriving FromJson, ToJson
 
 /-!
-After its argument structure, we define the `getType` method.
-RPCs method execute in the `RequestM` monad and must return a `RequestTask α`
-where `α` is the "actual" return type.
-The `Task` is so that requests can be handled concurrently.
-As a first guess, we'd use `Expr` as `α`.
-However, expressions in general can be large objects
-which depend on an `Environment` and `LocalContext`.
-Thus we cannot directly serialize an `Expr` and send it to JavaScript.
-Instead, there are two options:
+After its arguments, we define the `getType` method. Every RPC method executes in the `RequestM`
+monad and must return a `RequestTask α` where `α` is its "actual" return type. The `Task` is so
+that requests can be handled concurrently. A first guess for `α` might be `Expr`. However,
+expressions in general can be large objects which depend on an `Environment` and `LocalContext`.
+Thus we cannot directly serialize an `Expr` and send it to the widget. Instead, there are two
+options:
+- One is to send a *reference* which points to an object residing on the server. From JavaScript's
+  point of view, references are entirely opaque, but they can be sent back to other RPC methods for
+  further processing.
+- Two is to pretty-print the expression and send its textual representation called `CodeWithInfos`.
+  This representation contains extra data which the infoview uses for interactivity. We take this
+  strategy here.
 
-- One is to send a *reference* which points to an object residing on the server.
-  From JavaScript's point of view, references are entirely opaque,
-  but they can be sent back to other RPC methods for further processing.
-- The other is to pretty-print the expression and send its textual representation called `CodeWithInfos`.
-  This representation contains extra data which the infoview uses for interactivity.
-  We take this strategy here.
-
-RPC methods execute in the context of a file,
-but not of any particular `Environment`,
-so they don't know about the available `def`initions and `theorem`s.
-Thus, we need to pass in a position at which we want to use the local `Environment`.
-This is why we store it in `GetTypeParams`.
-The `withWaitFindSnapAtPos` method launches a concurrent computation
-whose job is to find such an `Environment` for us,
-in the form of a `snap : Snapshot`.
-With this in hand, we can call `MetaM` procedures
-to find out the type of `name` and pretty-print it.
+RPC methods execute in the context of a file, but not any particular `Environment` so they don't
+know about the available `def`initions and `theorem`s. Thus, we need to pass in a position at which
+we want to use the local `Environment`. This is why we store it in `GetTypeParams`. The `withWaitFindSnapAtPos`
+method launches a concurrent computation whose job is to find such an `Environment` and a bit
+more information for us, in the form of a `snap : Snapshot`. With this in hand, we can call
+`MetaM` procedures to find out the type of `name` and pretty-print it.
 -/
 
 open Server RequestM in
@@ -147,33 +118,30 @@ def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) :=
 /-!
 ## Using infoview components
 
-Now that we have all we need on the server side, let's write the widget module.
-By importing `@leanprover/infoview`, widgets can render UI components used to implement the infoview itself.
-For example, the `<InteractiveCode>` component displays expressions
-with `term : type` tooltips as seen in the goal view.
-We will use it to implement our custom `#check` display.
+Now that we have all we need on the server side, let's write the widget source. By importing
+`@leanprover/infoview`, widgets can render UI components used to implement the infoview itself.
+For example, the `<InteractiveCode>` component displays expressions with `term : type` tooltips
+as seen in the goal view. We will use it to implement our custom `#check` display.
 
 ⚠️ WARNING: Like the other widget APIs, the infoview JS API is **unstable** and subject to breaking changes.
 
-The code below demonstrates useful parts of the API.
-To make RPC method calls, we invoke the `useRpcSession` hook.
-The `useAsync` helper packs the results of an RPC call into an `AsyncState` structure
-which indicates whether the call has resolved successfully,
-has returned an error, or is still in-flight.
-Based on this we either display an `InteractiveCode` component with the result,
-`mapRpcError` the error in order to turn it into a readable message,
-or show a `Loading..` message, respectively.
+The code below demonstrates useful parts of the API. To make RPC method calls, we use the `RpcContext`.
+The `useAsync` helper packs the results of a call into an `AsyncState` structure which indicates
+whether the call has resolved successfully, has returned an error, or is still in-flight. Based
+on this we either display an `InteractiveCode` with the type, `mapRpcError` the error in order
+to turn it into a readable message, or show a `Loading..` message, respectively.
 -/
 
-@[widget_module]
-def checkWidget : Widget.Module where
+@[widget]
+def checkWidget : UserWidgetDefinition where
+  name := "#check as a service"
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
-import { useRpcSession, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
+import { RpcContext, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
 
 export default function(props) {
-  const rs = useRpcSession()
+  const rs = React.useContext(RpcContext)
   const [name, setName] = React.useState('getType')
 
   const st = useAsync(() =>
@@ -189,45 +157,45 @@ export default function(props) {
 "
 
 /-!
-We can now try out the widget.
+Finally we can try out the widget.
 -/
 
-#widget checkWidget
+#widget checkWidget .null
 
 /-!
 ![`#check` as a service](../images/widgets_caas.png)
 
 ## Building widget sources
 
-While typing JavaScript inline is fine for a simple example,
-for real developments we want to use packages from NPM, a proper build system, and JSX.
-Thus, most actual widget sources are built with Lake and NPM.
-They consist of multiple files and may import libraries which don't work as ESModules by default.
-On the other hand a widget module must be a single, self-contained ESModule in the form of a string.
-Readers familiar with web development may already have guessed that to obtain such a string, we need a *bundler*.
-Two popular choices are [`rollup.js`](https://rollupjs.org/guide/en/)
-and [`esbuild`](https://esbuild.github.io/).
-If we go with `rollup.js`, to make a widget work with the infoview we need to:
+While typing JavaScript inline is fine for a simple example, for real developments we want to use
+packages from NPM, a proper build system, and JSX. Thus, most actual widget sources are built with
+Lake and NPM. They consist of multiple files and may import libraries which don't work as ESModules
+by default. On the other hand a widget source must be a single, self-contained ESModule in the form
+of a string. Readers familiar with web development may already have guessed that to obtain such a
+string, we need a *bundler*. Two popular choices are [`rollup.js`](https://rollupjs.org/guide/en/)
+and [`esbuild`](https://esbuild.github.io/). If we go with `rollup.js`, to make a widget work with
+the infoview we need to:
 - Set [`output.format`](https://rollupjs.org/guide/en/#outputformat) to `'es'`.
 - [Externalize](https://rollupjs.org/guide/en/#external) `react`, `react-dom`, `@leanprover/infoview`.
   These libraries are already loaded by the infoview so they should not be bundled.
 
-ProofWidgets provides a working `rollup.js` build configuration in
-[rollup.config.js](https://github.com/leanprover-community/ProofWidgets4/blob/main/widget/rollup.config.js).
+In the RubiksCube sample, we provide a working `rollup.js` build configuration in
+[rollup.config.js](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/widget/rollup.config.js).
 
 ## Inserting text
 
-Besides making RPC calls, widgets can instruct the editor to carry out certain actions.
-We can insert text, copy text to the clipboard, or highlight a certain location in the document.
-To do this, use the `EditorContext` React context.
-This will return an `EditorConnection`
-whose `api` field contains a number of methods that interact with the editor.
+We can also instruct the editor to insert text, copy text to the clipboard, or
+reveal a certain location in the document.
+To do this, use the `React.useContext(EditorContext)` React context.
+This will return an `EditorConnection` whose `api` field contains a number of methods to
+interact with the text editor.
 
-The full API can be viewed [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52).
+You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52)
 -/
 
-@[widget_module]
-def insertTextWidget : Widget.Module where
+@[widget]
+def insertTextWidget : UserWidgetDefinition where
+  name := "textInserter"
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
@@ -243,4 +211,6 @@ export default function(props) {
 }
 "
 
-#widget insertTextWidget
+/-! Finally, we can try this out: -/
+
+#widget insertTextWidget .null

doc/expressions.md

@@ -396,7 +396,7 @@ Every expression in Lean has a natural computational interpretation, unless it i
 
 * *β-reduction* : An expression ``(λ x, t) s`` β-reduces to ``t[s/x]``, that is, the result of replacing ``x`` by ``s`` in ``t``.
 * *ζ-reduction* : An expression ``let x := s in t`` ζ-reduces to ``t[s/x]``.
-* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to ``t``.
+* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to to ``t``.
 * *ι-reduction* : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value, as described in [Inductive Types](inductive.md).
 
 The reduction relation is transitive, which is to say, is ``s`` reduces to ``s'`` and ``t`` reduces to ``t'``, then ``s t`` reduces to ``s' t'``, ``λ x, s`` reduces to ``λ x, s'``, and so on. If ``s`` and ``t`` reduce to a common term, they are said to be *definitionally equal*. Definitional equality is defined to be the smallest equivalence relation that satisfies all these properties and also includes α-equivalence and the following two relations:

doc/flake.lock

@@ -18,15 +18,12 @@
       }
     },
     "flake-utils": {
-      "inputs": {
-        "systems": "systems"
-      },
       "locked": {
-        "lastModified": 1710146030,
-        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "lastModified": 1656928814,
+        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
         "type": "github"
       },
       "original": {
@@ -38,12 +35,13 @@
     "lean": {
       "inputs": {
         "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-old": "nixpkgs-old"
+        "lean4-mode": "lean4-mode",
+        "nix": "nix",
+        "nixpkgs": "nixpkgs_2"
       },
       "locked": {
         "lastModified": 0,
-        "narHash": "sha256-saRAtQ6VautVXKDw1XH35qwP0KEBKTKZbg/TRa4N9Vw=",
+        "narHash": "sha256-YnYbmG0oou1Q/GE4JbMNb8/yqUVXBPIvcdQQJHBqtPk=",
         "path": "../.",
         "type": "path"
       },
@@ -52,20 +50,51 @@
         "type": "path"
       }
     },
-    "leanInk": {
+    "lean4-mode": {
       "flake": false,
       "locked": {
-        "lastModified": 1704976501,
-        "narHash": "sha256-FSBUsbX0HxakSnYRYzRBDN2YKmH9EkA0q9p7TSPEJTI=",
+        "lastModified": 1659020985,
+        "narHash": "sha256-+dRaXB7uvN/weSZiKcfSKWhcdJVNg9Vg8k0pJkDNjpc=",
         "owner": "leanprover",
-        "repo": "LeanInk",
-        "rev": "51821e3c2c032c88e4b2956483899d373ec090c4",
+        "repo": "lean4-mode",
+        "rev": "37d5c99b7b29c80ab78321edd6773200deb0bca6",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "refs/pull/57/merge",
+        "repo": "lean4-mode",
+        "type": "github"
+      }
+    },
+    "leanInk": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1666154782,
+        "narHash": "sha256-0ELqEca6jZT4BW/mqkDD+uYuxW5QlZUFlNwZkvugsg8=",
+        "owner": "digama0",
         "repo": "LeanInk",
+        "rev": "12a2aec9b5f4aa84e84fb01a9af1da00d8aaff4e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "repo": "LeanInk",
+        "type": "github"
+      }
+    },
+    "lowdown-src": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1633514407,
+        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
+        "owner": "kristapsdz",
+        "repo": "lowdown",
+        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
+        "type": "github"
+      },
+      "original": {
+        "owner": "kristapsdz",
+        "repo": "lowdown",
         "type": "github"
       }
     },
@@ -85,13 +114,65 @@
         "type": "github"
       }
     },
+    "nix": {
+      "inputs": {
+        "lowdown-src": "lowdown-src",
+        "nixpkgs": "nixpkgs",
+        "nixpkgs-regression": "nixpkgs-regression"
+      },
+      "locked": {
+        "lastModified": 1657097207,
+        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
+        "owner": "NixOS",
+        "repo": "nix",
+        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nix",
+        "type": "github"
+      }
+    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1710889954,
-        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
+        "lastModified": 1653988320,
+        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
+        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-22.05-small",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-regression": {
+      "locked": {
+        "lastModified": 1643052045,
+        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1657208011,
+        "narHash": "sha256-BlIFwopAykvdy1DYayEkj6ZZdkn+cVgPNX98QVLc0jM=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "2770cc0b1e8faa0e20eb2c6aea64c256a706d4f2",
         "type": "github"
       },
       "original": {
@@ -101,23 +182,6 @@
         "type": "github"
       }
     },
-    "nixpkgs-old": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1581379743,
-        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-19.03",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "root": {
       "inputs": {
         "alectryon": "alectryon",
@@ -129,21 +193,6 @@
         "leanInk": "leanInk",
         "mdBook": "mdBook"
       }
-    },
-    "systems": {
-      "locked": {
-        "lastModified": 1681028828,
-        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
-        "owner": "nix-systems",
-        "repo": "default",
-        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-systems",
-        "repo": "default",
-        "type": "github"
-      }
     }
   },
   "root": "root",

doc/flake.nix

@@ -12,12 +12,12 @@
     flake = false;
   };
   inputs.leanInk = {
-    url = "github:leanprover/LeanInk/refs/pull/57/merge";
+    url = "github:leanprover/LeanInk";
     flake = false;
   };
 
   outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system:
-    with inputs.lean.packages.${system}.deprecated; with nixpkgs;
+    with inputs.lean.packages.${system}; with nixpkgs;
     let
       doc-src = lib.sourceByRegex ../. ["doc.*" "tests(/lean(/beginEndAsMacro.lean)?)?"];
     in {
@@ -27,7 +27,7 @@
         src = inputs.mdBook;
         cargoDeps = drv.cargoDeps.overrideAttrs (_: {
           inherit src;
-          outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A=";
+          outputHash = "sha256-1YlPS6cqgxE4fjy9G8pWrpP27YrrbCDnfeyIsX81ZNw=";
         });
         doCheck = false;
       });
@@ -44,6 +44,21 @@
           mdbook build -d $out
         '';
       };
+      # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache
+      test = stdenv.mkDerivation {
+        name ="lean-doc-test";
+        src = doc-src;
+        buildInputs = [ lean-mdbook stage1.Lean.lean-package strace ];
+        patchPhase = ''
+          cd doc
+          patchShebangs test
+        '';
+        buildPhase = ''
+          mdbook test
+          touch $out
+        '';
+        dontInstall = true;
+      };
       leanInk = (buildLeanPackage {
         name = "Main";
         src = inputs.leanInk;

doc/functions.md

@@ -32,8 +32,8 @@ def fact x :=
 
 #eval fact 100
 ```
-By default, Lean only accepts total functions.
-The `partial` keyword may be used to define a recursive function without a termination proof; `partial` functions compute in compiled programs, but are opaque in proofs and during type checking.
+By default, Lean only accepts total functions. The `partial` keyword should be used when Lean cannot
+establish that a function always terminates.
 ```lean
 partial def g (x : Nat) (p : Nat -> Bool) : Nat :=
   if p x then

doc/int.md

@@ -13,7 +13,7 @@ Recall that nonnegative numerals are considered to be a `Nat` if there are no ty
 
 The operator `/` for `Int` implements integer division.
 ```lean
-#eval -10 / 4 -- -3
+#eval -10 / 4 -- -2
 ```
 
 Similar to `Nat`, the internal representation of `Int` is optimized. Small integers are

doc/latex/lean4.py

@@ -0,0 +1,100 @@
+# -*- coding: utf-8 -*-
+"""
+    pygments.lexers.theorem
+    ~~~~~~~~~~~~~~~~~~~~~~~
+
+    Lexers for theorem-proving languages.
+
+    :copyright: Copyright 2006-2017 by the Pygments team, see AUTHORS.
+    :license: BSD, see LICENSE for details.
+"""
+
+import re
+
+from pygments.lexer import RegexLexer, default, words
+from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
+    Number, Punctuation, Generic
+
+__all__ = ['Lean4Lexer']
+
+class Lean4Lexer(RegexLexer):
+    """
+    For the `Lean 4 <https://github.com/leanprover/lean4>`_
+    theorem prover.
+
+    .. versionadded:: 2.0
+    """
+    name = 'Lean4'
+    aliases = ['lean4']
+    filenames = ['*.lean']
+    mimetypes = ['text/x-lean']
+
+    flags = re.MULTILINE | re.UNICODE
+
+    keywords1 = (
+        'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition',
+        'renaming', 'inline', 'hiding', 'parameter', 'lemma', 'variable',
+        'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias',
+        'help', 'options', 'precedence', 'postfix', 'prefix',
+        'infix', 'infixl', 'infixr', 'notation', '#eval',
+        '#check', '#reduce', '#exit', 'coercion', 'end', 'private', 'using', 'namespace',
+        'including', 'instance', 'section', 'context', 'protected', 'expose',
+        'export', 'set_option', 'extends', 'open', 'example',
+        'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible',
+        'def', 'macro', 'elab', 'syntax', 'macro_rules', 'reduce', 'where',
+        'abbrev', 'noncomputable', 'class', 'attribute', 'synth', 'mutual',
+    )
+
+    keywords2 = (
+        'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume',
+        'take', 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin',
+        'proof', 'qed', 'calc', 'match', 'nomatch', 'do', 'at',
+    )
+
+    keywords3 = (
+        # Sorts
+        'Type', 'Prop', 'Sort',
+    )
+
+    operators = (
+        u'!=', u'#', u'&', u'&&', u'*', u'+', u'-', u'/', u'@', u'!', u'`',
+        u'-.', u'->', u'.', u'..', u'...', u'::', u':>', u';', u';;', u'<',
+        u'<-', u'=', u'==', u'>', u'_', u'|', u'||', u'~', u'=>', u'<=', u'>=',
+        u'/\\', u'\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥',
+        u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞',
+        u'⌟', u'≡', u'⟨', u'⟩',
+    )
+
+    punctuation = (u'(', u')', u':', u'{', u'}', u'[', u']', u'⦃', u'⦄',
+                   u':=', u',')
+
+    tokens = {
+        'root': [
+            (r'\s+', Text),
+            (r'/-', Comment, 'comment'),
+            (r'--.*?$', Comment.Single),
+            (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace),
+            (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword),
+            (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type),
+            (words(operators), Name.Builtin.Pseudo),
+            (words(punctuation), Operator),
+            (u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]"
+             u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079"
+             u"\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*", Name),
+            (r'\d+', Number.Integer),
+            (r'"', String.Double, 'string'),
+            (r'[~?][a-z][\w\']*:', Name.Variable)
+        ],
+        'comment': [
+            # Multiline Comments
+            (r'[^/-]', Comment.Multiline),
+            (r'/-', Comment.Multiline, '#push'),
+            (r'-/', Comment.Multiline, '#pop'),
+            (r'[/-]', Comment.Multiline)
+        ],
+        'string': [
+            (r'[^\\"]+', String.Double),
+            (r'\\[n"\\]', String.Escape),
+            ('"', String.Double, '#pop'),
+        ],
+    }

doc/lexical_structure.md

@@ -8,7 +8,7 @@ A Lean program consists of a stream of UTF-8 tokens where each token
 is one of the following:
 
 ```
-   token: symbol | command | ident | string | raw_string | char | numeral |
+   token: symbol | command | ident | string | char | numeral |
         : decimal | doc_comment | mod_doc_comment | field_notation
 ```
 
@@ -79,35 +79,15 @@ special characters:
 [Unicode table](https://unicode-table.com/en/) so "\xA9 Copyright 2021" is "© Copyright 2021".
 - `\uHHHH` puts the character represented by the 4 digit hexadecimal into the string, so the following
 string "\u65e5\u672c" will become "日本" which means "Japan".
-- `\` followed by a newline and then any amount of whitespace is a "gap" that is equivalent to the empty string,
-useful for letting a string literal span across multiple lines. Gaps spanning multiple lines can be confusing,
-so the parser raises an error if the trailing whitespace contains any newlines.
 
 So the complete syntax is:
 
 ```
    string       : '"' string_item '"'
-   string_item  : string_char | char_escape | string_gap
-   string_char  : [^"\\]
-   char_escape  : "\" ("\" | '"' | "'" | "n" | "t" | "x" hex_char{2} | "u" hex_char{4})
+   string_item  : string_char | string_escape
+   string_char  : [^\\]
+   string_escape: "\" ("\" | '"' | "'" | "n" | "t" | "x" hex_char{2} | "u" hex_char{4} )
    hex_char     : [0-9a-fA-F]
-   string_gap   : "\" newline whitespace*
-```
-
-Raw String Literals
-===================
-
-Raw string literals are string literals without any escape character processing.
-They begin with `r##...#"` (with zero or more `#` characters) and end with `"#...##` (with the same number of `#` characters).
-The contents of a raw string literal may contain `"##..#` so long as the number of `#` characters
-is less than the number of `#` characters used to begin the raw string literal.
-
-```
-   raw_string          : raw_string_aux(0) | raw_string_aux(1) | raw_string_aux(2) | ...
-   raw_string_aux(n)   : 'r' '#'{n} '"' raw_string_item '"' '#'{n}
-   raw_string_item(n)  : raw_string_char | raw_string_quote(n)
-   raw_string_char     : [^"]
-   raw_string_quote(n) : '"' '#'{0..n-1}
 ```
 
 Char Literals
@@ -116,9 +96,7 @@ Char Literals
 Char literals are enclosed by single quotes (``'``).
 
 ```
-   char      : "'" char_item "'"
-   char_item : char_char | char_escape
-   char_char : [^'\\]
+   char: "'" string_item "'"
 ```
 
 Numeric Literals
@@ -128,16 +106,16 @@ Numeric literals can be specified in various bases.
 
 ```
    numeral    : numeral10 | numeral2 | numeral8 | numeral16
-   numeral10  : [0-9]+ ("_"+ [0-9]+)*
-   numeral2   : "0" [bB] ("_"* [0-1]+)+
-   numeral8   : "0" [oO] ("_"* [0-7]+)+
-   numeral16  : "0" [xX] ("_"* hex_char+)+
+   numeral10  : [0-9]+
+   numeral2   : "0" [bB] [0-1]+
+   numeral8   : "0" [oO] [0-7]+
+   numeral16  : "0" [xX] hex_char+
 ```
 
 Floating point literals are also possible with optional exponent:
 
 ```
-   float    : numeral10 "." numeral10? [eE[+-]numeral10]
+   float    : [0-9]+ "." [0-9]+ [[eE[+-][0-9]+]
 ```
 
 For example:
@@ -147,7 +125,6 @@ constant w : Int := 55
 constant x : Nat := 26085
 constant y : Nat := 0x65E5
 constant z : Float := 2.548123e-05
-constant b : Bool := 0b_11_01_10_00
 ```
 
 Note: that negative numbers are created by applying the "-" negation prefix operator to the number, for example:

doc/make/index.md

@@ -1,48 +1,58 @@
-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](../dev/index.md).
-
-We strongly suggest that new users instead follow the [Quickstart](../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
 ------------
 
 - C++14 compatible compiler
 - [CMake](http://www.cmake.org)
 - [GMP (GNU multiprecision library)](http://gmplib.org/)
-- [LibUV](https://libuv.org/)
 
 Platform-Specific Setup
 -----------------------
 
 - [Linux (Ubuntu)](ubuntu.md)
 - [Windows (msys2)](msys2.md)
+- [Windows (Visual Studio)](msvc.md)
 - [Windows (WSL)](wsl.md)
 - [macOS (homebrew)](osx-10.9.md)
-- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix develop` in the project root. That's it.
+- Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
+- There is also an [**experimental** setup based purely on Nix](nix.md) that works fundamentally differently from the
+  make/CMake setup described on this page.
 
 Generic Build Instructions
 --------------------------
 
-Setting up a basic parallelized release build:
+Setting up a basic release build:
 
 ```bash
-git clone https://github.com/leanprover/lean4
+git clone https://github.com/leanprover/lean4 --recurse-submodules
 cd lean4
-cmake --preset release
-make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
+mkdir -p build/release
+cd build/release
+cmake ../..
+make
 ```
-You can replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount.
+
+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/...`.
 
 The above commands will compile the Lean library and binaries into the
-`stage1` subfolder; see below for details.
+`stage1` subfolder; see below for details. Add `-j N` for an
+appropriate `N` to `make` for a parallel build.
 
-You should not usually run `cmake --install` after a successful build.
+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.
 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 --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).
+Pass these along with the `cmake ../..` command.
 
 * `-D CMAKE_BUILD_TYPE=`\
   Select the build type. Valid values are `RELEASE` (default), `DEBUG`,

doc/make/msvc.md

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

doc/make/msys2.md

@@ -15,24 +15,17 @@ Mode](https://docs.microsoft.com/en-us/windows/apps/get-started/enable-your-devi
 which will allow Lean to create symlinks that e.g. enable go-to-definition in
 the stdlib.
 
-## Installing the Windows SDK
-
-Install the Windows SDK from [Microsoft](https://developer.microsoft.com/en-us/windows/downloads/windows-sdk/).
-The oldest supported version is 10.0.18362.0. If you installed the Windows SDK to the default location,
-then there should be a directory with the version number at `C:\Program Files (x86)\Windows Kits\10\Include`.
-If there are multiple directories, only the highest version number matters.
-
 ## Installing dependencies
 
 [The official webpage of MSYS2][msys2] provides one-click installers.
-Once installed, you should run the "MSYS2 CLANG64" shell from the start menu (the one that runs `clang64.exe`).
-Do not run "MSYS2 MSYS" or "MSYS2 MINGW64" instead!
-MSYS2 has a package management system, [pacman][pacman].
+Once installed, you should run the "MSYS2 MinGW 64-bit shell" from the start menu (the one that runs `mingw64.exe`).
+Do not run "MSYS2 MSYS" instead!
+MSYS2 has a package management system, [pacman][pacman], which is used in Arch Linux.
 
 Here are the commands to install all dependencies needed to compile Lean on your machine.
 
 ```bash
-pacman -S make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache mingw-w64-clang-x86_64-libuv mingw-w64-clang-x86_64-gmp git unzip diffutils binutils
+pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x86_64-ccache git unzip diffutils binutils
 ```
 
 You should now be able to run these commands:
@@ -45,9 +38,10 @@ cmake --version
 Then follow the [generic build instructions](index.md) in the MSYS2
 MinGW shell, using:
 ```
-cmake --preset release -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
+cmake ../.. -G "Unix Makefiles"  -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
 ```
-instead of `cmake --preset release`. This will use the clang compiler instead of gcc, which is required with msys2.
+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.
 
 ## Install lean
 
@@ -68,9 +62,9 @@ If you want a version that can run independently of your MSYS install
 then you need to copy the following dependent DLL's from where ever
 they are installed in your MSYS setup:
 
-- libc++.dll
+- libgcc_s_seh-1.dll
+- libstdc++-6.dll
 - libgmp-10.dll
-- libuv-1.dll
 - libwinpthread-1.dll
 
 The following linux command will do that:
@@ -88,6 +82,6 @@ version clang to your path.
 
 **-bash: gcc: command not found**
 
-Make sure `/clang64/bin` is in your PATH environment.  If it is not then
-check you launched the MSYS2 CLANG64 shell from the start menu.
-(The one that runs `clang64.exe`).
+Make sure `/mingw64/bin` is in your PATH environment.  If it is not then
+check you launched the MSYS2 MinGW 64-bit shell from the start menu.
+(The one that runs `mingw64.exe`).

doc/make/nix.md

@@ -0,0 +1,110 @@
+# Building with Nix
+
+While [Nix](https://nixos.org/nix/) can be used to quickly open a shell with all dependencies for the [standard setup](index.md) installed, the user-facing [Nix Setup](../setup.md#nix-setup) can also be used to work *on* Lean.
+
+## Setup
+
+Follow the setup in the link above; to open the Lean shell inside a Lean checkout, you can also use
+```bash
+# in the Lean root directory
+$ nix-shell -A nix
+```
+
+On top of the local and remote Nix cache, we do still rely on CCache as well to make C/C++ build steps incremental, which are atomic steps from Nix's point of view.
+To enable CCache, add the following line to the config file mentioned in the setup:
+```bash
+extra-sandbox-paths = /nix/var/cache/ccache
+```
+Then set up that directory as follows:
+```bash
+sudo mkdir -m0770 -p /nix/var/cache/ccache
+# macOS standard chown doesn't support --reference
+nix shell .#nixpkgs.coreutils -c sudo chown --reference=/nix/store /nix/var/cache/ccache
+```
+
+## Basic Build Commands
+
+From the Lean root directory inside the Lean shell:
+```bash
+nix build .#stage1  # build this stage's stdlib & executable
+nix build .#stage1.test  # run all tests
+nix run .#stage1.update-stage0  # update ./stage0 from this stage
+nix run .#stage1.update-stage0-commit  # ...and commit the results
+```
+The `stage1.` part in each command is optional:
+```bash
+nix build .#test  # run tests for stage 1
+nix build .  # build stage 1
+nix build  # ditto
+```
+
+## Build Process Description
+
+The Nix build process conceptually works the same as described in [Lean Build Pipeline](index.md#lean-build-pipeline).
+However, there are two important differences in practice apart from the standard Nix properties (hermeneutic, reproducible builds stored in a global hash-indexed store etc.):
+* Only files tracked by git (using `git add` or at least `git add --intent-to-add`) are compiled.
+This is actually a general property of Nix flakes, and has the benefit of making it basically impossible to forget to commit a file (at least in `src/`).
+* Only files reachable from `src/Lean.lean` are compiled.
+This is because modules are discovered not from a directory listing anymore but by recursively compiling all dependencies of that top module.
+
+## Editor Integration
+
+As in the standard Nix setup.
+After adding `src/` as an LSP workspace, it should automatically fall back to using stage 0 in there.
+
+Note that the UX of `{emacs,vscode}-dev` is quite different from the Make-based setup regarding the compilation of dependencies:
+there is no mutable directory incrementally filled by the build that we could point the editor at for .olean files.
+Instead, `emacs-dev` will gather the individual dependency outputs from the Nix store when checking a file -- and build them on the fly when necessary.
+However, it will only ever load changes saved to disk, not ones opened in other buffers.
+
+The absence of a mutable output directory also means that the Lean server will not automatically pick up `.ilean` metadata from newly compiled files.
+Instead, you can run `nix run .#link-ilean` to symlink the `.ilean` tree of the stdlib state at that point in time to `src/build/lib`, where the server should automatically find them.
+
+## Other Fun Stuff to Do with Nix
+
+Open Emacs with Lean set up from an arbitrary commit (without even cloning Lean beforehand... if your Nix is new enough):
+```bash
+nix run github:leanprover/lean4/7e4edeb#emacs-package
+```
+
+Open a shell with `lean` and `LEAN_PATH` set up for compiling a specific module (this is exactly what `emacs-dev` is doing internally):
+```bash
+nix develop .#mods.\"Lean.Parser.Basic\"
+# alternatively, directly pass a command to execute:
+nix develop .#stage2.mods.\"Init.Control.Basic\" -c bash -c 'lean $src -Dtrace.Elab.command=true'
+```
+
+Not sure what you just broke? Run Lean from (e.g.) the previous commit on a file:
+```bash
+nix run .\?rev=$(git rev-parse @^) scratch.lean
+```
+
+Work on two adjacent stages at the same time without the need for repeatedly updating and reverting `stage0/`:
+```bash
+# open an editor that will use only committed changes (so first commit them when changing files)
+nix run .#HEAD-as-stage1.emacs-dev&
+# open a second editor that will use those committed changes as stage 0
+# (so don't commit changes done here until you are done and ran a final `update-stage0-commit`)
+nix run .#HEAD-as-stage0.emacs-dev&
+```
+To run `nix build` on the second stage outside of the second editor, use
+```bash
+nix build .#stage0-from-input --override-input lean-stage0 .\?rev=$(git rev-parse HEAD)
+```
+This setup will inadvertently change your `flake.lock` file, which you can revert when you are done.
+
+...more surely to come...
+
+## Debugging
+
+Since Nix copies all source files before compilation, you will need to map debug symbols back to the original path using `set substitute-path` in GDB.
+For example, for a build on Linux with the Nix sandbox activated:
+```bash
+(gdb) f
+#1  0x0000000000d23a4f in lean_inc (o=0x1) at /build/source/build/include/lean/lean.h:562
+562	/build/source/build/include/lean/lean.h: No such file or directory.
+(gdb) set substitute-path /build/source/build src
+(gdb) f
+#1  0x0000000000d23a4f in lean_inc (o=0x1) at /build/source/build/include/lean/lean.h:562
+562	static inline void lean_inc(lean_object * o) { if (!lean_is_scalar(o)) lean_inc_ref(o); }
+```

doc/make/osx-10.9.md

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

doc/make/ubuntu.md

@@ -8,5 +8,5 @@ follow the [generic build instructions](index.md).
 ## Basic packages
 
 ```bash
-sudo apt-get install git libgmp-dev libuv1-dev cmake ccache clang
+sudo apt-get install git libgmp-dev cmake ccache clang
 ```

doc/metaprogramming-arith.md

@@ -60,7 +60,7 @@ While parsing `a * (b + c)`, `(b + c)` is assigned a precedence `60` by the addi
 the right argument to have precedence **at least** 71. Thus, this parse is invalid. In contrast, `(a * b) + c` assigns
 a precedence of `70` to `(a * b)`. This is compatible with addition which expects the left argument to have precedence
 **at least `60` ** (`70` is greater than `60`). Thus, the string `a * b + c` is parsed as `(a * b) + c`.
-For more details, please look at the [Lean manual on syntax extensions](./notation.md#notations-and-precedence).
+For more details, please look at the [Lean manual on syntax extensions](../syntax.md#notations-and-precedence).
 
 To go from strings into `Arith`, we define a macro to
 translate the syntax category `arith` into an `Arith` inductive value that

doc/monads/applicatives.lean

@@ -138,8 +138,8 @@ definition:
 
 -/
 instance : Applicative List where
-  pure := List.singleton
-  seq f x := List.flatMap f fun y => Functor.map y (x ())
+  pure := List.pure
+  seq f x := List.bind f fun y => Functor.map y (x ())
 /-!
 
 Notice you can now sequence a _list_ of functions and a _list_ of items.

doc/monads/except.lean

@@ -33,7 +33,7 @@ convert the pure non-monadic value `x / y` into the required `Except` object.  S
 
 Now this return typing would get tedious if you had to include it everywhere that you call this
 function, however, Lean type inference can clean this up. For example, you can define a test
-function that calls the `divide` function and you don't need to say anything here about the fact that
+function can calls the `divide` function and you don't need to say anything here about the fact that
 it might throw an error, because that is inferred:
 -/
 def test := divide 5 0

doc/monads/laws.lean

@@ -128,8 +128,8 @@ Applying the identity function through an applicative structure should not chang
 values or structure.  For example:
 -/
 instance : Applicative List where
-  pure := List.singleton
-  seq f x := List.flatMap f fun y => Functor.map y (x ())
+  pure := List.pure
+  seq f x := List.bind f fun y => Functor.map y (x ())
 
 #eval pure id <*> [1, 2, 3]  -- [1, 2, 3]
 /-!
@@ -171,7 +171,7 @@ of data contained in the container resulting in a new container that has the sam
 
 `u <*> pure y = pure (. y) <*> u`.
 
-This law is a little more complicated, so don't sweat it too much. It states that the order that
+This law is is a little more complicated, so don't sweat it too much. It states that the order that
 you wrap things shouldn't matter. One the left, you apply any applicative `u` over a pure wrapped
 object. On the right, you first wrap a function applying the object as an argument. Note that `(·
 y)` is short hand for: `fun f => f y`. Then you apply this to the first applicative `u`. These
@@ -235,8 +235,8 @@ structure or its values.
 Left identity is `x >>= pure = x` and is demonstrated by the following examples on a monadic `List`:
 -/
 instance : Monad List  where
-  pure := List.singleton
-  bind := List.flatMap
+  pure := List.pure
+  bind := List.bind
 
 def a := ["apple", "orange"]
 

doc/monads/monads.lean

@@ -192,8 +192,8 @@ implementation of `pure` and `bind`.
 
 -/
 instance : Monad List  where
-  pure := List.singleton
-  bind := List.flatMap
+  pure := List.pure
+  bind := List.bind
 /-!
 
 Like you saw with the applicative `seq` operator, the `bind` operator applies the given function

doc/monads/readers.lean

@@ -139,7 +139,7 @@ You might be wondering, how does the context actually move through the `ReaderM`
 add an input argument to a function by modifying its return type?  There is a special command in
 Lean that will show you the reduced types:
 -/
-#reduce (types := true) ReaderM Environment String   -- Environment → String
+#reduce ReaderM Environment String   -- Environment → String
 /-!
 And you can see here that this type is actually a function!  It's a function that takes an
 `Environment` as input and returns a `String`.
@@ -196,4 +196,4 @@ entirely.
 
 Now it's time to move on to [StateM Monad](states.lean.md) which is like a `ReaderM` that is
 also updatable.
--/
+-/

doc/monads/states.lean

@@ -15,7 +15,7 @@ data type containing several important pieces of information. First and foremost
 current player, and it has a random generator.
 -/
 
-open Batteries (HashMap)
+open Std (HashMap)
 abbrev TileIndex := Nat × Nat -- a 2D index
 
 inductive TileState where

doc/quickstart.md

@@ -1,23 +1,55 @@
 # Quickstart
 
-These instructions will walk you through setting up Lean 4 together with VS Code as an editor for Lean 4.
-See [Setup](./setup.md) for supported platforms and other ways to set up Lean 4.
+These instructions will walk you through setting up Lean using the "basic" setup and VS Code as the editor.
+See [Setup](./setup.md) for other ways, supported platforms, and more details on setting up Lean.
+
+See quick [walkthrough demo video](https://www.youtube.com/watch?v=yZo6k48L0VY).
 
 1. Install [VS Code](https://code.visualstudio.com/).
 
-1. Launch VS Code and install the `Lean 4` extension by clicking on the 'Extensions' sidebar entry and searching for 'Lean 4'.
+1. Launch VS Code and install the `lean4` extension.
 
-   ![installing the vscode-lean4 extension](images/code-ext.png)
+    ![installing the vscode-lean4 extension](images/code-ext.png)
 
-1. Open the Lean 4 setup guide by creating a new text file using 'File > New Text File' (`Ctrl+N` / `Cmd+N`), clicking on the ∀-symbol in the top right and selecting 'Documentation… > Docs: Show Setup Guide'.
+1. Create a new file using "File > New Text File" (`Ctrl+N`). Click the `Select a language` prompt, type in `lean4`, and hit ENTER.  You should see the following popup:
+    ![elan](images/install_elan.png)
 
-   ![show setup guide](images/show-setup-guide.png)
+    Click the "Install Lean using Elan" button. You should see some progress output like this:
 
-1. Follow the Lean 4 setup guide. It will:
+    ```
+    info: syncing channel updates for 'stable'
+    info: latest update on stable, lean version v4.0.0
+    info: downloading component 'lean'
+    ```
+    If there is no popup, you probably have Elan installed already.
+    You may want to make sure that your default toolchain is Lean 4 in this case by running `elan default leanprover/lean4:stable` and reopen the file, as the next step will fail otherwise.
 
-   - walk you through learning resources for Lean,
-   - teach you how to set up Lean's dependencies on your platform,
-   - install Lean 4 for you at the click of a button,
-   - help you set up your first project.
+1. While it is installing, you can paste the following Lean program into the new file:
 
-   ![setup guide](images/setup_guide.png)
+    ```lean
+    #eval Lean.versionString
+    ```
+
+    When the installation has finished, the Lean Language Server should start automatically and you should get syntax-highlighting and a "Lean Infoview" popping up on the right.  You will see the output of the `#eval` statement when
+    you place your cursor at the end of the statement.
+
+    ![successful setup](images/code-success.png)
+
+You are set up!
+
+## Create a Lean Project
+
+*If your goal is to contribute to [mathlib4](https://github.com/leanprover-community/mathlib4) or use it as a dependency, please see its readme for specific instructions on how to do that.*
+
+You can now create a Lean project in a new folder. Run `lake init foo` from "View > Terminal" to create a package, followed by `lake build` to get an executable version of your Lean program.
+On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.
+
+Note: Packages **have** to be opened using "File > Open Folder..." for imports to work.
+Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (`Ctrl+Shift+X`).
+
+## Troubleshooting
+
+**The InfoView says "Waiting for Lean server to start..." forever.**
+
+Check that the VS Code Terminal is not showing some installation errors from `elan`.
+If that doesn't work, try also running the VS Code command `Developer: Reload Window`.

doc/setup.md

@@ -2,21 +2,21 @@
 
 ### Tier 1
 
-Platforms built & tested by our CI, available as binary releases via elan (see below)
+Platforms built & tested by our CI, available as nightly releases via elan (see below)
 
 * x86-64 Linux with glibc 2.27+
 * x86-64 macOS 10.15+
-* aarch64 (Apple Silicon) macOS 10.15+
-* x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022
+* x86-64 Windows 10+
 
 ### Tier 2
 
-Platforms cross-compiled but not tested by our CI, available as binary releases
+Platforms cross-compiled but not tested by our CI, available as nightly releases
 
 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
 
@@ -50,10 +50,10 @@ Foo.lean       # main file, import via `import Foo`
 Foo/
   A.lean       # further files, import via e.g. `import Foo.A`
   A/...        # further nesting
-.lake/         # `lake` build output directory
+build/         # `lake` build output directory
 ```
 
-After running `lake build` you will see a binary named `./.lake/build/bin/foo` and when you run it you should see the output:
+After running `lake build` you will see a binary named `./build/bin/foo` and when you run it you should see the output:
 ```
 Hello, world!
 ```

doc/setup/nix.md

@@ -0,0 +1,71 @@
+# Nix Setup
+
+An alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension.
+However, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling [Nix Flakes](https://www.tweag.io/blog/2020-05-25-flakes/). The setup has been tested on NixOS, other Linux distributions, and macOS.
+
+After installing (any version of) Nix (<https://nixos.org/download.html>), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
+```bash
+$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
+```
+While this shell is sufficient for executing the steps below, it is recommended to also set the following options in `/etc/nix/nix.conf` (`nix.extraOptions` in NixOS):
+```
+max-jobs = auto  # Allow building multiple derivations in parallel
+keep-outputs = true  # Do not garbage-collect build time-only dependencies (e.g. clang)
+# Allow fetching build results from the Lean Cachix cache
+trusted-substituters = https://lean4.cachix.org/
+trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=
+```
+On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:
+```bash
+sudo pkill nix-daemon
+```
+
+The [Cachix](https://cachix.org/) integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above.
+It can be set up analogously as a cache for your own project.
+
+Note: Your system Nix might print warnings about not knowing some of the settings used by the Lean shell Nix, which can be ignored.
+
+## Basic Commands
+
+From a Lean shell, run
+```bash
+$ nix flake new mypkg -t github:leanprover/lean4
+```
+to create a new Lean package in directory `mypkg` using the latest commit of Lean 4.
+Such packages follow the same directory layout as described in the standard setup, except for a `lakefile.lean` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
+```bash
+$ nix build  # build package and all dependencies
+$ nix build .#executable  # compile `main` definition into executable (after you've added one)
+$ nix run .#emacs-dev  # open a pinned version of Emacs with lean4-mode fully set up
+$ nix run .#emacs-dev MyPackage.lean  # arguments can be passed as well, e.g. the file to open
+$ nix run .#vscode-dev MyPackage.lean  # ditto, using VS Code
+```
+Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
+Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix.
+
+As in the standard setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command.
+
+If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the `lean` wrapper script the commands above use internally:
+```bash
+$ nix build .#lean-dev -o result-lean-dev
+```
+The resulting `./result-lean-dev/bin/lean` script essentially runs `nix run .#lean` in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed.
+This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](./make/nix.md#editor-integration).
+
+Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: <https://github.com/Kha/testpkg2/blob/master/flake.nix#L5>
+
+For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
+```bash
+$ nix build --override-input somedep path/to/somedep
+```
+
+On a build error, Nix will show the last 10 lines of the output by default. You can pass `-L` to `nix build` to show all lines, or pass the shown `*.drv` path to `nix log` to show the full log after the fact.
+
+Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when `/nix/store/` has grown too large:
+```bash
+nix-collect-garbage
+```
+This will remove everything not reachable from "GC roots" such as the `./result` symlink created by `nix build`.
+
+Note that the package information in `flake.nix` is currently completely independent from `lakefile.lean` used in the standard setup.
+Unifying the two formats is TBD.

doc/syntax_highlight_in_latex.md

@@ -43,8 +43,7 @@ $ pdflatex test.tex
 
 ## Example with `minted`
 
-First [install Pygments](https://pygments.org/download/) (version 2.18 or newer).
-Then save the following sample LaTeX file `test.tex` into the same directory:
+First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`](https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lean4.py), which contains an version of the Lean highlighter updated for Lean 4, and the following sample LaTeX file `test.tex` into the same directory:
 
 ```latex
 \documentclass{article}
@@ -52,8 +51,9 @@ Then save the following sample LaTeX file `test.tex` into the same directory:
 % switch to a monospace font supporting more Unicode characters
 \setmonofont{FreeMono}
 \usepackage{minted}
-\newmintinline[lean]{lean4}{bgcolor=white}
-\newminted[leancode]{lean4}{fontsize=\footnotesize}
+% instruct minted to use our local theorem.py
+\newmintinline[lean]{lean4.py:Lean4Lexer -x}{bgcolor=white}
+\newminted[leancode]{lean4.py:Lean4Lexer -x}{fontsize=\footnotesize}
 \usemintedstyle{tango}  % a nice, colorful theme
 
 \begin{document}
@@ -78,14 +78,11 @@ Some remarks:
  - either `xelatex` or `lualatex` is required to handle Unicode characters in the code.
  - `--shell-escape` is needed to allow `xelatex` to execute `pygmentize` in a shell.
  - If the chosen monospace font is missing some Unicode symbols, you can direct them to be displayed using a fallback font or other replacement LaTeX code.
-   ``` latex
-   \usepackage{newunicodechar}
-   \newfontfamily{\freeserif}{DejaVu Sans}
-   \newunicodechar{✝}{\freeserif{✝}}
-   \newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
-   ```
- - If you are using an old version of Pygments, you can copy 
-   [`lean.py`](https://raw.githubusercontent.com/pygments/pygments/master/pygments/lexers/lean.py) into your working directory,
-   and use `lean4.py:Lean4Lexer -x` instead of `lean4` above.
-   If your version of `minted` is v2.7 or newer, but before v3.0,
-   you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
+``` latex
+\usepackage{newunicodechar}
+\newfontfamily{\freeserif}{DejaVu Sans}
+\newunicodechar{✝}{\freeserif{✝}}
+\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
+```
+ - minted has a "helpful" feature that draws red boxes around characters the chosen lexer doesn't recognize.
+ Since the Lean lexer cannot encompass all user-defined syntax, it is advisable to [work around](https://tex.stackexchange.com/a/343506/14563) this feature.

doc/tour.md

@@ -15,7 +15,7 @@ The most fundamental pieces of any Lean program are functions organized into nam
 [Functions](./functions.md) perform work on inputs to produce outputs,
 and they are organized under [namespaces](./namespaces.md),
 which are the primary way you group things in Lean.
-They are defined using the `def` command,
+They are defined using the [`def`](./definitions.md) command,
 which give the function a name and define its arguments.
 
 ```lean

doc/typeclass.md

@@ -99,11 +99,11 @@ Let us start with the first step of the program above, declaring an appropriate
 
 ```lean
 # namespace Ex
-class Inhabited (a : Sort u) where
+class Inhabited (a : Type u) where
   default : a
 
 #check @Inhabited.default
--- Inhabited.default : {a : Sort u} → [self : Inhabited a] → a
+-- Inhabited.default : {a : Type u} → [self : Inhabited a] → a
 # end Ex
 ```
 Note `Inhabited.default` doesn't have any explicit argument.
@@ -114,7 +114,7 @@ Now we populate the class with some instances:
 
 ```lean
 # namespace Ex
-# class Inhabited (a : Sort _) where
+# class Inhabited (a : Type _) where
 #  default : a
 instance : Inhabited Bool where
   default := true
@@ -138,7 +138,7 @@ instance : Inhabited Prop where
 You can use the command `export` to create the alias `default` for `Inhabited.default`
 ```lean
 # namespace Ex
-# class Inhabited (a : Sort _) where
+# class Inhabited (a : Type _) where
 #  default : a
 # instance : Inhabited Bool where
 #  default := true
@@ -174,7 +174,7 @@ instance [Inhabited a] [Inhabited b] : Inhabited (a × b) where
 With this added to the earlier instance declarations, type class instance can infer, for example, a default element of ``Nat × Bool``:
 ```lean
 # namespace Ex
-# class Inhabited (a : Sort u) where
+# class Inhabited (a : Type u) where
 #  default : a
 # instance : Inhabited Bool where
 #  default := true
@@ -191,14 +191,8 @@ instance [Inhabited a] [Inhabited b] : Inhabited (a × b) where
 ```
 Similarly, we can inhabit type function with suitable constant functions:
 ```lean
-# namespace Ex
-# class Inhabited (a : Sort u) where
-#  default : a
-# opaque default [Inhabited a] : a :=
-#  Inhabited.default
 instance [Inhabited b] : Inhabited (a -> b) where
   default := fun _ => default
-# end Ex
 ```
 As an exercise, try defining default instances for other types, such as `List` and `Sum` types.
 

doc/whatIsLean.md

@@ -37,6 +37,6 @@ Lean has numerous features, including:
 - [Extensible syntax](./syntax.md)
 - Hygienic macros
 - [Dependent types](https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html)
-- [Metaprogramming](./macro_overview.md)
+- [Metaprogramming](./metaprogramming.md)
 - Multithreading
 - Verification: you can prove properties of your functions using Lean itself

flake.lock

@@ -1,15 +1,12 @@
 {
   "nodes": {
     "flake-utils": {
-      "inputs": {
-        "systems": "systems"
-      },
       "locked": {
-        "lastModified": 1710146030,
-        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "lastModified": 1656928814,
+        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
         "type": "github"
       },
       "original": {
@@ -18,13 +15,97 @@
         "type": "github"
       }
     },
+    "lean4-mode": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1676498134,
+        "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
+        "owner": "leanprover",
+        "repo": "lean4-mode",
+        "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover",
+        "repo": "lean4-mode",
+        "type": "github"
+      }
+    },
+    "lowdown-src": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1633514407,
+        "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
+        "owner": "kristapsdz",
+        "repo": "lowdown",
+        "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
+        "type": "github"
+      },
+      "original": {
+        "owner": "kristapsdz",
+        "repo": "lowdown",
+        "type": "github"
+      }
+    },
+    "nix": {
+      "inputs": {
+        "lowdown-src": "lowdown-src",
+        "nixpkgs": "nixpkgs",
+        "nixpkgs-regression": "nixpkgs-regression"
+      },
+      "locked": {
+        "lastModified": 1657097207,
+        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
+        "owner": "NixOS",
+        "repo": "nix",
+        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nix",
+        "type": "github"
+      }
+    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1710889954,
-        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
+        "lastModified": 1653988320,
+        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
+        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-22.05-small",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-regression": {
+      "locked": {
+        "lastModified": 1643052045,
+        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1686089707,
+        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
         "type": "github"
       },
       "original": {
@@ -34,60 +115,12 @@
         "type": "github"
       }
     },
-    "nixpkgs-cadical": {
-      "locked": {
-        "lastModified": 1722221733,
-        "narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
-        "type": "github"
-      }
-    },
-    "nixpkgs-old": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1581379743,
-        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-19.03",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "root": {
       "inputs": {
         "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-cadical": "nixpkgs-cadical",
-        "nixpkgs-old": "nixpkgs-old"
-      }
-    },
-    "systems": {
-      "locked": {
-        "lastModified": 1681028828,
-        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
-        "owner": "nix-systems",
-        "repo": "default",
-        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-systems",
-        "repo": "default",
-        "type": "github"
+        "lean4-mode": "lean4-mode",
+        "nix": "nix",
+        "nixpkgs": "nixpkgs_2"
       }
     }
   },

flake.nix

@@ -1,77 +1,63 @@
 {
-  description = "Lean development flake. Not intended for end users.";
+  description = "Lean interactive theorem prover";
 
   inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
-  # old nixpkgs used for portable release with older glibc (2.27)
-  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
-  inputs.nixpkgs-old.flake = false;
-  # for cadical 1.9.5; sync with CMakeLists.txt
-  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/12bf09802d77264e441f48e25459c10c93eada2e";
   inputs.flake-utils.url = "github:numtide/flake-utils";
+  inputs.nix.url = "github:NixOS/nix";
+  inputs.lean4-mode = {
+    url = "github:leanprover/lean4-mode";
+    flake = false;
+  };
+  # used *only* by `stage0-from-input` below
+  #inputs.lean-stage0 = {
+  #  url = github:leanprover/lean4;
+  #  inputs.nixpkgs.follows = "nixpkgs";
+  #  inputs.flake-utils.follows = "flake-utils";
+  #  inputs.nix.follows = "nix";
+  #  inputs.lean4-mode.follows = "lean4-mode";
+  #};
 
-  outputs = { self, nixpkgs, nixpkgs-old, flake-utils, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
+  outputs = { self, nixpkgs, flake-utils, nix, lean4-mode, ... }@inputs: flake-utils.lib.eachDefaultSystem (system:
     let
-      pkgs = import nixpkgs { inherit system; };
-      # An old nixpkgs for creating releases with an old glibc
-      pkgsDist-old = import nixpkgs-old { inherit system; };
-      # An old nixpkgs for creating releases with an old glibc
-      pkgsDist-old-aarch = import nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
-      pkgsCadical = import inputs.nixpkgs-cadical { inherit system; };
-      cadical = if pkgs.stdenv.isLinux then
-        # use statically-linked cadical on Linux to avoid glibc versioning troubles
-        pkgsCadical.pkgsStatic.cadical.overrideAttrs { doCheck = false; }
-      else pkgsCadical.cadical;
-
-      lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
-
-      devShellWithDist = pkgsDist: pkgs.mkShell.override {
-          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
-        } ({
-          buildInputs = with pkgs; [
-            cmake gmp libuv ccache cadical
-            lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
-            gdb
-            tree  # for CI
-          ];
-          # https://github.com/NixOS/nixpkgs/issues/60919
-          hardeningDisable = [ "all" ];
-          # more convenient `ctest` output
-          CTEST_OUTPUT_ON_FAILURE = 1;
-        } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
-          GMP = (pkgsDist.gmp.override { withStatic = true; }).overrideAttrs (attrs:
-            pkgs.lib.optionalAttrs (pkgs.stdenv.system == "aarch64-linux") {
-              # would need additional linking setup on Linux aarch64, we don't use it anywhere else either
-              hardeningDisable = [ "stackprotector" ];
-            });
-          LIBUV = pkgsDist.libuv.overrideAttrs (attrs: {
-            configureFlags = ["--enable-static"];
-            hardeningDisable = [ "stackprotector" ];
-            # Sync version with CMakeLists.txt
-            version = "1.48.0";
-            src = pkgs.fetchFromGitHub {
-              owner = "libuv";
-              repo = "libuv";
-              rev = "v1.48.0";
-              sha256 = "100nj16fg8922qg4m2hdjh62zv4p32wyrllsvqr659hdhjc03bsk";
-            };
-            doCheck = false;
-          });
-          GLIBC = pkgsDist.glibc;
-          GLIBC_DEV = pkgsDist.glibc.dev;
-          GCC_LIB = pkgsDist.gcc.cc.lib;
-          ZLIB = pkgsDist.zlib;
-          GDB = pkgsDist.gdb;
-        });
+      pkgs = import nixpkgs {
+        inherit system;
+        # for `vscode-with-extensions`
+        config.allowUnfree = true;
+      };
+      lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; inherit nix lean4-mode; };
     in {
-      packages = {
-        # to be removed when Nix CI is not needed anymore
-        inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
-        deprecated = lean-packages;
+      packages = lean-packages // rec {
+        debug = lean-packages.override { debug = true; };
+        stage0debug = lean-packages.override { stage0debug = true; };
+        asan = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address" "-DLEANC_EXTRA_FLAGS=-fsanitize=address" "-DSMALL_ALLOCATOR=OFF" "-DSYMBOLIC=OFF" ]; };
+        asandebug = asan.override { debug = true; };
+        tsan = lean-packages.override {
+          extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
+          stage0 = (lean-packages.override {
+            # Compressed headers currently trigger data race reports in tsan.
+            # Turn them off for stage 0 as well so stage 1 can read its own stdlib.
+            extraCMakeFlags = [ "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
+          }).stage1;
+        };
+        tsandebug = tsan.override { debug = true; };
+        stage0-from-input = lean-packages.override {
+          stage0 = pkgs.writeShellScriptBin "lean" ''
+            exec ${inputs.lean-stage0.packages.${system}.lean}/bin/lean -Dinterpreter.prefer_native=false "$@"
+          '';
+        };
+        inherit self;
+      };
+      defaultPackage = lean-packages.lean-all;
+
+      inherit (lean-packages) devShell;
+
+      checks.lean = lean-packages.test;
+    }) // rec {
+      templates.pkg = {
+        path = ./nix/templates/pkg;
+        description = "A custom Lean package";
       };
 
-      # The default development shell for working on lean itself
-      devShells.default = devShellWithDist pkgs;
-      devShells.oldGlibc = devShellWithDist pkgsDist-old;
-      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
-    });
+      defaultTemplate = templates.pkg;
+    };
 }

lean.code-workspace

@@ -13,8 +13,6 @@
 	"settings": {
 		"files.insertFinalNewline": true,
 		"files.trimTrailingWhitespace": true,
-		"cmake.buildDirectory": "${workspaceFolder}/build/release",
-		"cmake.generator": "Unix Makefiles",
 		"[markdown]": {
 			"rewrap.wrappingColumn": 70
 		},
@@ -48,10 +46,5 @@
 				}
 			}
 		]
-	},
-	"extensions": {
-		"recommendations": [
-			"leanprover.lean4"
-		]
 	}
 }

nix/bootstrap.nix

@@ -1,13 +1,13 @@
 { src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
+  stdenv, lib, cmake, gmp, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
   ... } @ args:
 with builtins;
-lib.warn "The Nix-based build is deprecated" rec {
+rec {
   inherit stdenv;
   sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
   buildCMake = args: stdenv.mkDerivation ({
     nativeBuildInputs = [ cmake ];
-    buildInputs = [ gmp libuv llvmPackages.llvm ];
+    buildInputs = [ gmp llvmPackages.llvm ];
     # https://github.com/NixOS/nixpkgs/issues/60919
     hardeningDisable = [ "all" ];
     dontStrip = (args.debug or debug);
@@ -17,7 +17,7 @@ lib.warn "The Nix-based build is deprecated" rec {
     '';
   } // args // {
     src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
-    cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
+    cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
     preConfigure = args.preConfigure or "" + ''
       # ignore absence of submodule
       sed -i 's!lake/Lake.lean!!' CMakeLists.txt
@@ -26,7 +26,11 @@ lib.warn "The Nix-based build is deprecated" rec {
   lean-bin-tools-unwrapped = buildCMake {
     name = "lean-bin-tools";
     outputs = [ "out" "leanc_src" ];
-    realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "[a-z].*" ".*\.in" "Leanc\.lean" ];
+    realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "cmake.*" "bin.*" "include.*" ".*\.in" "Leanc\.lean" ];
+    preConfigure = ''
+      touch empty.cpp
+      sed -i 's/add_subdirectory.*//;s/set(LEAN_OBJS.*/set(LEAN_OBJS empty.cpp)/' CMakeLists.txt
+    '';
     dontBuild = true;
     installPhase = ''
       mkdir $out $leanc_src
@@ -41,10 +45,11 @@ lib.warn "The Nix-based build is deprecated" rec {
   leancpp = buildCMake {
     name = "leancpp";
     src = src + "/src";
-    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "leanshell" "leanmain" ];
+    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" ];
     installPhase = ''
       mkdir -p $out
       mv lib/ $out/
+      mv shell/CMakeFiles/shell.dir/lean.cpp.o $out/lib
       mv runtime/libleanrt_initial-exec.a $out/lib
     '';
   };
@@ -60,7 +65,12 @@ lib.warn "The Nix-based build is deprecated" rec {
     installPhase = ''
       mkdir -p $out/bin $out/lib/lean
       mv bin/lean $out/bin/
-      mv lib/lean/*.{so,dylib} $out/lib/lean
+      mv lib/lean/libleanshared.* $out/lib/lean
+   '' + lib.optionalString stdenv.isDarwin ''
+      for lib in $(otool -L $out/bin/lean | tail -n +2 | cut -d' ' -f1); do
+        if [[ "$lib" == *lean* ]]; then install_name_tool -change "$lib" "$out/lib/lean/$(basename $lib)" $out/bin/lean; fi
+      done
+      otool -L $out/bin/lean
     '';
     meta.mainProgram = "lean";
   });
@@ -73,17 +83,16 @@ lib.warn "The Nix-based build is deprecated" rec {
         # use same stage for retrieving dependencies
         lean-leanDeps = stage0;
         lean-final = self;
+        leanFlags = [ "-DwarningAsError=true" ];
       } ({
         src = src + "/src";
         roots = [ { mod = args.name; glob = "andSubmodules"; } ];
         fullSrc = src;
         srcPath = "$PWD/src:$PWD/src/lake";
         inherit debug;
-        leanFlags = [ "-DwarningAsError=true" ];
       } // args);
       Init' = build { name = "Init"; deps = []; };
-      Std' = build { name = "Std"; deps = [ Init' ]; };
-      Lean' = build { name = "Lean"; deps = [ Std' ]; };
+      Lean' = build { name = "Lean"; deps = [ Init' ]; };
       attachSharedLib = sharedLib: pkg: pkg // {
         inherit sharedLib;
         mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
@@ -91,61 +100,49 @@ lib.warn "The Nix-based build is deprecated" rec {
     in (all: all // all.lean) rec {
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
       Init = attachSharedLib leanshared Init';
-      Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
-      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
+      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
       Lake = build {
         name = "Lake";
-        sharedLibName = "Lake_shared";
         src = src + "/src/lake";
         deps = [ Init Lean ];
       };
       Lake-Main = build {
-        name = "LakeMain";
-        roots = [{ glob = "one"; mod = "LakeMain"; }];
+        name = "Lake.Main";
+        roots = [ "Lake.Main" ];
         executableName = "lake";
         deps = [ Lake ];
         linkFlags = lib.optional stdenv.isLinux "-rdynamic";
         src = src + "/src/lake";
       };
-      stdlib = [ Init Std Lean Lake ];
+      stdlib = [ Init Lean Lake ];
       modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
       depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
-      libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
-        mkdir $out
-        touch empty.c
-        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
-      '';
-      leanshared_1 = runCommand "leanshared_1" { buildInputs = [ stdenv.cc ]; libName = "leanshared_1${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
-        mkdir $out
-        touch empty.c
-        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
-      '';
+      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
         LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
-          -Wl,--whole-archive ${leancpp}/lib/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ \
-          -lm ${stdlibLinkFlags} \
+          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
+            else "-Wl,--whole-archive -lInit -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';
       mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
       print-paths = Lean.makePrintPathsFor [] mods;
       leanc = writeShellScriptBin "leanc" ''
-        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} -L${Lake.sharedLib} "$@"
+        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@"
       '';
       lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
         mkdir -p $out/bin
-        ${leanc}/bin/leanc ${leancpp}/lib/temp/libleanmain.a ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* -o $out/bin/lean
+        ${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean
       '';
       # derivation following the directory layout of the "basic" setup, mostly useful for running tests
       lean-all = stdenv.mkDerivation {
         name = "lean-${desc}";
         buildCommand = ''
           mkdir -p $out/bin $out/lib/lean
-          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* ${Lake.sharedLib}/* $out/lib/lean/
+          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${leanshared}/* $out/lib/lean/
           # put everything in a single final derivation so `IO.appDir` references work
           cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
           # NOTE: `lndir` will not override existing `bin/leanc`
@@ -153,13 +150,15 @@ lib.warn "The Nix-based build is deprecated" rec {
         '';
         meta.mainProgram = "lean";
       };
-      cacheRoots = linkFarmFromDrvs "cacheRoots" ([
+      cacheRoots = linkFarmFromDrvs "cacheRoots" [
         stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
-      ] ++ map (lib: lib.oTree) stdlib);
+        # .o files are not a runtime dependency on macOS because of lack of thin archives
+        Lean.oTree Lake.oTree
+      ];
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
-        buildInputs = [ gmp libuv perl git cadical ];
+        buildInputs = [ gmp perl git ];
         preConfigure = ''
           cd src
         '';
@@ -170,17 +169,16 @@ lib.warn "The Nix-based build is deprecated" rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-         ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
+          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
-          mkdir $out
-          mv test-results.xml $out
+          touch $out
         '';
       };
       update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) (stdlib ++ [Lake-Main]); }; in
+        let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
         writeShellScriptBin "update-stage0" ''
-          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
+          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"}
         '';
       update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
         set -euo pipefail

nix/buildLeanPackage.nix

@@ -1,16 +1,16 @@
 { lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
-  stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs,
+  stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, lean-vscode, nix, substituteAll, symlinkJoin, linkFarmFromDrvs,
   runCommand, darwin, mkShell, ... }:
 let lean-final' = lean-final; in
 lib.makeOverridable (
 { name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
   # Lean dependencies. Each entry should be an output of buildLeanPackage.
-  deps ? [ lean.Init lean.Std lean.Lean ],
+  deps ? [ lean.Lean ],
   # Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
   staticLibDeps ? [],
   # Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
   groupStaticLibs ? false,
-  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
+  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a 
   # shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
   # These libs are also linked to in packages that depend on this one.
   nativeSharedLibs ? [],
@@ -30,7 +30,7 @@ lib.makeOverridable (
   pluginDeps ? [],
   # `overrideAttrs` for `buildMod`
   overrideBuildModAttrs ? null,
-  debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
+  debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name,
   srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
 with builtins; let
   # "Init.Core" ~> "Init/Core"
@@ -88,9 +88,9 @@ with builtins; let
   allNativeSharedLibs =
     lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
 
-  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
+  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`, 
   # plus every dep module itself: `dep.staticLib`
-  allStaticLibDeps =
+  allStaticLibDeps = 
     lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
 
   pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
@@ -176,7 +176,7 @@ with builtins; let
       # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
       ln -s ${drv.c}/${drv.cPath} src.c
       # on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
-      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
+      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
     '';
   };
   mkMod = mod: deps:
@@ -197,6 +197,19 @@ with builtins; let
              then map (m: m.module) header.imports
              else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
     in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
+  makeEmacsWrapper = name: emacs: lean: writeShellScriptBin name ''
+    ${emacs} --eval "(progn (setq lean4-rootdir \"${lean}\"))" "$@"
+  '';
+  makeVSCodeWrapper = name: lean: writeShellScriptBin name ''
+    PATH=${lean}/bin:$PATH ${lean-vscode}/bin/code "$@"
+  '';
+  printPaths = deps: writeShellScriptBin "print-paths" ''
+    echo '${toJSON {
+      oleanPath = [(depRoot "print-paths" deps)];
+      srcPath = ["."] ++ map (dep: dep.src) allExternalDeps;
+      loadDynlibPaths = map pathOfSharedLib (loadDynlibsOfDeps deps);
+    }}'
+  '';
   expandGlob = g:
     if typeOf g == "string" then [g]
     else if g.glob == "one" then [g.mod]
@@ -211,8 +224,7 @@ with builtins; let
   allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
 
   objects   = mapAttrs (_: m: m.obj) mods';
-  bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
-  staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
+  staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
     mkdir -p $out
     ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
   '';
@@ -233,7 +245,7 @@ in rec {
   cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
   oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
   iTree     = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };
-  sharedLib = mkSharedLib "lib${sharedLibName}" ''
+  sharedLib = mkSharedLib "lib${libName}" ''
     ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
     ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
   executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
@@ -244,4 +256,48 @@ in rec {
         -o $out/bin/${executableName} \
         ${lib.concatStringsSep " " allLinkFlags}
     '') {};
+
+  lean-package = writeShellScriptBin "lean" ''
+    LEAN_PATH=${modRoot}:$LEAN_PATH LEAN_SRC_PATH=$LEAN_SRC_PATH:${src} exec ${lean-final}/bin/lean "$@"
+  '';
+  emacs-package = makeEmacsWrapper "emacs-package" lean-package;
+  vscode-package = makeVSCodeWrapper "vscode-package" lean-package;
+
+  link-ilean = writeShellScriptBin "link-ilean" ''
+    dest=''${1:-.}
+    mkdir -p $dest/build/lib
+    ln -sf ${iTree}/* $dest/build/lib
+  '';
+
+  makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods;
+  print-paths = makePrintPathsFor [] (mods' // externalModMap);
+  # `lean` wrapper that dynamically runs Nix for the actual `lean` executable so the same editor can be
+  # used for multiple projects/after upgrading the `lean` input/for editing both stage 1 and the tests
+  lean-bin-dev = substituteAll {
+    name = "lean";
+    dir = "bin";
+    src = ./lean-dev.in;
+    isExecutable = true;
+    srcRoot = fullSrc;  # use root flake.nix in case of Lean repo
+    inherit bash nix srcTarget srcArgs;
+  };
+  lake-dev = substituteAll {
+    name = "lake";
+    dir = "bin";
+    src = ./lake-dev.in;
+    isExecutable = true;
+    srcRoot = fullSrc;  # use root flake.nix in case of Lean repo
+    inherit bash nix srcTarget srcArgs;
+  };
+  lean-dev = symlinkJoin { name = "lean-dev"; paths = [ lean-bin-dev lake-dev ]; };
+  emacs-dev = makeEmacsWrapper "emacs-dev" "${lean-emacs}/bin/emacs" lean-dev;
+  emacs-path-dev = makeEmacsWrapper "emacs-path-dev" "emacs" lean-dev;
+  vscode-dev = makeVSCodeWrapper "vscode-dev" lean-dev;
+
+  devShell = mkShell {
+    buildInputs = [ nix ];
+    shellHook = ''
+      export LEAN_SRC_PATH="${srcPath}"
+    '';
+  };
 })

nix/packages.nix

@@ -1,6 +1,9 @@
-{ src, pkgs, ... } @ args:
+{ src, pkgs, nix, ... } @ args:
 with pkgs;
 let
+  nix-pinned = writeShellScriptBin "nix" ''
+    ${nix.packages.${system}.default}/bin/nix --experimental-features 'nix-command flakes' --extra-substituters https://lean4.cachix.org/ --option warn-dirty false "$@"
+  '';
   # https://github.com/NixOS/nixpkgs/issues/130963
   llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15;
   cc = (ccacheWrapper.override rec {
@@ -39,9 +42,40 @@ let
     inherit (lean) stdenv;
     lean = lean.stage1;
     inherit (lean.stage1) leanc;
+    inherit lean-emacs lean-vscode;
+    nix = nix-pinned;
   }));
+  lean4-mode = emacsPackages.melpaBuild {
+    pname = "lean4-mode";
+    version = "1";
+    commit = "1";
+    src = args.lean4-mode;
+    packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash f flycheck magit-section lsp-mode s ];
+    recipe = pkgs.writeText "recipe" ''
+      (lean4-mode
+       :repo "leanprover/lean4-mode"
+       :fetcher github
+       :files ("*.el" "data"))
+    '';
+  };
+  lean-emacs = emacsWithPackages [ lean4-mode ];
+  # updating might be nicer by building from source from a flake input, but this is good enough for now
+  vscode-lean4 = vscode-utils.extensionFromVscodeMarketplace {
+      name = "lean4";
+      publisher = "leanprover";
+      version = "0.0.63";
+      sha256 = "sha256-kjEex7L0F2P4pMdXi4NIZ1y59ywJVubqDqsoYagZNkI=";
+  };
+  lean-vscode = vscode-with-extensions.override {
+    vscodeExtensions = [ vscode-lean4 ];
+  };
 in {
-  inherit cc buildLeanPackage llvmPackages;
+  inherit cc lean4-mode buildLeanPackage llvmPackages vscode-lean4;
+  lean = lean.stage1;
+  stage0print-paths = lean.stage1.Lean.print-paths;
+  HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcTarget = "..#stage0-from-input.stage0"; srcArgs = "(--override-input lean-stage0 ..\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
+  HEAD-as-stage1 = (lean.stage1.Lean.overrideArgs { srcTarget = "..\?rev=$(git rev-parse HEAD)#stage0"; });
+  nix = nix-pinned;
   nixpkgs = pkgs;
   ciShell = writeShellScriptBin "ciShell" ''
     set -o pipefail
@@ -49,4 +83,5 @@ in {
     # prefix lines with cumulative and individual execution time
     "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
   '';
-} // lean.stage1
+  vscode = lean-vscode;
+} // lean.stage1.Lean // lean.stage1 // lean

releases_drafts/README.md

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

script/apply.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
 import Lean.Runtime
 
 abbrev M := ReaderT IO.FS.Stream IO
@@ -21,7 +16,7 @@ def mkTypedefFn (i : Nat) : M Unit := do
   emit s!"typedef obj* (*fn{i})({args}); // NOLINT\n"
   emit s!"#define FN{i}(f) reinterpret_cast<fn{i}>(lean_closure_fun(f))\n"
 
-def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String :=
+def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String := 
   List.range n |>.map f |>.intersperse sep |> .join
 
 -- make string: "obj* a1, obj* a2, ..., obj* an"

script/collideProfiles.lean

@@ -1,28 +0,0 @@
-import Lean.Util.Profiler
-
-/-!
-
-Usage:
-```sh
-lean --run ./script/collideProfiles.lean **/*.lean.json ... > merged.json
-```
-
-Merges multiple `trace.profiler.output` profiles into a single one while deduplicating samples with
-the same stack. This is useful for building cumulative profiles of medium-to-large projects because
-Firefox Profiler cannot handle hundreds of tracks and the deduplication will also ensure that the
-profile is small enough for uploading.
-
-As ordering of samples is not meaningful after this transformation, only "Call Tree" and "Flame
-Graph" are useful for such profiles.
--/
-
-open Lean
-
-def main (args : List String) : IO Unit := do
-  let profiles ← args.toArray.mapM fun path => do
-    let json ← IO.FS.readFile ⟨path⟩
-    let profile ← IO.ofExcept $ Json.parse json
-    IO.ofExcept <| fromJson? profile
-  -- NOTE: `collide` should not be interpreted
-  let profile := Firefox.Profile.collide profiles
-  IO.println <| Json.compress <| toJson profile

script/issues_summary.sh

@@ -1,39 +0,0 @@
-#!/bin/bash
-
-# https://chat.openai.com/share/7469c7c3-aceb-4d80-aee5-62982e1f1538
-
-# Output CSV Header
-echo '"Issue URL","Title","Days Since Creation","Days Since Last Update","Total Reactions","Assignee","Labels"'
-
-# Get the current date in YYYY-MM-DD format
-today=$(date +%Y-%m-%d)
-
-# Fetch only open issues (excluding PRs and closed issues) from the repository 'leanprover/lean4'
-issues=$(gh api repos/leanprover/lean4/issues --paginate --jq '.[] | select(.pull_request == null and .state == "open") | {url: .html_url, title: .title, created_at: (.created_at | split("T")[0]), updated_at: (.updated_at | split("T")[0]), number: .number, assignee: (.assignee.login // ""), labels: [.labels[].name] | join(",")}')
-
-# Process each JSON object
-echo "$issues" | while IFS= read -r issue; do
-    # Extract fields from JSON
-    url=$(echo "$issue" | jq -r '.url')
-    title=$(echo "$issue" | jq -r '.title')
-    created_at=$(echo "$issue" | jq -r '.created_at')
-    updated_at=$(echo "$issue" | jq -r '.updated_at')
-    issue_number=$(echo "$issue" | jq -r '.number')
-    assignee=$(echo "$issue" | jq -r '.assignee')
-    labels=$(echo "$issue" | jq -r '.labels')
-
-    # Calculate days since creation and update using macOS compatible date calculation
-    days_since_created=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$created_at" +%s)) / 86400 ))
-    days_since_updated=$(( ($(date -jf "%Y-%m-%d" "$today" +%s) - $(date -jf "%Y-%m-%d" "$updated_at" +%s)) / 86400 ))
-
-    # Fetch the total number of reactions for each issue
-    reaction_data=$(gh api repos/leanprover/lean4/issues/$issue_number/reactions --paginate --jq 'length' 2>&1)
-    if [[ $reaction_data == *"Not Found"* ]]; then
-        total_reactions="Error fetching reactions"
-    else
-        total_reactions=$reaction_data
-    fi
-
-    # Format output as CSV by escaping quotes and delimiting with commas
-    echo "\"$url\",\"${title//\"/\"\"}\",\"$days_since_created\",\"$days_since_updated\",\"$total_reactions\",\"$assignee\",\"$labels\""
-done

script/lib/README.md

@@ -1,2 +0,0 @@
-This directory contains various scripts that are *not* meant to be called
-directly, but through other scripts or makefiles.

script/lib/rebase-editor.sh

@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-
-
-# Script internal to `./script/rebase-stage0.sh`
-
-# Determine OS type for sed in-place editing
-SED_CMD=("sed" "-i")
-if [[ "$OSTYPE" == "darwin"* ]]
-then
-    # macOS requires an empty string argument with -i for in-place editing
-    SED_CMD=("sed" "-i" "")
-fi
-
-if [ "$STAGE0_WITH_NIX" = true ]
-then
-  "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x nix run .#update-stage0-commit,' "$1"
-else
-  "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x make -j32 -C build/release update-stage0 \&\& git commit -m "chore: update stage0",' "$1"
-fi

script/lib/update-stage0

@@ -1,33 +0,0 @@
-#!/usr/bin/env bash
-set -euo pipefail
-
-rm -r stage0 || true
-# don't copy untracked files
-# `:!` is git glob flavor for exclude patterns
-for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do
-    if [[ $f == *.lean ]]; then
-        f=${f#src/}
-        f=${f%.lean}.c
-        mkdir -p $(dirname stage0/stdlib/$f)
-        cp ${CP_C_PARAMS:-} $CSRCS/$f stage0/stdlib/$f
-    else
-        mkdir -p $(dirname stage0/$f)
-        cp $f stage0/$f
-    fi
-done
-
-# special handling for Lake files due to its nested directory
-# copy the README to ensure the `stage0/src/lake` directory is committed
-for f in $(git ls-files 'src/lake/Lake/*' src/lake/Lake.lean src/lake/LakeMain.lean src/lake/README.md ':!:src/lakefile.toml'); do
-    if [[ $f == *.lean ]]; then
-        f=${f#src/lake}
-        f=${f%.lean}.c
-        mkdir -p $(dirname stage0/stdlib/$f)
-        cp ${CP_C_PARAMS:-} $CSRCS/$f stage0/stdlib/$f
-    else
-        mkdir -p $(dirname stage0/$f)
-        cp $f stage0/$f
-    fi
-done
-
-git add stage0

script/mathlib-bench

@@ -1,12 +0,0 @@
-#! /bin/env bash
-# Open a Mathlib4 PR for benchmarking a given Lean 4 PR
-
-set -euo pipefail
-
-[ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
-
-LEAN_PR=$1
-PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
-PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
-echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
-gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null

script/most-recent-nightly-tag.sh

@@ -0,0 +1,16 @@
+#!/bin/bash
+
+# Prefix for tags to search for
+tag_prefix="nightly-"
+
+# Fetch all tags from the remote repository
+git fetch https://github.com/leanprover/lean4-nightly.git --tags > /dev/null
+
+# Get the most recent commit that has a matching tag
+tag_name=$(git tag --merged HEAD --list "${tag_prefix}*" | sort -rV | head -n 1 | sed "s/^$tag_prefix//")
+
+if [ -z "$tag_name" ]; then
+    exit 1
+fi
+
+echo "$tag_name"

script/prepare-llvm-linux.sh

@@ -25,8 +25,6 @@ cp -L llvm/bin/llvm-ar stage1/bin/
 # dependencies of the above
 $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/
 $CP $ZLIB/lib/libz.so* stage1/lib/
-# general clang++ dependency, breaks cross-library C++ exceptions if linked statically
-$CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/
 # bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run)
 $CP $GCC_LIB/lib/libatomic.so* stage1/lib/
 
@@ -38,7 +36,7 @@ $CP $GLIBC/lib/*crt* llvm/lib/
 $CP $GLIBC/lib/*crt* stage1/lib/
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
-$CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
+$CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a stage1/lib/
 # LLVM 15 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
 # but clang-15 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
@@ -48,8 +46,6 @@ $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/
 $CP -r llvm/include/*-*-* llvm-host/include/
 # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
 $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
-# libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function.
-$CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc
 for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
 OPTIONS=()
 echo -n " -DLEAN_STANDALONE=ON"
@@ -64,8 +60,8 @@ fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
 echo -n " -DLEANC_INTERNAL_FLAGS='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests
 echo -n " -DLEAN_TEST_VARS=''"

script/prepare-llvm-macos.sh

@@ -9,7 +9,6 @@ set -uxo pipefail
 # use full LLVM release for compiling C++ code, but subset for compiling C code and distribution
 
 GMP=${GMP:-$(brew --prefix)}
-LIBUV=${LIBUV:-$(brew --prefix)}
 
 [[ -d llvm ]] || (mkdir llvm; gtar xf $1 --strip-components 1 --directory llvm)
 [[ -d llvm-host ]] || if [[ "$#" -gt 1 ]]; then
@@ -47,9 +46,8 @@ echo -n " -DLEAN_EXTRA_CXX_FLAGS='${EXTRA_FLAGS:-}'"
 if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"
   gcp $GMP/lib/libgmp.a stage1/lib/
-  gcp $LIBUV/lib/libuv.a stage1/lib/
   echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"
-  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -luv'"
+  echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp'"
 else
   echo -n " -DCMAKE_C_COMPILER=$PWD/llvm-host/bin/clang -DLEANC_OPTS='--sysroot $PWD/stage1 -resource-dir $PWD/stage1/lib/clang/15.0.1 ${EXTRA_FLAGS:-}'"
   echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/libc -fuse-ld=lld'"

script/prepare-llvm-mingw.sh

@@ -31,21 +31,15 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # runtime
 (cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1)
 # further dependencies
-# Note: even though we're linking against libraries like `libbcrypt.a` which appear to be static libraries from the file name,
-# we're not actually linking statically against the code.
-# Rather, `libbcrypt.a` is an import library (see https://en.wikipedia.org/wiki/Dynamic-link_library#Import_libraries) that just
-# tells the compiler how to dynamically link against `bcrypt.dll` (which is located in the System32 folder).
-# This distinction is relevant specifically for `libicu.a`/`icu.dll` because there we want updates to the time zone database to
-# be delivered to users via Windows Update without having to recompile Lean or Lean programs.
-cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase,psapi,iphlpapi,userenv,ws2_32,dbghelp,ole32,icu}.* /clang64/lib/libgmp.a /clang64/lib/libuv.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
+cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase}.* /clang64/lib/libgmp.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'"
 echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter /clang64/include/'"
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang.exe"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp $(pkg-config --static --libs libuv) -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
-# when not using the above flags, link GMP dynamically/as usual. Always link ICU dynamically.
-echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp $(pkg-config --libs libuv) -lucrtbase'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -static-libgcc -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -fuse-ld=lld'"
+# when not using the above flags, link GMP dynamically/as usual
+echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-lgmp -lucrtbase'"
 # do not set `LEAN_CC` for tests
 echo -n " -DAUTO_THREAD_FINALIZATION=OFF -DSTAGE0_AUTO_THREAD_FINALIZATION=OFF"
 echo -n " -DLEAN_TEST_VARS=''"

script/rebase-stage0.sh

@@ -1,24 +0,0 @@
-#!/usr/bin/env bash
-
-# This script rebases onto the given branch/commit, and updates
-# all `chore: update stage0` commits along the way.
-
-# Whether to use nix or make to update stage0
-if [ "$1" = "-nix" ]
-then
-   export STAGE0_WITH_NIX=true
-   shift
-fi
-
-# Check if an argument is provided
-if [ "$#" -eq 0 ]; then
-    echo "Usage: $0 [-nix] <options to git rebase -i>"
-    exit 1
-fi
-
-REPO_ROOT=$(git rev-parse --show-toplevel)
-
-# Run git rebase in interactive mode, but automatically edit the todo list
-# using the defined GIT_SEQUENCE_EDITOR command
-GIT_SEQUENCE_EDITOR="$REPO_ROOT/script/lib/rebase-editor.sh" git rebase -i "$@"
-

script/update-stage0

@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+rm -r stage0 || true
+# don't copy untracked files
+# `:!` is git glob flavor for exclude patterns
+for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do
+    if [[ $f == *.lean ]]; then
+        f=${f#src/}
+        f=${f%.lean}.c
+        mkdir -p $(dirname stage0/stdlib/$f)
+        cp ${CP_C_PARAMS:-} $CSRCS/$f stage0/stdlib/$f
+    else
+        mkdir -p $(dirname stage0/$f)
+        cp $f stage0/$f
+    fi
+done
+git add stage0

shell.nix

@@ -0,0 +1,27 @@
+let
+  flake = (import ./default.nix);
+  flakePkgs = flake.packages.${builtins.currentSystem};
+in { pkgs ? flakePkgs.nixpkgs, pkgsDist ? pkgs }:
+# use `shell` as default
+(attribs: attribs.shell // attribs) rec {
+  shell = pkgs.mkShell.override {
+    stdenv = pkgs.overrideCC pkgs.stdenv flakePkgs.llvmPackages.clang;
+  } (rec {
+    buildInputs = with pkgs; [
+      cmake gmp ccache
+      flakePkgs.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+    ];
+    # https://github.com/NixOS/nixpkgs/issues/60919
+    hardeningDisable = [ "all" ];
+    # more convenient `ctest` output
+    CTEST_OUTPUT_ON_FAILURE = 1;
+  } // pkgs.lib.optionalAttrs pkgs.stdenv.isLinux {
+    GMP = pkgsDist.gmp.override { withStatic = true; };
+    GLIBC = pkgsDist.glibc;
+    GLIBC_DEV = pkgsDist.glibc.dev;
+    GCC_LIB = pkgsDist.gcc.cc.lib;
+    ZLIB = pkgsDist.zlib;
+    GDB = pkgsDist.gdb;
+  });
+  nix = flake.devShell.${builtins.currentSystem};
+}