merge master

There is a test file in Std that should later be reunited with this
code.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

.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,45 @@
+---
+name: Bug report
+about: Create a bug report
+title: ''
+labels: bug
+assignees: ''
+
+---
+
+### Prerequisites
+
+* [ ] Put an X between the brackets on this line if you have done all of the following:
+    * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
+    * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
+
+### Description
+
+[Clear and concise description of the issue]
+
+### Context
+
+[Broader context that the issue occured in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
+
+### Steps to Reproduce
+
+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 `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
+[OS version]
+
+### 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,14 @@
+# 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.
+* 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.
+
+---
+
+Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)

.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@v3
+    - name: actionlint
+      uses: raven-actions/actionlint@v1
+      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/ci.yml

@@ -6,85 +6,252 @@ on:
     tags:
       - '*'
   pull_request:
-    branches:
-      - master
+    types: [opened, synchronize, reopened, labeled]
+  merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
 
+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 }}
+      # Should we run only a quick CI? Yes on a pull request without the full-ci label
+      quick: ${{ steps.set-quick.outputs.quick }}
+      # The build matrix, dynamically generated here
+      matrix: ${{ steps.set-matrix.outputs.result }}
+      # Should we make a nightly release? If so, this output contains the lean version string, else it is empty
+      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: Run quick CI?
+        id: set-quick
+        env:
+          quick: ${{
+            github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
+           }}
+        run: |
+          echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
+
+      - name: Configure build matrix
+        id: set-matrix
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const quick = ${{ steps.set-quick.outputs.quick }};
+            console.log(`quick: ${quick}`)
+            let matrix = [
+              {
+                // portable release build: use channel with older glibc (2.27)
+                "name": "Linux LLVM",
+                "os": "ubuntu-latest",
+                "release": false,
+                "quick": false,
+                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
+                "binary-check": "ldd -v",
+                // foreign code may be linked against more recent glibc
+                // reverse-ffi needs to be updated to link to LLVM libraries
+                "CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
+                "CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
+              },
+              {
+                "name": "Linux release",
+                "os": "ubuntu-latest",
+                "release": true,
+                "quick": true,
+                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{}}\" --run \"bash -euxo pipefail {0}\"",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
+                "binary-check": "ldd -v",
+                // foreign code may be linked against more recent glibc
+                "CTEST_OPTIONS": "-E 'foreign'"
+              },
+              {
+                "name": "Linux",
+                "os": "ubuntu-latest",
+                "check-stage3": true,
+                "test-speedcenter": true,
+                "quick": false,
+              },
+              {
+                "name": "Linux Debug",
+                "os": "ubuntu-latest",
+                "quick": false,
+                "CMAKE_OPTIONS": "-DCMAKE_BUILD_TYPE=Debug",
+                // exclude seriously slow tests
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
+              },
+              {
+                "name": "Linux fsanitize",
+                "os": "ubuntu-latest",
+                "quick": false,
+                // turn off custom allocator & symbolic functions to make LSAN do its magic
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF",
+                // exclude seriously slow/problematic tests (laketests crash)
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
+              },
+              {
+                "name": "macOS",
+                "os": "macos-latest",
+                "release": true,
+                "quick": false,
+                "shell": "bash -euxo pipefail {0}",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
+                "binary-check": "otool -L",
+                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
+              },
+              {
+                "name": "macOS aarch64",
+                "os": "macos-latest",
+                "release": true,
+                "quick": false,
+                "cross": true,
+                "cross_target": "aarch64-apple-darwin",
+                "shell": "bash -euxo pipefail {0}",
+                "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm-aarch64-* lean-llvm-x86_64-*",
+                "binary-check": "otool -L",
+                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
+              },
+              {
+                "name": "Windows",
+                "os": "windows-2022",
+                "release": true,
+                "quick": false,
+                "shell": "msys2 {0}",
+                "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
+                // for reasons unknown, interactivetests are flaky on Windows
+                "CTEST_OPTIONS": "--repeat until-pass:2",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
+                "binary-check": "ldd"
+              },
+              {
+                "name": "Linux aarch64",
+                "os": "ubuntu-latest",
+                "CMAKE_OPTIONS": "-DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64",
+                "release": true,
+                "quick": false,
+                "cross": true,
+                "cross_target": "aarch64-unknown-linux-gnu",
+                "shell": "nix-shell --arg pkgsDist \"import (fetchTarball \\\"channel:nixos-19.03\\\") {{ localSystem.config = \\\"aarch64-unknown-linux-gnu\\\"; }}\" --run \"bash -euxo pipefail {0}\"",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm-aarch64-* lean-llvm-x86_64-*"
+              },
+              {
+                "name": "Linux 32bit",
+                "os": "ubuntu-latest",
+                // Use 32bit on stage0 and stage1 to keep oleans compatible
+                "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86",
+                "cmultilib": true,
+                "release": true,
+                "quick": false,
+                "cross": true,
+                "shell": "bash -euxo pipefail {0}"
+              },
+              {
+                "name": "Web Assembly",
+                "os": "ubuntu-latest",
+                // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
+                "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32",
+                "wasm": true,
+                "cmultilib": true,
+                "release": true,
+                "quick": false,
+                "cross": true,
+                "shell": "bash -euxo pipefail {0}",
+                // Just a few selected tests because wasm is slow
+                "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean\""
+              }
+            ];
+            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
+            if (quick) {
+              return matrix.filter((job) => job.quick)
+            } else {
+              return matrix
+            }
+
       - name: Checkout
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
+        # don't schedule nightlies on forks
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
       - name: Set Nightly
-        id: set
+        if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4'
+        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
+
   build:
-    needs: set-nightly
-    if: always()
+    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/13.0.0/lean-llvm-x86_64-linux-gnu.tar.zst
-            prepare-llvm: script/prepare-llvm-linux.sh lean-llvm*
-            binary-check: ldd -v
-          - 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/13.0.0/lean-llvm-x86_64-apple-darwin.tar.zst
-            prepare-llvm: script/prepare-llvm-macos.sh lean-llvm*
-            binary-check: otool -L
-          - 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/13.0.0/lean-llvm-x86_64-w64-windows-gnu.tar.zst
-            prepare-llvm: script/prepare-llvm-mingw.sh lean-llvm*
-            binary-check: ldd
-      # complete all jobs
-      fail-fast: false
     name: ${{ matrix.name }}
     env:
       # must be inside workspace
@@ -95,46 +262,90 @@ jobs:
       # squelch error message about missing nixpkgs channel
       NIX_BUILD_SHELL: bash
       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
+        uses: actions/checkout@v3
         with:
           submodules: true
+          # the default is to use a virtual merge commit between the PR and master: just use the PR
+          ref: ${{ github.event.pull_request.head.sha }}
       - name: Install Nix
-        uses: cachix/install-nix-action@v15
-        if: matrix.os == 'ubuntu-latest'
+        uses: cachix/install-nix-action@v18
+        with:
+          install_url: https://releases.nixos.org/nix/nix-2.12.0/install
+        if: matrix.os == 'ubuntu-latest' && !matrix.cmultilib
       - name: Install MSYS2
         uses: msys2/setup-msys2@v2
         with:
           msystem: clang64
-          install: make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache git zip unzip diffutils binutils tree mingw-w64-clang-x86_64-zstd tar
+          # `:p` means prefix with appropriate msystem prefix
+          pacboy: "make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
         if: matrix.os == 'windows-2022'
       - name: Install Brew Packages
         run: |
-          brew install ccache tree zstd coreutils
+          brew install ccache tree zstd coreutils gmp
         if: matrix.os == 'macos-latest'
+      - name: Setup emsdk
+        uses: mymindstorm/setup-emsdk@v12
+        with:
+          version: 3.1.44
+          actions-cache-folder: emsdk
+        if: matrix.wasm
+      - name: Install 32bit c libs
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y gcc-multilib g++-multilib ccache
+        if: matrix.cmultilib
       - name: Cache
-        uses: actions/cache@v2
+        uses: actions/cache@v3
         with:
           path: .ccache
-          key: ${{ matrix.name }}-build-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
-            ${{ matrix.name }}-build
+            ${{ matrix.name }}-build-v3
       - name: Setup
         run: |
           # open nix-shell once for initial setup
           true
         if: matrix.os == 'ubuntu-latest'
+      - name: Set up core dumps
+        run: |
+          mkdir -p $PWD/coredumps
+          # store in current directory, for easy uploading together with binary
+          echo $PWD/coredumps/%e.%p.%t | sudo tee /proc/sys/kernel/core_pattern
+        if: matrix.os == 'ubuntu-latest'
       - name: Build
         run: |
           mkdir build
           cd build
-          OPTIONS=()
-          [[ -z '${{ matrix.llvm-url }}' ]] || wget -q ${{ matrix.llvm-url }}
-          [[ -z '${{ matrix.prepare-llvm }}' ]] || eval "OPTIONS+=($(../${{ matrix.prepare-llvm }}))"
-          if [[ -n '${{ matrix.release }}' && -n '${{ needs.set-nightly.outputs.nightly }}' ]]; then
-            OPTIONS+=(-DLEAN_SPECIAL_VERSION_DESC=${{ needs.set-nightly.outputs.nightly }})
+          ulimit -c unlimited # coredumps
+          # 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.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/..
@@ -145,19 +356,19 @@ jobs:
       - name: List Install Tree
         run: |
           # omit contents of Init/, ...
-          tree --du -h lean-* | grep -E ' (Init|Std|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
-            tar cf - $dir | zstd -T0 --no-progress -19 -o pack/$dir.tar.zst
+          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
-            tar cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
+            ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
           fi
-      - uses: actions/upload-artifact@v2
+      - uses: actions/upload-artifact@v3
         if: matrix.release
         with:
           name: build-${{ matrix.name }}
@@ -165,79 +376,130 @@ jobs:
       - name: Lean stats
         run: |
           build/stage1/bin/lean --stats src/Lean.lean
+        if: ${{ !matrix.cross }}
       - name: Test
         run: |
           cd build/stage1
+          ulimit -c unlimited # coredumps
+          # exclude nonreproducible test
           ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
+        if: (matrix.wasm || !matrix.cross) && needs.configure.outputs.quick == 'false'
       - name: Check Test Binary
         run: ${{ matrix.binary-check }} tests/compiler/534.lean.out
+        if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
       - name: Build Stage 2
         run: |
           cd build
+          ulimit -c unlimited # coredumps
           make -j4 stage2
-        if: matrix.build-stage2 || matrix.check-stage3
+        if: matrix.test-speedcenter
       - name: Check Stage 3
         run: |
           cd build
+          ulimit -c unlimited # coredumps
           make -j4 check-stage3
-        if: matrix.check-stage3
+        if: matrix.test-speedcenter
       - name: Test Speedcenter Benchmarks
         run: |
           echo -1 | sudo tee /proc/sys/kernel/perf_event_paranoid
           export BUILD=$PWD/build PATH=$PWD/build/stage1/bin:$PATH
-          nix-shell -A with-temci --run "cd tests/bench; temci exec --config speedcenter.yaml --included_blocks fast --runs 1"
+          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
+          ulimit -c unlimited # coredumps
           make update-stage0 && make -j4
-        if: matrix.name == 'Linux'
+        if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
       - name: CCache stats
         run: ccache -s
-        
+      - name: Show stacktrace for coredumps
+        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        run: |
+          for c in coredumps/*; do
+            progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
+            echo bt | $GDB/bin/gdb -q $progbin $c || true
+          done
+      - name: Upload coredumps
+        uses: actions/upload-artifact@v3
+        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        with:
+          name: coredumps-${{ matrix.name }}
+          path: |
+            ./coredumps
+            ./build/stage0/bin/lean
+            ./build/stage0/lib/lean/libleanshared.so
+            ./build/stage1/bin/lean
+            ./build/stage1/lib/lean/libleanshared.so
+            ./build/stage2/bin/lean
+            ./build/stage2/lib/lean/libleanshared.so
+
+  # This job collects results from all the matrix jobs
+  # This can be made the “required” job, instead of listing each
+  # matrix job separately
+  all-done:
+    name: Build matrix complete
+    runs-on: ubuntu-latest
+    needs: build
+    if: ${{ always() }}
+    steps:
+    - if: contains(needs.*.result, 'failure') ||  contains(needs.*.result, 'cancelled')
+      uses: actions/github-script@v7
+      with:
+        script: |
+            core.setFailed('Some jobs failed')
+
+  # This job creates releases from tags
+  # (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.)
+  # We do not attempt to automatically construct a changelog here:
+  # unofficial releases don't need them, and official release notes will be written by a human.
   release:
-    if: ${{ 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@v3
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@v1       
+        uses: softprops/action-gh-release@v1
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_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@v3
         with:
           # needed for tagging
           fetch-depth: 0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v2
+      - uses: actions/download-artifact@v3
         with:
           path: artifacts
       - name: Prepare Nightly Release
         run: |
           git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
           git fetch nightly --tags
-          git tag ${{ needs.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
         with:
@@ -245,7 +507,7 @@ jobs:
           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 }}

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

@@ -0,0 +1,43 @@
+# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, or `WIP` labels,
+# by commenting on the PR or issue.
+# Other labels from this set are removed automatically at the same time.
+
+name: Label PR based on Comment
+
+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'))
+    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');
+
+          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'] });
+          }

.github/workflows/nix-ci.yml

@@ -6,110 +6,130 @@ on:
     tags:
       - '*'
   pull_request:
-    branches:
-      - master
+  merge_group:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
 
 jobs:
   Build:
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        # Can't use `nix-shell` without configured nixpkgs path on macOS
-        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
-            # latest builds on https://hydra.nixos.org/jobset/nix/master/all at the time
-            nix_url: https://hydra.nixos.org/build/135773533/download/1/nix-2.4pre20210125_36c4d6f-x86_64-linux.tar.xz
           #- name: Nix macOS
           #  os: macos-latest
-          #  nix_url: https://hydra.nixos.org/build/135773542/download/1/nix-2.4pre20210125_36c4d6f-x86_64-darwin.tar.xz
       # 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
-      # Install flakes-enabled Nix manually from Hydra since `install-nix-action` doesn't accept raw tarballs
-      - name: Install Nix
-        shell: bash -euo pipefail {0}
-        run: |
-          curl ${{ matrix.nix_url }} | tar -xJ
-          # Do a single-user install so actions/cache doesn't get confused about permissions
-          nix-*/install --no-daemon --no-channel-add --darwin-use-unencrypted-nix-store-volume
-          rm -rf nix-*
-      # Call `install-nix-action` anyways to run its Actions-specific setup
-      - name: Setup Nix
-        uses: cachix/install-nix-action@v12
-      - name: Fixup install-nix-action
-        shell: bash -euo pipefail {0}
-        run: |
-          # the path set by install-nix-action is valid only for multi-user installations
-          echo "NIX_SSL_CERT_FILE=$HOME/.nix-profile/etc/ssl/certs/ca-bundle.crt" > $GITHUB_ENV
-        if: matrix.name == 'macOS'
-      - name: Further setup Nix
-        run: |
-          mkdir -p ~/.config/nix
-          echo '
-            max-jobs = auto
-            extra-sandbox-paths = /nix/var/cache/ccache
-            extra-substituters = file://${{ github.workspace }}/nix-store-cache?priority=10&trusted=true
-            extra-trusted-substituters = https://lean4.cachix.org/
-            extra-trusted-public-keys = lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=' > ~/.config/nix/nix.conf
-          sudo mkdir -m0770 -p /nix/var/cache/ccache
-          # macOS standard chown doesn't support --reference
-          nix shell .#nixpkgs.coreutils -c sudo chown --reference=/nix /nix/var/cache/ccache
-          echo 'max_size = 50M' > /nix/var/cache/ccache/ccache.conf
-
-          # install & use Cachix manually since `cachix-action` pushes *all* derivations (incl. `$mod-deps`, stage 2&3, etc.)
-          [ -z '${{ secrets.CACHIX_AUTH_TOKEN }}' ] || nix-env -iA cachix -f https://cachix.org/api/v1/install
-      - name: Setup CCache Cache
-        uses: actions/cache@v2
+        uses: actions/checkout@v3
         with:
-          path: /nix/var/cache/ccache
-          key: ${{ matrix.name }}-nix-ccache-${{ github.sha }}
-          # fall back to (latest) previous cache
-          restore-keys: |
-            ${{ matrix.name }}-nix-ccache
-      - name: Setup Nix Cache
-        uses: actions/cache@v2
+          # 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@v3
         with:
           path: nix-store-cache
           key: ${{ matrix.name }}-nix-store-cache-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
             ${{ matrix.name }}-nix-store-cache
+      - 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
+        run: |
+          sudo mkdir -m0770 -p /nix/var/cache/ccache
+          sudo chown -R $USER /nix/var/cache/ccache
+      - name: Setup CCache Cache
+        uses: actions/cache@v3
+        with:
+          path: /nix/var/cache/ccache
+          key: ${{ matrix.name }}-nix-ccache-${{ github.sha }}
+          # fall back to (latest) previous cache
+          restore-keys: |
+            ${{ matrix.name }}-nix-ccache
+      - name: Further Set Up CCache Cache
+        run: |
+          sudo chown -R root:nixbld /nix/var/cache
+          sudo chmod -R 770 /nix/var/cache
+      - name: Install Cachix
+        uses: cachix/cachix-action@v12
+        with:
+          name: lean4
+          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+          skipPush: true  # we push specific outputs only
       - name: Build
         run: |
-          # .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 -o push-build
+          nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
       - name: Test
         run: |
           nix build $NIX_BUILD_ARGS .#test -o push-test
       - name: Build manual
         run: |
-          nix build $NIX_BUILD_ARGS .#mdbook .#doc-test -o push-doc
-          nix build $NIX_BUILD_ARGS .#doc
-        if: matrix.name == 'Linux'
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
+          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
+          # https://github.com/netlify/cli/issues/1809
+          cp -r --dereference ./result ./dist
+        if: matrix.name == 'Nix Linux'
+      - name: Check manual for broken links
+        id: lychee
+        uses: lycheeverse/lychee-action@v1.9.0
+        with:
+          fail: false  # report errors but do not block CI on temporary failures
+          # gmplib.org consistently times out from GH actions
+          # the GitHub token is to avoid rate limiting
+          args: --base './dist' --no-progress --github-token ${{ secrets.GITHUB_TOKEN }} --exclude 'gmplib.org' './dist/**/*.html'
       - name: Push to Cachix
         run: |
-          [ -z "$CACHIX_AUTH_TOKEN" ] || cachix push -j4 lean4 ./push-* || true
-        env:
-          CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_AUTH_TOKEN }}'
+          [ -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@v2.0
+        id: publish-manual
         with:
-          github_token: ${{ secrets.GITHUB_TOKEN }}
-          publish_dir: ./result
-          destination_dir: ./doc
-        if: matrix.name == '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-release.yml

@@ -0,0 +1,339 @@
+# 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@v2 # https://github.com/marketplace/actions/download-workflow-artifact
+        with:
+          run_id: ${{ github.event.workflow_run.id }}
+          path: artifacts
+          name: build-.*
+          name_is_regexp: true
+
+      - name: Push tag
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        run: |
+          git init --bare lean4.git
+          git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
+          git -C lean4.git fetch -n origin master
+          git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
+          git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+      - name: Delete existing release if present
+        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@v1
+        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@v6
+        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@v1.0.1
+
+      # Check that the most recently nightly coincides with 'git merge-base HEAD master'
+      - name: Check merge-base and nightly-testing-YYYY-MM-DD
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        id: ready
+        run: |
+          echo "Most recent nightly release in your branch: $MOST_RECENT_NIGHTLY"
+          NIGHTLY_SHA=$(git -C lean4.git rev-parse "nightly-$MOST_RECENT_NIGHTLY^{commit}")
+          echo "SHA of most recent nightly release: $NIGHTLY_SHA"
+          MERGE_BASE_SHA=$(git -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
+          echo "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"
+
+            MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+
+            if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
+              echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE=""
+            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
+
+            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+
+            if [[ -n "$STD_REMOTE_TAGS" ]]; then
+              echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE=""
+            else
+              echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE="- ❗ Std 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\`, Std 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
+
+            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch."
+          fi
+
+          if [[ -n "$MESSAGE" ]]; then
+
+            echo "Checking existing messages"
+
+            # The code for updating comments is duplicated in mathlib's
+            # scripts/lean-pr-testing-comments.sh
+            # so keep in sync
+
+            # Use GitHub API to check if a comment already exists
+            existing_comment="$(curl -L -s -H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
+                                    -H "Accept: application/vnd.github.v3+json" \
+                                    "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
+                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-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_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_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_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@v6
+        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 Std branch using this toolchain.
+      # Std 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 Std fails.
+      - name: Cleanup workspace
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
+        run: |
+          sudo rm -rf ./*
+
+      # Checkout the Std repository with all branches
+      - name: Checkout Std repository
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
+        uses: actions/checkout@v3
+        with:
+          repository: leanprover/std4
+          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_std_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 Std. 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 Std `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@v3
+        with:
+          repository: leanprover-community/mathlib4
+          token: ${{ secrets.MATHLIB4_BOT }}
+          ref: nightly-testing
+          fetch-depth: 0 # This ensures we check out all tags and branches.
+
+      - name: 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 std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
+            git add lakefile.lean
+            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 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
+            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/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@v8
+        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,64 @@
+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@v3
+      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 "<>"
+    - if: env.should_update_stage0 == 'yes'
+      uses: DeterminateSystems/nix-installer-action@main
+    # 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: Install Cachix
+      uses: cachix/cachix-action@v12
+      with:
+        name: lean4
+    - 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,10 @@
 \#*
 .#*
 *.lock
+.lake
+lake-manifest.json
 build
+!/src/lake/Lake/Build
 GPATH
 GRTAGS
 GSYMS
@@ -25,4 +28,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

.ignore

@@ -0,0 +1 @@
+stage0/

.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,17 @@ 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()
+
 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 +46,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 +55,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 +65,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

CODEOWNERS

@@ -0,0 +1,22 @@
+# 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 @semorrison
+/RELEASES.md @semorrison
+/src/ @leodemoura @Kha
+/src/Init/IO.lean @joehendrix
+/src/kernel/ @leodemoura
+/src/lake/ @tydeu
+/src/Lean/Compiler/ @leodemoura
+/src/Lean/Data/Lsp/ @mhuisi
+/src/Lean/Elab/Deriving/ @semorrison
+/src/Lean/Elab/Tactic/ @semorrison
+/src/Lean/Meta/Tactic/ @leodemoura
+/src/Lean/Parser/ @Kha
+/src/Lean/PrettyPrinter/ @Kha
+/src/Lean/Server/ @mhuisi
+/src/Lean/Widget/ @Vtec234
+/src/runtime/io.cpp @joehendrix

CONTRIBUTING.md

@@ -1,57 +1,79 @@
-# 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:
+----
+
+**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.

README.md

@@ -1,17 +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
 
-- [Homepage](https://leanprover.github.io)
-- [Theorem Proving Tutorial](https://leanprover.github.io/theorem_proving_in_lean4/)
-- [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
-- [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
 
@@ -19,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).

doc/BoolExpr.lean

@@ -1,4 +1,3 @@
-import Std
 open Std
 open Lean
 
@@ -104,9 +103,9 @@ syntax entry := ident " ↦ " term:max
 syntax entry,* "⊢" term : term
 
 macro_rules
-  | `( $[$xs:ident ↦ $vs:term],* ⊢ $p:term ) =>
+  | `( $[$xs ↦ $vs],* ⊢ $p) =>
     let xs := xs.map fun x => quote x.getId.toString
-    `(denote (List.toAssocList [$[( $xs , $vs )],*]) `[BExpr| $p])
+    `(denote (List.toAssocList [$[($xs, $vs)],*]) `[BExpr| $p])
 
 #check b ↦ true ⊢ b ∨ b
 #eval  a ↦ false, b ↦ false ⊢ b ∨ a

doc/SUMMARY.md

@@ -2,32 +2,44 @@
 
 - [What is Lean](./whatIsLean.md)
 - [Tour of Lean](./tour.md)
-- [Setting Up Lean](./setup.md)
-  - [Quickstart](./quickstart.md)
+- [Setting Up Lean](./quickstart.md)
+  - [Extended Setup Notes](./setup.md)
+- [Theorem Proving in Lean](./tpil.md)
+- [Functional Programming in Lean](fplean.md)
+- [Examples](./examples.md)
+  - [Palindromes](examples/palindromes.lean.md)
+  - [Binary Search Trees](examples/bintree.lean.md)
+  - [A Certified Type Checker](examples/tc.lean.md)
+  - [The Well-Typed Interpreter](examples/interp.lean.md)
+  - [Dependent de Bruijn Indices](examples/deBruijn.lean.md)
+  - [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.md)
 
 # Language Manual
-- [Using Lean](./using_lean.md)
-- [Lexical Structure](./lexical_structure.md)
-- [Expressions](./expressions.md)
-- [Declarations](./declarations.md)
+<!-- - [Using Lean](./using_lean.md) -->
+<!-- - [Lexical Structure](./lexical_structure.md) -->
+<!-- - [Expressions](./expressions.md) -->
+<!-- - [Declarations](./declarations.md) -->
 - [Organizational features](./organization.md)
   - [Sections](./sections.md)
   - [Namespaces](./namespaces.md)
   - [Implicit Arguments](./implicit.md)
   - [Auto Bound Implicit Arguments](./autobound.md)
-- [Dependent Types](./deptypes.md)
-  - [Simple Type Theory](./simptypes.md)
-  - [Types as objects](./typeobjs.md)
-  - [Function Abstraction and Evaluation](./funabst.md)
-  - [Introducing Definitions](./introdef.md)
-  - [What makes dependent type theory dependent?](./dep.md)
-- [Tactics](./tactics.md)
+<!-- - [Dependent Types](./deptypes.md) -->
+<!--   - [Simple Type Theory](./simptypes.md) -->
+<!--   - [Types as objects](./typeobjs.md) -->
+<!--   - [Function Abstraction and Evaluation](./funabst.md) -->
+<!--   - [Introducing Definitions](./introdef.md) -->
+<!--   - [What makes dependent type theory dependent?](./dep.md) -->
+<!-- - [Tactics](./tactics.md) -->
 - [Syntax Extensions](./syntax.md)
   - [The `do` Notation](./do.md)
-  - [User-defined notation](./notation.md)
   - [String Interpolation](./stringinterp.md)
+  - [User-Defined Notation](./notation.md)
   - [Macro Overview](./macro_overview.md)
-  - [A Guided Example](./syntax_example.md)
+  - [Elaborators](./elaborators.md)
+  - [Examples](./syntax_examples.md)
+    - [Balanced Parentheses](./syntax_example.md)
+    - [Arithmetic DSL](./metaprogramming-arith.md)
 - [Declaring New Types](./decltypes.md)
   - [Enumerated Types](./enum.md)
   - [Inductive Types](./inductive.md)
@@ -47,26 +59,35 @@
   - [Thunk](./thunk.md)
   - [Task and Thread](./task.md)
 - [Functions](./functions.md)
+- [Monads](./monads/intro.md)
+  - [Functor](./monads/functors.lean.md)
+  - [Applicative](./monads/applicatives.lean.md)
+  - [Monad](./monads/monads.lean.md)
+  - [Reader](./monads/readers.lean.md)
+  - [State](./monads/states.lean.md)
+  - [Except](./monads/except.lean.md)
+  - [Transformers](./monads/transformers.lean.md)
+  - [Laws](./monads/laws.lean.md)
 
 # Other
 
 - [Frequently Asked Questions](./faq.md)
 - [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
 
 - [Development Guide](./dev/index.md)
-- [Commit Convention](./dev/commit_convention.md)
 - [Building Lean](./make/index.md)
   - [Ubuntu Setup](./make/ubuntu.md)
   - [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)
-- [Foreign Function Interface](./dev/ffi.md)
-- [Unit Testing](./dev/testing.md)
-- [Building This Manual](./dev/mdbook.md)
-- [Fixing Tests](./dev/fixing_tests.md)
+- [Bootstrapping](./dev/bootstrap.md)
+- [Testing](./dev/testing.md)
 - [Debugging](./dev/debugging.md)
-- [C++ Coding Style](./dev/cpp_coding_style.md)
+- [Commit Convention](./dev/commit_convention.md)
+- [Building This Manual](./dev/mdbook.md)
+- [Foreign Function Interface](./dev/ffi.md)

doc/alectryon.css

@@ -0,0 +1,786 @@
+@charset "UTF-8";
+/*
+Copyright © 2019 Clément Pit-Claudel
+
+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.
+*/
+
+/*******************************/
+/* CSS reset for .alectryon-io */
+/*******************************/
+
+.content {
+    /*
+    Use `initial` instead of `contents` to avoid a browser bug which removes
+    the element from the accessibility tree.
+    https://developer.mozilla.org/en-US/docs/Web/CSS/display#display_contents
+     */
+    display: initial;
+}
+
+.alectryon-io blockquote {
+    line-height: inherit;
+}
+
+.alectryon-io blockquote:after {
+    display: none;
+}
+
+.alectryon-io label {
+    display: inline;
+    font-size: inherit;
+    margin: 0;
+}
+
+.alectryon-io a {
+    text-decoration: none !important;
+    font-style: oblique !important;
+    color: unset;
+}
+
+/* Undo <small> and <blockquote>, added to improve RSS rendering. */
+
+.alectryon-io small.alectryon-output,
+.alectryon-io small.alectryon-type-info {
+    font-size: inherit;
+}
+
+.alectryon-io blockquote.alectryon-goal,
+.alectryon-io blockquote.alectryon-message {
+    font-weight: normal;
+    font-size: inherit;
+}
+
+/***************/
+/* Main styles */
+/***************/
+
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .comment,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-mref,
+.alectryon-block, .alectryon-io,
+.alectryon-toggle-label, .alectryon-banner {
+    font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important;
+    font-size: 0.875em;
+    font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
+    line-height: initial;
+}
+
+.alectryon-io, .alectryon-block, .alectryon-toggle-label, .alectryon-banner {
+    overflow: visible;
+    overflow-wrap: break-word;
+    position: relative;
+    white-space: pre-wrap;
+}
+
+/*
+CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply
+respects the user's `bidi-display-reordering` setting), so don't turn it off
+here either.  But beware unexpected results like `Definition test_אב := 0.`
+
+.alectryon-io span {
+    direction: ltr;
+    unicode-bidi: bidi-override;
+}
+
+In any case, make an exception for comments:
+
+.highlight .c {
+    direction: embed;
+    unicode-bidi: initial;
+}
+*/
+
+.alectryon-mref,
+.alectryon-mref-marker {
+    align-self: center;
+    box-sizing: border-box;
+    display: inline-block;
+    font-size: 80%;
+    font-weight: bold;
+    line-height: 1;
+    box-shadow: 0 0 0 1pt black;
+    padding: 1pt 0.3em;
+    text-decoration: none;
+}
+
+.alectryon-block .alectryon-mref-marker,
+.alectryon-io .alectryon-mref-marker {
+    user-select: none;
+    margin: -0.25em 0 -0.25em 0.5em;
+}
+
+.alectryon-inline .alectryon-mref-marker {
+    margin: -0.25em 0.15em -0.25em 0.625em; /* 625 = 0.5em / 80% */
+}
+
+.alectryon-mref {
+    color: inherit;
+    margin: -0.5em 0.25em;
+}
+
+.alectryon-goal:target .goal-separator .alectryon-mref-marker,
+:target > .alectryon-mref-marker {
+    animation: blink 0.2s step-start 0s 3 normal none;
+    background-color: #fcaf3e;
+    position: relative;
+}
+
+@keyframes blink {
+    50% {
+        box-shadow: 0 0 0 3pt #fcaf3e, 0 0 0 4pt black;
+        z-index: 10;
+    }
+}
+
+.alectryon-toggle,
+.alectryon-io .alectryon-extra-goal-toggle {
+    display: none;
+}
+
+.alectryon-bubble,
+.alectryon-io label,
+.alectryon-toggle-label {
+    cursor: pointer;
+}
+
+.alectryon-toggle-label {
+    display: block;
+    font-size: 0.8em;
+}
+
+.alectryon-io .alectryon-input {
+    padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */
+}
+
+.alectryon-io .alectryon-token {
+    white-space: pre-wrap;
+    display: inline;
+}
+
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-input {
+    /* FIXME if keywords were ‘bolder’ we wouldn't need !important */
+    font-weight: bold !important; /* Use !important to avoid a * selector */
+}
+
+.alectryon-bubble:before,
+.alectryon-toggle-label:before,
+.alectryon-io label.alectryon-input:after,
+.alectryon-io .alectryon-goal > label:before {
+    border: 1px solid #babdb6;
+    border-radius: 1em;
+    box-sizing: border-box;
+    content: '';
+    display: inline-block;
+    font-weight: bold;
+    height: 0.25em;
+    margin-bottom: 0.15em;
+    vertical-align: middle;
+    width: 0.75em;
+}
+
+.alectryon-toggle-label:before,
+.alectryon-io .alectryon-goal > label:before {
+    margin-right: 0.25em;
+}
+
+.alectryon-io .alectryon-goal > label:before {
+    margin-top: 0.125em;
+}
+
+.alectryon-io label.alectryon-input {
+    padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
+}
+
+.alectryon-io label.alectryon-input:after {
+    margin-left: 0.25em;
+    margin-right: -1em; /* Compensate for the anti-wrapping space */
+}
+
+.alectryon-failed {
+    /* Underlines are broken in Chrome (they reset at each element boundary)… */
+    /* text-decoration: red wavy underline; */
+    /* … but it isn't too noticeable with dots */
+    text-decoration: red dotted underline;
+    text-decoration-skip-ink: none;
+    /* Chrome prints background images in low resolution, yielding a blurry underline */
+    /* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
+}
+
+/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
+   doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to
+   hide its output causes it to remain visible (its :hover state gets triggered.
+   We only do it for the default style though, since other styles don't put the
+   output over the main text, so showing too much is not an issue. */
+@media (any-hover: hover) {
+    .alectryon-bubble:hover:before,
+    .alectryon-toggle-label:hover:before,
+    .alectryon-io label.alectryon-input:hover:after {
+        background: #eeeeec;
+    }
+
+    .alectryon-io label.alectryon-input:hover {
+        text-decoration: underline dotted #babdb6;
+	    text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */
+    }
+
+    .alectryon-io .alectryon-sentence:hover .alectryon-output,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {
+        z-index: 2; /* Place hovered goals above .alectryon-sentence.alectryon-target ones */
+    }
+}
+
+.alectryon-toggle:checked + .alectryon-toggle-label:before,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked + label.alectryon-input:after,
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal > label:before {
+    background-color: #babdb6;
+    border-color: #babdb6;
+}
+
+/* Disable clicks on sentences when the document-wide toggle is set. */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input {
+    cursor: unset;
+    pointer-events: none;
+}
+
+/* Hide individual checkboxes when the document-wide toggle is set. */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input:after {
+    display: none;
+}
+
+/* .alectryon-output is displayed by toggles, :hover, and .alectryon-target rules */
+.alectryon-io .alectryon-output {
+    box-sizing: border-box;
+    display: none;
+    left: 0;
+    right: 0;
+    position: absolute;
+    padding: 0.25em 0;
+    overflow: visible; /* Let box-shadows overflow */
+    z-index: 1; /* Default to an index lower than that used by :hover */
+}
+
+.alectryon-io .alectryon-type-info-wrapper {
+    position: absolute;
+    display: inline-block;
+    width: 100%;
+}
+
+.alectryon-io .alectryon-type-info-wrapper.full-width {
+    left: 0;
+    min-width: 100%;
+    max-width: 100%;
+}
+
+.alectryon-io .alectryon-type-info .goal-separator {
+    height: unset;
+    margin-top: 0em;
+}
+
+.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info {
+    box-sizing: border-box;
+    bottom: 100%;
+    position: absolute;
+    /*padding: 0.25em 0;*/
+    visibility: hidden;
+    overflow: visible; /* Let box-shadows overflow */
+    z-index: 1; /* Default to an index lower than that used by :hover */
+    white-space: pre-wrap !important;
+}
+
+.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info .alectryon-goal.alectryon-docstring {
+    white-space: pre-wrap !important;
+}
+
+@media (any-hover: hover) { /* See note above about this @media query */
+    .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) {
+        display: block;
+    }
+
+    .alectryon-io.output-hidden .alectryon-sentence:hover .alectryon-output:not(:hover) {
+        display: none !important;
+    }
+
+    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
+    .alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+        /*visibility: hidden !important;*/
+    }
+
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
+    .alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+        visibility: visible;
+        transition-delay: 0.5s;
+    }
+}
+
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output {
+    display: block;
+}
+
+/* Indicate active (hovered or targeted) goals with a shadow. */
+.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
+.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
+.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals,
+.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
+    box-shadow: 2px 2px 2px gray;
+}
+
+.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-hyps {
+    display: none;
+}
+
+.alectryon-io .alectryon-extra-goals .alectryon-extra-goal-toggle:not(:checked) + .alectryon-goal label.goal-separator hr {
+    /* Dashes indicate that the hypotheses are hidden */
+    border-top-style: dashed;
+}
+
+
+/* Show just a small preview of the other goals; this is undone by the
+   "extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */
+.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-conclusion {
+    max-height: 5.2em;
+    overflow-y: auto;
+    /* Combining ‘overflow-y: auto’ with ‘display: inline-block’ causes extra space
+       to be added below the box. ‘vertical-align: middle’ gets rid of it. */
+    vertical-align: middle;
+}
+
+.alectryon-io .alectryon-goals,
+.alectryon-io .alectryon-messages {
+    background: #f6f7f6;
+	/*border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
+    display: block;
+    padding: 0.25em;
+}
+
+.alectryon-message::before {
+    content: '';
+    float: right;
+    /* etc/svg/square-bubble-xl.svg */
+    background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat;
+    height: 14px;
+    width: 14px;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container {
+    width: unset;
+}
+
+/* Show goals when a toggle is set */
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output {
+    display: block;
+    position: static;
+    width: unset;
+    background: unset; /* Override the backgrounds set in floating in windowed mode */
+    padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
+}
+
+.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output .goal-hyps {
+    /* Overridden back in windowed style */
+    flex-flow: row wrap;
+    justify-content: flex-start;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
+    display: block;
+}
+
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-hyps {
+    display: flex;
+}
+
+.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion {
+    max-height: unset;
+    overflow-y: unset;
+}
+
+.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence > .alectryon-toggle ~ .alectryon-wsp,
+.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-wsp {
+    display: none;
+}
+
+.alectryon-io .alectryon-messages,
+.alectryon-io .alectryon-message,
+.alectryon-io .alectryon-goals,
+.alectryon-io .alectryon-goal,
+.alectryon-io .goal-hyps > span,
+.alectryon-io .goal-conclusion {
+    border-radius: 0.15em;
+}
+
+.alectryon-io .alectryon-goal,
+.alectryon-io .alectryon-message {
+    align-items: center;
+    background: #f6f7f6;
+    border: 0em;
+    display: block;
+    flex-direction: column;
+    margin: 0.25em;
+    padding: 0.5em;
+    position: relative;
+}
+
+.alectryon-io .goal-hyps {
+    align-content: space-around;
+    align-items: baseline;
+    display: flex;
+    flex-flow: column nowrap; /* re-stated in windowed mode */
+    justify-content: space-around;
+    /* LATER use a ‘gap’ property instead of margins once supported */
+    margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
+    padding-bottom: 0.35em; /* 0.5em-0.15em to cancel the 0.5em of .goal-separator */
+}
+
+.alectryon-io .goal-hyps > br {
+    display: none; /* Only for RSS readers */
+}
+
+.alectryon-io .goal-hyps > span,
+.alectryon-io .goal-conclusion {
+    /*background: #eeeeec;*/
+    display: inline-block;
+    padding: 0.15em 0.35em;
+}
+
+.alectryon-io .goal-hyps > span {
+    align-items: baseline;
+    display: inline-flex;
+    margin: 0.15em 0.25em;
+}
+
+.alectryon-block var,
+.alectryon-inline var,
+.alectryon-io .goal-hyps > span > var {
+    font-weight: 600;
+    font-style: unset;
+}
+
+.alectryon-io .goal-hyps > span > var {
+    /* Shrink the list of names, but let it grow as long as space is available. */
+    flex-basis: min-content;
+    flex-grow: 1;
+}
+
+.alectryon-io .goal-hyps > span b {
+    font-weight: 600;
+    margin: 0 0 0 0.5em;
+    white-space: pre;
+}
+
+.alectryon-io .hyp-body,
+.alectryon-io .hyp-type {
+    display: flex;
+    align-items: baseline;
+}
+
+.alectryon-io .goal-separator {
+    align-items: center;
+    display: flex;
+    flex-direction: row;
+    height: 1em; /* Fixed height to ignore goal name and markers */
+    margin-top: -0.5em; /* Compensated in .goal-hyps when shown */
+}
+
+.alectryon-io .goal-separator hr {
+    border: none;
+    border-top: thin solid #555753;
+    display: block;
+    flex-grow: 1;
+    margin: 0;
+}
+
+.alectryon-io .goal-separator .goal-name {
+    font-size: 0.75em;
+    margin-left: 0.5em;
+}
+
+/**********/
+/* Banner */
+/**********/
+
+.alectryon-banner {
+    background: #eeeeec;
+    border: 1px solid #babcbd;
+    font-size: 0.75em;
+    padding: 0.25em;
+    text-align: center;
+    margin: 1em 0;
+}
+
+.alectryon-banner a {
+    cursor: pointer;
+    text-decoration: underline;
+}
+
+.alectryon-banner kbd {
+    background: #d3d7cf;
+    border-radius: 0.15em;
+    border: 1px solid #babdb6;
+    box-sizing: border-box;
+    display: inline-block;
+    font-family: inherit;
+    font-size: 0.9em;
+    height: 1.3em;
+    line-height: 1.2em;
+    margin: -0.25em 0;
+    padding: 0 0.25em;
+    vertical-align: middle;
+}
+
+/**********/
+/* Toggle */
+/**********/
+
+.alectryon-toggle-label {
+    margin: 1rem 0;
+}
+
+/******************/
+/* Floating style */
+/******************/
+
+/* If there's space, display goals to the right of the code, not below it. */
+@media (min-width: 80rem) {
+    /* Unlike the windowed case, we don't want to move output blocks to the side
+       when they are both :checked and -targeted, since it gets confusing as
+       things jump around; hence the commented-output part of the selector,
+       which would otherwise increase specificity */
+    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output,
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
+        top: 0;
+        left: 100%;
+        right: -100%;
+        padding: 0 0.5em;
+        position:  absolute;
+    }
+
+    .alectryon-floating .alectryon-output {
+        min-height: 100%;
+    }
+
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output {
+        background: white; /* Ensure that short goals hide long ones */
+    }
+
+    /* This odd margin-bottom property prevents the sticky div from bumping
+       against the bottom of its container (.alectryon-output).  The alternative
+       would be enlarging .alectryon-output, but that would cause overflows,
+       enlarging scrollbars and yielding scrolling towards the bottom of the
+       page.  Doing things this way instead makes it possible to restrict
+       .alectryon-output to a reasonable size (100%, through top = bottom = 0).
+       See also https://stackoverflow.com/questions/43909940/. */
+    /* See note on specificity above */
+    .alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output > div,
+    .alectryon-floating .alectryon-sentence:hover .alectryon-output > div {
+        margin-bottom: -200%;
+        position: sticky;
+        top: 0;
+    }
+
+    .alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
+    .alectryon-floating .alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
+        margin-bottom: unset; /* Undo the margin */
+    }
+
+    /* Float underneath the current fragment
+    @media (max-width: 80rem) {
+        .alectryon-floating .alectryon-output {
+            top: 100%;
+        }
+    } */
+}
+
+/********************/
+/* Multi-pane style */
+/********************/
+
+.alectryon-windowed {
+    border: 0 solid #2e3436;
+    box-sizing: border-box;
+}
+
+.alectryon-windowed .alectryon-sentence:hover .alectryon-output {
+    background: white; /* Ensure that short goals hide long ones */
+}
+
+.alectryon-windowed .alectryon-output {
+    position: fixed; /* Overwritten by the ‘:checked’ rules */
+}
+
+/* See note about specificity below */
+.alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
+    padding: 0.5em;
+    overflow-y: auto; /* Windowed contents may need to scroll */
+}
+
+.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-messages,
+.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output  .alectryon-goals {
+    box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */
+}
+
+.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .goal-hyps {
+    /* Restated to override the :checked style */
+    flex-flow: column nowrap;
+    justify-content: space-around;
+}
+
+
+.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-extra-goals .alectryon-goal .goal-conclusion
+/* Like .alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion */ {
+    max-height: unset;
+    overflow-y: unset;
+}
+
+.alectryon-windowed .alectryon-output > div {
+    display: flex; /* Put messages after goals */
+    flex-direction: column-reverse;
+}
+
+/*********************/
+/* Standalone styles */
+/*********************/
+
+.alectryon-standalone {
+    font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
+    line-height: 1.5;
+}
+
+@media screen and (min-width: 50rem) {
+    html.alectryon-standalone {
+        /* Prevent flickering when hovering a block causes scrollbars to appear. */
+        margin-left: calc(100vw - 100%);
+        margin-right: 0;
+    }
+}
+
+/* Coqdoc */
+
+.alectryon-coqdoc .doc .code,
+.alectryon-coqdoc .doc .inlinecode,
+.alectryon-coqdoc .doc .comment {
+    display: inline;
+}
+
+.alectryon-coqdoc .doc .comment {
+    color: #eeeeec;
+}
+
+.alectryon-coqdoc .doc .paragraph {
+    height: 0.75em;
+}
+
+/* Centered, Floating */
+
+.alectryon-standalone .alectryon-centered,
+.alectryon-standalone .alectryon-floating {
+    max-width: 50rem;
+    margin: auto;
+}
+
+@media (min-width: 80rem) {
+    .alectryon-standalone .alectryon-floating {
+        max-width: 80rem;
+    }
+
+    .alectryon-standalone .alectryon-floating > * {
+        width: 50%;
+        margin-left: 0;
+    }
+}
+
+/* Windowed */
+
+.alectryon-standalone .alectryon-windowed {
+    display: block;
+    margin: 0;
+    overflow-y: auto;
+    position: absolute;
+    padding: 0 1em;
+}
+
+.alectryon-standalone .alectryon-windowed > * {
+    /* Override properties of docutils_basic.css */
+    margin-left: 0;
+    max-width: unset;
+}
+
+.alectryon-standalone .alectryon-windowed .alectryon-io {
+    box-sizing: border-box;
+    width: 100%;
+}
+
+/* No need to predicate the ‘:hover’ rules below on ‘:not(:checked)’, since ‘left’,
+   ‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting
+   ‘position’ to ‘static’ */
+
+
+/* Specificity: We want the output to stay inline when hovered while unfolded
+   (:checked), but we want it to move when it's targeted (i.e. when the user
+   is browsing goals one by one using the keyboard, in which case we want to
+   goals to appear in consistent locations).  The selectors below ensure
+   that :hover < :checked < -targeted in terms of specificity. */
+/* LATER: Reimplement this stuff with CSS variables */
+.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
+    position: fixed;
+}
+
+@media screen and (min-width: 60rem) {
+    .alectryon-standalone .alectryon-windowed {
+        border-right-width: thin;
+        bottom: 0;
+        left: 0;
+        right: 50%;
+        top: 0;
+    }
+
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
+        bottom: 0;
+        left: 50%;
+        right: 0;
+        top: 0;
+    }
+}
+
+@media screen and (max-width: 60rem) {
+    .alectryon-standalone .alectryon-windowed {
+        border-bottom-width: 1px;
+        bottom: 40%;
+        left: 0;
+        right: 0;
+        top: 0;
+    }
+
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
+    .alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
+        bottom: 0;
+        left: 0;
+        right: 0;
+        top: 60%;
+    }
+}

