import all

This PR upstreams existing lemmas about `Vector` from Batteries.

Thanks to @fgdorais for preparing these in
https://github.com/leanprover-community/batteries/pull/1062. Further
contributions to the `Vector` API welcome via PR here.

.gitattributes

@@ -1,3 +1,6 @@
+*.lean text eol=lf
 *.expected.out -text
 RELEASES.md merge=union
 stage0/** binary linguist-generated
+# The following file is often manually edited, so do show it in diffs
+stage0/src/stdlib_flags.h -binary -linguist-generated

.github/ISSUE_TEMPLATE.md

@@ -1,30 +0,0 @@
-### Prerequisites
-
-* [ ] Put an X between the brackets on this line if you have done all of the following:
-    * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues).
-    * Reduced the issue to a self-contained, reproducible test case.
-
-### Description
-
-[Description of the issue]
-
-### Steps to Reproduce
-
-1. [First Step]
-2. [Second Step]
-3. [and so on...]
-
-**Expected behavior:** [What you expect to happen]
-
-**Actual behavior:** [What actually happens]
-
-**Reproduces how often:** [What percentage of the time does it reproduce?]
-
-### Versions
-
-You can get this information from copy and pasting the output of `lean --version`,
-please include the OS and what version of the OS you're running.
-
-### Additional Information
-
-Any additional information, configuration or data that might be necessary to reproduce the issue.

.github/ISSUE_TEMPLATE/bug_report.md

@@ -0,0 +1,51 @@
+---
+name: Bug report
+about: Create a bug report
+title: ''
+labels: bug
+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”)
+
+### Description
+
+[Clear and concise description of the issue]
+
+### 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.]
+
+### Steps to Reproduce
+
+1.
+2.
+3.
+
+**Expected behavior:** [Clear and concise description of what you expect to happen]
+
+**Actual behavior:** [Clear and concise description of what actually happens]
+
+### Versions
+
+[Output of `#version` or `#eval Lean.versionString`]
+[OS version, if not using live.lean-lang.org.]
+
+### Additional Information
+
+[Additional information, configuration or data that might be necessary to reproduce the issue]
+
+### Impact
+
+Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others are impacted by this issue, please ask them to add :+1: to it.

.github/ISSUE_TEMPLATE/rfc.md

@@ -0,0 +1,26 @@
+---
+name: Request for comments
+about: Create a feature proposal
+title: 'RFC: '
+labels: RFC
+assignees: ''
+
+---
+
+### Proposal
+
+Clear and detailed description of the proposal. Consider the following questions:
+
+  - **User Experience**: How does this feature improve the user experience?
+
+  - **Beneficiaries**: Which Lean users and projects benefit most from this feature/change?
+
+  - **Maintainability**: Will this change streamline code maintenance or simplify its structure?
+
+### Community Feedback
+
+Ideas should be discussed on [the Lean Zulip](https://leanprover.zulipchat.com) prior to submitting a proposal. Summarize all prior discussions and link them here.
+
+### Impact
+
+Add :+1: to [issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

.github/PULL_REQUEST_TEMPLATE.md

@@ -0,0 +1,21 @@
+# Read 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.
+* 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.
+
+---
+
+This PR <short changelog summary for feat/fix, see above>.
+
+Closes <`RFC` or `bug` issue number fixed by this PR, if any>

.github/dependabot.yml

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

.github/workflows/actionlint.yml

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

@@ -0,0 +1,26 @@
+name: Backport
+on:
+  pull_request_target:
+    types:
+      - closed
+      - labeled
+
+jobs:
+  backport:
+    name: Backport
+    runs-on: ubuntu-latest
+    # Only react to merged PRs for security reasons.
+    # See https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#pull_request_target.
+    if: >
+      github.event.pull_request.merged
+      && (
+        github.event.action == 'closed'
+        || (
+          github.event.action == 'labeled'
+          && contains(github.event.label.name, 'backport')
+        )
+      )
+    steps:
+      - uses: tibdex/backport@v2
+        with:
+          github_token: ${{ secrets.GITHUB_TOKEN }}

.github/workflows/check-prelude.yml

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

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

@@ -6,107 +6,275 @@ on:
     tags:
       - '*'
   pull_request:
-    branches:
-      - master
+  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 }}
+  cancel-in-progress: true
 
 jobs:
-  set-nightly:
-    # don't schedule nightlies on forks
-    if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
+
+  # This job determines various settings for the following CI runs; see the `outputs` for details
+  configure:
     runs-on: ubuntu-latest
     outputs:
-      nightly: ${{ steps.set.outputs.nightly }}
+      # 0: PRs without special label
+      # 1: PRs with `merge-ci` label, merge queue checks, master commits
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
+      check-level: ${{ steps.set-level.outputs.check-level }}
+      # The build matrix, dynamically generated here
+      matrix: ${{ steps.set-matrix.outputs.result }}
+      # Should we make a nightly release? If so, this output contains the lean version string, else it is empty
+      nightly: ${{ steps.set-nightly.outputs.nightly }}
+      # Should this be the CI for a tagged release?
+      # Yes only if a tag is pushed to the `leanprover` repository, and the tag is "v" followed by a valid semver.
+      # It sets `set-release.outputs.RELEASE_TAG` to the tag
+      # and sets `set-release.outputs.{LEAN_VERSION_MAJOR,LEAN_VERSION_MINOR,LEAN_VERSION_PATCH,LEAN_SPECIAL_VERSION_DESC}`
+      # to the semver components parsed via regex.
+      LEAN_VERSION_MAJOR: ${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}
+      LEAN_VERSION_MINOR: ${{ steps.set-release.outputs.LEAN_VERSION_MINOR }}
+      LEAN_VERSION_PATCH: ${{ steps.set-release.outputs.LEAN_VERSION_PATCH }}
+      LEAN_SPECIAL_VERSION_DESC: ${{ steps.set-release.outputs.LEAN_SPECIAL_VERSION_DESC }}
+      RELEASE_TAG: ${{ steps.set-release.outputs.RELEASE_TAG }}
+
     steps:
       - name: Checkout
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
+        # don't schedule nightlies on forks
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
       - name: Set Nightly
-        id: set
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
+        id: set-nightly
         run: |
           if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             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 "::set-output name=nightly::$LEAN_VERSION_STRING"
+            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
 
+      - name: Check for official release
+        if: startsWith(github.ref, 'refs/tags/') && github.repository == 'leanprover/lean4'
+        id: set-release
+        run: |
+          TAG_NAME="${GITHUB_REF##*/}"
+
+          # From https://github.com/fsaintjacques/semver-tool/blob/master/src/semver
+
+          NAT='0|[1-9][0-9]*'
+          ALPHANUM='[0-9]*[A-Za-z-][0-9A-Za-z-]*'
+          IDENT="$NAT|$ALPHANUM"
+          FIELD='[0-9A-Za-z-]+'
+
+          SEMVER_REGEX="\
+          ^[vV]?\
+          ($NAT)\\.($NAT)\\.($NAT)\
+          (\\-(${IDENT})(\\.(${IDENT}))*)?\
+          (\\+${FIELD}(\\.${FIELD})*)?$"
+
+          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"
+          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: set-nightly
-    # `always` *must* be used to continue even after a dependency has been skipped
-    if: always() && (github.event_name != 'schedule' || github.repository == 'leanprover/lean4')
+    needs: [configure]
+    if: github.event_name != 'schedule' || github.repository == 'leanprover/lean4'
+    strategy:
+      matrix:
+        include: ${{fromJson(needs.configure.outputs.matrix)}}
+      # complete all jobs
+      fail-fast: false
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        shell: ${{ matrix.shell || 'nix-shell --run "bash -euxo pipefail {0}"' }}
-    strategy:
-      matrix:
-        include:
-          # portable release build: use channel with older glibc (2.27)
-          - name: Linux release
-            os: ubuntu-latest
-            release: 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/14.0.0/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|leanlaketest_git'
-          - name: Linux
-            os: ubuntu-latest
-            check-stage3: true
-            test-speedcenter: true
-          - name: Linux Debug
-            os: ubuntu-latest
-            CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
-          - name: Linux fsanitize
-            os: ubuntu-latest
-            # 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 problematic tests
-            CTEST_OPTIONS: -E laketest
-          - name: macOS
-            os: macos-latest
-            release: true
-            shell: bash -euxo pipefail {0}
-            CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.15
-            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/14.0.0/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
-            cross: true
-            shell: bash -euxo pipefail {0}
-            CMAKE_OPTIONS: -DCMAKE_OSX_DEPLOYMENT_TARGET=10.15 -DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64
-            llvm-url: https://github.com/leanprover/lean-llvm/releases/download/14.0.0/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/14.0.0/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
-            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/14.0.0/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: -DCMAKE_PREFIX_PATH=$GMP -DLEAN_INSTALL_SUFFIX=-linux_aarch64
-            release: true
-            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/14.0.0/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/14.0.0/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-*
-      # complete all jobs
-      fail-fast: false
+        shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
     name: ${{ matrix.name }}
     env:
       # must be inside workspace
@@ -119,73 +287,123 @@ jobs:
       LSAN_OPTIONS: max_leaks=10
       # somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
       CXX: c++
+      MACOSX_DEPLOYMENT_TARGET: 10.15
     steps:
-      - name: Checkout
-        uses: actions/checkout@v2
-        with:
-          submodules: true
       - name: Install Nix
-        uses: cachix/install-nix-action@v15
-        if: matrix.os == 'ubuntu-latest'
+        uses: DeterminateSystems/nix-installer-action@main
+        if: runner.os == 'Linux' && !matrix.cmultilib
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
           msystem: clang64
-          # `: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'
+          # `:` 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'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd coreutils
-        if: matrix.os == 'macos-latest'
+          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)
+      - name: Setup emsdk
+        uses: mymindstorm/setup-emsdk@v14
+        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
+        if: matrix.cmultilib
       - name: Cache
-        uses: actions/cache@v2
+        uses: actions/cache@v4
         with:
           path: .ccache
-          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.event.pull_request.head.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: |
-          # open nix-shell once for initial setup
-          true
-        if: matrix.os == 'ubuntu-latest'
+          ccache --zero-stats
+        if: runner.os == 'Linux'
+      - name: Set up NPROC
+        run: |
+          echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
       - name: Build
         run: |
           mkdir build
           cd build
-          OPTIONS=()
+          # arguments passed to `cmake`
+          # 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 }})"
             eval "OPTIONS+=($PREPARE)"
           fi
-          if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
-            OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-nightly.outputs.nightly }})
+          if [[ -n '${{ matrix.release }}' && -n '${{ needs.configure.outputs.nightly }}' ]]; then
+            OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.nightly }})
+          fi
+          if [[ -n '${{ matrix.release }}' && -n '${{ needs.configure.outputs.RELEASE_TAG }}' ]]; then
+            OPTIONS+=(-DLEAN_VERSION_MAJOR=${{ needs.configure.outputs.LEAN_VERSION_MAJOR }})
+            OPTIONS+=(-DLEAN_VERSION_MINOR=${{ needs.configure.outputs.LEAN_VERSION_MINOR }})
+            OPTIONS+=(-DLEAN_VERSION_PATCH=${{ needs.configure.outputs.LEAN_VERSION_PATCH }})
+            OPTIONS+=(-DLEAN_VERSION_IS_RELEASE=1)
+            OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.configure.outputs.LEAN_SPECIAL_VERSION_DESC }})
           fi
           # contortion to support empty OPTIONS with old macOS bash
-          cmake .. ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-          make -j4
-          make install
+          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
       - 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/, ...
-          tree --du -h lean-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
+          tree --du -h lean-*-* | grep -E ' (Init|Lean|Lake|LICENSE|[a-z])'
       - name: Pack
         run: |
-          dir=$(echo lean-*)
+          dir=$(echo lean-*-*)
           mkdir pack
           # high-compression tar.zst + zip for release, fast tar.zst otherwise
-          if [[ '${{ startsWith(github.ref, 'refs/tags/v') && matrix.release }}' == true || -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
+          if [[ '${{ startsWith(github.ref, 'refs/tags/') && matrix.release }}' == true || -n '${{ needs.configure.outputs.nightly }}' || -n '${{ needs.configure.outputs.RELEASE_TAG }}' ]]; then
             ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst
             zip -rq pack/$dir.zip $dir
           else
             ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
           fi
-      - uses: actions/upload-artifact@v2
+      - uses: actions/upload-artifact@v4
         if: matrix.release
         with:
           name: build-${{ matrix.name }}
@@ -195,94 +413,146 @@ jobs:
           build/stage1/bin/lean --stats src/Lean.lean
         if: ${{ !matrix.cross }}
       - name: Test
+        id: test
         run: |
-          cd build/stage1
-          # exclude nonreproducible test
-          ctest -j4 --output-on-failure -E leanlaketest_git ${{ matrix.CTEST_OPTIONS }} < /dev/null
-        if: ${{ !matrix.cross }}
+          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'
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
-        if: ${{ !matrix.cross }}
+        if: (!matrix.cross) && steps.test.conclusion != 'skipped'
       - name: Build Stage 2
         run: |
-          cd build
-          make -j4 stage2
-        if: matrix.build-stage2 || matrix.check-stage3
+          make -C build -j$NPROC stage2
+        if: matrix.test-speedcenter
       - name: Check Stage 3
         run: |
-          cd build
-          make -j4 check-stage3
-        if: matrix.check-stage3
+          make -C build -j$NPROC check-stage3
+        if: matrix.test-speedcenter
       - name: Test Speedcenter Benchmarks
         run: |
-          echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
+          # 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
           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: |
-          cd build
-          make update-stage0 && make -j4
-        if: matrix.name == 'Linux'
+          # 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
       - name: CCache stats
         run: ccache -s
 
+  # This job collects results from all the matrix jobs
+  # 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() }}
+    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')
+      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:
+  # unofficial releases don't need them, and official release notes will be written by a human.
   release:
-    # When GitHub says "If a job fails, all jobs that need it are skipped unless
-    # the jobs use a conditional expression that causes the job to continue.", don't believe
-    # their lies. It's actually the entire closure (i.e. including `set-nightly`) that
-    # must succeed for subsequent to be run without `always()`.
-    if: always() && needs.build.result == 'success' && startsWith(github.ref, 'refs/tags/v')
+    if: startsWith(github.ref, 'refs/tags/')
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
         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.
   release-nightly:
-    needs: [set-nightly, build]
-    if: needs.set-nightly.outputs.nightly
+    needs: [configure, build]
+    if: needs.configure.outputs.nightly
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
         with:
           # needed for tagging
           fetch-depth: 0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v4
         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.set-nightly.outputs.nightly }}
-          git push nightly ${{ needs.set-nightly.outputs.nightly }}
-          last_tag=$(git describe HEAD^ --abbrev=0 --tags)
+          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)"
           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@v1