doc/alectryon.js

@@ -0,0 +1,190 @@
+var Alectryon;
+(function(Alectryon) {
+    (function (slideshow) {
+        function anchor(sentence) { return "#" + sentence.id; }
+
+        function current_sentence() { return slideshow.sentences[slideshow.pos]; }
+
+        function unhighlight() {
+            var sentence = current_sentence();
+            if (sentence) sentence.classList.remove("alectryon-target");
+            slideshow.pos = -1;
+        }
+
+        function highlight(sentence) {
+            sentence.classList.add("alectryon-target");
+        }
+
+        function scroll(sentence) {
+            // Put the top of the current fragment close to the top of the
+            // screen, but scroll it out of view if showing it requires pushing
+            // the sentence past half of the screen.  If sentence is already in
+            // a reasonable position, don't move.
+            var parent = sentence.parentElement;
+            /* We want to scroll the whole document, so start at root… */
+            while (parent && !parent.classList.contains("alectryon-root"))
+                parent = parent.parentElement;
+            /* … and work up from there to find a scrollable element.
+               parent.scrollHeight can be greater than parent.clientHeight
+               without showing scrollbars, so we add a 10px buffer. */
+            while (parent && parent.scrollHeight <= parent.clientHeight + 10)
+                parent = parent.parentElement;
+            /* <body> and <html> elements can have their client rect overflow
+             * the window if their height is unset, so scroll the window
+             * instead */
+            if (parent && (parent.nodeName == "BODY" || parent.nodeName == "HTML"))
+                parent = null;
+
+            var rect = function(e) { return e.getBoundingClientRect(); };
+            var parent_box = parent ? rect(parent) : { y: 0, height: window.innerHeight },
+                sentence_y = rect(sentence).y - parent_box.y,
+                fragment_y = rect(sentence.parentElement).y - parent_box.y;
+
+            // The assertion below sometimes fails for the first element in a block.
+            // console.assert(sentence_y >= fragment_y);
+
+            if (sentence_y < 0.1 * parent_box.height ||
+                sentence_y > 0.7 * parent_box.height) {
+                (parent || window).scrollBy(
+                    0, Math.max(sentence_y - 0.5 * parent_box.height,
+                                fragment_y - 0.1 * parent_box.height));
+            }
+        }
+
+        function highlighted(pos) {
+            return slideshow.pos == pos;
+        }
+
+        function navigate(pos, inhibitScroll) {
+            unhighlight();
+            slideshow.pos = Math.min(Math.max(pos, 0), slideshow.sentences.length - 1);
+            var sentence = current_sentence();
+            highlight(sentence);
+            if (!inhibitScroll)
+                scroll(sentence);
+        }
+
+        var keys = {
+            PAGE_UP: 33,
+            PAGE_DOWN: 34,
+            ARROW_UP: 38,
+            ARROW_DOWN: 40,
+            h: 72, l: 76, p: 80, n: 78
+        };
+
+        function onkeydown(e) {
+            e = e || window.event;
+            if (e.ctrlKey || e.metaKey) {
+                if (e.keyCode == keys.ARROW_UP)
+                    slideshow.previous();
+                else if (e.keyCode == keys.ARROW_DOWN)
+                    slideshow.next();
+                else
+                    return;
+            } else {
+                // if (e.keyCode == keys.PAGE_UP || e.keyCode == keys.p || e.keyCode == keys.h)
+                //     slideshow.previous();
+                // else if (e.keyCode == keys.PAGE_DOWN || e.keyCode == keys.n || e.keyCode == keys.l)
+                //     slideshow.next();
+                // else
+                return;
+            }
+            e.preventDefault();
+        }
+
+        function start() {
+            slideshow.navigate(0);
+        }
+
+        function toggleHighlight(idx) {
+            if (highlighted(idx))
+                unhighlight();
+            else
+                navigate(idx, true);
+        }
+
+        function handleClick(evt) {
+            if (evt.ctrlKey || evt.metaKey) {
+                var sentence = evt.currentTarget;
+
+                // Ensure that the goal is shown on the side, not inline
+                var checkbox = sentence.getElementsByClassName("alectryon-toggle")[0];
+                if (checkbox)
+                    checkbox.checked = false;
+
+                toggleHighlight(sentence.alectryon_index);
+                evt.preventDefault();
+            }
+        }
+
+        function init() {
+            document.onkeydown = onkeydown;
+            slideshow.pos = -1;
+            slideshow.sentences = Array.from(document.getElementsByClassName("alectryon-sentence"));
+            slideshow.sentences.forEach(function (s, idx) {
+                s.addEventListener('click', handleClick, false);
+                s.alectryon_index = idx;
+            });
+        }
+
+        slideshow.start = start;
+        slideshow.end = unhighlight;
+        slideshow.navigate = navigate;
+        slideshow.next = function() { navigate(slideshow.pos + 1); };
+        slideshow.previous = function() { navigate(slideshow.pos + -1); };
+        window.addEventListener('DOMContentLoaded', init);
+    })(Alectryon.slideshow || (Alectryon.slideshow = {}));
+
+    (function (styles) {
+        var styleNames = ["centered", "floating", "windowed"];
+
+        function className(style) {
+            return "alectryon-" + style;
+        }
+
+        function setStyle(style) {
+            var root = document.getElementsByClassName("alectryon-root")[0];
+            styleNames.forEach(function (s) {
+                root.classList.remove(className(s)); });
+            root.classList.add(className(style));
+        }
+
+        function init() {
+            var banner = document.getElementsByClassName("alectryon-banner")[0];
+            if (banner) {
+                banner.append(" Style: ");
+                styleNames.forEach(function (styleName, idx) {
+                    var s = styleName;
+                    var a = document.createElement("a");
+                    a.onclick = function() { setStyle(s); };
+                    a.append(styleName);
+                    if (idx > 0) banner.append("; ");
+                    banner.appendChild(a);
+                });
+                banner.append(".");
+            }
+        }
+
+        window.addEventListener('DOMContentLoaded', init);
+
+        styles.setStyle = setStyle;
+    })(Alectryon.styles || (Alectryon.styles = {}));
+})(Alectryon || (Alectryon = {}));
+
+function setHidden(elements, isVisible, token) {
+    for (let i = 0; i < elements.length; i++) {
+        if (isVisible) {
+            elements[i].classList.remove(token)
+        } else {
+            elements[i].classList.add(token)
+        }
+    }
+}
+
+function toggleShowTypes(checkbox) {
+    setHidden(document.getElementsByClassName("alectryon-io"), checkbox.checked, "type-info-hidden")
+}
+
+function toggleShowGoals(checkbox) {
+    setHidden(document.getElementsByClassName("alectryon-io"), checkbox.checked, "output-hidden")
+}