+        uses: softprops/action-gh-release@v2
         with:
           body_path: diff.md
           prerelease: true
           files: artifacts/*/*
           fail_on_unmatched_files: true
-          tag_name: ${{ needs.set-nightly.outputs.nightly }}
+          tag_name: ${{ needs.configure.outputs.nightly }}
           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

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

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

@@ -0,0 +1,67 @@
+# 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.
+
+name: Label PR based on Comment
+
+on:
+  issue_comment:
+    types: [created]
+
+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-'))
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Add label based on comment
+      uses: actions/github-script@v7
+      with:
+        github-token: ${{ secrets.GITHUB_TOKEN }}
+        script: |
+          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(() => {});
+            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-author' }).catch(() => {});
+            await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'WIP' }).catch(() => {});
+          }
+
+          if (awaitingReview) {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-review'] });
+          }
+          if (awaitingAuthor) {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['awaiting-author'] });
+          }
+          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

@@ -6,103 +6,137 @@ on:
     tags:
       - '*'
   pull_request:
-    branches:
-      - master
+  merge_group:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  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 -v --experimental-features "nix-command flakes" run .#ciShell -- bash -euxo pipefail {0}
+        shell: nix run .#ciShell -- bash -euxo pipefail {0}
     strategy:
       matrix:
-        include:
-          - name: Nix Linux
-            os: ubuntu-latest
-          #- name: Nix macOS
-          #  os: macos-latest
+        include: ${{fromJson(needs.configure.outputs.matrix)}}
       # complete all jobs
       fail-fast: false
     name: ${{ matrix.name }}
     env:
-      NIX_BUILD_ARGS: -v --print-build-logs --fallback
+      NIX_BUILD_ARGS: --print-build-logs --fallback
     steps:
       - name: Checkout
-        uses: actions/checkout@v2
-      - name: Install Nix
-        uses: cachix/install-nix-action@v15
+        uses: actions/checkout@v4
         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
+          # 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: Set Up Nix Cache
-        uses: actions/cache@v2
+        uses: actions/cache@v4
         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@v2
+        uses: actions/cache@v4
         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@v10
-        with:
-          name: lean4
-          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-          skipPush: true  # we push specific outputs only
       - name: Build
         run: |
-          # .o files are not a runtime dependency on macOS because of lack of thin archives
-          nix build $NIX_BUILD_ARGS .#stage0 .#stage1.lean-all .#Lean.oTree .#iTree .#modDepsFiles -o push-build
+          nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
-          nix build $NIX_BUILD_ARGS .#test -o push-test
+          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
       - name: Build manual
         run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test} -o push-doc
+          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
+          # 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
-      - name: Publish manual
-        uses: peaceiris/actions-gh-pages@v3
+      - 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
         with:
-          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'
+          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"
       - 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

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

@@ -0,0 +1,350 @@
+# Push a release to the lean4-pr-releases repository, whenever someone pushes to a PR branch.
+
+# This needs to run with the `secrets.PR_RELEASES_TOKEN` token available,
+# but PR branches will generally come from forks,
+# so it is not possible to run this using the `pull_request` or `pull_request_target` workflows.
+# 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:
+  workflow_run: # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#workflow_run
+    workflows: [CI]
+    types: [completed]
+
+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'
+    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: Download artifact from the previous workflow.
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        id: download-artifact
+        uses: dawidd6/action-download-artifact@v6 # 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
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        run: |
+          # 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
+        env:
+          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+      - name: Release
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: softprops/action-gh-release@v2
+        with:
+          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          # There are coredumps files here as well, but all in deeper subdirectories.
+          files: artifacts/*/*
+          fail_on_unmatched_files: true
+          draft: false
+          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+          repository: ${{ github.repository_owner }}/lean4-pr-releases
+        env:
+          # 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
+        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']
+            })
+
+      # Next, determine the most recent nightly release in this PR's history.
+      - name: Find most recent nightly in feature branch
+        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"
+
+      - name: 'Setup jq'
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: dcarbone/install-jq-action@v2.1.0
+
+      # 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 "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"
+
+            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")"
+
+            if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
+              echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              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."
+            fi
+
+          else
+            echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA"
+            echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
+            git -C lean4.git log -10 origin/master
+
+            git -C lean4.git fetch origin nightly-with-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\`."
+          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 }}" \
+                                    -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)"
+
+            if [[ "$existing_comment_body" != *"$MESSAGE"* ]]; then
+              MESSAGE="$MESSAGE ($(date "+%Y-%m-%d %H:%M:%S"))"
+
+              echo "Posting message to the comments: $MESSAGE"
+
+              # Append new result to the existing comment or post a new comment
+              # It's essential we use the MATHLIB4_COMMENT_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 "Accept: application/vnd.github.v3+json" \
+                  -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
+                  "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
+              else
+                # Append new result to the existing comment
+                echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
+                curl -L -s \
+                  -X PATCH \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                  -H "Accept: application/vnd.github.v3+json" \
+                  -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
+                  "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
+              fi
+            else
+              echo "The message already exists in the comment body."
+            fi
+            echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
+          else
+            echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
+          fi
+
+      - name: Report mathlib base
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
+        uses: actions/github-script@v7
+        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 ./*
+
+      # 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
+        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
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
+        id: check_mathlib_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}' branch at Mathlib. Falling back to 'nightly-testing'."
+            BASE=nightly-testing
+          fi
+
+          echo "Using base tag: $BASE"
+
+          EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)"
+          echo "Branch exists: $EXISTS"
+          if [ "$EXISTS" = "0" ]; then
+            echo "Branch does not exist, creating it."
+            git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > 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
+            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 }}

.github/workflows/pr-title.yml

@@ -0,0 +1,20 @@
+name: Check PR title for commit convention
+
+on:
+  merge_group:
+  pull_request:
+    types: [opened, synchronize, reopened, edited]
+
+jobs:
+  check-pr-title:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check PR title
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
+            console.log(`Message: ${msg}`)
+            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(msg)) {
+              core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
+            }

.github/workflows/pr.yml

@@ -1,31 +0,0 @@
-name: sanity-check opened PRs
-
-on:
-  # needs read/write GH token, do *not* execute arbitrary code from PR
-  pull_request_target:
-    types: [opened]
-
-jobs:
-  check-pr:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check Commit Message
-        uses: actions/github-script@v3
-        with:
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          script: |
-            const { data: commits } = await github.pulls.listCommits({
-              owner: context.repo.owner,
-              repo: context.repo.repo,
-              pull_number: context.issue.number,
-            });
-            console.log(commits[0].commit.message);
-            // check first commit only (and only once) since later commits might be intended to be squashed away
-            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(commits[0].commit.message)) {
-              await github.issues.createComment({
-                owner: context.repo.owner,
-                repo: context.repo.repo,
-                issue_number: context.issue.number,
-                body: 'Thanks for your contribution! Please make sure to follow our [Commit Convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).',
-              });
-            }

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

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

@@ -0,0 +1,20 @@
+name: 'Label stale PRs'
+on:
+  schedule:
+    - cron: '30 1 * * *'
+  workflow_dispatch:
+
+permissions:
+  pull-requests: write
+
+jobs:
+  stale:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/stale@v9
+        with:
+          days-before-stale: -1
+          days-before-pr-stale: 30
+          days-before-close: -1
+          stale-pr-label: 'stale'
+          only-labels: 'awaiting-author'

.github/workflows/update-stage0.yml

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

@@ -2,7 +2,12 @@
 \#*
 .#*
 *.lock
-build
+.lake
+lake-manifest.json
+/build
+/src/lakefile.toml
+/tests/lakefile.toml
+/lakefile.toml
 GPATH
 GRTAGS
 GSYMS
@@ -25,4 +30,4 @@ fwIn.txt
 fwOut.txt
 wdErr.txt
 wdIn.txt
-wdOut.txt
+wdOut.txt

.gitmodules

@@ -1,4 +0,0 @@
-[submodule "lake"]
-        path = src/lake
-        url = https://github.com/leanprover/lake.git
-        ignore = untracked

.vscode/settings.json

@@ -1,7 +0,0 @@
-{
-    "files.insertFinalNewline": true,
-    "files.trimTrailingWhitespace": true,
-    "[markdown]": {
-        "rewrap.wrappingColumn": 70
-    }
-}

CMakeLists.txt

@@ -11,10 +11,13 @@ foreach(var ${vars})
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if("${var}" STREQUAL "USE_GMP")
+    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
+    if("${var}" MATCHES "LLVM*")
+      list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
+    endif()
   elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
     list(APPEND PLATFORM_ARGS "-D${var}=${${var}}")
   endif()
@@ -23,28 +26,46 @@ endforeach()
 include(ExternalProject)
 project(LEAN CXX C)
 
-if("${CMAKE_SYSTEM_NAME}" MATCHES "Emscripten")
-  # For Emscripten, we build GMP before any of the stages and reuse it in all of them.
-  set(GMP_INSTALL_PREFIX ${CMAKE_BINARY_DIR}/gmp-root)
-  set(EMSCRIPTEN_FLAGS "-s ALLOW_MEMORY_GROWTH=1 -s MAIN_MODULE=1 -O3")
-  ExternalProject_Add(
-    gmp
-    URL https://gmplib.org/download/gmp/gmp-6.2.1.tar.bz2
-    URL_HASH SHA256=eae9326beb4158c386e39a356818031bd28f3124cf915f8c5b1dc4c7a36b4d7c
-    BUILD_IN_SOURCE 1
-    CONFIGURE_COMMAND emconfigure ./configure "CFLAGS=${EMSCRIPTEN_FLAGS}" --host=wasm32-unknown-emscripten --disable-assembly --prefix=${GMP_INSTALL_PREFIX}
-    BUILD_COMMAND emmake make -j4
-    INSTALL_COMMAND emmake make install
-  )
-  set(EXTRA_DEPENDS "gmp")
-  list(APPEND CL_ARGS "-DGMP_INSTALL_PREFIX=${GMP_INSTALL_PREFIX}")
-  list(APPEND PLATFORM_ARGS "-DGMP_INSTALL_PREFIX=${GMP_INSTALL_PREFIX}")
+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
   BINARY_DIR stage0
   # do not rebuild stage0 when git hash changes; it's not from this commit anyway
+  # (however, `CHECK_OLEAN_VERSION=ON` in CI will override this as we need to
+  # embed the githash into the stage 1 library built by stage 0)
   CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
   BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
   INSTALL_COMMAND ""  # skip install
@@ -54,7 +75,7 @@ ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage0
@@ -63,7 +84,7 @@ ExternalProject_add(stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage2
-  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage1
@@ -73,7 +94,7 @@ ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage3
-  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage2
@@ -86,6 +107,10 @@ 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

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

CODEOWNERS

@@ -0,0 +1,48 @@
+# Code Owners
+#
+# Documents responsible people per component.
+# 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/ @Kha @kim-em
+/RELEASES.md @kim-em
+/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/Meta/Tactic/ @leodemoura
+/src/Lean/Parser/ @Kha
+/src/Lean/PrettyPrinter/ @Kha
+/src/Lean/PrettyPrinter/Delaborator/ @kmill
+/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

CONTRIBUTING.md

@@ -1,57 +1,93 @@
-# Contribution Guidelines
+External Contribution Guidelines
+============
 
-Thank you for your interest in contributing to Lean! There are many ways to contribute and we appreciate all of them.
+In the past, we accepted most pull requests. This practice produced hard to maintain code, performance problems, and bugs. In order to improve the quality and maintainability of our codebase, we've established the following guidelines for external contributions.
 
-## Bug reports
+Helpful links
+-------
 
-Bug reports as new issues are always welcome. Please check the existing [issues](https://github.com/leanprover/lean4/issues) first.
-Reduce the issue to a self-contained, reproducible test case.
-If you have the chance, before reporting a bug, please search existing issues, as it's possible that
-someone else has already reported your error.
-If you're not sure if something is a bug or not, feel free to file a bug anyway. You may also want to discuss it with the Lean
-community using the [lean4 Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4).
+* [Development Setup](./doc/dev/index.md)
+* [Testing](./doc/dev/testing.md)
+* [Commit convention](./doc/dev/commit_convention.md)
 
-## Simple fixes
+Before You Submit a Pull Request (PR):
+-------
 
-Simple fixes for **typos and clear bugs** are welcome.
+**Start with an Issue**: Before submitting a PR, always open an issue discussing the problem you wish to solve or the feature you'd like to add. Use the prefix `RFC:` (request for comments) if you are proposing a new feature. Ask for feedback from other users. Take the time to summarize all the feedback. This allows the maintainers to evaluate your proposal more efficiently. When creating a RFC, consider the following questions:
 
-## Documentation
+  - **User Experience**: How does this feature improve the user experience?
 
-Tutorial-like examples are very welcome.
-They are useful for finding rough edges and bugs in Lean 4, for highlighting new features, and for showing how to use Lean.
-If you want to store your tutorial in the Lean 4 repository to make sure future changes will not break it, we suggest the following workflow:
-* Contact one of the Lean developers on Zulip, and check whether your tutorial is a good match for the Lean 4 repository.
-* Send bug reports and report rough edges. We will work with you until the tutorial looks great.
-* Add plenty of comments and make sure others will be able to follow it.
-* Create a pull request in the Lean 4 repository. After merging, we will link it to the official documentation and make sure it becomes part of our test suite.
+  - **Beneficiaries**: Which Lean users and projects do benefit most from this feature/change?
 
-You can use `.lean` or `.md` files to create your tutorial. The `.md` files are ideal when you want to format your prose using markdown. For an example, see [this `.md` file](https://github.com/leanprover/lean4/blob/master/doc/lean3changes.md).
+  - **Community Feedback**: Have you sought feedback or insights from other Lean users?
 
-Contributions to the reference manual are also welcome, but since Lean 4 is changing rapidly, please contact us first using Zulip
-to find out which parts are stable enough to document. We will work with you to get this kind of
-pull request merged. We are also happy to meet using Zoom, Skype or Google hangout to coordinate this kind of effort.
+  - **Maintainability**: Will this change streamline code maintenance or simplify its structure?
 
-As Lean 4 matures, other forms of documentation (e.g., doc-strings) will be welcome too.
+**Understand the Project**: Familiarize yourself with the project, existing issues, and latest commits. Ensure your contribution aligns with the project's direction and priorities.
 
-## "Help wanted"
+**Stay Updated**: Regularly fetch and merge changes from the main branch to ensure your branch is up-to-date and can be smoothly integrated.
 
-For issues marked as [`help wanted`](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22), pull requests (PR) are welcome and we will work with you to get a PR merged. Some of these issues are nontrivial. If you are interested, please consider adding comments to the issue and/or messaging the Lean developers in [Zulip](https://leanprover.zulipchat.com/#).
+**Help wanted**: We have issues tagged with ["help wanted"](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22), if you want to contribute to the project, please take a look at them. If you are interested in one of them, post comments, ask questions, and engage with the core developers there.
 
-## Unexpected Pull Requests
+Quality Over Quantity:
+-----
 
-We have very few core developers, and we cannot review arbitrary pull requests (PRs). Moreover, many features involve subtle tradeoffs, and it may require significant time and energy to even assess a proposed design. We suggest the following workflow:
+**Focused Changes**: Each PR should address a single, clearly-defined issue or feature. Avoid making multiple unrelated changes in a single PR.
 
-* First, discuss your idea with the Lean community on Zulip. Ask the community to help collect examples, document the requirements, and detect complications.
-* If there is broad support, create a detailed issue for it on the Lean 4 repository at GitHub, and tag the issue with `RFC`.
-* Ask the community for help documenting the requirements, and for collecting examples and concerns.
-* Wait for one of the core developers to give you a "go ahead". At this point, the core developers will work with you to make sure your PR gets merged.
+**Write Tests**: Every new feature or bug fix should come with relevant tests. This ensures the robustness and reliability of the contribution.
 
-We don't want to waste your time by you implementing a feature and then us not being able to merge it.
+**Documentation**: Update relevant documentation, including comments in the code, to explain the logic and reasoning behind your changes.
 
-## How to Contribute
+Coding Standards:
+----
 
-* Always follow the [commit convention](https://leanprover.github.io/lean4/doc/dev/commit_convention.html).
-* Follow the style of the surrounding code. When in doubt, look at other files using the particular syntax as well.
-* Make sure your code is documented.
-* New features or bug fixes should come with appropriate tests.
-* Ensure all tests work before submitting a PR; see [Development Setup](https://leanprover.github.io/lean4/doc/make/index.html#development-setup) and [Fixing Tests](https://leanprover.github.io/lean4/doc/dev/fixing_tests.html).
+**Follow the Code Style**: Ensure that your code follows the established coding style of the project.
+
+**Lean on Lean**: Use Lean's built-in features and libraries effectively, avoiding reinventions.
+
+**Performance**: Make sure that your changes do not introduce performance regressions. If possible, optimize the solution for speed and resource usage.
+
+PR Submission:
+---
+
+**Descriptive Title and Summary**: The PR title should briefly explain the purpose of the PR. The summary should give more detailed information on what changes are made and why. Links to Zulip threads are not acceptable as a summary. You are responsible for summarizing the discussion, and getting support for it.
+
+**Follow the commit convention**: Pull requests are squash merged, and the
+commit message is taken from the pull request title and body, so make sure they adhere to the [commit convention](https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md). Put questions and extra information, which should not be part of the final commit message, into a first comment rather than the Pull Request description.
+Because the change will be squashed, there is no need to polish the commit messages and history on the branch.
+
+**Link to Relevant Issues**: Reference any issues that your PR addresses to provide context.
+
+**Stay Responsive**: Once the PR is submitted, stay responsive to feedback and be prepared to make necessary revisions. We will close any PR that has been inactive (no response or updates from the submitter) for more than a month.
+
+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.
+
+**Continuous Integration**: Ensure that all CI checks pass on your PR. Failed checks will delay the review process. The maintainers will not check PRs containing failures.
+
+What to Expect:
+----
+
+**Not All PRs Get Merged**: While we appreciate every contribution, not all PRs will be merged. Ensure your changes align with the project's goals and quality standards.
+
+**Feedback is a Gift**: It helps improve the project and can also help you grow as a developer or contributor.
+
+**Community Involvement**: Engage with the Lean community on our communication channels. This can lead to better collaboration and understanding of the project's direction.

LICENSES

@@ -1341,3 +1341,33 @@ 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,22 +1,20 @@
-This is the repository for **Lean 4**, which is currently being released as milestone releases towards a first stable release.
-[Lean 3](https://github.com/leanprover/lean) is still the latest stable release.
+This is the repository for **Lean 4**.
 
 # About
 
-- [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://leanprover.github.io)
-- [Theorem Proving Tutorial](https://leanprover.github.io/theorem_proving_in_lean4/)
-- [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/) **first chapter is available!**
-- [Manual](https://leanprover.github.io/lean4/doc/)
+- [Quickstart](https://lean-lang.org/lean4/doc/quickstart.html)
+- [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/)
+- [Manual](https://lean-lang.org/lean4/doc/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://leanprover.github.io/lean4/doc/examples.html)
-- [FAQ](https://leanprover.github.io/lean4/doc/faq.html)
+- [Examples](https://lean-lang.org/lean4/doc/examples.html)
+- [External Contribution Guidelines](CONTRIBUTING.md)
+- [FAQ](https://lean-lang.org/lean4/doc/faq.html)
 
 # Installation
 
-See [Setting Up Lean](https://leanprover.github.io/lean4/doc/setup.html).
+See [Setting Up Lean](https://lean-lang.org/lean4/doc/setup.html).
 
 # Contributing
 
@@ -24,4 +22,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
 
 # Building from Source
 
-See [Building Lean](https://leanprover.github.io/lean4/doc/make/index.html).
+See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).

debug.log

@@ -0,0 +1 @@
+[0829/202002.254:ERROR:crashpad_client_win.cc(868)] not connected

default.nix

@@ -1,9 +0,0 @@
-# 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 Std
+open Batteries
 open Lean
 
 inductive BoolExpr where

doc/SUMMARY.md

@@ -75,6 +75,7 @@
 - [Significant Changes from Lean 3](./lean3changes.md)
 - [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md)
 - [User Widgets](examples/widgets.lean.md)
+- [Semantic Highlighting](./semantic_highlighting.md)
 
 # Development
 
@@ -84,10 +85,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/autobound.md

@@ -43,3 +43,5 @@ set_option autoImplicit false
 -- def compose (g : β → γ) (f : α → β) (x : α) : γ :=
 --   g (f x)
 ```
+The Lean language server provides [semantic highlighting](./semantic_highlighting.md) information to editors, and it provides
+visual feedback whether an identifier has been interpreted as an auto bound implicit argument.

doc/bin/README.md

@@ -11,4 +11,4 @@ the following command executes a simple set of examples
 
 % bin/lean examples/ex.lean
 
-For more information on Lean and supported editors, please see https://leanprover.github.io/documentation/.
+For more information on Lean and supported editors, please see https://lean-lang.org/documentation/.

doc/char.md

@@ -1 +1,11 @@
 # 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/dev/bootstrap.md

@@ -65,19 +65,59 @@ 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 stage 0 compiler, which can be done via `make -C stageN update-stage0`.
-`make update-stage0` without `-C` defaults to stage1.
+update the archived C source code of the stage 0 compiler in `stage0/src`.
+
+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
+```
+gh workflow run update-stage0.yml
+```
+
+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 need to build the stage using `-Dinterpreter.prefer_native=false` -
+  this, we build stage 1 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!
@@ -95,26 +135,11 @@ 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.
 
-  For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
+  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 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`).
+  For a `prefer_native` example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb.
 
 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/commit_convention.md

@@ -1,10 +1,15 @@
 Git Commit Convention
 =====================
 
-We are using the following convention for writing git-commit messages.
-It is based on the one from AngularJS project([doc][angularjs-doc],
+We are using the following convention for writing git commit messages. For pull
+requests, make sure the pull request title and description follow this
+convention, as the squash-merge commit will inherit title and body from the
+pull request.
+
+This convention is based on the one from the AngularJS project ([doc][angularjs-doc],
 [commits][angularjs-git]).
 
+
 [angularjs-git]: https://github.com/angular/angular.js/commits/master
 [angularjs-doc]: https://docs.google.com/document/d/1QrDFcIiPjSLDn3EL15IJygNPiHORgU1_OOAqWjiDU5Y/edit#
 

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,7 +22,9 @@ 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.
-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.
+
+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.
 
 ## Debuggers
 

doc/dev/ffi.md

@@ -11,6 +11,8 @@ There are two primary attributes for interoperating with other languages:
   It can also be used with `def` to provide an internal definition, but ensuring consistency of both definitions is up to the user.
 * `@[export sym] def leanSym : ...` exports `leanSym` under the unmangled symbol name `sym`.
 
+For simple examples of how to call foreign code from Lean and vice versa, see <https://github.com/leanprover/lean4/blob/master/src/lake/examples/ffi> and <https://github.com/leanprover/lean4/blob/master/src/lake/examples/reverse-ffi>, respectively.
+
 ## The Lean ABI
 
 The Lean Application Binary Interface (ABI) describes how the signature of a Lean declaration is encoded as a native calling convention.
@@ -21,7 +23,7 @@ If `n` is 0, the corresponding C declaration is
 extern s sym;
 ```
 where `s` is the C translation of `β` as specified in the next section.
-In the case of an `@[extern]` definition, the symbol's value is guaranteed to be initialized only after calling the Lean module's initializer or that of an importing module; see [Initialization](.#init).
+In the case of an `@[extern]` definition, the symbol's value is guaranteed to be initialized only after calling the Lean module's initializer or that of an importing module; see [Initialization](#initialization).
 
 If `n` is greater than 0, the corresponding C declaration is
 ```c
@@ -32,7 +34,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
 
 ### Translating Types from Lean to C
 
-* The integer types `UInt8`, ..., `UInt64`, `USize` are represented by the C types `uint8_t`, ..., `uint64_t`, `usize_t`, respectively
+* The integer types `UInt8`, ..., `UInt64`, `USize` are represented by the C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively
 * `Char` is represented by `uint32_t`
 * `Float` is represented by `double`
 * An *enum* inductive type of at least 2 and at most 2^32 constructors, each of which with no parameters, is represented by the first type of `uint8_t`, `uint16_t`, `uint32_t` that is sufficient to represent all constructor indices.
@@ -45,16 +47,65 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   * it has a single constructor with a single parameter of *relevant* type
 
   is represented by the representation of that parameter's type.
-  
+
   For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
 * `Nat` is represented by `lean_object *`.
   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 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.
+  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.
 
   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`.
@@ -70,13 +121,13 @@ When including Lean code as part of a larger program, modules must be *initializ
 Module initialization entails
 * initialization of all "constants" (nullary functions), including closed terms lifted out of other functions
 * execution of all `[init]` functions
-* execution of all `[builtinInit]` functions, if the `builtin` parameter of the module initializer has been set
+* execution of all `[builtin_init]` functions, if the `builtin` parameter of the module initializer has been set
 
 The module initializer is automatically run with the `builtin` flag for executables compiled from Lean code and for "plugins" loaded with `lean --plugin`.
 For all other modules imported by `lean`, the initializer is run without `builtin`.
-Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtinInit]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
+Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtin_init]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
 `lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping).
-  
+
 The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
 Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
 Together with initialization of the Lean runtime, you should execute code like the following exactly once before accessing any Lean declarations:
@@ -109,6 +160,15 @@ 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.
@@ -119,4 +179,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` for an example.
+See [`tests/compiler/foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) for an example.

doc/dev/index.md

@@ -1,6 +1,6 @@
 # Development Workflow
 
-If you want to make changes to Lean itself, start by [building Lean](../make/index.html) from a clean checkout to make sure that everything is set up correctly.
+If you want to make changes to Lean itself, start by [building Lean](../make/index.md) from a clean checkout to make sure that everything is set up correctly.
 After that, read on below to find out how to set up your editor for changing the Lean source code, followed by further sections of the development manual where applicable such as on the [test suite](testing.md) and [commit convention](commit_convention.md).
 
 If you are planning to make any changes that may affect the compilation of Lean itself, e.g. changes to the parser, elaborator, or compiler, you should first read about the [bootstrapping pipeline](bootstrap.md).
@@ -30,20 +30,14 @@ powershell -f elan-init.ps1 --default-toolchain none
 del elan-init.ps1
 ```
 
-You can use `elan toolchain link` to give a specific stage build
-directory a reference name, then use `elan override set` to associate
-such a name to the current directory. We usually want to use `stage0`
-for editing files in `src` and `stage1` for everything else (e.g.
-tests).
+The `lean-toolchain` files in the Lean 4 repository are set up to use the `lean4-stage0`
+toolchain for editing files in `src` and the `lean4` toolchain for editing files in `tests`.
+
+Run the following commands to make `lean4` point at `stage1` and `lean4-stage0` point at `stage0`:
 ```bash
 # in the Lean rootdir
 elan toolchain link lean4 build/release/stage1
 elan toolchain link lean4-stage0 build/release/stage0
-# make `lean` etc. point to stage1 in the rootdir and subdirs
-elan override set lean4
-cd src
-# make `lean` etc. point to stage0 anywhere inside `src`
-elan override set lean4-stage0
 ```
 
 You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch
@@ -57,3 +51,32 @@ You might find that debugging through elan, e.g. via `gdb lean`, disables some
 things like symbol autocompletion because at first only the elan proxy binary
 is loaded. You can instead pass the explicit path to `bin/lean` in your build
 folder to gdb, or use `gdb $(elan which lean)`.
+
+It is also possible to generate releases that others can use,
+simply by pushing a tag to your fork of the Lean 4 github repository
+(and waiting about an hour; check the `Actions` tab for completion).
+If you push `my-tag` to a fork in your github account `my_name`,
+you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`.
+(You must use a tag name that does not start with a numeral, or contain `_`).
+
+### VS Code
+
+There is a `lean.code-workspace` file that correctly sets up VS Code with workspace roots for the stage0/stage1 setup described above as well as with other settings.
+You should always load it when working on Lean, such as by invoking
+```
+code lean.code-workspace
+```
+on the command line.
+
+### `ccache`
+
+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/mdbook.md

@@ -1,7 +1,7 @@
 # Documentation
 
-The Lean `doc` folder contains the [Lean Manual](https://leanprover.github.io/lean4/doc/) and is
-authored in a combination of markdown (*.md) files and literate Lean files.  The .lean files are
+The Lean `doc` folder contains the [Lean Manual](https://lean-lang.org/lean4/doc/) and is
+authored in a combination of markdown (`*.md`) files and literate Lean files.  The .lean files are
 preprocessed using a tool called [LeanInk](https://github.com/leanprover/leanink) and
 [Alectryon](https://github.com/Kha/alectryon) which produces a generated markdown file.  We then run
 `mdbook` on the result to generate the html pages.
@@ -53,25 +53,28 @@ Then run the following:
     cargo install --git https://github.com/leanprover/mdBook mdbook
     ```
 
-1. Clone https://github.com/leanprover/LeanInk.git and run `lake build` then copy the resulting
-executable to your `$HOME/.elan/bin` folder or `%USERPROFILE%\.elan\bin` so Alectryon can find it
-there.
+1. Clone https://github.com/leanprover/LeanInk.git and run `lake build` then make the resulting
+   binary available to Alectryon using e.g.
+    ```bash
+    # make `leanInk` available in the current shell
+    export PATH=$PWD/build/bin:$PATH
+    ```
 
 1. Create a Python 3.10 environment.
 
-1. Install the following packages:
+1. Install Alectryon:
     ```
     python3 -m pip install git+https://github.com/Kha/alectryon.git@typeid
     ```
 
-1. Now you are ready to process the *.lean files using Alectryon as follows:
+1. Now you are ready to process the `*.lean` files using Alectryon as follows:
 
     ```
     cd lean4/doc
-    alectryon --frontend lean4+markup examples\palindromes.lean --backend webpage -o palindromes.lean.md
+    alectryon --frontend lean4+markup examples/palindromes.lean --backend webpage -o palindromes.lean.md
     ```
 
-And repeat this for the other .lean files you care about or write a script to process them all.
+    Repeat this for the other .lean files you care about or write a script to process them all.
 
 1. Now you can build the book using:
     ```
@@ -80,7 +83,7 @@ And repeat this for the other .lean files you care about or write a script to pr
     ```
 
 This will put the HTML in a `out` folder so you can load `out/index.html` in your web browser and
-it should look like https://leanprover.github.io/lean4/doc/.
+it should look like https://lean-lang.org/lean4/doc/.
 
 1. It is also handy to use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html)
    in the `doc/` folder so that it keeps the html up to date while you are editing.

doc/dev/release_checklist.md

@@ -0,0 +1,262 @@
+# 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,7 +5,6 @@ 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
@@ -17,6 +16,12 @@ 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:
 
@@ -24,6 +29,9 @@ 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
@@ -33,17 +41,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`: contains tests that come equipped with a
-  .lean.expected.out file. The driver script `test_single.sh` runs
+- [`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
   each test and checks the actual output (*.produced.out) with the
   checked in expected output.
 