doc/array.md

@@ -39,16 +39,17 @@ To create an array of size `n` in which all the elements are initialized to some
 
 You can access array elements by using brackets (`[` and `]`).
 ```lean
-#eval #['a', 'b', 'c'][1]
--- 'b'
-
-def getThird (xs : Array Nat) : Nat :=
-  xs[2]
-
-#eval getThird #[10, 20, 30, 40]
--- 30
+def f (a : Array Nat) (i : Fin a.size) :=
+  a[i] + a[i]
+```
+Note that the index `i` has type `Fin a.size`, i.e., it is natural number less than `a.size`.
+You can also write
+```lean
+def f (a : Array Nat) (i : Nat) (h  : i < a.size) :=
+  a[i] + a[i]
 ```
 The bracket operator is whitespace sensitive.
+
 ```lean
 def f (xs : List Nat) : List Nat :=
   xs ++ xs
@@ -56,7 +57,21 @@ def f (xs : List Nat) : List Nat :=
 def as : Array Nat :=
   #[1, 2, 3, 4]
 
+def idx : Fin 4 :=
+  2
+
 #eval f [1, 2, 3] -- This is a function application
 
-#eval as[2] -- This is an array access
+#eval as[idx] -- This is an array access
+```
+The notation `a[i]` has two variants: `a[i]!` and `a[i]?`. In both cases, `i` has type `Nat`. The first one
+produces a panic error message if the index `i` is out of bounds. The latter returns an `Option` type.
+
+```lean
+#eval #['a', 'b', 'c'][1]?
+-- some 'b'
+#eval #['a', 'b', 'c'][5]?
+-- none
+#eval #['a', 'b', 'c'][1]!
+-- 'b!
 ```

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/book.toml

@@ -10,6 +10,12 @@ build-dir = "out"
 
 [output.html]
 git-repository-url = "https://github.com/leanprover/lean4"
+additional-css = ["alectryon.css", "pygments.css"]
+additional-js = ["alectryon.js"]
+
+[output.html.fold]
+enable = true
+level = 0
 
 [output.html.playground.boring-prefixes]
 lean = "# "

doc/dev/bootstrap.md

@@ -1,4 +1,3 @@
-
 # Lean Build Bootstrapping
 
 Since version 4, Lean is a partially bootstrapped program: most parts of the
@@ -16,17 +15,18 @@ stage0/
   bin/lean
 stage1/
   include/
-    config.h  # config variables used to build `lean` such as use allocator
-    runtime/lean.h  # runtime headers, used by extracted C code, uses `config.h`
+    config.h  # config variables used to build `lean` such as used allocator
+    runtime/lean.h  # runtime header, used by extracted C code, uses `config.h`
   share/lean/
-    Makefile  # used by `leanmake`
+    lean.mk  # used by `leanmake`
   lib/
     lean/**/*.olean  # the Lean library (incl. the compiler) compiled by the previous stage's `lean`
     temp/**/*.{c,o}  # the library extracted to C and compiled by `leanc`
-    libInit.a libStd.a libLean.a  # static libraries of the Lean library
+    libInit.a libLean.a  # static libraries of the Lean library
     libleancpp.a  # a static library of the C++ sources of Lean