-- `tests/lean/run`: contains tests that are run through the lean
+- [`tests/lean/run`](https://github.com/leanprover/lean4/tree/master/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`: are designed to test server requests at a
+- [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/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:
@@ -53,7 +61,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` will simulate an
+    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
     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
@@ -70,23 +78,33 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     --^ collectDiagnostics
     ```
 
-- `tests/lean/server`: Tests more of the Lean `--server` protocol.
+- [`tests/lean/server`](https://github.com/leanprover/lean4/tree/master/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`: contains tests that will run the Lean compiler and
+- [`tests/compiler`](https://github.com/leanprover/lean4/tree/master/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` which shows how to extend Lean using C++.
+  [`foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) which shows how to extend Lean using C++.
 
-- `tests/lean/trust0`: tests that run Lean in a mode that Lean doesn't
+- [`tests/lean/trust0`](https://github.com/leanprover/lean4/tree/master/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`: contains performance tests.
+- [`tests/bench`](https://github.com/leanprover/lean4/tree/master/tests/bench/): contains performance tests.
 
-- `tests/plugin`: tests that compiled Lean code can be loaded into
+- [`tests/plugin`](https://github.com/leanprover/lean4/tree/master/tests/plugin/): tests that compiled Lean code can be loaded into
   `lean` via the `--plugin` command line option.
 
+## Writing Good Tests
+
+Every test file should contain:
+* an initial `/-! -/` module docstring summarizing the test's purpose
+* a module docstring for each test section that describes what is tested
+  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).
+
 ## Fixing Tests
 
 When the Lean source code or the standard library are modified, some of the
@@ -101,7 +119,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 `test/lean` directory and
+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
 executing
 
 ```
@@ -114,8 +132,3 @@ 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/ex1.lean

@@ -0,0 +1,22 @@
+/- "Hello world" -/
+
+#eval "hello" ++ " " ++ "world"
+-- "hello world"
+
+#check true
+-- Bool
+
+def x := 10
+
+#eval x + 2
+-- 12
+
+def double (x : Int) := 2*x
+
+#eval double 3
+-- 6
+#check double
+-- Int → Int
+example : double 4 = 8 := rfl
+
+

doc/examples/Certora2022/ex10.lean

@@ -0,0 +1,19 @@
+/- Dependent pattern matching -/
+
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+
+infix:67 "::" => Vector.cons
+
+def Vector.zip : Vector α n → Vector β n → Vector (α × β) n
+  | nil, nil => nil
+  | a::as, b::bs => (a, b) :: zip as bs
+
+#print Vector.zip
+/-
+def Vector.zip.{u_1, u_2} : {α : Type u_1} → {n : Nat} → {β : Type u_2} → Vector α n → Vector β n → Vector (α × β) n :=
+fun {α} {n} {β} x x_1 =>
+  Vector.brecOn (motive := fun {n} x => {β : Type u_2} → Vector β n → Vector (α × β) n) x
+    ...
+-/

doc/examples/Certora2022/ex11.lean

@@ -0,0 +1,22 @@
+/- Structures -/
+
+structure Point where
+  x : Int := 0
+  y : Int := 0
+  deriving Repr
+
+#eval Point.x (Point.mk 10 20)
+-- 10
+
+#eval { x := 10, y := 20 : Point }
+
+def p : Point := { y := 20 }
+
+#eval p.x
+#eval p.y
+#eval { p with x := 5 }
+-- { x := 5, y := 20 }
+
+structure Point3D extends Point where
+  z : Int
+

doc/examples/Certora2022/ex12.lean

@@ -0,0 +1,28 @@
+/- Type classes -/
+namespace Example
+
+class ToString (α : Type u) where
+  toString : α → String
+
+#check @ToString.toString
+-- {α : Type u_1} → [self : ToString α] → α → String
+
+instance : ToString String where
+  toString s := s
+
+instance : ToString Bool where
+  toString b := if b then "true" else "false"
+
+#eval ToString.toString "hello"
+export ToString (toString)
+#eval toString true
+-- "true"
+-- #eval toString (true, "hello") -- Error
+
+instance [ToString α] [ToString β] : ToString (α × β) where
+  toString p := "(" ++ toString p.1 ++ ", " ++ toString p.2 ++ ")"
+
+#eval toString (true, "hello")
+-- "(true, hello)"
+
+end Example

doc/examples/Certora2022/ex13.lean

@@ -0,0 +1,44 @@
+/- Type classes are heavily used in Lean -/
+namespace Example
+
+class Mul (α : Type u) where
+  mul : α → α → α
+
+infixl:70 " * " => Mul.mul
+
+def double [Mul α] (a : α) := a * a
+
+class Semigroup (α : Type u) extends Mul α where
+  mul_assoc : ∀ a b c : α, (a * b) * c = a * (b * c)
+
+instance : Semigroup Nat where
+  mul := Nat.mul
+  mul_assoc := Nat.mul_assoc
+
+#eval double 5
+
+class Functor (f : Type u → Type v) : Type (max (u+1) v) where
+  map : (α → β) → f α → f β
+
+infixr:100 " <$> " => Functor.map
+
+class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
+  id_map   (x : f α) : id <$> x = x
+  comp_map (g : α → β) (h : β → γ) (x : f α) :(h ∘ g) <$> x = h <$> g <$> x
+
+end Example
+
+/-
+`Deriving instances automatically`
+
+We have seen `deriving Repr` in a few examples.
+It is an instance generator.
+Lean comes equipped with generators for the following classes.
+`Repr`, `Inhabited`, `BEq`, `DecidableEq`,
+`Hashable`, `Ord`, `FromToJson`, `SizeOf`
+-/
+
+inductive Tree (α : Type u) where
+  | leaf (val : α)
+  | node (left right : Tree α)
+  deriving DecidableEq, Ord, Inhabited, Repr

doc/examples/Certora2022/ex14.lean

@@ -0,0 +1,31 @@
+/- Tactics -/
+
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq
+  apply And.intro
+  exact hp
+  apply And.intro
+  exact hq
+  exact hp
+
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq; apply And.intro hp; exact And.intro hq hp
+
+/- Structuring proofs -/
+
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq
+  apply And.intro
+  case left => exact hp
+  case right =>
+    apply And.intro
+    case left => exact hq
+    case right => exact hp
+
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq
+  apply And.intro
+  . exact hp
+  . apply And.intro
+    . exact hq
+    . exact hp

doc/examples/Certora2022/ex15.lean

@@ -0,0 +1,19 @@
+/- intro tactic variants -/
+
+example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro h
+  match h with
+  | Exists.intro w (And.intro hp hq) => exact Exists.intro w (And.intro hq hp)
+
+example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro (Exists.intro _ (And.intro hp hq))
+  exact Exists.intro _ (And.intro hq hp)
+
+example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro ⟨_, hp, hq⟩
+  exact ⟨_, hq, hp⟩
+
+example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by
+  intro
+    | ⟨_, .inl h⟩ => exact ⟨_, .inr h⟩
+    | ⟨_, .inr h⟩ => exact ⟨_, .inl h⟩

doc/examples/Certora2022/ex16.lean

@@ -0,0 +1,12 @@
+/- Inaccessible names -/
+
+example : ∀ x y : Nat, x = y → y = x := by
+  intros
+  apply Eq.symm
+  assumption
+
+example : ∀ x y : Nat, x = y → y = x := by
+  intros
+  apply Eq.symm
+  rename_i a b hab
+  exact hab

doc/examples/Certora2022/ex17.lean

@@ -0,0 +1,19 @@
+/- More tactics -/
+
+example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro h
+  cases h with
+  | intro x hpq =>
+    cases hpq with
+    | intro hp hq =>
+      exists x
+
+example : p ∧ q → q ∧ p := by
+  intro p
+  cases p
+  constructor <;> assumption
+
+example : p ∧ ¬ p → q := by
+  intro h
+  cases h
+  contradiction

doc/examples/Certora2022/ex18.lean

@@ -0,0 +1,20 @@
+/- Structuring proofs (cont.) -/
+
+example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
+  intro h
+  have hp : p := h.left
+  have hqr : q ∨ r := h.right
+  show (p ∧ q) ∨ (p ∧ r)
+  cases hqr with
+  | inl hq => exact Or.inl ⟨hp, hq⟩
+  | inr hr => exact Or.inr ⟨hp, hr⟩
+
+example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
+  intro ⟨hp, hqr⟩
+  cases hqr with
+  | inl hq =>
+    have := And.intro hp hq
+    apply Or.inl; exact this
+  | inr hr =>
+    have := And.intro hp hr
+    apply Or.inr; exact this

doc/examples/Certora2022/ex19.lean

@@ -0,0 +1,10 @@
+/- Tactic combinators -/
+
+example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
+  intros
+  repeat (any_goals constructor)
+  all_goals assumption
+
+example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
+  intros
+  repeat (any_goals (first | assumption | constructor))

doc/examples/Certora2022/ex2.lean

@@ -0,0 +1,14 @@
+/- First-class functions -/
+
+def twice (f : Nat → Nat) (a : Nat) :=
+  f (f a)
+
+#check twice
+-- (Nat → Nat) → Nat → Nat
+
+#eval twice (fun x => x + 2) 10
+
+theorem twice_add_2 (a : Nat) : twice (fun x => x + 2) a = a + 4 := rfl
+
+-- `(· + 2)` is syntax sugar for `(fun x => x + 2)`.
+#eval twice (· + 2) 10

doc/examples/Certora2022/ex20.lean

@@ -0,0 +1,22 @@
+/- Rewriting -/
+
+example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
+  rw [h₂] -- replace k with 0
+  rw [h₁] -- replace f 0 with 0
+
+example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
+  rw [h₂, h₁]
+
+example (f : Nat → Nat) (a b : Nat) (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := by
+  rw [← h₁, h₂]
+
+example (f : Nat → Nat) (a : Nat) (h : 0 + a = 0) : f a = f 0 := by
+  rw [Nat.zero_add] at h
+  rw [h]
+
+def Tuple (α : Type) (n : Nat) :=
+  { as : List α // as.length = n }
+
+example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by
+  rw [h] at t
+  exact t

doc/examples/Certora2022/ex21.lean

@@ -0,0 +1,21 @@
+/- Simplifier -/
+
+example (p : Nat → Prop) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
+  simp
+
+example (p : Nat → Prop) (h : p (x * y)) : p ((x + 0) * (0 + y * 1 + z * 0)) := by
+  simp; assumption
+
+example (p : Nat → Prop) (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := by
+  simp at h; assumption
+
+def f (m n : Nat) : Nat :=
+  m + n + m
+
+example (h : n = 1) (h' : 0 = m) : (f m n) = n := by
+  simp [h, ←h', f]
+
+example (p : Nat → Prop) (h₁ : x + 0 = x') (h₂ : y + 0 = y')
+        : x + y + 0 = x' + y' := by
+  simp at *
+  simp [*]

doc/examples/Certora2022/ex22.lean

@@ -0,0 +1,13 @@
+/- Simplifier -/
+
+def mk_symm (xs : List α) :=
+  xs ++ xs.reverse
+
+@[simp] theorem reverse_mk_symm : (mk_symm xs).reverse = mk_symm xs := by
+  simp [mk_symm]
+
+theorem tst : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
+  simp
+
+#print tst
+-- Lean reverse_mk_symm, and List.reverse_append

doc/examples/Certora2022/ex23.lean

@@ -0,0 +1,26 @@
+/- split tactic -/
+
+def f (x y z : Nat) : Nat :=
+  match x, y, z with
+  | 5, _, _ => y
+  | _, 5, _ => y
+  | _, _, 5 => y
+  | _, _, _ => 1
+
+example : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := by
+  intros
+  simp [f]
+  split
+  . contradiction
+  . contradiction
+  . contradiction
+  . rfl
+
+def g (xs ys : List Nat) : Nat :=
+  match xs, ys with
+  | [a, b], _ => a+b+1
+  | _, [b, c] => b+1
+  | _, _      => 1
+
+example (xs ys : List Nat) (h : g xs ys = 0) : False := by
+  unfold g at h; split at h <;> simp_arith at h

doc/examples/Certora2022/ex24.lean

@@ -0,0 +1,9 @@
+/- induction tactic -/
+
+example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
+  induction as with
+  | nil => rfl
+  | cons _ xs ih => simp [List.concat, ih]
+
+example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
+  induction as <;> simp! [*]

doc/examples/Certora2022/ex3.lean

@@ -0,0 +1,59 @@
+/- Enumerated types -/
+
+inductive Weekday where
+  | sunday | monday | tuesday | wednesday
+  | thursday | friday | saturday
+
+#check Weekday.sunday
+-- Weekday
+
+open Weekday
+#check sunday
+
+def natOfWeekday (d : Weekday) : Nat :=
+  match d with
+  | sunday    => 1
+  | monday    => 2
+  | tuesday   => 3
+  | wednesday => 4
+  | thursday  => 5
+  | friday    => 6
+  | saturday  => 7
+
+def Weekday.next (d : Weekday) : Weekday :=
+  match d with
+  | sunday    => monday
+  | monday    => tuesday
+  | tuesday   => wednesday
+  | wednesday => thursday
+  | thursday  => friday
+  | friday    => saturday
+  | saturday  => sunday
+
+def Weekday.previous : Weekday → Weekday
+  | sunday    => saturday
+  | monday    => sunday
+  | tuesday   => monday
+  | wednesday => tuesday
+  | thursday  => wednesday
+  | friday    => thursday
+  | saturday  => friday
+
+/- Proving theorems using tactics -/
+
+theorem Weekday.next_previous (d : Weekday) : d.next.previous = d :=
+  match d with
+  | sunday    => rfl
+  | monday    => rfl
+  | tuesday   => rfl
+  | wednesday => rfl
+  | thursday  => rfl
+  | friday    => rfl
+  | saturday  => rfl
+
+theorem Weekday.next_previous' (d : Weekday) : d.next.previous = d := by -- switch to tactic mode
+  cases d -- Creates 7 goals
+  rfl; rfl; rfl; rfl; rfl; rfl; rfl
+
+theorem Weekday.next_previous'' (d : Weekday) : d.next.previous = d := by
+  cases d <;> rfl

doc/examples/Certora2022/ex4.lean

@@ -0,0 +1,20 @@
+/- What is the type of Nat? -/
+
+#check 0
+-- Nat
+#check Nat
+-- Type
+#check Type
+-- Type 1
+#check Type 1
+-- Type 2
+#check Eq.refl 2
+-- 2 = 2
+#check 2 = 2
+-- Prop
+#check Prop
+-- Type
+
+example : Prop = Sort 0   := rfl
+example : Type = Sort 1   := rfl
+example : Type 1 = Sort 2 := rfl

doc/examples/Certora2022/ex5.lean

@@ -0,0 +1,21 @@
+/- Implicit arguments and universe polymorphism -/
+
+def f (α β : Sort u) (a : α) (b : β) : α := a
+
+#eval f Nat String 1 "hello"
+-- 1
+
+def g {α β : Sort u} (a : α) (b : β) : α := a
+
+#eval g 1 "hello"
+
+def h (a : α) (b : β) : α := a
+
+#check g
+-- ?m.1 → ?m.2 → ?m.1
+#check @g
+-- {α β : Sort u} → α → β → α
+#check @h
+-- {α : Sort u_1} → {β : Sort u_2} → α → β → α
+#check g (α := Nat) (β := String)
+-- Nat → String → Nat

doc/examples/Certora2022/ex6.lean

@@ -0,0 +1,14 @@
+/- Inductive Types -/
+
+inductive Tree (β : Type v) where
+  | leaf
+  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
+  deriving Repr
+
+#eval Tree.node .leaf 10 true .leaf
+-- Tree.node Tree.leaf 10 true Tree.leaf
+
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+

doc/examples/Certora2022/ex7.lean

@@ -0,0 +1,25 @@
+/- Recursive functions -/
+
+#print Nat -- Nat is an inductive datatype
+
+def fib (n : Nat) : Nat :=
+  match n with
+  | 0 => 1
+  | 1 => 1
+  | n+2 => fib (n+1) + fib n
+
+example : fib 5 = 8 := rfl
+
+example : fib (n+2) = fib (n+1) + fib n := rfl
+
+#print fib
+/-
+def fib : Nat → Nat :=
+fun n =>
+  Nat.brecOn n fun n f =>
+    (match (motive := (n : Nat) → Nat.below n → Nat) n with
+      | 0 => fun x => 1
+      | 1 => fun x => 1
+      | Nat.succ (Nat.succ n) => fun x => x.fst.fst + x.fst.snd.fst.fst)
+      f
+-/

doc/examples/Certora2022/ex8.lean

@@ -0,0 +1,25 @@
+/- Well-founded recursion -/
+
+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)
+
+def sum (a : Array Int) : Int :=
+  let rec go (i : Nat) :=
+     if _ : i < a.size then
+        a[i] + go (i+1)
+     else
+        0
+  termination_by a.size - i
+  go 0
+
+set_option pp.proofs true
+#print sum.go
+/-
+def sum.go : Array Int → Nat → Int :=
+fun a =>
+  WellFounded.fix (sum.go.proof_1 a) fun i a_1 =>
+    if h : i < Array.size a then Array.getOp a i + a_1 (i + 1) (sum.go.proof_2 a i h) else 0
+-/

doc/examples/Certora2022/ex9.lean

@@ -0,0 +1,44 @@
+/- Mutual recursion -/
+
+inductive Term where
+ | const : String → Term
+ | app   : String → List Term → Term
+
+namespace Term
+mutual
+ def numConsts : Term → Nat
+   | const _ => 1
+   | app _ cs => numConstsLst cs
+
+ def numConstsLst : List Term → Nat
+   | [] => 0
+   | c :: cs => numConsts c + numConstsLst cs
+end
+
+mutual
+  def replaceConst (a b : String) : Term → Term
+   | const c => if a = c then const b else const c
+   | app f cs => app f (replaceConstLst a b cs)
+
+  def replaceConstLst (a b : String) : List Term → List Term
+   | [] => []
+   | c :: cs => replaceConst a b c :: replaceConstLst a b cs
+end
+
+/- Mutual recursion in theorems -/
+
+mutual
+  theorem numConsts_replaceConst (a b : String) (e : Term)
+            : numConsts (replaceConst a b e) = numConsts e := by
+    match e with
+    | const c => simp [replaceConst]; split <;> simp [numConsts]
+    | app f cs => simp [replaceConst, numConsts, numConsts_replaceConstLst a b cs]
+
+  theorem numConsts_replaceConstLst (a b : String) (es : List Term)
+            : numConstsLst (replaceConstLst a b es) = numConstsLst es := by
+    match es with
+    | [] => simp [replaceConstLst, numConstsLst]
+    | c :: cs =>
+      simp [replaceConstLst, numConstsLst, numConsts_replaceConst a b c,
+            numConsts_replaceConstLst a b cs]
+end

doc/examples/ICERM2022/ctor.lean

@@ -4,43 +4,42 @@ open Lean Meta
 
 def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
   /- Set `MetaM` context using `mvarId` -/
-  withMVarContext mvarId do 
+  mvarId.withContext do
     /- Fail if the metavariable is already assigned. -/
-    checkNotAssigned mvarId `ctor
+    mvarId.checkNotAssigned `ctor
     /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← getMVarType' mvarId
+    let target ← mvarId.getType'
     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
-      apply mvarId (.const ctors[idx - 1] us)
+      mvarId.apply (.const ctors[idx - 1] us)
     else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"  
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} constructors"
 
 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,15 +66,17 @@ 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 stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
+    let abStx ← exprToSyntax ab
+    let aStx ← exprToSyntax a
+    let stx ← `(fun x => if x < 10 then $abStx + x else x + $aStx)
     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 ack x y => (x, y)
+termination_by 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

@@ -5,7 +5,7 @@ If the type of keys can be totally ordered -- that is, it supports a well-behave
 then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time
 proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.
 
-This example is based on a similar example found in the ["Sofware Foundations"](https://softwarefoundations.cis.upenn.edu/vfa-current/SearchTree.html)
+This example is based on a similar example found in the ["Software Foundations"](https://softwarefoundations.cis.upenn.edu/vfa-current/SearchTree.html)
 book (volume 3).
 -/
 
@@ -81,9 +81,9 @@ def Tree.toList (t : Tree β) : List (Nat × β) :=
       |>.toList
 
 /-!
-The implemention of `Tree.toList` is inefficient because of how it uses the `++` operator.
+The implementation of `Tree.toList` is inefficient because of how it uses the `++` operator.
 On a balanced tree its running time is linearithmic, because it does a linear number of
-concatentations at each level of the tree. On an unbalanced tree it's quadratic time.
+concatenations at each level of the tree. On an unbalanced tree it's quadratic time.
 Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:
 -/
 def Tree.toListTR (t : Tree β) : List (Nat × β) :=
@@ -114,9 +114,9 @@ concatenating all goals produced by `tac'`. In this theorem, we use it to apply
 
 The `simp` parameters `toListTR.go` and `toList` instruct the simplifier to try to reduce
 and/or apply auto generated equation theorems for these two functions.
-The parameter `*` intructs the simplifier to use any equation in a goal as rewriting rules.
+The parameter `*` instructs the simplifier to use any equation in a goal as rewriting rules.
 In this particular case, `simp` uses the induction hypotheses as rewriting rules.
-Finally, the parameter `List.append_assoc` intructs the simplifier to use the
+Finally, the parameter `List.append_assoc` instructs the simplifier to use the
 `List.append_assoc` theorem as a rewriting rule.
 -/
 theorem Tree.toList_eq_toListTR (t : Tree β)
@@ -176,7 +176,8 @@ The modifier `local` specifies the scope of the macro.
 /-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
     and then replaces `lhs` with `rhs`. -/
 local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
-  `((have h : $lhs = $rhs :=
+  `(tactic|
+    (have h : $lhs = $rhs :=
        -- TODO: replace with linarith
        by simp_arith at *; apply Nat.le_antisymm <;> assumption
      try subst $lhs))
@@ -185,13 +186,13 @@ local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
 The `by_cases' e` is just the regular `by_cases` followed by `simp` using all
 hypotheses in the current goal as rewriting rules.
 Recall that the `by_cases` tactic creates two goals. One where we have `h : e` and
-another one containing `h : ¬ e`. The simplier uses the `h` to rewrite `e` to `True`
+another one containing `h : ¬ e`. The simplifier uses the `h` to rewrite `e` to `True`
 in the first subgoal, and `e` to `False` in the second. This is particularly
 useful if `e` is the condition of an `if`-statement.
 -/
 /-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
 local macro "by_cases' " e:term :  tactic =>
-  `(by_cases $e <;> simp [*])
+  `(tactic| by_cases $e <;> simp [*])
 
 
 /-!
@@ -276,14 +277,13 @@ 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 β) (h : k ≠ k') (v : β)
+theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
         : (b.insert k v).find? k' = b.find? k' := by
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    split <;> simp <;> split <;> simp
-    have_eq k k'
-    contradiction
+    intros le
+    exact Nat.lt_of_le_of_ne le ne
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h
     specialize ihl bl

doc/examples/compiler/.gitignore

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

doc/examples/deBruijn.lean

@@ -149,10 +149,10 @@ 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/simplications rules.
+use hypotheses such as `a = b` as rewriting/simplifications 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 simplier to use the equation as a rewriting rule in
+The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in
 the "reverse direction". That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.
 -/
 theorem Term.constFold_sound (e : Term ctx ty) : e.constFold.denote env = e.denote env := by

doc/examples/interp.lean

@@ -12,17 +12,17 @@ Remark: this example is based on an example found in the Idris manual.
 Vectors
 --------
 
-A `Vector` is a list of size `n` whose elements belong to a type `α`.
+A `Vec` is a list of size `n` whose elements belong to a type `α`.
 -/
 
-inductive Vector (α : Type u) : Nat → Type u
-  | nil : Vector α 0
-  | cons : α → Vector α n → Vector α (n+1)
+inductive Vec (α : Type u) : Nat → Type u
+  | nil : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
 
 /-!
-We can overload the `List.cons` notation `::` and use it to create `Vector`s.
+We can overload the `List.cons` notation `::` and use it to create `Vec`s.
 -/
-infix:67 " :: " => Vector.cons
+infix:67 " :: " => Vec.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 → Vector Ty n → Ty → Type where
+inductive HasType : Fin n → Vec Ty n → Ty → Type where
   | stop : HasType 0 (ty :: ctx) ty
   | pop  : HasType k ctx ty → HasType k.succ (u :: ctx) ty
 
-inductive Expr : Vector Ty n → Ty → Type where
+inductive Expr : Vec 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)
@@ -83,7 +83,7 @@ In practice, this means we use `stop` to refer to the most recently defined vari
 
 A value `Expr.val` carries a concrete representation of an integer.
 
-A lambda `Expr.lam` creates a function. In the scope of a function ot type `Ty.fn a ty`, there is a
+A lambda `Expr.lam` creates a function. In the scope of a function of type `Ty.fn a ty`, there is a
 new local variable of type `a`.
 
 A function application `Expr.app` produces a value of type `ty` given a function from `a` to `ty` and a value of type `a`.
@@ -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 : Vector Ty n → Type where
-  | nil  : Env Vector.nil
+inductive Env : Vec Ty n → Type where
+  | nil  : Env Vec.nil
   | cons : Ty.interp a → Env ctx → Env (a :: ctx)
 
 infix:67 " :: " => Env.cons
@@ -139,7 +139,7 @@ def add : Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int)) :=
 More interestingly, a factorial function fact (e.g. `fun x => if (x == 0) then 1 else (fact (x-1) * x)`), can be written as.
 Note that this is a recursive (non-terminating) definition. For every input value, the interpreter terminates, but the
 definition itself is non-terminating. We use two tricks to make sure Lean accepts it. First, we use the auxiliary constructor
-`Expr.delay` to delay its unfolding. Second, we add the annotation `decreasing_by sorry` which can be viwed as
+`Expr.delay` to delay its unfolding. Second, we add the annotation `decreasing_by sorry` which can be viewed as
 "trust me, this recursive definition makes sense". Recall that `sorry` is an unsound axiom in Lean.
 -/
 
@@ -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 => as.length
+termination_by as.length
 
 /-!
 We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds.

doc/examples/phoas.lean

@@ -225,10 +225,10 @@ 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/simplications rules.
+use hypotheses such as `a = b` as rewriting/simplifications 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 simplier to use the equation as a rewriting rule in
+The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in
 the "reverse direction. That is, given `h : a = b`, `← h` instructs the term simplifier to rewrite `b` subterms to `a`.
 -/
 theorem constFold_sound (e : Term' Ty.denote ty) : denote (constFold e) = denote e := by

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 the `cases` tactic. This tactic creates a new subgoal for every constructor,
+by using 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.
@@ -38,7 +38,7 @@ theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t
   cases h₁ <;> cases h₂ <;> rfl
 
 /-!
-The inductive type `Maybe p` has two contructors: `found a h` and `unknown`.
+The inductive type `Maybe p` has two constructors: `found a h` and `unknown`.
 The former contains an element `a : α` and a proof that `a` satisfies the predicate `p`.
 The constructor `unknown` is used to encode "failure".
 -/
@@ -82,9 +82,7 @@ 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. 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 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 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 lean -j 0 -Dlinter.all=false "$f"
+exec_check lean -Dlinter.all=false "$f"

doc/examples/widgets.lean

@@ -4,76 +4,97 @@ 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, simply type in the following code and place your cursor over the `#widget` command.
+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).
 -/
 
-@[widget]
-def helloWidget : UserWidgetDefinition where
-  name := "Hello"
+@[widget_module]
+def helloWidget : Widget.Module where
   javascript := "
     import * as React from 'react';
     export default function(props) {
       const name = props.name || 'world'
-      return React.createElement('p', {}, name + '!')
+      return React.createElement('p', {}, 'Hello ' + name + '!')
     }"
 
-#widget helloWidget .null
+#widget helloWidget
 
 /-!
 If you want to dive into a full sample right away, check out
-[`RubiksCube`](https://github.com/leanprover/lean4-samples/blob/main/RubiksCube/).
+[`Rubiks`](https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/Rubiks.lean).
+This sample uses higher-level widget components from the ProofWidgets library.
+
 Below, we'll explain the system piece by piece.
 
 ⚠️ WARNING: All of the user widget APIs are **unstable** and subject to breaking changes.
 
-## Widget sources and instances
+## Widget modules and instances
 
-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 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.
 
-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:
+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:
 -/
 
-#widget helloWidget (Json.mkObj [("name", "<your name here>")])
+structure HelloWidgetProps where
+  name? : Option String := none
+  deriving Server.RpcEncodable
+
+#widget helloWidget with { name? := "<your name here>" : HelloWidgetProps }
 
 /-!
-💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case
-is the web-based infoview in VSCode.
+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".
+-/
 
+/-!
 ## Querying the Lean server
 
-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.
+💡 NOTE: The RPC system presented below does not depend on JavaScript.
+However, the primary use case is the web-based infoview in VSCode.
 
-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).
+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).
 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`. We'll see below why the position field is needed.
+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.
 -/
 
 structure GetTypeParams where
@@ -84,103 +105,142 @@ structure GetTypeParams where
   deriving FromJson, ToJson
 
 /-!
-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.
+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:
 
-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.
+- 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.
 -/
 
 open Server RequestM in
-@[serverRpcMethod]
+@[server_rpc_method]
 def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) :=
   withWaitFindSnapAtPos params.pos fun snap => do
     runTermElabM snap do
       let name ← resolveGlobalConstNoOverloadCore params.name
-      let some c ← Meta.getConst? name
-        | throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩
+      let c ← try getConstInfo name
+        catch _ => throwThe RequestError ⟨.invalidParams, s!"no constant named '{name}'"⟩
       Widget.ppExprTagged c.type
 
 /-!
 ## Using infoview components
 
-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.
+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.
 
 ⚠️ 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 use the `RpcContext`.
-The `useAsync` helper packs the results of a call into a `status` enum, the returned `val`ue in case
-the call was successful, and otherwise an `err`or. Based on the `status` we either display
-an `InteractiveCode`, or `mapRpcError` the error in order to turn it into a readable message.
+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.
 -/
 
-@[widget]
-def checkWidget : UserWidgetDefinition where
-  name := "#check as a service"
+@[widget_module]
+def checkWidget : Widget.Module where
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
-import { RpcContext, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
+import { useRpcSession, InteractiveCode, useAsync, mapRpcError } from '@leanprover/infoview';
 
 export default function(props) {
-  const rs = React.useContext(RpcContext)
+  const rs = useRpcSession()
   const [name, setName] = React.useState('getType')
 
-  const [status, val, err] = useAsync(() =>
+  const st = useAsync(() =>
     rs.call('getType', { name, pos: props.pos }), [name, rs, props.pos])
 
-  const type = status === 'fulfilled' ? val && e(InteractiveCode, {fmt: val})
-    : status === 'rejected' ? e('p', null, mapRpcError(err).message)
-      : e('p', null, 'Loading..')
-
+  const type = st.state === 'resolved' ? st.value && e(InteractiveCode, {fmt: st.value})
+    : st.state === 'rejected' ? e('p', null, mapRpcError(st.error).message)
+    : e('p', null, 'Loading..')
   const onChange = (event) => { setName(event.target.value) }
   return e('div', null,
-    e('input', { value: name, onChange }),
-    ' : ',
-    type)
+    e('input', { value: name, onChange }), ' : ', type)
 }
 "
 
 /-!
-Finally we can try out the widget.
+We can now try out the widget.
 -/
 
-#widget checkWidget .null
+#widget checkWidget
 
 /-!
 ![`#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 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:
+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:
 - 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.
 
-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).
+ProofWidgets provides a working `rollup.js` build configuration in
+[rollup.config.js](https://github.com/leanprover-community/ProofWidgets4/blob/main/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.
+
+The full API can be viewed [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52).
 -/
+
+@[widget_module]
+def insertTextWidget : Widget.Module where
+  javascript := "
+import * as React from 'react';
+const e = React.createElement;
+import { EditorContext } from '@leanprover/infoview';
+
+export default function(props) {
+  const editorConnection = React.useContext(EditorContext)
+  function onClick() {
+    editorConnection.api.insertText('-- hello!!!', 'above')
+  }
+
+  return e('div', null, e('button', { value: name, onClick }, 'insert'))
+}
+"
+
+#widget insertTextWidget

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 to ``t``.
+* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces 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:
@@ -406,7 +406,7 @@ The reduction relation is transitive, which is to say, is ``s`` reduces to ``s'`
 
 This last fact reflects the intuition that once we have proved a proposition ``p``, we only care that is has been proved; the proof does nothing more than witness the fact that ``p`` is true.
 
-Definitional equality is a strong notion of equalty of values. Lean's logical foundations sanction treating definitionally equal terms as being the same when checking that a term is well-typed and/or that it has a given type.
+Definitional equality is a strong notion of equality of values. Lean's logical foundations sanction treating definitionally equal terms as being the same when checking that a term is well-typed and/or that it has a given type.
 
 The reduction relation is believed to be strongly normalizing, which is to say, every sequence of reductions applied to a term will eventually terminate. The property guarantees that Lean's type-checking algorithm terminates, at least in principle. The consistency of Lean and its soundness with respect to set-theoretic semantics do not depend on either of these properties.
 

doc/faq.md

@@ -7,15 +7,6 @@ Lean is a new open source theorem prover being developed at Microsoft Research.
 It is a research project that aims to bridge the gap between interactive and automated theorem proving.
 Lean can be also used as a programming language. Actually, some Lean features are implemented in Lean itself.
 
-### Are pull requests welcome?
-
-In the past, we accepted most pull requests. This practice produced hard to maintain code, performance problems, and bugs.
-It takes time to review a pull request and make sure it is correct, useful and is not in conflict with our plans.
-Small bug fixes (few lines of code) are always welcome. Any other kind of unrequested pull request is not.
-Thus, before implementing a feature or modifying the system, please ask whether the change is welcome or not.
-We have issues tagged with ["help wanted"](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+label%3A%22help+wanted%22), if you want to contribute to the project, please take a look at them.
-If you are interested in one of them, post comments, ask questions, and engage with the core developers there.
-
 ### Should I use Lean?
 
 Lean is under heavy development, and we are constantly trying new
@@ -36,7 +27,7 @@ It is a good place to interact with other Lean users.
 ### Should I use Lean to teach a course?
 
 Lean has been used to teach courses on logic, type theory and programming languages at CMU and the University of Washington.
-The lecture notes for the CMU course [Logic and Proof](https://leanprover.github.io/logic_and_proof) are available online,
+The lecture notes for the CMU course [Logic and Proof](https://lean-lang.org/logic_and_proof) are available online,
 but they are for Lean 3.
 If you decide to teach a course using Lean, we suggest you prepare all material before the beginning of the course, and
 make sure that Lean attends all your needs. You should not expect we will fix bugs and/or add features needed for your course.
@@ -56,7 +47,7 @@ We expect similar independent checkers will be built for Lean 4.
 
 We use [GitHub](https://github.com/leanprover/lean4/issues) to track bugs and new features.
 Bug reports are always welcome, but nitpicking issues are not (e.g., the error message is confusing).
-See also our [contribution guidelines](../CONTRIBUTING.md).
+See also our [contribution guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md).
 
 ### Is it Lean, LEAN, or L∃∀N?
 

doc/flake.lock

@@ -18,12 +18,15 @@
       }
     },
     "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
       "locked": {
-        "lastModified": 1644229661,
-        "narHash": "sha256-1YdnJAsNy69bpcjuoKdOYQX0YxZBiCYZo4Twxerqv7k=",
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "3cecb5b042f7f209c56ffd8371b2711a290ec797",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
         "type": "github"
       },
       "original": {
@@ -35,14 +38,12 @@
     "lean": {
       "inputs": {
         "flake-utils": "flake-utils",
-        "lean-stage0": "lean-stage0",
-        "lean4-mode": "lean4-mode",
-        "nix": "nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs",
+        "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
         "lastModified": 0,
-        "narHash": "sha256-AfBkKX6Ahb9YbZke+eWLmsUk1Z9BwdJ1CpIoPY8Msx8=",
+        "narHash": "sha256-saRAtQ6VautVXKDw1XH35qwP0KEBKTKZbg/TRa4N9Vw=",
         "path": "../.",
         "type": "path"
       },
@@ -51,69 +52,23 @@
         "type": "path"
       }
     },
-    "lean-stage0": {
-      "locked": {
-        "lastModified": 0,
-        "narHash": "sha256-3K/43lSW4WIHNG+HHVKCD1odS63mHuaQ4ueHyTIkcls=",
-        "owner": "leanprover",
-        "repo": "lean4",
-        "rev": "0000000000000000000000000000000000000000",
-        "type": "github"
-      },
-      "original": {
-        "owner": "leanprover",
-        "repo": "lean4",
-        "type": "github"
-      }
-    },
-    "lean4-mode": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1647694750,
-        "narHash": "sha256-0rV61KhevG9IAjZDN2Ts2VS65fiUAPAezbf282u7yy8=",
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "rev": "c016c7aeee92564836355083664c49ed57024427",
-        "type": "github"
-      },
-      "original": {
-        "owner": "leanprover",
-        "repo": "lean4-mode",
-        "type": "github"
-      }
-    },
     "leanInk": {
       "flake": false,
       "locked": {
-        "lastModified": 1656863690,
-        "narHash": "sha256-9tmynTTeJGhYZaltS4xhSJgLTpe7Ta1ofV6U1SA/5V4=",
+        "lastModified": 1704976501,
+        "narHash": "sha256-FSBUsbX0HxakSnYRYzRBDN2YKmH9EkA0q9p7TSPEJTI=",
         "owner": "leanprover",
         "repo": "LeanInk",
-        "rev": "4b5e606ea8cc54c2447ce48706f8ec1d133d19e9",
+        "rev": "51821e3c2c032c88e4b2956483899d373ec090c4",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
+        "ref": "refs/pull/57/merge",
         "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"
-      }
-    },
     "mdBook": {
       "flake": false,
       "locked": {
@@ -130,63 +85,13 @@
         "type": "github"
       }
     },
-    "nix": {
-      "inputs": {
-        "lowdown-src": "lowdown-src",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-regression": "nixpkgs-regression"
-      },
-      "locked": {
-        "lastModified": 1648022028,
-        "narHash": "sha256-HtwmifW6STPcym+3uJ4YavgTKTYVIoiQHg3f0wXOm+Q=",
-        "owner": "NixOS",
-        "repo": "nix",
-        "rev": "98ce1a21b7d959c5575fac566c8699e91703a9f7",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nix",
-        "type": "github"
-      }
-    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1632864508,
-        "narHash": "sha256-d127FIvGR41XbVRDPVvozUPQ/uRHbHwvfyKHwEt5xFM=",
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "82891b5e2c2359d7e58d08849e4c89511ab94234",
-        "type": "github"
-      },
-      "original": {
-        "id": "nixpkgs",
-        "ref": "nixos-21.05-small",
-        "type": "indirect"
-      }
-    },
-    "nixpkgs-regression": {
-      "locked": {
-        "lastModified": 1643052045,
-        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "github"
-      },
-      "original": {
-        "id": "nixpkgs",
-        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
-        "type": "indirect"
-      }
-    },
-    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1648219316,
-        "narHash": "sha256-Ctij+dOi0ZZIfX5eMhgwugfvB+WZSrvVNAyAuANOsnQ=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "30d3d79b7d3607d56546dd2a6b49e156ba0ec634",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
         "type": "github"
       },
       "original": {
@@ -196,6 +101,23 @@
         "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",
@@ -207,6 +129,21 @@
         "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

@@ -4,20 +4,20 @@
   inputs.lean.url = path:../.;
   inputs.flake-utils.follows = "lean/flake-utils";
   inputs.mdBook = {
-    url = github:leanprover/mdBook;
+    url = "github:leanprover/mdBook";
     flake = false;
   };
   inputs.alectryon = {
-    url = github:Kha/alectryon/typeid;
+    url = "github:Kha/alectryon/typeid";
     flake = false;
   };
   inputs.leanInk = {
-    url = github:leanprover/LeanInk;
+    url = "github:leanprover/LeanInk/refs/pull/57/merge";
     flake = false;
   };
 
   outputs = inputs@{ self, ... }: inputs.flake-utils.lib.eachDefaultSystem (system:
-    with inputs.lean.packages.${system}; with nixpkgs;
+    with inputs.lean.packages.${system}.deprecated; 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-mhTWHs/bsmm3FH59SkUxBTl5lEH2Rlz/aF9CuBTu1TE=";
+          outputHash = "sha256-CO3A9Kpp4sIvkT9X3p+GTidazk7Fn4jf0AP2PINN44A=";
         });
         doCheck = false;
       });
@@ -44,21 +44,6 @@
           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;
@@ -78,22 +63,30 @@
           (with python3Packages; [ pygments dominate beautifulsoup4 docutils ]);
         doCheck = false;
       };
-      renderLean = name: file: runCommandNoCC "${name}.md" { buildInputs = [ alectryon ]; } ''
-        mkdir -p $(basename $out/${name})
-        alectryon --frontend lean4+markup ${file} --backend webpage -o $out/${name}.md
-      '';
-      listFilesRecursiveRel = root: dir: lib.flatten (lib.mapAttrsToList (name: type:
-        if type == "directory" then
-          listFilesRecursiveRel root ("${dir}/${name}")
-        else
-          dir + "/${name}"
-      ) (builtins.readDir "${root}/${dir}"));
-      renderDir = dir: let
-        inputs = builtins.filter (n: builtins.match ".*\.lean" n != null) (listFilesRecursiveRel dir ".");
-        outputs = lib.genAttrs inputs (n: renderLean n "${dir}/${n}");
-      in
-        outputs // symlinkJoin { inherit name; paths = lib.attrValues outputs; };
-      inked = renderDir ./.;
+      renderLeanMod = mod: mod.overrideAttrs (final: prev: {
+        name = "${prev.name}.md";
+        buildInputs = prev.buildInputs ++ [ alectryon ];
+        outputs = [ "out" ];
+        buildCommand = ''
+          dir=$(dirname $relpath)
+          mkdir -p $dir out/$dir
+          if [ -d $src ]; then cp -r $src/. $dir/; else cp $src $leanPath; fi
+          alectryon --frontend lean4+markup $leanPath --backend webpage -o $out/$leanPath.md
+        '';
+      });
+      renderPackage = pkg: symlinkJoin {
+        name = "${pkg.name}-mds";
+        paths = map renderLeanMod (lib.attrValues pkg.mods);
+      };
+      literate = buildLeanPackage {
+        name = "literate";
+        src = ./.;
+        roots = [
+          { mod = "examples"; glob = "submodules"; }
+          { mod = "monads"; glob = "submodules"; }
+        ];
+      };
+      inked = renderPackage literate;
       doc = book;
     };
     defaultPackage = self.packages.${system}.doc;