+    libleanshared.so  # a dynamic library including the static libraries above
   bin/
-    lean  # the Lean compiler & server linked together from the above libraries
+    lean  # the Lean compiler & server, a small executable that calls directly into libleanshared.so
     leanc  # a wrapper around a C compiler supplying search paths etc
     leanmake  # a wrapper around `make` supplying the Makefile above
 stage2/...
@@ -55,7 +55,7 @@ We are not aware of any "meta-meta" parts that influence more than two stages of
 compilation, so stage 3 should always be identical to stage 2 and only exists as
 a sanity check.
 
-In summary, doing a standard build via `make` involves these steps:
+In summary, doing a standard build via `make` internally involves these steps:
 
 1. compile the `stage0/src` archived sources into `stage0/bin/lean`
 1. use it to compile the current library (*including* your changes) into `stage1/lib`
@@ -65,9 +65,36 @@ 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 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/nomeata/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 preferrable, but should you need
+to do it locally, you can use `make update-stage0` in `build/release`, to
+update `stage0` from `stage1`, `make -C stageN update-stage0` to update from
+another stage, or `nix run .#update-stage0-commit` to update using nix.
+
+Updates to `stage0` should be their own commits in the Git history. So should
+you have to include the stage0 update in your PR (rather than using above
+automation after merging changes), commit your work before running `make
+update-stage0`, commit the updated `stage0` compiler code with the commit
+message:
+```
+chore: update stage0
+```
+and coordinate with the admins to not squash your PR.
 
 ## Further Bootstrapping Complications
 
@@ -119,4 +146,4 @@ affect later stages. This is an issue in two specific cases.
 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
 on the next `update-stage0` when the file is overwritten with the original
-version in `src/`.
+version in `src/`.

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/cpp_coding_style.md

@@ -1,155 +0,0 @@
-[google-style]: https://google.github.io/styleguide/cppguide.html
-[cpplint]: /src/cmake/Modules/cpplint.py
-
-# Coding Style
-
-The Lean project is moving away from using any C++ as more and more of
-the compiler is being bootstrapped in Lean itself. But the remaining
-C++ codebase is using modified version of [Google's C++ Style
-Guide][google-style].
-
-## [C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features
-
-Lean makes extensive use of new features in the C++ 11 standard.
-Developers must be familiar with the standard to be able to understand
-the code. Here are some of the features that are extensively used.
-
-- Type inference (aka `auto` keyword).
-- Initializer lists.
-- Lambda functions and expressions.
-- `nullptr` constant.
-- Strongly typed enumerations.
-- Right angle brackets with no space is now allowed in C++ 11.
-- Thread local storage.
-- Threading facilities.
-- Tuple types.
-- Smart pointers.
-- When using ``std::list`` make sure to include the `std::`
-  qualifier so you do not accidentally use the ``lean::list`` type.
-- When using ``std::copy`` make sure to include the `std::`
-  qualifier so you do not accidentally use the ``lean::copy`` type.
-- Small and focused functions are preferred: foo().  Try not to
-  exceed 500 lines in a function, except in tests.
-- Do **not** use the `#ifndef-#define-#endif` idiom for header files.
-  Instead use `#pragma once`.
-- Write `type const & v` instead of `const type & v`.
-- Use `const` extensively.
-- Use the macro `lean_assert` for assertions. The macro `lean_assert`
-  is extensively used when writing unit tests.
-
-## Naming
-
-- Class, method, and function names are lower case
-Use `_` for composite names. Example: `type_checker`.
-- Class/struct fields should start with the prefix `m_`.
-
-  Example:
-  ```c++
-  class point {
-      int m_x;
-      int m_y;
-  public:
-      ...
-  };
-  ```
-
-## Namespaces
-
-All code is in the `lean` namespace. Each frontend is stored in a
-separate nested namespace. For example, the SMT 2.0 frontend is stored
-in the `lean::smt` namespace.
-
-Exception: some debugging functions are stored outside of the `lean`
-namespace. These functions are called `print` and are meant to be used
-when debugging Lean using `gdb`.
-
-Do not use `using namespace` in a header file.
-
-## Templates
-
-Organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code
-
-## Idioms
-
-Use some popular C++ idioms:
-
-- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom)
-- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization
-
-## Formatting
-
-* Use 4 spaces for indentation.
-
-* `if-then-else` curly brackets not always required.  The following
-  forms are acceptable:
-
-  ```c++
-  if (cond) {
-      ...
-  } else {
-      ...
-  }
-  ```
-  and
-
-  ```c++
-  if (cond)
-    statement1;
-  else
-    statement2;
-  ```
-
-  In *exceptional cases*, we also use
-
-  ```c++
-  if (cond) statement;
-  ```
-
-  and
-
-  ```c++
-  if (cond) statement1; else stament2;
-  ```
-  * `if-then-else-if-else`
-
-  The following forms are acceptable:
-
-  ```c++
-  if (cond) {
-      ...
-  } else if (cond) {
-      ...
-  } else {
-      ...
-  }
-  ```c++
-  and
-
-  ```c++
-  if (cond)
-      statement1;
-  else if (cond)
-      statement2;
-  else
-      statement3;
-  ```
-
-* Format code using extra spaces to make code more readable.  For example:
-
-  ```c++
-  environment const & m_env;
-  cache               m_cache;
-  normalizer          m_normalizer;
-  volatile bool       m_interrupted;
-  ```
-  instead of:
-
-  ```c++
-  environment const & m_env;
-  cache m_cache;
-  normalizer m_normalizer;
-  volatile bool m_interrupted;
-  ```
-
-* Spaces in expressions.  Write `a == b` instead of `a==b`. Similarly,
-  we write `x < y + 1` instead of `x<y+1`.

doc/dev/debugging.md

@@ -20,8 +20,9 @@ Notable trace classes:
 * `Meta.isDefEq`: unification
 * `interpreter`: full execution trace of the interpreter. Only available in debug builds.
 
-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 directly to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
+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.
 
 ## 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.
@@ -43,8 +45,9 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   * it is none of the types described above
   * it is not marked `unsafe`
   * 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`).
@@ -69,13 +72,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:
@@ -118,4 +121,4 @@ Thus to e.g. run `#eval` on such a declaration, you need to
 Note that it is not sufficient to load the foreign library containing the external symbol because the interpreter depends on code that is emitted for each `@[extern]` declaration.
 Thus it is not possible to interpret an `@[extern]` declaration in the same file.
 
-See `tests/compiler/foreign` for an example.
+See [`tests/compiler/foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) for an example.

doc/dev/fixing_tests.md

@@ -1,39 +0,0 @@
-Fixing Tests
-============
-
-The test suite contains some tests that compare the produced output
-with the expected output. For example, the directory `tests/lean`
-contains files such as [`bad_class.lean`](../tests/lean/bad_class.lean) and
-[`bad_class.lean.expected.out`](../tests/lean/bad_class.lean.expected.out).
-The later contains the expected output for the test file `bad_class.lean`.
-
-When the Lean source code or the standard library are modified, some of these
-tests break because the produced output is slightly different, and we have
-to reflect the changes in the `.lean.expected.out` files.
-We should not blindly copy the new produced output since we may accidentally
-miss a bug introduced by recent changes.
-The test suite contains commands that allow us to see what changed in a convenient way.
-First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
-
-```
-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
-executing
-
-```
-./test_single.sh -i bad_class.lean
-```
-
-When the `-i` option is provided, `meld` is automatically invoked
-whenever there is discrepancy between the produced and expected
-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/dev/index.md

@@ -1,68 +1,45 @@
 # Development Workflow
-- [Commit Convention](./commit_convention.md)
-- [Building Lean](../make/index.md)
-  - [Ubuntu Setup](../make/ubuntu.md)
-  - [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)
-- [Unit Testing](./testing.md)
-- [Building This Manual](./mdbook.md)
-- [Fixing Tests](./fixing_tests.md)
-- [Debugging](./debugging.md)
-- [C++ Coding Style](./dev/cpp_coding_style.md)
 
-You will notice there is a `stage0` folder. This is for bootstrapping
-the compiler development.  Generally you do not change any code in
-`stage0` manually.  It is important that you read [bootstrapping
-pipeline](bootstrap.md) so you understand how this works.
+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).
 
-The dev team uses `elan` to manage which `lean` toolchain to use
-locally and `elan` can be used to setup the version of Lean you are
-manually building.  This means you generally do not use `make
-install`. You use `elan` instead.
+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).
+You should not edit the `stage0` directory except using the commands described in that section when necessary.
 
 ## Development Setup
 
-You can use any of the [supported editors](../setup.md) for editing
-the Lean source code. If you set up `elan` as below, opening `src/` as
-a *workspace folder* should ensure that stage 0 will be used for file
-in that directory.
+You can use any of the [supported editors](../setup.md) for editing the Lean source code.
+If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
 