doc/fplean.md

@@ -1,7 +1,7 @@
 Functional Programming in Lean
 =======================
 
-The goal of [this book](https://leanprover.github.io/functional_programming_in_lean/) is to be an accessible introduction to using Lean 4 as a programming language.
+The goal of [this book](https://lean-lang.org/functional_programming_in_lean/) is to be an accessible introduction to using Lean 4 as a programming language.
 It should be useful both to people who want to use Lean as a general-purpose programming language and to mathematicians who want to develop larger-scale proof automation but do not have a background in functional programming.
 It does not assume any background with functional programming, though it's probably not a good first book on programming in general.
 New content will be added once per month until it's done.

doc/functions.md

@@ -32,8 +32,8 @@ def fact x :=
 
 #eval fact 100
 ```
-By default, Lean only accepts total functions. The `partial` keyword should be used when Lean cannot
-establish that a function always terminates.
+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.
 ```lean
 partial def g (x : Nat) (p : Nat -> Bool) : Nat :=
   if p x then

doc/highlight.js

@@ -1143,7 +1143,7 @@ hljs.registerLanguage("lean", function(hljs) {
       'sorry admit',
   };
 
-  var LEAN_IDENT_RE = /[A-Za-z_][\\w\u207F-\u209C\u1D62-\u1D6A\u2079\'0-9]*/;
+  var LEAN_IDENT_RE = /[A-Za-z_][\\w\u207F-\u209C\u1D62-\u1D6A\u2079\'0-9?]*/;
 
   var DASH_COMMENT = hljs.COMMENT('--', '$');
   var MULTI_LINE_COMMENT = hljs.COMMENT('/-[^-]', '-/');
@@ -1167,7 +1167,7 @@ hljs.registerLanguage("lean", function(hljs) {
 
   var LEAN_DEFINITION =	{
     className: 'theorem',
-    beginKeywords: 'def theorem lemma class instance structure',
+    begin: '\\b(def|theorem|lemma|class|structure|(?<!deriving\\s+)instance)\\b',
     end: ':= | where',
     excludeEnd: true,
     contains: [

doc/inductive.md

@@ -1,3 +1,3 @@
 # Inductive Types
 
-[Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html) has a chapter about inductive datatypes.
+[Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html) has a chapter about inductive datatypes.

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 -- -2
+#eval -10 / 4 -- -3
 ```
 
 Similar to `Nat`, the internal representation of `Int` is optimized. Small integers are

doc/latex/lean4.py

@@ -1,100 +0,0 @@
-# -*- 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/latex/lstlean.tex

@@ -4,7 +4,7 @@
 
 \lstdefinelanguage{lean} {
 
-% Anything betweeen $ becomes LaTeX math mode
+% Anything between $ becomes LaTeX math mode
 mathescape=false,
 % Comments may or not include Latex commands
 texcl=false,
@@ -201,6 +201,7 @@ literate=
 
 {ₙ}{{\ensuremath{_n}}}1
 {ₘ}{{\ensuremath{_m}}}1
+{ₚ}{{\ensuremath{_p}}}1
 {↑}{{\ensuremath{\uparrow}}}1
 {↓}{{\ensuremath{\downarrow}}}1
 
@@ -264,7 +265,7 @@ columns=[l]fullflexible,
 % Style for (listings') identifiers
 identifierstyle={\ttfamily\color{black}},
 % Note : highlighting of Coq identifiers is done through a new
-% delimiter definition through an lstset at the begining of the
+% delimiter definition through an lstset at the beginning of the
 % document. Don't know how to do better.
 
 % Style for declaration keywords

doc/lean3changes.md

@@ -42,7 +42,7 @@ def Sum.str : Option Nat → String :=
 ## Implicit lambdas
 
 In Lean 3 stdlib, we find many [instances](https://github.com/leanprover/lean/blob/master/library/init/category/reader.lean#L39) of the dreadful `@`+`_` idiom.
-It is often used when we the expected type is a function type with implicit arguments,
+It is often used when the expected type is a function type with implicit arguments,
 and we have a constant (`reader_t.pure` in the example) which also takes implicit arguments. In Lean 4, the elaborator automatically introduces lambdas
 for consuming implicit arguments. We are still exploring this feature and analyzing its impact, but the experience so far has been very positive. As an example,
 here is the example in the link above using Lean 4 implicit lambdas.
@@ -85,7 +85,7 @@ def id5 : {α : Type} → α → α :=
 
 ## Sugar for simple functions
 
-In Lean 3, we can create simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` As a placeholder. Here are a few examples:
+In Lean 3, we can create simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` as a placeholder. Here are a few examples:
 
 ```lean
 # namespace ex3
@@ -196,6 +196,8 @@ example (f : Nat → Nat) (a b c : Nat) : f (a + b + c) = f (a + (b + c)) :=
   congrArg f (Nat.add_assoc ..)
 ```
 
+In Lean 4, writing `f(x)` in place of `f x` is no longer allowed, you must use whitespace between the function and its arguments (e.g., `f (x)`).
+
 ## Dependent function types
 
 Given `α : Type` and `β : α → Type`, `(x : α) → β x` denotes the type of functions `f` with the property that,
@@ -287,11 +289,11 @@ Lean execution runtime. For example, we cannot prove in Lean that arrays have a
 the runtime used to execute Lean programs guarantees that an array cannot have more than 2^64 (2^32) elements
 in a 64-bit (32-bit) machine. We can take advantage of this fact to provide a more efficient implementation for
 array functions. However, the efficient version would not be very useful if it can only be used in
-unsafe code. Thus, Lean 4 provides the attribute `@[implementedBy functionName]`. The idea is to provide
+unsafe code. Thus, Lean 4 provides the attribute `@[implemented_by functionName]`. The idea is to provide
 an unsafe (and potentially more efficient) version of a safe definition or constant. The function `f`
-at the attribute `@[implementedBy f]` is very similar to an extern/foreign function,
+at the attribute `@[implemented_by f]` is very similar to an extern/foreign function,
 the key difference is that it is implemented in Lean itself. Again, the logical soundness of the system
-cannot be compromised by using the attribute `implementedBy`, but if the implementation is incorrect your
+cannot be compromised by using the attribute `implemented_by`, but if the implementation is incorrect your
 program may crash at runtime. In the following example, we define `withPtrUnsafe a k h` which
 executes `k` using the memory address where `a` is stored in memory. The argument `h` is proof
 that `k` is a constant function. Then, we "seal" this unsafe implementation at `withPtr`. The proof `h`
@@ -302,7 +304,7 @@ unsafe
 def withPtrUnsafe {α β : Type} (a : α) (k : USize → β) (h : ∀ u, k u = k 0) : β :=
   k (ptrAddrUnsafe a)
 
-@[implementedBy withPtrUnsafe]
+@[implemented_by withPtrUnsafe]
 def withPtr {α β : Type} (a : α) (k : USize → β) (h : ∀ u, k u = k 0) : β :=
   k 0
 ```
@@ -340,8 +342,7 @@ partial def f (x : Nat) : IO Unit := do
 
 These are changes to the library which may trip up Lean 3 users:
 
-- `Option` and `List` are no longer monads. Instead there is `OptionM`. This was done to avoid some performance traps. For example `o₁ <|> o₂` where `o₁ o₂ : Option α` will evaluate both `o₁` and `o₂` even if `o₁` evaluates to `some x`. This can be a problem if `o₂` requires a lot of compute to evaluate. A zulip discussion on this design choice is [here](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Option.20do.20notation.20regression.3F).
-
+- `List` is no longer a monad.
 
 ## Style changes