-## Dev setup using elan
+### Dev setup using elan
 
 You can use [`elan`](https://github.com/leanprover/elan) to easily
 switch between stages and build configurations based on the current
 directory, both for the `lean`, `leanc`, and `leanmake` binaries in your shell's
 PATH and inside your editor.
 
-To install elan, you can do so, without installing a default version of Lean, using
+To install elan, you can do so, without installing a default version of Lean, using (Unix)
 
 ```bash
-[Unix]
 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
-
-[Windows]
+```
+or (Windows)
+```
 curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
 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
 toolchains on the spot. `lean4-mode` will automatically use the `lean` executable
 associated with the directory of the current file as long as `lean4-rootdir` is
@@ -74,3 +51,26 @@ 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.

doc/dev/mdbook.md

@@ -1,3 +1,12 @@
+# Documentation
+
+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.
+
+
 ## Settings
 
 We are using the following settings while editing the markdown docs.
@@ -14,30 +23,87 @@ We are using the following settings while editing the markdown docs.
 
 ## Build
 
-This manual is generated by
-[mdBook](https://github.com/rust-lang/mdBook). We are currently using
-a [fork](https://github.com/leanprover/mdBook) of it for the following
-additional features:
+### Using Nix
+
+Building the manual using Nix (which is what the CI does) is as easy as
+```bash
+$ nix build --update-input lean ./doc
+```
+You can also open a shell with `mdbook` for running the commands mentioned below with
+`nix develop ./doc#book`. Otherwise, read on.
+
+### Manually
+
+To build and test the book you have to preprocess the .lean files with Alectryon then use our own
+fork of the Rust tool named [mdbook](https://github.com/leanprover/mdbook). We have our own fork of
+mdBook with the following additional features:
 
 * Add support for hiding lines in other languages
   [#1339](https://github.com/rust-lang/mdBook/pull/1339)
-* Replace calling `rustdoc --test` from `mdbook test` with `./test`
+* Make `mdbook test` call the `lean` compiler to test the snippets.
+* Ability to test a single chapter at a time which is handy when you
+are working on that chapter.  See the `--chapter` option.
 
-To build this manual, first install the fork via
-```bash
-cargo install --git https://github.com/leanprover/mdBook mdbook
-```
-Then use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html) in the `doc/` folder:
+So you need to setup these tools before you can run `mdBook`.
 
-```bash
-cd doc
-mdbook watch --open  # opens the output in `out/` in your default browser
-```
+1. install [Rust](https://www.rust-lang.org/tools/install)
+which provides you with the `cargo` tool for building rust packages.
+Then run the following:
+    ```bash
+    cargo install --git https://github.com/leanprover/mdBook mdbook
+    ```
 
-Run `mdbook test` to test all `lean` code blocks.
+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
+    ```
 
-Using the [Nix setup](make/nix.md), you can instead open a shell with
-the mdBook fork downloaded from our binary cache:
-```bash
-nix develop .#doc
-```
+1. Create a Python 3.10 environment.
+
+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:
+
+    ```
+    cd lean4/doc
+    alectryon --frontend lean4+markup examples/palindromes.lean --backend webpage -o palindromes.lean.md
+    ```
+
+    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:
+    ```
+    cd lean4/doc
+    mdbook build
+    ```
+
+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://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.
+
+    ```bash
+    mdbook watch --open  # opens the output in `out/` in your default browser
+    ```
+
+## Testing Lean Snippets
+
+You can run the following in the `doc/` folder to test all the lean code snippets.
+
+    ```bash
+    mdbook test
+    ```
+
+and you can use the `--chapter` option to test a specific chapter that you are working on:
+
+    ```bash
+    mdbook test --chapter Array
+    ```
+
+Use chapter name `?` to get a list of all the chapter names.

doc/dev/testing.md

@@ -1,13 +1,10 @@
-# Unit Testing
+# Test Suite
 
-You can run the unit tests after completing a build using the following:
-
-After [building lean](../make/index.md) you can run all the tests using
+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
@@ -19,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:
 
@@ -26,25 +29,29 @@ 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
-information is displayed. This option will show all test output
+information is displayed. This option will show all test output.
 
-Here is the summary of the test source code organization.
-All these tests are included by [/src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
+## Test Suite Organization
 
-- `tests/lean`: contains tests that come equipped with a
-  .lean.expected.out file. The driver script `test_single.sh` runs
+All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
+
+- [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/): contains tests that come equipped with a
+  .lean.expected.out file. The driver script [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/test_single.sh) runs
   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:
@@ -54,7 +61,7 @@ All these tests are included by [/src/shell/CMakeLists.txt](https://github.com/l
     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
@@ -71,19 +78,57 @@ All these tests are included by [/src/shell/CMakeLists.txt](https://github.com/l
     --^ 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
+tests break because the produced output is slightly different, and we have
+to reflect the changes in the `.lean.expected.out` files.
+We should not blindly copy the new produced output since we may accidentally
+miss a bug introduced by recent changes.
+The test suite contains commands that allow us to see what changed in a convenient way.
+First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
+
+```
+sudo apt-get install meld
+```
+
+Now, suppose `bad_class.lean` test is broken. We can see the problem by going to [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean) directory and
+executing
+
+```
+./test_single.sh -i bad_class.lean
+```
+
+When the `-i` option is provided, `meld` is automatically invoked
+whenever there is discrepancy between the produced and expected
+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`.

doc/elaborators.md

@@ -0,0 +1,8 @@
+## Elaborators
+
+TODO. See [Lean Together 2021: Metaprogramming in Lean
+4](https://youtu.be/hxQ1vvhYN_U) for an overview as well [the
+continuation](https://youtu.be/vy4JWIiiXSY) about tactic programming.
+For more information on antiquotations, see also §4.1 of [Beyond
+Notations: Hygienic Macro Expansion for Theorem Proving
+Languages](https://arxiv.org/pdf/2001.10490.pdf#page=11).

doc/examples.md

@@ -0,0 +1,9 @@
+Examples
+========
+
+- [Palindromes](examples/palindromes.lean.md)
+- [Binary Search Trees](examples/bintree.lean.md)
+- [A Certified Type Checker](examples/tc.lean.md)
+- [The Well-Typed Interpreter](examples/interp.lean.md)
+- [Dependent de Bruijn Indices](examples/deBruijn.lean.md)
+- [Parametric Higher-Order Abstract Syntax](examples/phoas.lean.md)

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 ack 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
+  go 0
+termination_by go i => a.size - i
+
+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

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

doc/examples/ICERM2022/meta.lean

@@ -0,0 +1,80 @@
+import Lean
+
+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 
+    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 
+    trace[Meta.debug] "{declName} : {val}"
+
+#eval ex2 ``Add.add
+
+set_option trace.Meta.debug true in
+#eval ex2 ``Add.add
+
+def ex3 (declName : Name) : MetaM Unit := do
+  let info ← getConstInfo declName
+  forallTelescope info.type fun xs type => do
+    trace[Meta.debug] "hypotheses : {xs}"
+    trace[Meta.debug] "resultType : {type}"
+    for x in xs do
+      trace[Meta.debug] "{x} : {← inferType x}"
+
+def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
+  if a < b then 
+    a
+  else 
+    b
+
+set_option trace.Meta.debug true in
+#eval ex3 ``myMin
+
+def ex4 : MetaM Unit := do
+  let nat := mkConst ``Nat
+  withLocalDeclD `a nat fun a => 
+  withLocalDeclD `b nat fun b => do
+    let e ← mkAppM ``HAdd.hAdd #[a, b]
+    trace[Meta.debug] "{e} : {← inferType e}"
+    let e ← mkAdd a (mkNatLit 5)
+    trace[Meta.debug] "added 5: {e}"
+    let e ← whnf e
+    trace[Meta.debug] "whnf: {e}"
+    let e ← reduce e
+    trace[Meta.debug] "reduced: {e}"
+    let a_plus_1 ← mkAdd a (mkNatLit 1)
+    let succ_a   := mkApp (mkConst ``Nat.succ) a
+    trace[Meta.debug] "({a_plus_1} =?= {succ_a}) == {← isDefEq a_plus_1 succ_a}"
+    let m ← mkFreshExprMVar nat
+    let m_plus_1 ← mkAdd m (mkNatLit 1)
+    trace[Meta.debug] "m_plus_1: {m_plus_1}"
+    unless (← isDefEq m_plus_1 succ_a) do throwError "isDefEq failed"
+    trace[Meta.debug] "m_plus_1: {m_plus_1}"
+
+set_option trace.Meta.debug true in
+#eval ex4
+
+open Elab Term
+
+def ex5 : TermElabM Unit := do
+  let nat := Lean.mkConst ``Nat
+  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 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/ICERM2022/notation.lean

@@ -0,0 +1,49 @@
+import Lean
+
+def f (x y : Nat) := x * y + 1
+
+infixl:65 " *' " => f
+
+#check 2 *' 3
+
+notation "unitTest " x => Prod.mk x ()
+
+#check unitTest 42
+
+notation "parenthesisTest " x => Nat.sub (x)
+#check parenthesisTest 12
+
+def Set (α : Type u) := α → Prop
+def setOf {α : Type} (p : α → Prop) : Set α := p
+notation "{ " x " | " p " }" => setOf (fun x => p)
+
+#check { x | x ≤ 1 }
+
+notation "cdotTest " "(" x ", " y ")" => Prod.map (· + 1) (1 + ·) (x, y)
+
+#check cdotTest (13, 12)
+
+notation "tupleFunctionTest " "(" x ", " y ")"=> Prod.map (Nat.add 1) (Nat.add 2) (x, y)
+
+#check tupleFunctionTest (15, 12)
+
+notation "diag " x => Prod.mk x x
+
+#check diag 12
+
+open Lean Meta PrettyPrinter Delaborator SubExpr in
+@[delab app.Prod.mk] def delabDoubleRhsTest : Delab := do
+   let e ← getExpr
+   let #[_, _, x, y] := e.getAppArgs | failure
+   guard (← isDefEq x y) 
+   let stx ← withAppArg delab
+   `(diag $stx)     
+
+#check diag 3
+#check (3, 3)
+#check (3, 4)
+#check (2+1, 3)
+#check (true, true)
+
+
+

doc/examples/NFM2022/nfm1.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/NFM2022/nfm10.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/NFM2022/nfm11.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/NFM2022/nfm12.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/NFM2022/nfm13.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/NFM2022/nfm14.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/NFM2022/nfm15.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/NFM2022/nfm16.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/NFM2022/nfm17.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/NFM2022/nfm18.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/NFM2022/nfm19.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/NFM2022/nfm2.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/NFM2022/nfm20.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/NFM2022/nfm21.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/NFM2022/nfm22.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/NFM2022/nfm23.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/NFM2022/nfm24.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 x xs ih => simp [List.concat, ih]
+
+example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
+  induction as <;> simp! [*]

doc/examples/NFM2022/nfm3.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/NFM2022/nfm4.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/NFM2022/nfm5.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/NFM2022/nfm6.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/NFM2022/nfm7.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/NFM2022/nfm8.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 ack 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
+  go 0
+termination_by go i => a.size - i
+
+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/NFM2022/nfm9.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/bintree.lean

@@ -0,0 +1,296 @@
+/-!
+# Binary Search Trees
+
+If the type of keys can be totally ordered -- that is, it supports a well-behaved `≤` comparison --
+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 ["Software Foundations"](https://softwarefoundations.cis.upenn.edu/vfa-current/SearchTree.html)
+book (volume 3).
+-/
+
+/-!
+We use `Nat` as the key type in our implementation of BSTs,
+since it has a convenient total order with lots of theorems and automation available.
+We leave as an exercise to the reader the generalization to arbitrary types.
+-/
+
+inductive Tree (β : Type v) where
+  | leaf
+  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
+  deriving Repr
+
+/-!
+The function `contains` returns `true` iff the given tree contains the key `k`.
+-/
+def Tree.contains (t : Tree β) (k : Nat) : Bool :=
+  match t with
+  | leaf => false
+  | node left key value right =>
+    if k < key then
+      left.contains k
+    else if key < k then
+      right.contains k
+    else
+      true
+
+/-!
+`t.find? k` returns `some v` if `v` is the value bound to key `k` in the tree `t`. It returns `none` otherwise.
+-/
+def Tree.find? (t : Tree β) (k : Nat) : Option β :=
+  match t with
+  | leaf => none
+  | node left key value right =>
+    if k < key then
+      left.find? k
+    else if key < k then
+      right.find? k
+    else
+      some value
+
+/-!
+`t.insert k v` is the map containing all the bindings of `t` along with a binding of `k` to `v`.
+-/
+def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
+  match t with
+  | leaf => node leaf k v leaf
+  | node left key value right =>
+    if k < key then
+      node (left.insert k v) key value right
+    else if key < k then
+      node left key value (right.insert k v)
+    else
+      node left k v right
+/-!
+Let's add a new operation to our tree: converting it to an association list that contains the key--value bindings from the tree stored as pairs.
+If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list.
+Here's a function that does so with an in-order traversal of the tree.
+-/
+def Tree.toList (t : Tree β) : List (Nat × β) :=
+  match t with
+  | leaf => []
+  | node l k v r => l.toList ++ [(k, v)] ++ r.toList
+
+#eval Tree.leaf.insert 2 "two"
+      |>.insert 3 "three"
+      |>.insert 1 "one"
+
+#eval Tree.leaf.insert 2 "two"
+      |>.insert 3 "three"
+      |>.insert 1 "one"
+      |>.toList
+
+/-!
+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
+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 × β) :=
+  go t []
+where
+  go (t : Tree β) (acc : List (Nat × β)) : List (Nat × β) :=
+    match t with
+    | leaf => acc
+    | node l k v r => go l ((k, v) :: go r acc)
+
+/-!
+We now prove that `t.toList` and `t.toListTR` return the same list.
+The proof is on induction, and as we used the auxiliary function `go`
+to define `Tree.toListTR`, we use the auxiliary theorem `go` to prove the theorem.
+
+The proof of the auxiliary theorem is by induction on `t`.
+The `generalizing acc` modifier instructs Lean to revert `acc`, apply the
+induction theorem for `Tree`s, and then reintroduce `acc` in each case.
+By using `generalizing`, we obtain the more general induction hypotheses
+
+- `left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc`
+
+- `right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc`
+
+Recall that the combinator `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
+concatenating all goals produced by `tac'`. In this theorem, we use it to apply
+`simp` and close each subgoal produced by the `induction` tactic.
+
+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 `*` 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` instructs the simplifier to use the
+`List.append_assoc` theorem as a rewriting rule.
+-/
+theorem Tree.toList_eq_toListTR (t : Tree β)
+        : t.toList = t.toListTR := by
+  simp [toListTR, go t []]
+where
+  go (t : Tree β) (acc : List (Nat × β))
+     : toListTR.go t acc = t.toList ++ acc := by
+    induction t generalizing acc <;>
+      simp [toListTR.go, toList, *, List.append_assoc]
+
+/-!
+The `[csimp]` annotation instructs the Lean code generator to replace
+any `Tree.toList` with `Tree.toListTR` when generating code.
+-/
+@[csimp] theorem Tree.toList_eq_toListTR_csimp
+                 : @Tree.toList = @Tree.toListTR := by
+  funext β t
+  apply toList_eq_toListTR
+
+/-!
+The implementations of `Tree.find?` and `Tree.insert` assume that values of type tree obey the BST invariant:
+for any non-empty node with key `k`, all the values of the `left` subtree are less than `k` and all the values
+of the right subtree are greater than `k`. But that invariant is not part of the definition of tree.
+
+So, let's formalize the BST invariant. Here's one way to do so. First, we define a helper `ForallTree`
+to express that idea that a predicate holds at every node of a tree:
+-/
+inductive ForallTree (p : Nat → β → Prop) : Tree β → Prop
+  | leaf : ForallTree p .leaf
+  | node :
+     ForallTree p left →
+     p key value →
+     ForallTree p right →
+     ForallTree p (.node left key value right)
+
+/-!
+Second, we define the BST invariant:
+An empty tree is a BST.
+A non-empty tree is a BST if all its left nodes have a lesser key, its right nodes have a greater key, and the left and right subtrees are themselves BSTs.
+-/
+inductive BST : Tree β → Prop
+  | leaf : BST .leaf
+  | node :
+     ForallTree (fun k v => k < key) left →
+     ForallTree (fun k v => key < k) right →
+     BST left → BST right →
+     BST (.node left key value right)
+
+/-!
+We can use the `macro` command to create helper tactics for organizing our proofs.
+The macro `have_eq x y` tries to prove `x = y` using linear arithmetic, and then
+immediately uses the new equality to substitute `x` with `y` everywhere in the goal.
+
+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 =>
+  `(tactic|
+    (have h : $lhs = $rhs :=
+       -- TODO: replace with linarith
+       by simp_arith at *; apply Nat.le_antisymm <;> assumption
+     try subst $lhs))
+
+/-!
+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 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 =>
+  `(tactic| by_cases $e <;> simp [*])
+
+
+/-!
+We can use the attribute `[simp]` to instruct the simplifier to reduce given definitions or
+apply rewrite theorems. The `local` modifier limits the scope of this modification to this file.
+-/
+attribute [local simp] Tree.insert
+
+/-!
+We now prove that `Tree.insert` preserves the BST invariant using induction and case analysis.
+Recall that the tactic `. tac` focuses on the main goal and tries to solve it using `tac`, or else fails.
+It is used to structure proofs in Lean.
+The notation `‹e›` is just syntax sugar for `(by assumption : e)`. That is, it tries to find a hypothesis `h : e`.
+It is useful to access hypothesis that have auto generated names (aka "inaccessible") names.
+-/
+
+theorem Tree.forall_insert_of_forall
+        (h₁ : ForallTree p t) (h₂ : p key value)
+        : ForallTree p (t.insert key value) := by
+  induction h₁ with
+  | leaf => exact .node .leaf h₂ .leaf
+  | node hl hp hr ihl ihr =>
+    rename Nat => k
+    by_cases' key < k
+    . exact .node ihl hp hr
+    . by_cases' k < key
+      . exact .node hl hp ihr
+      . have_eq key k
+        exact .node hl h₂ hr
+
+theorem Tree.bst_insert_of_bst
+        {t : Tree β} (h : BST t) (key : Nat) (value : β)
+        : BST (t.insert key value) := by
+  induction h with
+  | leaf => exact .node .leaf .leaf .leaf .leaf
+  | node h₁ h₂ b₁ b₂ ih₁ ih₂ =>
+    rename Nat => k
+    simp
+    by_cases' key < k
+    . exact .node (forall_insert_of_forall h₁ ‹key < k›) h₂ ih₁ b₂
+    . by_cases' k < key
+      . exact .node h₁ (forall_insert_of_forall h₂ ‹k < key›) b₁ ih₂
+      . have_eq key k
+        exact .node h₁ h₂ b₁ b₂
+
+/-!
+Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`s.
+-/
+def BinTree (β : Type u) := { t : Tree β // BST t }
+
+def BinTree.mk : BinTree β :=
+  ⟨.leaf, .leaf⟩
+
+def BinTree.contains (b : BinTree β) (k : Nat) : Bool :=
+  b.val.contains k
+
+def BinTree.find? (b : BinTree β) (k : Nat) : Option β :=
+  b.val.find? k
+
+def BinTree.insert (b : BinTree β) (k : Nat) (v : β) : BinTree β :=
+  ⟨b.val.insert k v, b.val.bst_insert_of_bst b.property k v⟩
+
+/-!
+Finally, we prove that `BinTree.find?` and `BinTree.insert` satisfy the map properties.
+-/
+
+attribute [local simp]
+  BinTree.mk BinTree.contains BinTree.find?
+  BinTree.insert Tree.find? Tree.contains Tree.insert
+
+theorem BinTree.find_mk (k : Nat)
+        : BinTree.mk.find? k = (none : Option β) := by
+  simp
+
+theorem BinTree.find_insert (b : BinTree β) (k : Nat) (v : β)
+        : (b.insert k v).find? k = some v := by
+  let ⟨t, h⟩ := b; simp
+  induction t with simp
+  | node left key value right ihl ihr =>
+    by_cases' k < key
+    . cases h; apply ihl; assumption
+    . by_cases' key < k
+      cases h; apply ihr; assumption
+
+theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
+        : (b.insert k v).find? k' = b.find? k' := by
+  let ⟨t, h⟩ := b; simp
+  induction t with simp
+  | leaf =>
+    split <;> (try simp) <;> split <;> (try simp)
+    have_eq k k'
+    contradiction
+  | node left key value right ihl ihr =>
+    let .node hl hr bl br := h
+    specialize ihl bl
+    specialize ihr br
+    by_cases' k < key; by_cases' key < k
+    have_eq key k
+    by_cases' k' < k; by_cases' k  < k'
+    have_eq k k'
+    contradiction

doc/examples/bintree.lean.md

@@ -0,0 +1,5 @@
+(this example is rendered by Alectryon in the CI)
+
+```lean
+{{#include bintree.lean}}
+```

doc/examples/deBruijn.lean

@@ -0,0 +1,163 @@
+/-!
+# Dependent de Bruijn Indices
+
+In this example, we represent program syntax terms in a type family parameterized by a list of types,
+representing the typing context, or information on which free variables are in scope and what
+their types are.
+
+
+Remark: this example is based on an example in the book [Certified Programming with Dependent Types](http://adam.chlipala.net/cpdt/) by Adam Chlipala.
+-/
+
+/-!
+Programmers who move to statically typed functional languages from scripting languages
+often complain about the requirement that every element of a list have the same type. With
+fancy type systems, we can partially lift this requirement. We can index a list type with a
+“type-level” list that explains what type each element of the list should have. This has been
+done in a variety of ways in Haskell using type classes, and we can do it much more cleanly
+and directly in Lean.
+
+We parameterize our heterogeneous lists by at type `α` and an `α`-indexed type `β`.
+-/
+
+inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v)
+  | nil  : HList β []
+  | cons : β i → HList β is → HList β (i::is)
+
+/-!
+We overload the `List.cons` notation `::` so we can also use it to create
+heterogeneous lists.
+-/
+infix:67 " :: " => HList.cons
+
+/-! We similarly overload the `List` notation `[]` for the empty heterogeneous list. -/
+notation "[" "]" => HList.nil
+
+/-!
+Variables are represented in a way isomorphic to the natural numbers, where
+number 0 represents the first element in the context, number 1 the second element, and so
+on. Actually, instead of numbers, we use the `Member` inductive family.
+
+The value of type `Member a as` can be viewed as a certificate that `a` is
+an element of the list `as`. The constructor `Member.head` says that `a`
+is in the list if the list begins with it. The constructor `Member.tail`
+says that if `a` is in the list `bs`, it is also in the list `b::bs`.
+-/
+inductive Member : α → List α → Type
+  | head : Member a (a::as)
+  | tail : Member a bs → Member a (b::bs)
+
+/-!
+Given a heterogeneous list `HList β is` and value of type `Member i is`, `HList.get`
+retrieves an element of type `β i` from the list.
+The pattern `.head` and `.tail h` are sugar for `Member.head` and `Member.tail h` respectively.
+Lean can infer the namespace using the expected type.
+-/
+def HList.get : HList β is → Member i is → β i
+  | a::as, .head => a
+  | a::as, .tail h => as.get h
+
+/-!
+Here is the definition of the simple type system for our programming language, a simply typed
+lambda calculus with natural numbers as the base type.
+-/
+inductive Ty where
+  | nat
+  | fn : Ty → Ty → Ty
+
+/-!
+We can write a function to translate `Ty` values to a Lean type
+— remember that types are first class, so can be calculated just like any other value.
+We mark `Ty.denote` as `[reducible]` to make sure the typeclass resolution procedure can
+unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
+`Add (Ty.denote Ty.nat)`. Since `Ty.denote` is marked as `[reducible]`,
+the typeclass resolution procedure can reduce `Ty.denote Ty.nat` to `Nat`, and use
+the builtin instance for `Add Nat` as the solution.
+
+Recall that the term `a.denote` is sugar for `denote a` where `denote` is the function being defined.
+We call it the "dot notation".
+-/
+@[reducible] def Ty.denote : Ty → Type
+  | nat    => Nat
+  | fn a b => a.denote → b.denote
+
+/-!
+Here is the definition of the `Term` type, including variables, constants, addition,
+function application and abstraction, and let binding of local variables.
+Since `let` is a keyword in Lean, we use the "escaped identifier" `«let»`.
+You can input the unicode (French double quotes) using `\f<<` (for `«`) and `\f>>` (for `»`).
+The term `Term ctx .nat` is sugar for `Term ctx Ty.nat`, Lean infers the namespace using the expected type.
+-/
+inductive Term : List Ty → Ty → Type
+  | var   : Member ty ctx → Term ctx ty
+  | const : Nat → Term ctx .nat
+  | plus  : Term ctx .nat → Term ctx .nat → Term ctx .nat
+  | app   : Term ctx (.fn dom ran) → Term ctx dom → Term ctx ran
+  | lam   : Term (dom :: ctx) ran → Term ctx (.fn dom ran)
+  | «let» : Term ctx ty₁ → Term (ty₁ :: ctx) ty₂ → Term ctx ty₂
+
+/-!
+Here are two example terms encoding, the first addition packaged as a two-argument
+curried function, and the second of a sample application of addition to constants.
+
+The command `open Ty Term Member` opens the namespaces `Ty`, `Term`, and `Member`. Thus,
+you can write `lam` instead of `Term.lam`.
+-/
+open Ty Term Member
+def add : Term [] (fn nat (fn nat nat)) :=
+  lam (lam (plus (var (tail head)) (var head)))
+
+def three_the_hard_way : Term [] nat :=
+  app (app add (const 1)) (const 2)
+
+/-!
+Since dependent typing ensures that any term is well-formed in its context and has a particular type,
+it is easy to translate syntactic terms into Lean values.
+
+The attribute `[simp]` instructs Lean to always try to unfold `Term.denote` applications when one applies
+the `simp` tactic. We also say this is a hint for the Lean term simplifier.
+-/
+@[simp] def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
+  | var h,     env => env.get h
+  | const n,   _   => n
+  | plus a b,  env => a.denote env + b.denote env
+  | app f a,   env => f.denote env (a.denote env)
+  | lam b,     env => fun x => b.denote (x :: env)
+  | «let» a b, env => b.denote (a.denote env :: env)
+
+/-!
+You can show that the denotation of `three_the_hard_way` is indeed `3` using reflexivity.
+-/
+example : three_the_hard_way.denote [] = 3 :=
+  rfl
+
+/-!
+We now define the constant folding optimization that traverses a term if replaces subterms such as
+`plus (const m) (const n)` with `const (n+m)`.
+-/
+@[simp] def Term.constFold : Term ctx ty → Term ctx ty
+  | const n   => const n
+  | var h     => var h
+  | app f a   => app f.constFold a.constFold
+  | lam b     => lam b.constFold
+  | «let» a b => «let» a.constFold b.constFold
+  | plus a b  =>
+    match a.constFold, b.constFold with
+    | const n, const m => const (n+m)
+    | a',      b'      => plus a' b'
+
+/-!
+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.
+We use the `split` to break the nested `match` expression in the `plus` case into two cases.
+The local variables `iha` and `ihb` are the induction hypotheses for `a` and `b`.
+The modifier `←` in a term simplifier argument instructs the term simplifier to use the equation as a rewriting rule in
+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
+  induction e with simp [*]
+  | plus a b iha ihb =>
+    split
+    next he₁ he₂ => simp [← iha, ← ihb, he₁, he₂]
+    next => simp [iha, ihb]

doc/examples/deBruijn.lean.md

@@ -0,0 +1,5 @@
+(this example is rendered by Alectryon in the CI)
+
+```lean
+{{#include deBruijn.lean}}
+```

doc/examples/interp.lean

@@ -0,0 +1,152 @@
+/-!
+# The Well-Typed Interpreter
+
+In this example, we build an interpreter for a simple functional programming language,
+with variables, function application, binary operators and an `if...then...else` construct.
+We will use the dependent type system to ensure that any programs which can be represented are well-typed.
+
+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 `α`.
+-/
+
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+
+/-!
+We can overload the `List.cons` notation `::` and use it to create `Vector`s.
+-/
+infix:67 " :: " => Vector.cons
+
+/-!
+Now, we define the types of our simple functional language.
+We have integers, booleans, and functions, represented by `Ty`.
+-/
+inductive Ty where
+  | int
+  | bool
+  | fn (a r : Ty)
+
+/-!
+We can write a function to translate `Ty` values to a Lean type
+— remember that types are first class, so can be calculated just like any other value.
+We mark `Ty.interp` as `[reducible]` to make sure the typeclass resolution procedure can
+unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
+`Add (Ty.interp Ty.int)`. Since `Ty.interp` is marked as `[reducible]`,
+the typeclass resolution procedure can reduce `Ty.interp Ty.int` to `Int`, and use
+the builtin instance for `Add Int` as the solution.
+-/
+@[reducible] def Ty.interp : Ty → Type
+  | int    => Int
+  | bool   => Bool
+  | fn a r => a.interp → r.interp
+
+/-!
+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
+  | 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
+  | 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)
+  | app   : Expr ctx (Ty.fn a ty) → Expr ctx a → Expr ctx ty
+  | op    : (a.interp → b.interp → c.interp) → Expr ctx a → Expr ctx b → Expr ctx c
+  | ife   : Expr ctx Ty.bool → Expr ctx a → Expr ctx a → Expr ctx a
+  | delay : (Unit → Expr ctx a) → Expr ctx a
+
+/-!
+We use the command `open` to create the aliases `stop` and `pop` for `HasType.stop` and `HasType.pop` respectively.
+-/
+open HasType (stop pop)
+
+/-!
+Since expressions are indexed by their type, we can read the typing rules of the language from the definitions of the constructors.
+Let us look at each constructor in turn.
+
+We use a nameless representation for variables — they are de Bruijn indexed.
+Variables are represented by a proof of their membership in the context, `HasType i ctx ty`,
+which is a proof that variable `i` in context `ctx` has type `ty`.
+
+We can treat `stop` as a proof that the most recently defined variable is well-typed,
+and `pop n` as a proof that, if the `n`th most recently defined variable is well-typed, so is the `n+1`th.
+In practice, this means we use `stop` to refer to the most recently defined variable,
+`pop stop` to refer to the next, and so on, via the `Expr.var` constructor.
+
+A value `Expr.val` carries a concrete representation of an integer.
+
+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`.
+
+The constructor `Expr.op` allows us to use arbitrary binary operators, where the type of the operator informs what the types of the arguments must be.
+
+Finally, the constructor `Exp.ife` represents a `if-then-else` expression. The condition is a Boolean, and each branch must have the same type.
+
+The auxiliary constructor `Expr.delay` is used to delay evaluation.
+-/
+
+
+/-!
+When we evaluate an `Expr`, we’ll need to know the values in scope, as well as their types. `Env` is an environment,
+indexed over the types in scope. Since an environment is just another form of list, albeit with a strongly specified connection
+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
+  | cons : Ty.interp a → Env ctx → Env (a :: ctx)
+
+infix:67 " :: " => Env.cons
+
+def Env.lookup : HasType i ctx ty → Env ctx → ty.interp
+  | stop,  x :: xs => x
+  | pop k, x :: xs => lookup k xs
+
+/-!
+Given this, an interpreter is a function which translates an `Expr` into a Lean value with respect to a specific environment.
+-/
+def Expr.interp (env : Env ctx) : Expr ctx ty → ty.interp
+  | var i     => env.lookup i
+  | val x     => x
+  | lam b     => fun x => b.interp (Env.cons x env)
+  | app f a   => f.interp env (a.interp env)
+  | op o x y  => o (x.interp env) (y.interp env)
+  | ife c t e => if c.interp env then t.interp env else e.interp env
+  | delay a   => (a ()).interp env
+
+open Expr
+
+/-!
+We can make some simple test functions. Firstly, adding two inputs `fun x y => y + x` is written as follows.
+-/
+
+def add : Expr ctx (Ty.fn Ty.int (Ty.fn Ty.int Ty.int)) :=
+  lam (lam (op (·+·) (var stop) (var (pop stop))))
+
+#eval add.interp Env.nil 10 20
+
+/-!
+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 viewed as
+"trust me, this recursive definition makes sense". Recall that `sorry` is an unsound axiom in Lean.
+-/
+
+def fact : Expr ctx (Ty.fn Ty.int Ty.int) :=
+  lam (ife (op (·==·) (var stop) (val 0))
+           (val 1)
+           (op (·*·) (delay fun _ => app fact (op (·-·) (var stop) (val 1))) (var stop)))
+  decreasing_by sorry
+
+#eval fact.interp Env.nil 10