chore: address feedback

Motivations:
- We can simplify the big mutual recursion and the implementation.
- We can implement the support for `match`-expressions in the `pre` method.
- It is easier to define and simplify `Simprocs`.

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,13 +1,14 @@
-# Read and remove this section before submitting
+# 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!
-* Add the link to your `RFC` or `bug` issue below.
+* 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.
-* Remove this section before submitting.
+* 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.
 
-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.
+---
 
-# Summary
-
-Link to `RFC` or `bug` issue:
+Closes #0000 (`RFC` or `bug` issue number fixed by this PR, if any)

.github/workflows/changelog.yml

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

.github/workflows/ci.yml

@@ -6,6 +6,7 @@ on:
     tags:
       - '*'
   pull_request:
+    types: [opened, synchronize, reopened, labeled]
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
@@ -49,7 +50,7 @@ jobs:
 
       - name: Configure build matrix
         id: set-matrix
-        uses: actions/github-script@v3
+        uses: actions/github-script@v7
         with:
           script: |
             const quick = ${{ steps.set-quick.outputs.quick }};
@@ -320,6 +321,7 @@ jobs:
           ulimit -c unlimited # coredumps
           # this also enables githash embedding into stage 1 library
           OPTIONS=(-DCHECK_OLEAN_VERSION=ON)
+          OPTIONS+=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
           if [[ -n '${{ matrix.prepare-llvm }}' ]]; then
             wget -q ${{ matrix.llvm-url }}
             PREPARE="$(${{ matrix.prepare-llvm }})"
@@ -371,10 +373,10 @@ jobs:
           ulimit -c unlimited # coredumps
           # exclude nonreproducible test
           ctest -j4 --output-on-failure ${{ matrix.CTEST_OPTIONS }} < /dev/null
-        if: matrix.wasm || !matrix.cross
+        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 }}
+        if: ${{ !matrix.cross && needs.configure.outputs.quick == 'false' }}
       - name: Build Stage 2
         run: |
           cd build
@@ -399,7 +401,7 @@ jobs:
           cd build
           ulimit -c unlimited # coredumps
           make update-stage0 && make -j4
-        if: matrix.name == 'Linux' && !needs.configure.outputs.quick
+        if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
       - name: CCache stats
         run: ccache -s
       - name: Show stacktrace for coredumps
@@ -433,7 +435,7 @@ jobs:
     if: ${{ always() }}
     steps:
     - if: contains(needs.*.result, 'failure') ||  contains(needs.*.result, 'cancelled')
-      uses: actions/github-script@v3
+      uses: actions/github-script@v7
       with:
         script: |
             core.setFailed('Some jobs failed')

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

@@ -15,7 +15,7 @@ jobs:
 
     steps:
     - name: Add label based on comment
-      uses: actions/github-script@v6
+      uses: actions/github-script@v7
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |

.github/workflows/nix-ci.yml

@@ -17,7 +17,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     defaults:
       run:
-        shell: nix -v --experimental-features "nix-command flakes" run .#ciShell -- bash -euxo pipefail {0}
+        shell: nix run .#ciShell -- bash -euxo pipefail {0}
     strategy:
       matrix:
         include:
@@ -29,21 +29,13 @@ 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@v3
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
-      - name: Install Nix
-        uses: cachix/install-nix-action@v18
-        with:
-          # https://github.com/NixOS/nix/issues/6572
-          install_url: https://releases.nixos.org/nix/nix-2.7.0/install
-          extra_nix_config: |
-            extra-sandbox-paths = /nix/var/cache/ccache
-            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org
       - name: Set Up Nix Cache
         uses: actions/cache@v3
         with:
@@ -57,8 +49,13 @@ jobs:
         run: |
           # Nix seems to mutate the cache, so make a copy
           cp -r nix-store-cache nix-store-cache-copy || true
+      - name: Install Nix
+        uses: DeterminateSystems/nix-installer-action@main
+        with:
+          extra-conf: |
+            extra-sandbox-paths = /nix/var/cache/ccache?
+            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
       - name: Prepare CCache Cache
-        shell: bash -euxo pipefail {0}
         run: |
           sudo mkdir -m0770 -p /nix/var/cache/ccache
           sudo chown -R $USER /nix/var/cache/ccache
@@ -71,7 +68,6 @@ jobs:
           restore-keys: |
             ${{ matrix.name }}-nix-ccache
       - name: Further Set Up CCache Cache
-        shell: bash -euxo pipefail {0}
         run: |
           sudo chown -R root:nixbld /nix/var/cache
           sudo chmod -R 770 /nix/var/cache

.github/workflows/pr-release.yml

@@ -16,27 +16,16 @@ on:
 jobs:
   on-success:
     runs-on: ubuntu-latest
-    if: github.event.workflow_run.conclusion == 'success' && github.repository == 'leanprover/lean4'
+    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: Checkout
-        # Only proceed if the previous workflow had a pull request number.
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/checkout@v3
-        with:
-          token: ${{ secrets.PR_RELEASES_TOKEN }}
-          # Since `workflow_run` runs on master, we need to specify which commit to check out,
-          # so that we tag the PR.
-          # It's important that we use `sourceHeadSha` here, not `targetCommitSha`
-          # as we *don't* want the synthetic merge with master.
-          ref: ${{ steps.workflow-info.outputs.sourceHeadSha }}
-          # We need a full checkout, so that we can push the PR commits to the `lean4-pr-releases` repo.
-          fetch-depth: 0
 
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
@@ -47,14 +36,22 @@ jobs:
           path: artifacts
           name: build-.*
           name_is_regexp: true
-      - name: Prepare release
+
+      - name: Push branch and 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: |
-          git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           # Try to delete any existing release for the current PR.
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
-          git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
-          git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release
@@ -74,17 +71,25 @@ jobs:
 
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions-ecosystem/action-add-labels@v1
+        uses: actions/github-script@v7
         with:
-          number: ${{ steps.workflow-info.outputs.pullRequestNumber }}
-          labels: toolchain-available
+          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
+      - name: Find most recent nightly in feature branch
         id: most-recent-nightly-tag
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
-          echo "MOST_RECENT_NIGHTLY=$(script/most-recent-nightly-tag.sh)" >> $GITHUB_ENV
+          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 != '' }}
@@ -95,10 +100,10 @@ jobs:
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: ready
         run: |
-          echo "Most recent nightly: $MOST_RECENT_NIGHTLY"
-          NIGHTLY_SHA=$(git rev-parse nightly-$MOST_RECENT_NIGHTLY^{commit})
+          echo "Most recent nightly 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: $NIGHTLY_SHA"
-          MERGE_BASE_SHA=$(git merge-base origin/master HEAD)
+          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 "Most recent nightly tag agrees with the merge base."
@@ -116,7 +121,7 @@ jobs:
           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 log -10
+            git -C lean4.git log -10 origin/master
 
             MESSAGE="- ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch."
           fi
@@ -162,9 +167,9 @@ jobs:
             else
               echo "The message already exists in the comment body."
             fi
-            echo "::set-output name=mathlib_ready::false"
+            echo "mathlib_ready=false" >> $GITHUB_OUTPUT
           else
-            echo "::set-output name=mathlib_ready::true"
+            echo "mathlib_ready=true" >> $GITHUB_OUTPUT
           fi
 
       # We next automatically create a Mathlib branch using this toolchain.

.github/workflows/pr-title.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR title
-        uses: actions/github-script@v6
+        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;

.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

CODEOWNERS

@@ -18,4 +18,5 @@
 /src/Lean/Parser/ @Kha
 /src/Lean/PrettyPrinter/ @Kha
 /src/Lean/Server/ @mhuisi
+/src/Lean/Widget/ @Vtec234
 /src/runtime/io.cpp @joehendrix

RELEASES.md

@@ -8,30 +8,126 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.5.0 (development in progress)
+v4.6.0 (development in progress)
 ---------
 
+v4.5.0
+---------
+
+* Modify the lexical syntax of string literals to have string gaps, which are escape sequences of the form `"\" newline whitespace*`.
+  These have the interpetation of an empty string and allow a string to flow across multiple lines without introducing additional whitespace.
+  The following is equivalent to `"this is a string"`.
+  ```lean
+  "this is \
+     a string"
+  ```
+  [PR #2821](https://github.com/leanprover/lean4/pull/2821) and [RFC #2838](https://github.com/leanprover/lean4/issues/2838).
+
+* Add raw string literal syntax. For example, `r"\n"` is equivalent to `"\\n"`, with no escape processing.
+  To include double quote characters in a raw string one can add sufficiently many `#` characters before and after
+  the bounding `"`s, as in `r#"the "the" is in quotes"#` for `"the \"the\" is in quotes"`.
+  [PR #2929](https://github.com/leanprover/lean4/pull/2929) and [issue #1422](https://github.com/leanprover/lean4/issues/1422).
+
+* The low-level `termination_by'` clause is no longer supported.
+
+  Migration guide: Use `termination_by` instead, e.g.:
+  ```diff
+  -termination_by' measure (fun ⟨i, _⟩ => as.size - i)
+  +termination_by go i _ => as.size - i
+  ```
+
+  If the well-founded relation you want to use is not the one that the
+  `WellFoundedRelation` type class would infer for your termination argument,
+  you can use `WellFounded.wrap` from the std libarary to explicitly give one:
+  ```diff
+  -termination_by' ⟨r, hwf⟩
+  +termination_by _ x => hwf.wrap x
+  ```
+
+* Support snippet edits in LSP `TextEdit`s. See `Lean.Lsp.SnippetString` for more details.
+
+* Deprecations and changes in the widget API.
+  - `Widget.UserWidgetDefinition` is deprecated in favour of `Widget.Module`. The annotation `@[widget]` is deprecated in favour of `@[widget_module]`. To migrate a definition of type `UserWidgetDefinition`, remove the `name` field and replace the type with `Widget.Module`. Removing the `name` results in a title bar no longer being drawn above your panel widget. To add it back, draw it as part of the component using `<details open=true><summary class='mv2 pointer'>{name}</summary>{rest_of_widget}</details>`. See an example migration [here](https://github.com/leanprover/std4/pull/475/files#diff-857376079661a0c28a53b7ff84701afabbdf529836a6944d106c5294f0e68109R43-R83).
+  - The new command `show_panel_widgets` allows displaying always-on and locally-on panel widgets.
+  - `RpcEncodable` widget props can now be stored in the infotree.
+  - See [RFC 2963](https://github.com/leanprover/lean4/issues/2963) for more details and motivation. 
+
+* If no usable lexicographic order can be found automatically for a termination proof, explain why.
+  See [feat: GuessLex: if no measure is found, explain why](https://github.com/leanprover/lean4/pull/2960).
+
+* Option to print [inferred termination argument](https://github.com/leanprover/lean4/pull/3012).
+  With `set_option showInferredTerminationBy true` you will get messages like
+  ```
+  Inferred termination argument:
+  termination_by
+  ackermann n m => (sizeOf n, sizeOf m)
+  ```
+  for automatically generated `termination_by` clauses.
+
+* More detailed error messages for [invalid mutual blocks](https://github.com/leanprover/lean4/pull/2949).
+
+* [Multiple](https://github.com/leanprover/lean4/pull/2923) [improvements](https://github.com/leanprover/lean4/pull/2969) to the output of `simp?` and `simp_all?`.
+
+* Tactics with `withLocation *` [no longer fail](https://github.com/leanprover/lean4/pull/2917) if they close the main goal.
+
+* Implementation of a `test_extern` command for writing tests for `@[extern]` and `@[implemented_by]` functions.
+  Usage is 
+  ```
+  import Lean.Util.TestExtern
+
+  test_extern Nat.add 17 37
+  ```
+  The head symbol must be the constant with the `@[extern]` or `@[implemented_by]` attribute. The return type must have a `DecidableEq` instance.
+
+Bug fixes for 
+[#2853](https://github.com/leanprover/lean4/issues/2853), [#2953](https://github.com/leanprover/lean4/issues/2953), [#2966](https://github.com/leanprover/lean4/issues/2966), 
+[#2971](https://github.com/leanprover/lean4/issues/2971), [#2990](https://github.com/leanprover/lean4/issues/2990), [#3094](https://github.com/leanprover/lean4/issues/3094).
+
+Bug fix for [eager evaluation of default value](https://github.com/leanprover/lean4/pull/3043) in `Option.getD`.
+Avoid [panic in `leanPosToLspPos`](https://github.com/leanprover/lean4/pull/3071) when file source is unavailable.
+Improve [short-circuiting behavior](https://github.com/leanprover/lean4/pull/2972) for `List.all` and `List.any`.
+
+Several Lake bug fixes: [#3036](https://github.com/leanprover/lean4/issues/3036), [#3064](https://github.com/leanprover/lean4/issues/3064), [#3069](https://github.com/leanprover/lean4/issues/3069).
+
 v4.4.0
 ---------
 
+* Lake and the language server now support per-package server options using the `moreServerOptions` config field, as well as options that apply to both the language server and `lean` using the `leanOptions` config field. Setting either of these fields instead of `moreServerArgs` ensures that viewing files from a dependency uses the options for that dependency. Additionally, `moreServerArgs` is being deprecated in favor of the `moreGlobalServerArgs` field. See PR [#2858](https://github.com/leanprover/lean4/pull/2858).
+  
+  A Lakefile with the following deprecated package declaration:
+  ```lean
+  def moreServerArgs := #[
+    "-Dpp.unicode.fun=true"
+  ]
+  def moreLeanArgs := moreServerArgs
+  
+  package SomePackage where
+    moreServerArgs := moreServerArgs
+    moreLeanArgs := moreLeanArgs
+  ```
+  
+  ... can be updated to the following package declaration to use per-package options:
+  ```lean
+  package SomePackage where
+    leanOptions := #[⟨`pp.unicode.fun, true⟩]
+  ```
 * [Rename request handler](https://github.com/leanprover/lean4/pull/2462).
 * [Import auto-completion](https://github.com/leanprover/lean4/pull/2904).
 * [`pp.beta`` to apply beta reduction when pretty printing](https://github.com/leanprover/lean4/pull/2864).
-* [Per-package server options](https://github.com/leanprover/lean4/pull/2858).
 * [Embed and check githash in .olean](https://github.com/leanprover/lean4/pull/2766).
 * [Guess lexicographic order for well-founded recursion](https://github.com/leanprover/lean4/pull/2874).
 * [Allow trailing comma in tuples, lists, and tactics](https://github.com/leanprover/lean4/pull/2643).
 
-Bug fixes for [#2628](https://github.com/leanprover/lean4/issue/2628), [#2883](https://github.com/leanprover/lean4/issue/2883),
-[#2810](https://github.com/leanprover/lean4/issue/2810), [#2925](https://github.com/leanprover/lean4/issue/2925), and [#2914](https://github.com/leanprover/lean4/issue/2914).
+Bug fixes for [#2628](https://github.com/leanprover/lean4/issues/2628), [#2883](https://github.com/leanprover/lean4/issues/2883),
+[#2810](https://github.com/leanprover/lean4/issues/2810), [#2925](https://github.com/leanprover/lean4/issues/2925), and [#2914](https://github.com/leanprover/lean4/issues/2914).
 
 **Lake:**
 
 * `lake init .` and a bare `lake init` and will now use the current directory as the package name. [#2890](https://github.com/leanprover/lean4/pull/2890)
-* `lake new` and `lake init` will now produce errors on invalid package names such as `..`, `foo/bar`, `Init`, `Lean`, `Lake`, and `Main`. See issue [#2637](https://github.com/leanprover/lean4/issue/2637) and PR [#2890](https://github.com/leanprover/lean4/pull/2890).
-* `lean_lib` no longer converts its name to upper camel case (e.g., `lean_lib bar` will include modules named `bar.*` rather than `Bar.*`). See issue [#2567](https://github.com/leanprover/lean4/issue/2567) and PR [#2889](https://github.com/leanprover/lean4/pull/2889).
-* Lean and Lake now properly support non-identifier library names (e.g., `lake new 123-hello` and `import «123Hello»` now work correctly). See issue [#2865](https://github.com/leanprover/lean4/issue/2865) and PR [#2889](https://github.com/leanprover/lean4/pull/2888).
-* Lake now filters the environment extensions loaded from a compiled configuration (`lakefile.olean`) to include only those relevant to Lake's workspace loading process. This resolves segmentation faults caused by environment extension type mismatches (e.g., when defining custom elaborators via `elab` in configurations). See issue [#2632](https://github.com/leanprover/lean4/issue/2632) and PR [#2896](https://github.com/leanprover/lean4/pull/2896).
+* `lake new` and `lake init` will now produce errors on invalid package names such as `..`, `foo/bar`, `Init`, `Lean`, `Lake`, and `Main`. See issue [#2637](https://github.com/leanprover/lean4/issues/2637) and PR [#2890](https://github.com/leanprover/lean4/pull/2890).
+* `lean_lib` no longer converts its name to upper camel case (e.g., `lean_lib bar` will include modules named `bar.*` rather than `Bar.*`). See issue [#2567](https://github.com/leanprover/lean4/issues/2567) and PR [#2889](https://github.com/leanprover/lean4/pull/2889).
+* Lean and Lake now properly support non-identifier library names (e.g., `lake new 123-hello` and `import «123Hello»` now work correctly). See issue [#2865](https://github.com/leanprover/lean4/issues/2865) and PR [#2889](https://github.com/leanprover/lean4/pull/2888).
+* Lake now filters the environment extensions loaded from a compiled configuration (`lakefile.olean`) to include only those relevant to Lake's workspace loading process. This resolves segmentation faults caused by environment extension type mismatches (e.g., when defining custom elaborators via `elab` in configurations). See issue [#2632](https://github.com/leanprover/lean4/issues/2632) and PR [#2896](https://github.com/leanprover/lean4/pull/2896).
 * Cloud releases will now properly be re-unpacked if the build directory is removed. See PR [#2928](https://github.com/leanprover/lean4/pull/2928).
 * Lake's `math` template has been simplified. See PR [#2930](https://github.com/leanprover/lean4/pull/2930).
 * `lake exe <target>` now parses `target` like a build target (as the help text states it should) rather than as a basic name. For example, `lake exe @mathlib/runLinter` should now work. See PR [#2932](https://github.com/leanprover/lean4/pull/2932).

doc/SUMMARY.md

@@ -4,7 +4,6 @@
 - [Tour of Lean](./tour.md)
 - [Setting Up Lean](./quickstart.md)
   - [Extended Setup Notes](./setup.md)
-  - [Nix Setup](./setup/nix.md)
 - [Theorem Proving in Lean](./tpil.md)
 - [Functional Programming in Lean](fplean.md)
 - [Examples](./examples.md)
@@ -86,7 +85,6 @@
   - [macOS Setup](./make/osx-10.9.md)
   - [Windows MSYS2 Setup](./make/msys2.md)
   - [Windows with WSL](./make/wsl.md)
-  - [Nix Setup (*Experimental*)](./make/nix.md)
 - [Bootstrapping](./dev/bootstrap.md)
 - [Testing](./dev/testing.md)
 - [Debugging](./dev/debugging.md)

doc/dev/bootstrap.md

@@ -65,16 +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.
 
-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.
+## Updating stage0
 
-Updates to `stage0` should be their own commits in the Git history. In
-other words, before running `make update-stage0`, please commit your
-work. Then, commit the updated `stage0` compiler code with the commit message:
+Finally, when we want to use new language features in the library, we need to
+update the archived C source code of the stage 0 compiler in `stage0/src`.
+
+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
 

doc/dev/testing.md

@@ -5,7 +5,6 @@ After [building Lean](../make/index.md) you can run all the tests using
 cd build/release
 make test ARGS=-j4
 ```
-
 Change the 4 to the maximum number of parallel tests you want to
 allow. The best choice is the number of CPU cores on your machine as
 the tests are mostly CPU bound.  You can find the number of processors
@@ -17,6 +16,12 @@ adding the `-C stageN` argument. The default when run as above is stage 1.  The
 Lean tests will automatically use that stage's corresponding Lean
 executables
 
+Running `make test` will not pick up new test files; run
+```bash
+cmake build/release/stage1
+```
+to update the list of tests.
+
 You can also use `ctest` directly if you are in the right folder.  So
 to run stage1 tests with a 300 second timeout run this:
 
@@ -24,6 +29,9 @@ to run stage1 tests with a 300 second timeout run this:
 cd build/release/stage1
 ctest -j 4 --output-on-failure --timeout 300
 ```
+Useful `ctest` flags are `-R <name of test>` to run a single test, and
+`--rerun-failed` to run all tests that failed during the last run.
+You can also pass `ctest` flags via `make test ARGS="--rerun-failed"`.
 
 To get verbose output from ctest pass the `--verbose` command line
 option. Test output is normally suppressed and only summary
@@ -124,8 +132,3 @@ outputs. `meld` can also be used to repair the problems.
 
 In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
 To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.
-When using the Nix setup, add `--keep-failed` to the `nix build` call and then call
-```sh
-tests/lean/copy-produced <build-dir>/source/tests/lean
-```
-instead where `<build-dir>` is the path printed out by `nix build`.

doc/examples/widgets.lean

@@ -15,9 +15,8 @@ sections of a Lean document. User widgets are rendered in the Lean infoview.
 To try it out, simply type in the following code and place your cursor over the `#widget` command.
 -/
 
-@[widget]
-def helloWidget : UserWidgetDefinition where
-  name := "Hello"
+@[widget_module]
+def helloWidget : Widget.Module where
   javascript := "
     import * as React from 'react';
     export default function(props) {
@@ -25,7 +24,7 @@ def helloWidget : UserWidgetDefinition where
       return React.createElement('p', {}, name + '!')
     }"
 
-#widget helloWidget .null
+#widget helloWidget
 
 /-!
 If you want to dive into a full sample right away, check out
@@ -56,7 +55,11 @@ to the React component. In our first invocation of `#widget`, we set it to `.nul
 happens when you type in:
 -/
 
-#widget helloWidget (Json.mkObj [("name", "<your name here>")])
+structure HelloWidgetProps where
+  name? : Option String := none
+  deriving Server.RpcEncodable
+
+#widget helloWidget with { name? := "<your name here>" : HelloWidgetProps }
 
 /-!
 💡 NOTE: The RPC system presented below does not depend on JavaScript. However the primary use case
@@ -132,9 +135,8 @@ on this we either display an `InteractiveCode` with the type, `mapRpcError` the
 to turn it into a readable message, or show a `Loading..` message, respectively.
 -/
 
-@[widget]
-def checkWidget : UserWidgetDefinition where
-  name := "#check as a service"
+@[widget_module]
+def checkWidget : Widget.Module where
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
@@ -160,7 +162,7 @@ export default function(props) {
 Finally we can try out the widget.
 -/
 
-#widget checkWidget .null
+#widget checkWidget
 
 /-!
 ![`#check` as a service](../images/widgets_caas.png)
@@ -193,9 +195,8 @@ interact with the text editor.
 You can see the full API for this [here](https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview-api/src/infoviewApi.ts#L52)
 -/
 
-@[widget]
-def insertTextWidget : UserWidgetDefinition where
-  name := "textInserter"
+@[widget_module]
+def insertTextWidget : Widget.Module where
   javascript := "
 import * as React from 'react';
 const e = React.createElement;
@@ -213,4 +214,4 @@ export default function(props) {
 
 /-! Finally, we can try this out: -/
 
-#widget insertTextWidget .null
+#widget insertTextWidget

doc/lexical_structure.md

@@ -8,7 +8,7 @@ A Lean program consists of a stream of UTF-8 tokens where each token
 is one of the following:
 
 ```
-   token: symbol | command | ident | string | char | numeral |
+   token: symbol | command | ident | string | raw_string | char | numeral |
         : decimal | doc_comment | mod_doc_comment | field_notation
 ```
 
@@ -79,15 +79,35 @@ special characters:
 [Unicode table](https://unicode-table.com/en/) so "\xA9 Copyright 2021" is "© Copyright 2021".
 - `\uHHHH` puts the character represented by the 4 digit hexadecimal into the string, so the following
 string "\u65e5\u672c" will become "日本" which means "Japan".
+- `\` followed by a newline and then any amount of whitespace is a "gap" that is equivalent to the empty string,
+useful for letting a string literal span across multiple lines. Gaps spanning multiple lines can be confusing,
+so the parser raises an error if the trailing whitespace contains any newlines.
 
 So the complete syntax is:
 
 ```
    string       : '"' string_item '"'
-   string_item  : string_char | string_escape
-   string_char  : [^\\]
-   string_escape: "\" ("\" | '"' | "'" | "n" | "t" | "x" hex_char{2} | "u" hex_char{4} )
+   string_item  : string_char | char_escape | string_gap
+   string_char  : [^"\\]
+   char_escape  : "\" ("\" | '"' | "'" | "n" | "t" | "x" hex_char{2} | "u" hex_char{4})
    hex_char     : [0-9a-fA-F]
+   string_gap   : "\" newline whitespace*
+```
+
+Raw String Literals
+===================
+
+Raw string literals are string literals without any escape character processing.
+They begin with `r##...#"` (with zero or more `#` characters) and end with `"#...##` (with the same number of `#` characters).
+The contents of a raw string literal may contain `"##..#` so long as the number of `#` characters
+is less than the number of `#` characters used to begin the raw string literal.
+
+```
+   raw_string          : raw_string_aux(0) | raw_string_aux(1) | raw_string_aux(2) | ...
+   raw_string_aux(n)   : 'r' '#'{n} '"' raw_string_item '"' '#'{n}
+   raw_string_item(n)  : raw_string_char | raw_string_quote(n)
+   raw_string_char     : [^"]
+   raw_string_quote(n) : '"' '#'{0..n-1}
 ```
 
 Char Literals
@@ -96,7 +116,9 @@ Char Literals
 Char literals are enclosed by single quotes (``'``).
 
 ```
-   char: "'" string_item "'"
+   char      : "'" char_item "'"
+   char_item : char_char | char_escape
+   char_char : [^'\\]
 ```
 
 Numeric Literals

doc/make/index.md

@@ -14,8 +14,6 @@ Platform-Specific Setup
 - [Windows (WSL)](wsl.md)
 - [macOS (homebrew)](osx-10.9.md)
 - Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it.
-- There is also an [**experimental** setup based purely on Nix](nix.md) that works fundamentally differently from the
-  make/CMake setup described on this page.
 
 Generic Build Instructions
 --------------------------

doc/make/nix.md

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

doc/quickstart.md

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

doc/setup.md

@@ -50,10 +50,10 @@ Foo.lean       # main file, import via `import Foo`
 Foo/
   A.lean       # further files, import via e.g. `import Foo.A`
   A/...        # further nesting
-build/         # `lake` build output directory
+.lake/         # `lake` build output directory
 ```
 
-After running `lake build` you will see a binary named `./build/bin/foo` and when you run it you should see the output:
+After running `lake build` you will see a binary named `./.lake/build/bin/foo` and when you run it you should see the output:
 ```
 Hello, world!
 ```

doc/setup/nix.md

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

doc/syntax_highlight_in_latex.md

@@ -67,6 +67,9 @@ theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f
 \end{document}
 ```
 
+If your version of `minted` is v2.7 or newer, but before v3.0,
+you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
+
 You can then compile `test.tex` by executing the following command:
 
 ```bash

doc/typeclass.md

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

lean.code-workspace

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

nix/bootstrap.nix

@@ -83,13 +83,13 @@ rec {
         # use same stage for retrieving dependencies
         lean-leanDeps = stage0;
         lean-final = self;
-        leanFlags = [ "-DwarningAsError=true" ];
       } ({
         src = src + "/src";
         roots = [ { mod = args.name; glob = "andSubmodules"; } ];
         fullSrc = src;
         srcPath = "$PWD/src:$PWD/src/lake";
         inherit debug;
+        leanFlags = [ "-DwarningAsError=true" ];
       } // args);
       Init' = build { name = "Init"; deps = []; };
       Lean' = build { name = "Lean"; deps = [ Init' ]; };

script/most-recent-nightly-tag.sh

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

src/CMakeLists.txt

@@ -9,7 +9,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 5)
+set(LEAN_VERSION_MINOR 6)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init/Classical.lean

@@ -22,7 +22,7 @@ noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :
 theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
   (indefiniteDescription p h).property
 
-/-- Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality. -/
+/-- **Diaconescu's theorem**: excluded middle from choice, Function extensionality and propositional extensionality. -/
 theorem em (p : Prop) : p ∨ ¬p :=
   let U (x : Prop) : Prop := x = True ∨ p
   let V (x : Prop) : Prop := x = False ∨ p

src/Init/Data/ByteArray/Basic.lean

@@ -81,7 +81,7 @@ def isEmpty (s : ByteArray) : Bool :=
   If `exact` is `false`, the capacity will be doubled when grown. -/
 @[extern "lean_byte_array_copy_slice"]
 def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
-  ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + len) dest.data.size⟩
+  ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + min len (src.data.size - srcOff)) dest.data.size⟩
 
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)

src/Init/Data/List/Basic.lean

@@ -124,7 +124,8 @@ def appendTR (as bs : List α) : List α :=
   induction as with
   | nil  => rfl
   | cons a as ih =>
-    simp [reverseAux, List.append, ih, reverseAux_reverseAux]
+    rw [reverseAux, reverseAux_reverseAux]
+    simp [List.append, ih, reverseAux]
 
 instance : Append (List α) := ⟨List.append⟩
 
@@ -557,16 +558,22 @@ def takeWhile (p : α → Bool) : (xs : List α) → List α
 /--
 `O(|l|)`. Returns true if `p` is true for any element of `l`.
 * `any p [a, b, c] = p a || p b || p c`
+
+Short-circuits upon encountering the first `true`.
 -/
-@[inline] def any (l : List α) (p : α → Bool) : Bool :=
-  foldr (fun a r => p a || r) false l
+def any : List α -> (α → Bool) -> Bool
+  | [], _ => false
+  | h :: t, p => p h || any t p
 
 /--
 `O(|l|)`. Returns true if `p` is true for every element of `l`.
 * `all p [a, b, c] = p a && p b && p c`
+
+Short-circuits upon encountering the first `false`.
 -/
-@[inline] def all (l : List α) (p : α → Bool) : Bool :=
-  foldr (fun a r => p a && r) true l
+def all : List α -> (α → Bool) -> Bool
+  | [], _ => true
+  | h :: t, p => p h && all t p
 
 /--
 `O(|l|)`. Returns true if `true` is an element of the list of booleans `l`.

src/Init/Meta.lean

@@ -773,6 +773,16 @@ def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos)
   else
     none
 
+/--
+Decodes a valid string gap after the `\`.
+Note that this function matches `"\" whitespace+` rather than
+the more restrictive `"\" newline whitespace*` since this simplifies the implementation.
+Justification: this does not overlap with any other sequences beginning with `\`.
+-/
+def decodeStringGap (s : String) (i : String.Pos) : Option String.Pos := do
+  guard <| (s.get i).isWhitespace
+  s.nextWhile Char.isWhitespace (s.next i)
+
 partial def decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Option String := do
   let c := s.get i
   let i := s.next i
@@ -781,14 +791,49 @@ partial def decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Optio
   else if s.atEnd i then
     none
   else if c == '\\' then do
-    let (c, i) ← decodeQuotedChar s i
-    decodeStrLitAux s i (acc.push c)
+    if let some (c, i) := decodeQuotedChar s i then
+      decodeStrLitAux s i (acc.push c)
+    else if let some i := decodeStringGap s i then
+      decodeStrLitAux s i acc
+    else
+      none
   else
     decodeStrLitAux s i (acc.push c)
 
-def decodeStrLit (s : String) : Option String :=
-  decodeStrLitAux s ⟨1⟩ ""
+/--
+Takes a raw string literal, counts the number of `#`'s after the `r`, and interprets it as a string.
+The position `i` should start at `1`, which is the character after the leading `r`.
+The algorithm is simple: we are given `r##...#"...string..."##...#` with zero or more `#`s.
+By counting the number of leading `#`'s, we can extract the `...string...`.
+-/
+partial def decodeRawStrLitAux (s : String) (i : String.Pos) (num : Nat) : String :=
+  let c := s.get i
+  let i := s.next i
+  if c == '#' then
+    decodeRawStrLitAux s i (num + 1)
+  else
+    s.extract i ⟨s.utf8ByteSize - (num + 1)⟩
 
+/--
+Takes the string literal lexical syntax parsed by the parser and interprets it as a string.
+This is where escape sequences are processed for example.
+The string `s` is is either a plain string literal or a raw string literal.
+
+If it returns `none` then the string literal is ill-formed, which indicates a bug in the parser.
+The function is not required to return `none` if the string literal is ill-formed.
+-/
+def decodeStrLit (s : String) : Option String :=
+  if s.get 0 == 'r' then
+    decodeRawStrLitAux s ⟨1⟩ 0
+  else
+    decodeStrLitAux s ⟨1⟩ ""
+
+/--
+If the provided `Syntax` is a string literal, returns the string it represents.
+
+Even if the `Syntax` is a `str` node, the function may return `none` if its internally ill-formed.
+The parser should always create well-formed `str` nodes.
+-/
 def isStrLit? (stx : Syntax) : Option String :=
   match isLit? strLitKind stx with
   | some val => decodeStrLit val
@@ -1162,8 +1207,12 @@ private partial def decodeInterpStrLit (s : String) : Option String :=
     else if s.atEnd i then
       none
     else if c == '\\' then do
-      let (c, i) ← decodeInterpStrQuotedChar s i
-      loop i (acc.push c)
+      if let some (c, i) := decodeInterpStrQuotedChar s i then
+        loop i (acc.push c)
+      else if let some i := decodeStringGap s i then
+        loop i acc
+      else
+        none
     else
       loop i (acc.push c)
   loop ⟨1⟩ ""

src/Init/MetaTypes.lean

@@ -21,7 +21,14 @@ structure Module where
 namespace Meta
 
 inductive TransparencyMode where
-  | all | default | reducible | instances
+  /-- unfold all constants, even those tagged as `@[irreducible]`. -/
+  | all
+  /-- unfold all constants except those tagged as `@[irreducible]`. -/
+  | default
+  /-- unfold only constants tagged with the `@[reducible]` attribute. -/
+  | reducible
+  /-- unfold reducible constants and constants tagged with the `@[instance]` attribute. -/
+  | instances
   deriving Inhabited, BEq
 
 inductive EtaStructMode where

src/Init/Prelude.lean

@@ -66,6 +66,19 @@ example (b : Bool) : Function.const Bool 10 b = 10 :=
 @[inline] def Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
   fun _ => a
 
+/--
+The encoding of `let_fun x := v; b` is `letFun v (fun x => b)`.
+This is equal to `(fun x => b) v`, so the value of `x` is not accessible to `b`.
+This is in contrast to `let x := v; b`, where the value of `x` is accessible to `b`.
+
+There is special support for `letFun`.
+Both WHNF and `simp` are aware of `letFun` and can reduce it when zeta reduction is enabled,
+despite the fact it is marked `irreducible`.
+For metaprogramming, the function `Lean.Expr.letFun?` can be used to recognize a `let_fun` expression
+to extract its parts as if it were a `let` expression.
+-/
+@[irreducible] def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v
+
 set_option checkBinderAnnotations false in
 /--
 `inferInstance` synthesizes a value of any target type by typeclass
@@ -2213,9 +2226,10 @@ returns `a` if `opt = some a` and `dflt` otherwise.
 This function is `@[macro_inline]`, so `dflt` will not be evaluated unless
 `opt` turns out to be `none`.
 -/
-@[macro_inline] def Option.getD : Option α → α → α
-  | some x, _ => x
-  | none,   e => e
+@[macro_inline] def Option.getD (opt : Option α) (dflt : α) : α :=
+  match opt with
+  | some x => x
+  | none => dflt
 
 /--
 Map a function over an `Option` by applying the function to the contained

src/Init/SimpLemmas.lean

@@ -84,6 +84,10 @@ theorem dite_congr {_ : Decidable b} [Decidable c]
 @[simp] theorem ite_false (a b : α) : (if False then a else b) = b := rfl
 @[simp] theorem dite_true {α : Sort u} {t : True → α} {e : ¬ True → α} : (dite True t e) = t True.intro := rfl
 @[simp] theorem dite_false {α : Sort u} {t : False → α} {e : ¬ False → α} : (dite False t e) = e not_false := rfl
+@[simp ↓] theorem ite_cond_true {_ : Decidable c} (a b : α) (h : c) : (if c then a else b) = a := by simp [h]
+@[simp ↓] theorem ite_cond_false {_ : Decidable c} (a b : α) (h : ¬ c) : (if c then a else b) = b := by simp [h]
+@[simp ↓] theorem dite_cond_true {α : Sort u} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c) : (dite c t e) = t h := by simp [h]
+@[simp ↓] theorem dite_cond_false {α : Sort u} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : ¬ c) : (dite c t e) = e h := by simp [h]
 @[simp] theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a := by cases d <;> rfl
 @[simp] theorem and_self (p : Prop) : (p ∧ p) = p := propext ⟨(·.1), fun h => ⟨h, h⟩⟩
 @[simp] theorem and_true (p : Prop) : (p ∧ True) = p := propext ⟨(·.1), (⟨·, trivial⟩)⟩

src/Lean/Attributes.lean

@@ -330,7 +330,7 @@ private def AttributeExtension.mkInitial : IO AttributeExtensionState := do
 
 unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl :=
   match env.find? declName with
-  | none      => throw ("unknow constant '" ++ toString declName ++ "'")
+  | none      => throw ("unknown constant '" ++ toString declName ++ "'")
   | some info =>
     match info.type with
     | Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -658,7 +658,9 @@ where
       visit (f.beta e.getAppArgs)
 
   visitApp (e : Expr) : M Arg := do
-    if let .const declName _ := e.getAppFn then
+    if let some (args, n, t, v, b) := e.letFunAppArgs? then
+      visitCore <| mkAppN (.letE n t v b (nonDep := true)) args
+    else if let .const declName _ := e.getAppFn then
       if declName == ``Quot.lift then
         visitQuotLift e
       else if declName == ``Quot.mk then
@@ -725,11 +727,8 @@ where
       pushElement (.fun funDecl)
       return .fvar funDecl.fvarId
 
-  visitMData (mdata : MData) (e : Expr) : M Arg := do
-    if let some (.app (.lam n t b ..) v) := letFunAnnotation? (.mdata mdata e) then
-      visitLet (.letE n t v b (nonDep := true)) #[]
-    else
-      visit e
+  visitMData (_mdata : MData) (e : Expr) : M Arg := do
+    visit e
 
   visitProj (s : Name) (i : Nat) (e : Expr) : M Arg := do
     match (← visit e) with

src/Lean/CoreM.lean

@@ -315,7 +315,7 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla
     | _ => pure ()
 
 register_builtin_option compiler.enableNew : Bool := {
-  defValue := true
+  defValue := false
   group    := "compiler"
   descr    := "(compiler) enable the new code generator, this should have no significant effect on your code but it does help to test the new code generator; unset to only use the old code generator instead"
 }

src/Lean/Data/Array.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+import Init.Data.Array
+
+namespace Array
+
+/-!
+This module contains utility functions involving Arrays that are useful in a few places
+of the lean code base, but too specialized to live in `Init.Data.Array`, which arguably
+is part of the public, user-facing standard library.
+-/
+
+/--
+Given an array `a`, runs `f xᵢ xⱼ` for all `i < j`, removes those entries for which `f` returns
+`false` (and will subsequently skip pairs if one element is removed), and returns the array of
+remaining elements.
+
+This can be used to remove elements from an array where a “better” element, in some partial
+order, exists in the array.
+-/
+def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × Bool)) :
+    m (Array α) := do
+  let mut removed := Array.mkArray a.size false
+  let mut numRemoved := 0
+  for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do
+    unless removed[i]! || removed[j]! do
+      let xi := a[i]'h1.2
+      let xj := a[j]'h2.2
+      let (keepi, keepj) ← f xi xj
+      unless keepi do
+        numRemoved := numRemoved + 1
+        removed := removed.set! i true
+      unless keepj do
+        numRemoved := numRemoved + 1
+        removed := removed.set! j true
+  let mut a' := Array.mkEmpty numRemoved
+  for h : i in [:a.size] do
+    unless removed[i]! do
+      a' := a'.push (a[i]'h.2)
+  return a'
+
+end Array

src/Lean/Data/Lsp/Basic.lean

@@ -78,6 +78,38 @@ structure Command where
   arguments? : Option (Array Json) := none
   deriving ToJson, FromJson
 
+/-- A snippet is a string that gets inserted into a document,
+and can afterwards be edited by the user in a structured way.
+
+Snippets contain instructions that
+specify how this structured editing should proceed.
+They are expressed in a domain-specific language
+based on one from TextMate,
+including the following constructs:
+- Designated positions for subsequent user input,
+  called "tab stops" after their most frequently-used keybinding.
+  They are denoted with `$1`, `$2`, and so forth.
+  `$0` denotes where the cursor should be positioned after all edits are completed,
+  defaulting to the end of the string.
+  Snippet tab stops are unrelated to tab stops used for indentation.
+- Tab stops with default values, called _placeholders_, written `${1:default}`.
+  The default may itself contain a tab stop or a further placeholder
+  and multiple options to select from may be provided
+  by surrounding them with `|`s and separating them with `,`,
+  as in `${1|if $2 then $3 else $4,if let $2 := $3 then $4 else $5|}`.
+- One of a set of predefined variables that are replaced with their values.
+  This includes the current line number (`$TM_LINE_NUMBER`)
+  or the text that was selected when the snippet was invoked (`$TM_SELECTED_TEXT`).
+- Formatting instructions to modify variables using regular expressions
+  or a set of predefined filters.
+
+The full syntax and semantics of snippets,
+including the available variables and the rules for escaping control characters,
+are described in the [LSP specification](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#snippet_syntax). -/
+structure SnippetString where
+  value : String
+  deriving ToJson, FromJson
+
 /-- A textual edit applicable to a text document.
 
 [reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textEdit) -/
@@ -87,6 +119,21 @@ structure TextEdit where
   range : Range
   /-- The string to be inserted. For delete operations use an empty string. -/
   newText : String
+  /-- If this field is present and the editor supports it,
+  `newText` is ignored
+  and an interactive snippet edit is performed instead.
+
+  The use of snippets in `TextEdit`s
+  is a Lean-specific extension to the LSP standard,
+  so `newText` should still be set to a correct value
+  as fallback in case the editor does not support this feature.
+  Even editors that support snippets may not always use them;
+  for instance, if the file is not already open,
+  VS Code will perform a normal text edit in the background instead. -/
+  /- NOTE: Similar functionality may be added to LSP in the future:
+  see [issue #592](https://github.com/microsoft/language-server-protocol/issues/592).
+  If such an addition occurs, this field should be deprecated. -/
+  leanExtSnippet? : Option SnippetString := none
   /-- Identifier for annotated edit.
 
     `WorkspaceEdit` has a `changeAnnotations` field that maps these identifiers to a `ChangeAnnotation`.

src/Lean/Data/Lsp/Utf16.lean

@@ -62,21 +62,24 @@ end String
 namespace Lean
 namespace FileMap
 
+private def lineStartPos (text : FileMap) (line : Nat) : String.Pos :=
+  if h : line < text.positions.size then
+    text.positions.get ⟨line, h⟩
+  else if text.positions.isEmpty then
+    0
+  else
+    text.positions.back
+
 /-- Computes an UTF-8 offset into `text.source`
 from an LSP-style 0-indexed (ln, col) position. -/
 def lspPosToUtf8Pos (text : FileMap) (pos : Lsp.Position) : String.Pos :=
-  let colPos :=
-    if h : pos.line < text.positions.size then
-      text.positions.get ⟨pos.line, h⟩
-    else if text.positions.isEmpty then
-      0
-    else
-      text.positions.back
-  let chr := text.source.utf16PosToCodepointPosFrom pos.character colPos
-  text.source.codepointPosToUtf8PosFrom colPos chr
+  let lineStartPos := lineStartPos text pos.line
+  let chr := text.source.utf16PosToCodepointPosFrom pos.character lineStartPos
+  text.source.codepointPosToUtf8PosFrom lineStartPos chr
 
 def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
-  | ⟨ln, col⟩ => ⟨ln-1, text.source.codepointPosToUtf16PosFrom col (text.positions.get! $ ln - 1)⟩
+  | ⟨line, col⟩ =>
+    ⟨line - 1, text.source.codepointPosToUtf16PosFrom col (lineStartPos text (line - 1))⟩
 
 def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
   text.leanPosToLspPos (text.toPosition pos)

src/Lean/Data/SMap.lean

@@ -97,7 +97,7 @@ def toList (m : SMap α β) : List (α × β) :=
 
 end SMap
 
-def List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
+def _root_.List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
   es.foldl (init := {}) fun s (a, b) => s.insert a b
 
 instance {_ : BEq α} {_ : Hashable α} [Repr α] [Repr β] : Repr (SMap α β) where

src/Lean/Elab/Binders.lean

@@ -668,12 +668,11 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
       let body ← instantiateMVars body
       mkLetFVars #[x] body (usedLetOnly := usedLetOnly)
   else
-    let f ← withLocalDecl id.getId (kind := kind) .default type fun x => do
+    withLocalDecl id.getId (kind := kind) .default type fun x => do
       addLocalVarInfo id x
       let body ← elabTermEnsuringType body expectedType?
       let body ← instantiateMVars body
-      mkLambdaFVars #[x] body (usedLetOnly := false)
-    pure <| mkLetFunAnnotation (mkApp f val)
+      mkLetFun x val body
   if elabBodyFirst then
     forallBoundedTelescope type binders.size fun xs type => do
       -- the original `fvars` from above are gone, so add back info manually

src/Lean/Elab/BuiltinNotation.lean

@@ -241,7 +241,8 @@ where
 
 /--
   Helper method for elaborating terms such as `(.+.)` where a constant name is expected.
-  This method is usually used to implement tactics that function names as arguments (e.g., `simp`).
+  This method is usually used to implement tactics that take function names as arguments
+  (e.g., `simp`).
 -/
 def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
   let some stx ← liftMacroM <| expandCDotArg? stx | pure none

src/Lean/Elab/Declaration.lean

@@ -348,7 +348,7 @@ def elabMutual : CommandElab := fun stx => do
         throwErrorAt bad "invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword"
     elabMutualDef stx[1].getArgs hints
   else
-    throwError "invalid mutual block"
+    throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
 
 /- leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "]" >> many1 ident -/
 @[builtin_command_elab «attribute»] def elabAttr : CommandElab := fun stx => do

src/Lean/Elab/InfoTree/Main.lean

@@ -142,7 +142,7 @@ def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) :
   return f!"Macro expansion\n{stx}\n===>\n{output}"
 
 def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
-  f!"UserWidget {info.widgetId}\n{Std.ToFormat.format info.props}"
+  f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
   f!"FVarAlias {info.userName.eraseMacroScopes}"

src/Lean/Elab/InfoTree/Types.lean

@@ -9,6 +9,8 @@ import Lean.Data.OpenDecl
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Data.Json
+import Lean.Server.Rpc.Basic
+import Lean.Widget.Types
 
 namespace Lean.Elab
 
@@ -95,17 +97,12 @@ structure CustomInfo where
   stx : Syntax
   value : Dynamic
 
-/-- An info that represents a user-widget.
-User-widgets are custom pieces of code that run on the editor client.
-You can learn about user widgets at `src/Lean/Widget/UserWidget`
--/
-structure UserWidgetInfo where
+/-- Information about a user widget associated with a syntactic span.
+This must be a panel widget.
+A panel widget is a widget that can be displayed
+in the infoview alongside the goal state. -/
+structure UserWidgetInfo extends Widget.WidgetInstance where
   stx : Syntax
-  /-- Id of `WidgetSource` object to use. -/
-  widgetId : Name
-  /-- Json representing the props to be loaded in to the component. -/
-  props : Json
-  deriving Inhabited
 
 /--
 Specifies that the given free variables should be considered semantically identical.

src/Lean/Elab/PatternVar.lean

@@ -146,7 +146,6 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
       ```
       def namedPattern := check... >> trailing_parser "@" >> optional (atomic (ident >> ":")) >> termParser
       ```
-      TODO: pattern variable for equality proof
      -/
     let id := stx[0]
     discard <| processVar id

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -21,16 +21,25 @@ structure EqnInfoCore where
   value       : Expr
   deriving Inhabited
 
-partial def expand : Expr → Expr
-  | Expr.letE _ _ v b _ => expand (b.instantiate1 v)
-  | Expr.mdata _ b      => expand b
-  | e => e
+/--
+Zeta reduces `let` and `let_fun` while consuming metadata.
+Returns true if progress is made.
+-/
+partial def expand (progress : Bool) (e : Expr) : Bool × Expr :=
+  match e with
+  | Expr.letE _ _ v b _ => expand true (b.instantiate1 v)
+  | Expr.mdata _ b      => expand true b
+  | e =>
+    if let some (_, _, v, b) := e.letFun? then
+      expand true (b.instantiate1 v)
+    else
+      (progress, e)
 
 def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
   let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | return none
-  unless rhs.isLet || rhs.isMData do return none
-  return some (← mvarId.replaceTargetDefEq (← mkEq lhs (expand rhs)))
+  let (true, rhs') := expand false rhs | return none
+  return some (← mvarId.replaceTargetDefEq (← mkEq lhs rhs'))
 
 def funext? (mvarId : MVarId) : MetaM (Option MVarId) := do
   let target ← mvarId.getType'

src/Lean/Elab/PreDefinition/Main.lean

@@ -100,8 +100,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
   let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
   let preDefs ← betaReduceLetRecApps preDefs
   let cliques := partitionPreDefs preDefs
-  let mut terminationBy ← liftMacroM <| WF.expandTerminationBy hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
-  let mut decreasingBy  ← liftMacroM <| WF.expandTerminationHint hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
+  let mut terminationBy ← liftMacroM <| WF.expandTerminationBy? hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
+  let mut decreasingBy  ← liftMacroM <| WF.expandDecreasingBy? hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
   let mut hasErrors := false
   for preDefs in cliques do
     trace[Elab.definition.scc] "{preDefs.map (·.declName)}"

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -122,7 +122,7 @@ where
     match (← reduceRecMatcher? e) with
     | some e' => return Simp.Step.done { expr := e' }
     | none    =>
-      match (← Simp.simpMatchCore? app e SplitIf.discharge?) with
+      match (← Simp.simpMatchCore? app.matcherName e SplitIf.discharge?) with
       | some r => return r
       | none => return Simp.Step.visit { expr := e }
 

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -13,29 +13,25 @@ import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.Structural.BRecOn
+import Lean.Data.Array
 
 namespace Lean.Elab.WF
 open Meta
 
-private def applyDefaultDecrTactic (mvarId : MVarId) : TermElabM Unit := do
-  let remainingGoals ← Tactic.run mvarId do
-    Tactic.evalTactic (← `(tactic| decreasing_tactic))
-  unless remainingGoals.isEmpty do
-    Term.reportUnsolvedGoals remainingGoals
-
-private def mkDecreasingProof (decreasingProp : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
-  let mvar ← mkFreshExprSyntheticOpaqueMVar decreasingProp
+/-
+Creates a subgoal for a recursive call, as an unsolved `MVar`. The goal is cleaned up, and
+the current syntax reference is stored in the `MVar`’s type as a `RecApp` marker, for
+use by `solveDecreasingGoals` below.
+-/
+private def mkDecreasingProof (decreasingProp : Expr) : TermElabM Expr := do
+  -- We store the current Ref in the MVar as a RecApp annotation around the type
+  let ref ← getRef
+  let mvar ← mkFreshExprSyntheticOpaqueMVar (mkRecAppWithSyntax decreasingProp ref)
   let mvarId := mvar.mvarId!
-  let mvarId ← mvarId.cleanup
-  match decrTactic? with
-  | none => applyDefaultDecrTactic mvarId
-  | some decrTactic =>
-    -- make info from `runTactic` available
-    pushInfoTree (.hole mvarId)
-    Term.runTactic mvarId decrTactic
-  instantiateMVars mvar
+  let _mvarId ← mvarId.cleanup
+  return mvar
 
-private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) (F : Expr) (e : Expr) : TermElabM Expr := do
+private partial def replaceRecApps (recFnName : Name) (fixedPrefixSize : Nat) (F : Expr) (e : Expr) : TermElabM Expr := do
   trace[Elab.definition.wf] "replaceRecApps:{indentExpr e}"
   trace[Elab.definition.wf] "{F} : {← inferType F}"
   loop F e |>.run' {}
@@ -47,7 +43,7 @@ where
       let args := e.getAppArgs
       let r := mkApp F (← loop F args[fixedPrefixSize]!)
       let decreasingProp := (← whnf (← inferType r)).bindingDomain!
-      let r := mkApp r (← mkDecreasingProof decreasingProp decrTactic?)
+      let r := mkApp r (← mkDecreasingProof decreasingProp)
       return mkAppN r (← args[fixedPrefixSize+1:].toArray.mapM (loop F))
 
   processApp (F : Expr) (e : Expr) : StateRefT (HasConstCache recFnName) TermElabM Expr := do
@@ -164,6 +160,47 @@ private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (v
   else
     k F val
 
+private def applyDefaultDecrTactic (mvarId : MVarId) : TermElabM Unit := do
+  let remainingGoals ← Tactic.run mvarId do
+    Tactic.evalTactic (← `(tactic| decreasing_tactic))
+  unless remainingGoals.isEmpty do
+    Term.reportUnsolvedGoals remainingGoals
+
+/-
+Given an array of MVars, assign MVars with equal type and subsumed local context to each other.
+Returns those MVar that did not get assigned.
+-/
+def assignSubsumed (mvars : Array MVarId) : MetaM (Array MVarId) :=
+  mvars.filterPairsM fun mv₁ mv₂ => do
+    let mvdecl₁ ← mv₁.getDecl
+    let mvdecl₂ ← mv₂.getDecl
+    if mvdecl₁.type == mvdecl₂.type then
+      -- same goals; check contexts.
+        if mvdecl₁.lctx.isSubPrefixOf mvdecl₂.lctx then
+          -- mv₁ is better
+          mv₂.assign (.mvar mv₁)
+          return (true, false)
+        if mvdecl₂.lctx.isSubPrefixOf mvdecl₁.lctx then
+          -- mv₂ is better
+          mv₁.assign (.mvar mv₂)
+          return (false, true)
+    return (true, true)
+
+def solveDecreasingGoals (decrTactic? : Option Syntax) (value : Expr) : MetaM Expr := do
+  let goals ← getMVarsNoDelayed value
+  let goals ← assignSubsumed goals
+  goals.forM fun goal => Lean.Elab.Term.TermElabM.run' <|
+    match decrTactic? with
+    | none => do
+      let some ref := getRecAppSyntax? (← goal.getType)
+        | throwError "MVar does not look like like a recursive call"
+        withRef ref <| applyDefaultDecrTactic goal
+    | some decrTactic => do
+      -- make info from `runTactic` available
+      pushInfoTree (.hole goal)
+      Term.runTactic goal decrTactic
+  instantiateMVars value
+
 def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (decrTactic? : Option Syntax) : TermElabM Expr := do
   let type ← instantiateForall preDef.type prefixArgs
   let (wfFix, varName) ← forallBoundedTelescope type (some 1) fun x type => do
@@ -186,7 +223,8 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (wfRel : Expr) (dec
       let F   := xs[1]!
       let val := preDef.value.beta (prefixArgs.push x)
       let val ← processSumCasesOn x F val fun x F val => do
-        processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size decrTactic?)
+        processPSigmaCasesOn x F val (replaceRecApps preDef.declName prefixArgs.size)
+      let val ← solveDecreasingGoals decrTactic? val
       mkLambdaFVars prefixArgs (mkApp wfFix (← mkLambdaFVars #[x, F] val))
 
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -14,6 +14,8 @@ import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
 import Lean.Elab.PreDefinition.WF.TerminationHint
+import Lean.Elab.PreDefinition.WF.PackMutual
+import Lean.Data.Array
 
 
 /-!
@@ -31,7 +33,6 @@ In addition to measures derived from `sizeOf xᵢ`, it also considers measures
 that assign an order to the functions themselves. This way we can support mutual
 function definitions where no arguments decrease from one function to another.
 
-
 The result of this module is a `TerminationWF`, which is then passed on to `wfRecursion`; this
 design is crucial so that whatever we infer in this module could also be written manually by the
 user. It would be bad if there are function definitions that can only be processed with the
@@ -66,23 +67,39 @@ open Lean Meta Elab
 
 namespace Lean.Elab.WF.GuessLex
 
+register_builtin_option showInferredTerminationBy : Bool := {
+  defValue := false
+  descr    := "In recursive definitions, show the inferred `termination_by` measure."
+}
+
 /--
 Given a predefinition, find good variable names for its parameters.
 Use user-given parameter names if present; use x1...xn otherwise.
+
 The length of the returned array is also used to determine the arity
 of the function, so it should match what `packDomain` does.
+
+The names ought to accessible (no macro scopes) and still fresh wrt to the current environment,
+so that with `showInferredTerminationBy` we can print them to the user reliably.
+We do that by appending `'` as needed.
 -/
+partial
 def naryVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Name):= do
   lambdaTelescope preDef.value fun xs _ => do
     let xs := xs.extract fixedPrefixSize xs.size
-    let mut ns := #[]
+    let mut ns : Array Name := #[]
     for h : i in [:xs.size] do
       let n ← (xs[i]'h.2).fvarId!.getUserName
-      if n.hasMacroScopes then
-        ns := ns.push (← mkFreshUserName (.mkSimple s!"x{i+1}"))
-      else
-        ns := ns.push n
+      let n := if n.hasMacroScopes then .mkSimple s!"x{i+1}" else n
+      ns := ns.push (← freshen ns n)
     return ns
+  where
+    freshen  (ns : Array Name) (n : Name): MetaM Name := do
+      if !(ns.elem n) && (← resolveGlobalName n).isEmpty then
+        return n
+      else
+        freshen ns (n.appendAfter "'")
+
 
 /-- Internal monad used by `withRecApps` -/
 abbrev M (recFnName : Name) (α β : Type) : Type :=
@@ -207,6 +224,8 @@ def SavedLocalContext.run {α} (slc : SavedLocalContext) (k : MetaM α) :
 /-- A `RecCallWithContext` focuses on a single recursive call in a unary predefinition,
 and runs the given action in the context of that call.  -/
 structure RecCallWithContext where
+  /-- Syntax location of reursive call -/
+  ref : Syntax
   /-- Function index of caller -/
   caller : Nat
   /-- Parameters of caller -/
@@ -218,42 +237,32 @@ structure RecCallWithContext where
   ctxt : SavedLocalContext
 
 /-- Store the current recursive call and its context. -/
-def RecCallWithContext.create (caller : Nat) (params : Array Expr) (callee : Nat) (args : Array Expr) :
-    MetaM RecCallWithContext := do
-  return { caller, params, callee, args, ctxt := (← SavedLocalContext.create) }
+def RecCallWithContext.create (ref : Syntax) (caller : Nat) (params : Array Expr) (callee : Nat)
+    (args : Array Expr) : MetaM RecCallWithContext := do
+  return { ref, caller, params, callee, args, ctxt := (← SavedLocalContext.create) }
 
-/-- Given the packed argument of a (possibly) mutual and (possibly) nary call,
-return the function index that is called and the arguments individually.
 
-We expect precisely the expressions produced by `packMutual`, with manifest
-`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
-rather than using projectinos. -/
-def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) :
-    m (Nat × Array Expr) := do
-  -- count PSum injections to find out which function is doing the call
-  let mut funidx := 0
-  let mut e := e
-  while funidx + 1 < arities.size do
-    if e.isAppOfArity ``PSum.inr 3 then
-      e := e.getArg! 2
-      funidx := funidx + 1
-    else if e.isAppOfArity ``PSum.inl 3 then
-      e := e.getArg! 2
-      break
-    else
-      throwError "Unexpected expression while unpacking mutual argument"
-
-  -- now unpack PSigmas
-  let arity := arities[funidx]!
-  let mut args := #[]
-  while args.size + 1 < arity do
-    if e.isAppOfArity ``PSigma.mk 4 then
-      args := args.push (e.getArg! 2)
-      e := e.getArg! 3
-    else
-      throwError "Unexpected expression while unpacking n-ary argument"
-  args := args.push e
-  return (funidx, args)
+/--
+The elaborator is prone to duplicate terms, including recursive calls, even if the user
+only wrote a single one. This duplication is wasteful if we run the tactics on duplicated
+calls, and confusing in the output of GuessLex. So prune the list of recursive calls,
+and remove those where another call exists that has the same goal and context that is no more
+specific.
+-/
+def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext := Id.run do
+  rcs.filterPairsM fun rci rcj => do
+    if rci.caller == rcj.caller && rci.callee == rcj.callee &&
+      rci.params == rcj.params && rci.args == rcj.args then
+      -- same goals; check contexts.
+        let lci := rci.ctxt.savedLocalContext
+        let lcj := rcj.ctxt.savedLocalContext
+        if lci.isSubPrefixOf lcj then
+          -- rci is better
+          return (true, false)
+        else if lcj.isSubPrefixOf lci then
+          -- rcj is better
+          return (false, true)
+    return (true, true)
 
 /-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive
 call site.
@@ -273,18 +282,21 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat) (ariti
       let arg := args[fixedPrefixSize]!
       let (caller, params) ← unpackArg arities param
       let (callee, args) ← unpackArg arities arg
-      RecCallWithContext.create caller params callee args
+      RecCallWithContext.create (← getRef) caller params callee args
 
 /-- A `GuessLexRel` described how a recursive call affects a measure; whether it
 decreases strictly, non-strictly, is equal, or else.  -/
 inductive GuessLexRel | lt | eq | le | no_idea
 deriving Repr, DecidableEq
 
+instance : ToString GuessLexRel where
+  toString | .lt => "<"
+           | .eq => "="
+           | .le => "≤"
+           | .no_idea => "?"
+
 instance : ToFormat GuessLexRel where
-  format | .lt => "<"
-         | .eq => "="
-         | .le => "≤"
-         | .no_idea => "?"
+  format r := toString r
 
 /-- Given a `GuessLexRel`, produce a binary `Expr` that relates two `Nat` values accordingly. -/
 def GuessLexRel.toNatRel : GuessLexRel → Expr
@@ -370,16 +382,13 @@ def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLe
     rc.cache.modify (·.modify paramIdx (·.set! argIdx res))
     return res
 
-/-- Pretty-print the cache entries -/
-def RecCallCache.pretty (rc : RecCallCache) : IO Format := do
-  let mut r := Format.nil
-  let d ← rc.cache.get
-  for h₁ : paramIdx in [:d.size] do
-    for h₂ : argIdx in [:(d[paramIdx]'h₁.2).size] do
-      if let .some entry := (d[paramIdx]'h₁.2)[argIdx]'h₂.2 then
-        r := r ++
-          f!"(Param {paramIdx}, arg {argIdx}): {entry}" ++ Format.line
-  return r
+
+/-- Print a single cache entry as a string, without forcing it -/
+def RecCallCache.prettyEntry (rcc : RecCallCache) (paramIdx argIdx : Nat) : MetaM String := do
+  let cachedEntries ← rcc.cache.get
+  return match cachedEntries[paramIdx]![argIdx]! with
+  | .some rel => toString rel
+  | .none => "_"
 
 /-- The measures that we order lexicographically can be comparing arguments,
 or numbering the functions -/
@@ -535,21 +544,117 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
   for h : funIdx in [:varNamess.size] do
     let vars := (varNamess[funIdx]'h.2).map mkIdent
     let body ← mkTupleSyntax (← measures.mapM fun
-      | .args varIdxs =>
+      | .args varIdxs => do
           let v := vars.get! (varIdxs[funIdx]!)
-          let sizeOfIdent := mkIdent ``sizeOf
+          let sizeOfIdent := mkIdent (← unresolveNameGlobal ``sizeOf)
           `($sizeOfIdent $v)
       | .func funIdx' => if funIdx' == funIdx then `(1) else `(0)
       )
     let declName := declNames[funIdx]!
 
-    trace[Elab.definition.wf] "Using termination {declName}: {vars} => {body}"
     termByElements := termByElements.push
       { ref := .missing
         declName, vars, body,
         implicit := true
       }
-  return .ext termByElements
+  return termByElements
+
+
+/--
+Given a matrix (row-major) of strings, arranges them in tabular form.
+First column is left-aligned, others right-aligned.
+Single space as column separator.
+-/
+def formatTable : Array (Array String) → String := fun xss => Id.run do
+  let mut colWidths := xss[0]!.map (fun _ => 0)
+  for i in [:xss.size] do
+    for j in [:xss[i]!.size] do
+      if xss[i]![j]!.length > colWidths[j]! then
+        colWidths := colWidths.set! j xss[i]![j]!.length
+  let mut str := ""
+  for i in [:xss.size] do
+    for j in [:xss[i]!.size] do
+      let s := xss[i]![j]!
+      if j > 0 then -- right-align
+        for _ in [:colWidths[j]! - s.length] do
+          str := str ++ " "
+      str := str ++ s
+      if j = 0 then -- left-align
+        for _ in [:colWidths[j]! - s.length] do
+          str := str ++ " "
+      if j + 1 < xss[i]!.size then
+        str := str ++ " "
+    if i + 1 < xss.size then
+      str := str ++ "\n"
+  return str
+
+/-- Concise textual representation of the source location of a recursive call  -/
+def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
+  let fileMap ← getFileMap
+  let .some pos := rcc.ref.getPos? | return ""
+  let position := fileMap.toPosition pos
+  let endPosStr := match rcc.ref.getTailPos? with
+  | some endPos =>
+    let endPosition := fileMap.toPosition endPos
+    if endPosition.line = position.line then
+      s!"-{endPosition.column}"
+    else
+      s!"-{endPosition.line}:{endPosition.column}"
+  | none        => ""
+  return s!"{position.line}:{position.column}{endPosStr}"
+
+
+/-- Explain what we found out about the recursive calls (non-mutual case) -/
+def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do
+  let header := varNames.map (·.eraseMacroScopes.toString)
+  let mut table : Array (Array String) := #[#[""] ++ header]
+  for i in [:rcs.size], rc in rcs do
+    let mut row := #[s!"{i+1}) {← rc.rcc.posString}"]
+    for argIdx in [:varNames.size] do
+      row := row.push (← rc.prettyEntry argIdx argIdx)
+    table := table.push row
+
+  return formatTable table
+
+/-- Explain what we found out about the recursive calls (mutual case) -/
+def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name))
+    (rcs : Array RecCallCache) : MetaM Format := do
+  let mut r := Format.nil
+
+  for rc in rcs do
+    let caller := rc.rcc.caller
+    let callee := rc.rcc.callee
+    r := r ++ f!"Call from {declNames[caller]!} to {declNames[callee]!} " ++
+      f!"at {← rc.rcc.posString}:\n"
+
+    let header := varNamess[caller]!.map (·.eraseMacroScopes.toString)
+    let mut table : Array (Array String) := #[#[""] ++ header]
+    if caller = callee then
+      -- For self-calls, only the diagonal is interesting, so put it into one row
+      let mut row := #[""]
+      for argIdx in [:varNamess[caller]!.size] do
+        row := row.push (← rc.prettyEntry argIdx argIdx)
+      table := table.push row
+    else
+      for argIdx in [:varNamess[callee]!.size] do
+        let mut row := #[]
+        row := row.push varNamess[callee]![argIdx]!.eraseMacroScopes.toString
+        for paramIdx in [:varNamess[caller]!.size] do
+          row := row.push (← rc.prettyEntry paramIdx argIdx)
+        table := table.push row
+    r := r ++ formatTable table ++ "\n"
+
+  return r
+
+def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
+    (rcs : Array RecCallCache) : MetaM Format := do
+  let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
+    "(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
+  if declNames.size = 1 then
+    r := r ++ (← explainNonMutualFailure varNamess[0]! rcs)
+  else
+    r := r ++ (← explainMutualFailure declNames varNamess rcs)
+  return r
 
 end Lean.Elab.WF.GuessLex
 
@@ -566,33 +671,41 @@ terminates. See the module doc string for a high-level overview.
 def guessLex (preDefs : Array PreDefinition)  (unaryPreDef : PreDefinition)
     (fixedPrefixSize : Nat) (decrTactic? : Option Syntax) :
     MetaM TerminationWF := do
-  try
-    let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
-    let arities := varNamess.map (·.size)
-    trace[Elab.definition.wf] "varNames is: {varNamess}"
+  let varNamess ← preDefs.mapM (naryVarNames fixedPrefixSize ·)
+  let arities := varNamess.map (·.size)
+  trace[Elab.definition.wf] "varNames is: {varNamess}"
 
-    let forbiddenArgs ← preDefs.mapM fun preDef =>
-      getForbiddenByTrivialSizeOf fixedPrefixSize preDef
+  let forbiddenArgs ← preDefs.mapM fun preDef =>
+    getForbiddenByTrivialSizeOf fixedPrefixSize preDef
 
-    -- The list of measures, including the measures that order functions.
-    -- The function ordering measures come last
-    let measures ← generateMeasures forbiddenArgs arities
+  -- The list of measures, including the measures that order functions.
+  -- The function ordering measures come last
+  let measures ← generateMeasures forbiddenArgs arities
 
-    -- If there is only one plausible measure, use that
-    if let #[solution] := measures then
-      return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
+  -- If there is only one plausible measure, use that
+  if let #[solution] := measures then
+    return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution]
 
-    -- Collect all recursive calls and extract their context
-    let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
-    let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·)
-    let callMatrix := rcs.map (inspectCall ·)
+  -- Collect all recursive calls and extract their context
+  let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities
+  let recCalls := filterSubsumed recCalls
+  let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·)
+  let callMatrix := rcs.map (inspectCall ·)
 
-    match ← liftMetaM <| solve measures callMatrix with
-    | .some solution => do
-      let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
-      return wf
-    | .none => throwError "Cannot find a decreasing lexicographic order"
-  catch _ =>
-    -- Hide all errors from guessing lexicographic orderings, as before
-    -- Future work: explain the failure to the user, like  Isabelle does
-    throwError "failed to prove termination, use `termination_by` to specify a well-founded relation"
+  match ← liftMetaM <| solve measures callMatrix with
+  | .some solution => do
+    let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution
+
+    let wfStx ← withoutModifyingState do
+      preDefs.forM (addAsAxiom ·)
+      wf.unexpand
+
+    if showInferredTerminationBy.get (← getOptions) then
+      logInfo m!"Inferred termination argument:{wfStx}"
+
+    return wf
+  | .none =>
+    let explanation ← explainFailure (preDefs.map (·.declName)) varNamess rcs
+    Lean.throwError <| "Could not find a decreasing measure.\n" ++
+      explanation ++ "\n" ++
+      "Please use `termination_by` to specify a decreasing measure."

src/Lean/Elab/PreDefinition/WF/PackDomain.lean

@@ -40,6 +40,19 @@ where
     else
       return args[i]!
 
+/-- Unpacks a unary packed argument created with `mkUnaryArg`. -/
+def unpackUnaryArg {m} [Monad m] [MonadError m] (arity : Nat) (e : Expr) : m (Array Expr) := do
+  let mut e := e
+  let mut args := #[]
+  while args.size + 1 < arity do
+    if e.isAppOfArity ``PSigma.mk 4 then
+      args := args.push (e.getArg! 2)
+      e := e.getArg! 3
+    else
+      throwError "Unexpected expression while unpacking n-ary argument"
+  args := args.push e
+  return args
+
 private partial def mkPSigmaCasesOn (y : Expr) (codomain : Expr) (xs : Array Expr) (value : Expr) : MetaM Expr := do
   let mvar ← mkFreshExprSyntheticOpaqueMVar codomain
   let rec go (mvarId : MVarId) (y : FVarId) (ys : Array Expr) : MetaM Unit := do

src/Lean/Elab/PreDefinition/WF/PackMutual.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Cases
 import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.WF.PackDomain
 
 namespace Lean.Elab.WF
 open Meta
@@ -110,8 +111,60 @@ def withAppN (n : Nat) (e : Expr) (k : Array Expr → MetaM Expr) : MetaM Expr :
       mkLambdaFVars xs e'
 
 /--
-  Auxiliary function for replacing nested `preDefs` recursive calls in `e` with the new function `newFn`.
-  See: `packMutual`
+If `arg` is the argument to the `fidx`th of the `numFuncs` in the recursive group,
+then `mkMutualArg` packs that argument in `PSum.inl` and `PSum.inr` constructors
+to create the mutual-packed argument of type `domain`.
+-/
+partial def mkMutualArg (numFuncs : Nat) (domain : Expr) (fidx : Nat) (arg : Expr) : MetaM Expr := do
+  let rec go (i : Nat) (type : Expr) : MetaM Expr := do
+    if i == numFuncs - 1 then
+      return arg
+    else
+      (← whnfD type).withApp fun f args => do
+        assert! args.size == 2
+        if i == fidx then
+          return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! arg
+        else
+          let r ← go (i+1) args[1]!
+          return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r
+  go 0 domain
+
+/--
+Unpacks a mutually packed argument, returning the argument and function index.
+Inverse of `mkMutualArg`.  Cf. `unpackUnaryArg` and `unpackArg`, which does both
+-/
+def unpackMutualArg {m} [Monad m] [MonadError m] (numFuncs : Nat) (e : Expr) : m (Nat × Expr) := do
+  let mut funidx := 0
+  let mut e := e
+  while funidx + 1 < numFuncs do
+    if e.isAppOfArity ``PSum.inr 3 then
+      e := e.getArg! 2
+      funidx := funidx + 1
+    else if e.isAppOfArity ``PSum.inl 3 then
+      e := e.getArg! 2
+      break
+    else
+      throwError "Unexpected expression while unpacking mutual argument"
+  return (funidx, e)
+
+/--
+Given the packed argument of a (possibly) mutual and (possibly) nary call,
+return the function index that is called and the arguments individually.
+
+We expect precisely the expressions produced by `packMutual`, with manifest
+`PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
+rather than using projectinos.
+-/
+def unpackArg {m} [Monad m] [MonadError m] (arities : Array Nat) (e : Expr) :
+    m (Nat × Array Expr) := do
+  let (funidx, e) ← unpackMutualArg arities.size e
+  let args ← unpackUnaryArg arities[funidx]! e
+  return (funidx, args)
+
+
+/--
+Auxiliary function for replacing nested `preDefs` recursive calls in `e` with the new function `newFn`.
+See: `packMutual`
 -/
 private partial def post (fixedPrefix : Nat) (preDefs : Array PreDefinition) (domain : Expr) (newFn : Name) (e : Expr) : MetaM TransformStep := do
   let f := e.getAppFn
@@ -122,19 +175,9 @@ private partial def post (fixedPrefix : Nat) (preDefs : Array PreDefinition) (do
   if let some fidx := preDefs.findIdx? (·.declName == declName) then
     let e' ← withAppN (fixedPrefix + 1) e fun args => do
       let fixedArgs := args[:fixedPrefix]
-      let arg  := args[fixedPrefix]!
-      let rec mkNewArg (i : Nat) (type : Expr) : MetaM Expr := do
-        if i == preDefs.size - 1 then
-          return arg
-        else
-          (← whnfD type).withApp fun f args => do
-            assert! args.size == 2
-            if i == fidx then
-              return mkApp3 (mkConst ``PSum.inl f.constLevels!) args[0]! args[1]! arg
-            else
-              let r ← mkNewArg (i+1) args[1]!
-              return mkApp3 (mkConst ``PSum.inr f.constLevels!) args[0]! args[1]! r
-      return mkApp (mkAppN (mkConst newFn us) fixedArgs) (← mkNewArg 0 domain)
+      let arg := args[fixedPrefix]!
+      let packedArg ← mkMutualArg preDefs.size domain fidx arg
+      return mkApp (mkAppN (mkConst newFn us) fixedArgs) packedArg
     return TransformStep.done e'
   return TransformStep.done e
 

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -34,10 +34,10 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
     let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
     if element.vars.size > varNames.size then
       throwErrorAt element.vars[varNames.size]! "too many variable names"
-    for i in [:element.vars.size] do
-      let varStx := element.vars[i]!
-      if varStx.isIdent then
-        varNames := varNames.set! (varNames.size - element.vars.size + i) varStx.getId
+    for h : i in [:element.vars.size] do
+      let varStx := element.vars[i]'h.2
+      if let `($ident:ident) := varStx then
+        varNames := varNames.set! (varNames.size - element.vars.size + i) ident.getId
     return varNames
   let mut mvarId := mvarId
   for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
@@ -60,25 +60,18 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
   let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
   trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
   withDeclName unaryPreDefName do
-  match wf with
-  | TerminationWF.core wfStx =>
-      let wfRel ← instantiateMVars (← withSynthesize <| elabTermEnsuringType wfStx expectedType)
-      let pendingMVarIds ← getMVars wfRel
-      discard <| logUnassignedUsingErrorInfos pendingMVarIds
-      k wfRel
-  | TerminationWF.ext elements =>
-    withRef (getRefFromElems elements) do
-      let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
-      let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
-      let (d, fMVarId) ← fMVarId.intro1
-      let subgoals ← unpackMutual preDefs fMVarId d
-      for (d, mvarId) in subgoals, element in elements, preDef in preDefs do
-        let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
-        mvarId.withContext do
-          let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
-          mvarId.assign value
-      let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
-      wfRelMVarId.assign wfRelVal
-      k (← instantiateMVars (mkMVar mainMVarId))
+  withRef (getRefFromElems wf) do
+    let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
+    let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
+    let (d, fMVarId) ← fMVarId.intro1
+    let subgoals ← unpackMutual preDefs fMVarId d
+    for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
+      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
+      mvarId.withContext do
+        let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
+        mvarId.assign value
+    let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
+    wfRelMVarId.assign wfRelVal
+    k (← instantiateMVars (mkMVar mainMVarId))
 
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/TerminationHint.lean

@@ -5,130 +5,160 @@ Authors: Leonardo de Moura
 -/
 import Lean.Parser.Command
 
+set_option autoImplicit false
+
 namespace Lean.Elab.WF
 
-/-! # Support for `decreasing_by` and `termination_by'` notations -/
+/-! # Support for `decreasing_by` -/
 
-structure TerminationHintValue where
+structure DecreasingByTactic where
   ref   : Syntax
-  value : Syntax
+  value : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
   deriving Inhabited
 
-inductive TerminationHint where
+inductive DecreasingBy where
   | none
-  | one (val : TerminationHintValue)
-  | many (map : NameMap TerminationHintValue)
+  | one (val : DecreasingByTactic)
+  | many (map : NameMap DecreasingByTactic)
   deriving Inhabited
 
-def expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationHint := do
-  if let some terminationHint := terminationHint? then
-    let ref := terminationHint
-    let terminationHint := terminationHint[1]
-    if terminationHint.getKind == ``Parser.Command.terminationHint1 then
-      return TerminationHint.one { ref, value := terminationHint[0] }
-    else if terminationHint.getKind == ``Parser.Command.terminationHintMany then
-      let m ← terminationHint[0].getArgs.foldlM (init := {}) fun m arg =>
-        let declName? := cliques.findSome? fun clique => clique.findSome? fun declName =>
-          if arg[0].getId.isSuffixOf declName then some declName else none
-        match declName? with
-        | none => Macro.throwErrorAt arg[0] s!"function '{arg[0].getId}' not found in current declaration"
-        | some declName => return m.insert declName { ref := arg, value := arg[2] }
-      for clique in cliques do
-        let mut found? := Option.none
-        for declName in clique do
-          if let some { ref, .. } := m.find? declName then
-            if let some found := found? then
-              Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique"
-            found? := some declName
-      return TerminationHint.many m
-    else
-      Macro.throwUnsupported
-  else
-    return TerminationHint.none
+open Parser.Command in
+/--
+This function takes a user-specified `decreasing_by` clause (as `Sytnax`).
+If it is a `decreasingByMany` (a set of clauses guarded by the function name) then
+* checks that all mentioned names exist in the current declaration
+* check that at most one function from each clique is mentioned
+and sort the entries by function name.
+-/
+def expandDecreasingBy? (decreasingBy? : Option Syntax) (cliques : Array (Array Name)) : MacroM DecreasingBy := do
+  let some decreasingBy := decreasingBy? | return DecreasingBy.none
+  let ref := decreasingBy
+  match decreasingBy with
+  | `(decreasingBy|decreasing_by $hint1:tacticSeq) =>
+    return DecreasingBy.one { ref, value := hint1 }
+  | `(decreasingBy|decreasing_by $hints:decreasingByMany) => do
+    let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg => do
+      let arg : TSyntax `decreasingByElement := ⟨arg⟩ -- cannot use syntax pattern match with lookahead
+      let `(decreasingByElement| $declId:ident => $tac:tacticSeq) := arg | Macro.throwUnsupported
+      let declName? := cliques.findSome? fun clique => clique.findSome? fun declName =>
+        if declId.getId.isSuffixOf declName then some declName else none
+      match declName? with
+      | none => Macro.throwErrorAt declId s!"function '{declId.getId}' not found in current declaration"
+      | some declName => return m.insert declName { ref := arg, value := tac }
+    for clique in cliques do
+      let mut found? := Option.none
+      for declName in clique do
+        if let some { ref, .. } := m.find? declName then
+          if let some found := found? then
+            Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique"
+          found? := some declName
+    return DecreasingBy.many m
+  | _ => Macro.throwUnsupported
 
-def TerminationHint.markAsUsed (t : TerminationHint) (clique : Array Name) : TerminationHint :=
+def DecreasingBy.markAsUsed (t : DecreasingBy) (clique : Array Name) : DecreasingBy :=
   match t with
-  | TerminationHint.none   => TerminationHint.none
-  | TerminationHint.one .. => TerminationHint.none
-  | TerminationHint.many m => Id.run do
+  | DecreasingBy.none   => DecreasingBy.none
+  | DecreasingBy.one .. => DecreasingBy.none
+  | DecreasingBy.many m => Id.run do
     for declName in clique do
       if m.contains declName then
         let m := m.erase declName
         if m.isEmpty then
-          return TerminationHint.none
+          return DecreasingBy.none
         else
-          return TerminationHint.many m
+          return DecreasingBy.many m
     return t
 
-def TerminationHint.find? (t : TerminationHint) (clique : Array Name) : Option TerminationHintValue :=
+def DecreasingBy.find? (t : DecreasingBy) (clique : Array Name) : Option DecreasingByTactic :=
   match t with
-  | TerminationHint.none   => Option.none
-  | TerminationHint.one v  => some v
-  | TerminationHint.many m => clique.findSome? m.find?
+  | DecreasingBy.none   => Option.none
+  | DecreasingBy.one v  => some v
+  | DecreasingBy.many m => clique.findSome? m.find?
 
-def TerminationHint.ensureAllUsed (t : TerminationHint) : MacroM Unit := do
+def DecreasingBy.ensureAllUsed (t : DecreasingBy) : MacroM Unit := do
   match t with
-  | TerminationHint.one v   => Macro.throwErrorAt v.ref "unused termination hint element"
-  | TerminationHint.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
+  | DecreasingBy.one v   => Macro.throwErrorAt v.ref "unused termination hint element"
+  | DecreasingBy.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
   | _ => pure ()
 
 /-! # Support for `termination_by` notation -/
 
+/-- A single `termination_by` clause -/
 structure TerminationByElement where
   ref       : Syntax
   declName  : Name
-  vars      : Array Syntax
-  body      : Syntax
+  vars      : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
+  body      : Term
   implicit  : Bool
   deriving Inhabited
 
+/-- `termination_by` clauses, grouped by clique -/
 structure TerminationByClique where
   elements : Array TerminationByElement
   used     : Bool := false
 
-inductive TerminationBy where
-  | core (hint : TerminationHint)
-  | ext  (cliques : Array TerminationByClique)
+/--
+A `termination_by` hint, as specified by the user
+-/
+structure TerminationBy where
+  cliques : Array TerminationByClique
   deriving Inhabited
 
-inductive TerminationWF where
-  | core (stx : Syntax)
-  | ext  (clique : Array TerminationByElement)
+/--
+A `termination_by` hint, as applicable to a single clique
+-/
+abbrev TerminationWF := Array TerminationByElement
 
-/-
+open Parser.Command in
+/--
+Expands the syntax for a `termination_by` clause, checking that
+* each function is mentioned once
+* each function mentioned actually occurs in the current declaration
+* if anything is specified, then all functions have a clause
+* the else-case (`_`) occurs only once, and only when needed
+
+NB:
 ```
 def terminationByElement   := leading_parser ppLine >> (ident <|> hole) >> many (ident <|> hole) >> " => " >> termParser >> optional ";"
 def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
 ```
 -/
-private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy := do
-  let elementStxs := hint[1].getArgs
+def expandTerminationBy? (hint? : Option Syntax) (cliques : Array (Array Name)) :
+    MacroM TerminationBy := do
+  let some hint := hint?  | return { cliques := #[] }
+  let `(terminationBy|termination_by $elementStxs*) := hint | Macro.throwUnsupported
   let mut alreadyFound : NameSet := {}
   let mut elseElemStx? := none
   for elementStx in elementStxs do
-    let declStx := elementStx[0]
-    if declStx.isIdent then
-      let declSuffix := declStx.getId
+    match elementStx with
+    | `(terminationByElement|$ident:ident $_* => $_) =>
+      let declSuffix := ident.getId
       if alreadyFound.contains declSuffix then
         withRef elementStx <| Macro.throwError s!"invalid `termination_by` syntax, `{declSuffix}` case has already been provided"
       alreadyFound := alreadyFound.insert declSuffix
       if cliques.all fun clique => clique.all fun declName => !declSuffix.isSuffixOf declName then
         withRef elementStx <| Macro.throwError s!"function '{declSuffix}' not found in current declaration"
-    else if elseElemStx?.isSome then
-      withRef elementStx <| Macro.throwError "invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified"
-    else
-      elseElemStx? := some elementStx
-  let toElement (declName : Name) (elementStx : Syntax) : TerminationByElement :=
-    let vars     := elementStx[1].getArgs
-    let implicit := !elementStx[0].isIdent
-    let body     := elementStx[3]
+    | `(terminationByElement|_ $_vars* => $_term) =>
+      if elseElemStx?.isSome then
+        withRef elementStx <| Macro.throwError "invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified"
+      else
+        elseElemStx? := some elementStx
+    | _ => Macro.throwUnsupported
+  let toElement (declName : Name) (elementStx : TSyntax ``terminationByElement) : TerminationByElement :=
+    match elementStx with
+    | `(terminationByElement|$ioh $vars* => $body:term) =>
+    let implicit := !ioh.raw.isIdent
     { ref := elementStx, declName, vars, implicit, body }
+    | _ => unreachable!
+  let elementAppliesTo (declName : Name) : TSyntax ``terminationByElement → Bool
+    | `(terminationByElement|$ident:ident $_* => $_) => ident.getId.isSuffixOf declName
+    | _ => false
   let mut result := #[]
   let mut usedElse := false
   for clique in cliques do
     let mut elements := #[]
     for declName in clique do
-      if let some elementStx := elementStxs.find? fun elementStx => elementStx[0].isIdent && elementStx[0].getId.isSuffixOf declName then
+      if let some elementStx := elementStxs.find? (elementAppliesTo declName) then
         elements := elements.push (toElement declName elementStx)
       else if let some elseElemStx := elseElemStx? then
         elements := elements.push (toElement declName elseElemStx)
@@ -139,37 +169,28 @@ private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array N
       result := result.push { elements }
   if !usedElse && elseElemStx?.isSome then
     withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
-  return TerminationBy.ext result
+  return ⟨result⟩
 
-def expandTerminationBy (hint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy :=
-  if let some hint := hint? then
-    if hint.isOfKind ``Parser.Command.terminationByCore then
-      return TerminationBy.core (← expandTerminationHint hint? cliques)
-    else if hint.isOfKind ``Parser.Command.terminationBy then
-      expandTerminationByNonCore hint cliques
-    else
-      Macro.throwUnsupported
-  else
-      return TerminationBy.core TerminationHint.none
+open Parser.Command in
+def TerminationWF.unexpand (elements : TerminationWF) : MetaM Syntax := do
+  let elementStxs ← elements.mapM fun element => do
+    let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
+    `(terminationByElement|$fn $element.vars* => $element.body)
+  `(terminationBy|termination_by $elementStxs*)
 
 def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
-  match t with
-  | core hint   => core (hint.markAsUsed cliqueNames)
-  | ext cliques => ext <| cliques.map fun clique =>
+  .mk <| t.cliques.map fun clique =>
     if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
       { clique with used := true }
     else
       clique
 
 def TerminationBy.find? (t : TerminationBy) (cliqueNames : Array Name) : Option TerminationWF :=
-  match t with
-  | core hint => hint.find? cliqueNames |>.map fun v => TerminationWF.core v.value
-  | ext cliques =>
-    cliques.findSome? fun clique =>
-      if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
-        some <| TerminationWF.ext clique.elements
-      else
-        none
+  t.cliques.findSome? fun clique =>
+    if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
+      some <| clique.elements
+    else
+      none
 
 def TerminationByClique.allImplicit (c : TerminationByClique) : Bool :=
   c.elements.all fun elem => elem.implicit
@@ -177,19 +198,16 @@ def TerminationByClique.allImplicit (c : TerminationByClique) : Bool :=
 def TerminationByClique.getExplicitElement? (c : TerminationByClique) : Option TerminationByElement :=
   c.elements.find? (!·.implicit)
 
-def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit :=
-  match t with
-  | core hint => hint.ensureAllUsed
-  | ext cliques => do
-    let hasUsedAllImplicit := cliques.any fun c => c.allImplicit && c.used
-    let mut reportedAllImplicit := true
-    for clique in cliques do
-      unless clique.used do
-        if let some explicitElem := clique.getExplicitElement? then
-          Macro.throwErrorAt explicitElem.ref "unused termination hint element"
-        else if !hasUsedAllImplicit then
-          unless reportedAllImplicit do
-            reportedAllImplicit := true
-            Macro.throwErrorAt clique.elements[0]!.ref "unused termination hint element"
+def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit := do
+  let hasUsedAllImplicit := t.cliques.any fun c => c.allImplicit && c.used
+  let mut reportedAllImplicit := true
+  for clique in t.cliques do
+    unless clique.used do
+      if let some explicitElem := clique.getExplicitElement? then
+        Macro.throwErrorAt explicitElem.ref "unused termination hint element"
+      else if !hasUsedAllImplicit then
+        unless reportedAllImplicit do
+          reportedAllImplicit := true
+          Macro.throwErrorAt clique.elements[0]!.ref "unused termination hint element"
 
 end Lean.Elab.WF

src/Lean/Elab/Print.lean

@@ -83,7 +83,7 @@ private def printId (id : Syntax) : CommandElabM Unit := do
 
 @[builtin_command_elab «print»] def elabPrint : CommandElab
   | `(#print%$tk $id:ident) => withRef tk <| printId id
-  | `(#print%$tk $s:str) => logInfoAt tk s.getString
+  | `(#print%$tk $s:str)    => logInfoAt tk s.getString
   | _                       => throwError "invalid #print command"
 
 namespace CollectAxioms

src/Lean/Elab/Quotation/Precheck.lean

@@ -141,4 +141,36 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
   runPrecheck singleQuot.getQuotContent
   adaptExpander (fun _ => pure singleQuot) stx expectedType?
 
+section ExpressionTree
+
+@[builtin_quot_precheck Lean.Parser.Term.binrel] def precheckBinrel : Precheck
+  | `(binrel% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.binrel_no_prop] def precheckBinrelNoProp : Precheck
+  | `(binrel_no_prop% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.binop] def precheckBinop : Precheck
+  | `(binop% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.binop_lazy] def precheckBinopLazy : Precheck
+  | `(binop_lazy% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.leftact] def precheckLeftact : Precheck
+  | `(leftact% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.rightact] def precheckRightact : Precheck
+  | `(rightact% $f $a $b) => do precheck f; precheck a; precheck b
+  | _ => throwUnsupportedSyntax
+
+@[builtin_quot_precheck Lean.Parser.Term.unop] def precheckUnop : Precheck
+  | `(unop% $f $a) => do precheck f; precheck a
+  | _ => throwUnsupportedSyntax
+
+end ExpressionTree
+
 end Lean.Elab.Term.Quotation

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -72,7 +72,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
     throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}"
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
-   replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))
+  replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))
 
 private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
   TacticM Unit := do
@@ -94,23 +94,23 @@ private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i
 @[builtin_tactic Lean.Parser.Tactic.Conv.skip] def evalSkip : Tactic := fun _ => pure ()
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.lhs] def evalLhs : Tactic := fun _ => do
-   let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
-   selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2)
+  let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
+  selectIdx "lhs" mvarIds ((mvarIds.length : Int) - 2)
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.rhs] def evalRhs : Tactic := fun _ => do
-   let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
-   selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1)
+  let mvarIds ← congr (← getMainGoal) (nameSubgoals := false)
+  selectIdx "rhs" mvarIds ((mvarIds.length : Int) - 1)
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.arg] def evalArg : Tactic := fun stx => do
-   match stx with
-   | `(conv| arg $[@%$tk?]? $i:num) =>
-      let i := i.getNat
-      if i == 0 then
-        throwError "invalid 'arg' conv tactic, index must be greater than 0"
-      let i := i - 1
-      let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome) (nameSubgoals := false)
-      selectIdx "arg" mvarIds i
-   | _ => throwUnsupportedSyntax
+  match stx with
+  | `(conv| arg $[@%$tk?]? $i:num) =>
+    let i := i.getNat
+    if i == 0 then
+      throwError "invalid 'arg' conv tactic, index must be greater than 0"
+    let i := i - 1
+    let mvarIds ← congr (← getMainGoal) (addImplicitArgs := tk?.isSome) (nameSubgoals := false)
+    selectIdx "arg" mvarIds i
+  | _ => throwUnsupportedSyntax
 
 def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId) := do
   match lhs with
@@ -141,35 +141,35 @@ def extLetBodyCongr? (mvarId : MVarId) (lhs rhs : Expr) : MetaM (Option MVarId)
   | _ => return none
 
 private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :=
-   mvarId.withContext do
-     let (lhs, rhs) ← getLhsRhsCore mvarId
-     let lhs := (← instantiateMVars lhs).cleanupAnnotations
-     if let .forallE n d b bi := lhs then
-       let u ← getLevel d
-       let p : Expr := .lam n d b bi
-       let userName ← if let some userName := userName? then pure userName else mkFreshBinderNameForTactic n
-       let (q, h, mvarNew) ← withLocalDecl userName bi d fun a => do
-         let pa := b.instantiate1 a
-         let (qa, mvarNew) ← mkConvGoalFor pa
-         let q ← mkLambdaFVars #[a] qa
-         let h ← mkLambdaFVars #[a] mvarNew
-         let rhs' ← mkForallFVars #[a] qa
-         unless (← isDefEqGuarded rhs rhs') do
-           throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
-         return (q, h, mvarNew)
-       let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
-       mvarId.assign proof
-       return mvarNew.mvarId!
-     else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then
-       return mvarId
-     else
-       let lhsType ← whnfD (← inferType lhs)
-       unless lhsType.isForall do
-         throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
-       let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result"
-       let userNames := if let some userName := userName? then [userName] else []
-       let (_, mvarId) ← mvarId.introN 1 userNames
-       markAsConvGoal mvarId
+  mvarId.withContext do
+    let (lhs, rhs) ← getLhsRhsCore mvarId
+    let lhs := (← instantiateMVars lhs).cleanupAnnotations
+    if let .forallE n d b bi := lhs then
+      let u ← getLevel d
+      let p : Expr := .lam n d b bi
+      let userName ← if let some userName := userName? then pure userName else mkFreshBinderNameForTactic n
+      let (q, h, mvarNew) ← withLocalDecl userName bi d fun a => do
+        let pa := b.instantiate1 a
+        let (qa, mvarNew) ← mkConvGoalFor pa
+        let q ← mkLambdaFVars #[a] qa
+        let h ← mkLambdaFVars #[a] mvarNew
+        let rhs' ← mkForallFVars #[a] qa
+        unless (← isDefEqGuarded rhs rhs') do
+          throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
+        return (q, h, mvarNew)
+      let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
+      mvarId.assign proof
+      return mvarNew.mvarId!
+    else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then
+      return mvarId
+    else
+      let lhsType ← whnfD (← inferType lhs)
+      unless lhsType.isForall do
+        throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
+      let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result"
+      let userNames := if let some userName := userName? then [userName] else []
+      let (_, mvarId) ← mvarId.introN 1 userNames
+      markAsConvGoal mvarId
 
 private def ext (userName? : Option Name) : TacticM Unit := do
   replaceMainGoal [← extCore (← getMainGoal) userName?]

src/Lean/Elab/Tactic/Induction.lean

@@ -263,7 +263,8 @@ def reorderAlts (alts : Array Alt) (altsSyntax : Array Syntax) : Array Alt := Id
 
 def evalAlts (elimInfo : ElimInfo) (alts : Array Alt) (optPreTac : Syntax) (altsSyntax : Array Syntax)
     (initialInfo : Info)
-    (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) : TacticM Unit := do
+    (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[])
+    (toTag : Array (Ident × FVarId) := #[]) : TacticM Unit := do
   let hasAlts := altsSyntax.size > 0
   if hasAlts then
     -- default to initial state outside of alts
@@ -301,10 +302,13 @@ where
         let mut (_, altMVarId) ← altMVarId.introN numFields
         match (← Cases.unifyEqs? numEqs altMVarId {}) with
         | none   => pure () -- alternative is not reachable
-        | some (altMVarId', _) =>
+        | some (altMVarId', subst) =>
           (_, altMVarId) ← altMVarId'.introNP numGeneralized
           for fvarId in toClear do
             altMVarId ← altMVarId.tryClear fvarId
+          altMVarId.withContext do
+            for (stx, fvar) in toTag do
+              Term.addLocalVarInfo stx (subst.get fvar)
           let altMVarIds ← applyPreTac altMVarId
           if !hasAlts then
             -- User did not provide alternatives using `|`
@@ -323,7 +327,7 @@ where
           let mut (fvarIds, altMVarId) ← altMVarId.introN numFields (altVars.toList.map getNameOfIdent') (useNamesForExplicitOnly := !altHasExplicitModifier altStx)
           -- Delay adding the infos for the pattern LHS because we want them to nest
           -- inside tacticInfo for the current alternative (in `evalAlt`)
-          let addInfo := do
+          let addInfo : TermElabM Unit := do
             if (← getInfoState).enabled then
               if let some declName := declName? then
                 addConstInfo (getAltNameStx altStx) declName
@@ -336,10 +340,13 @@ where
               throwError "alternative '{altName}' is not needed"
           match (← Cases.unifyEqs? numEqs altMVarId {}) with
           | none => unusedAlt
-          | some (altMVarId', _) =>
+          | some (altMVarId', subst) =>
             (_, altMVarId) ← altMVarId'.introNP numGeneralized
             for fvarId in toClear do
               altMVarId ← altMVarId.tryClear fvarId
+            altMVarId.withContext do
+              for (stx, fvar) in toTag do
+                Term.addLocalVarInfo stx (subst.get fvar)
             let altMVarIds ← applyPreTac altMVarId
             if altMVarIds.isEmpty then
               unusedAlt
@@ -565,16 +572,23 @@ where
       if foundFVars.contains target.fvarId! then
         throwError "target (or one of its indices) occurs more than once{indentExpr target}"
 
-def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
+def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr × Array (Ident × FVarId)) :=
   withMainContext do
-    let args ← targets.mapM fun target => do
-      let hName? := if target[0].isNone then none else some target[0][0].getId
+    let mut hIdents := #[]
+    let mut args := #[]
+    for target in targets do
+      let hName? ← if target[0].isNone then
+        pure none
+      else
+        hIdents := hIdents.push ⟨target[0][0]⟩
+        pure (some target[0][0].getId)
       let expr ← elabTerm target[1] none
-      return { expr, hName? : GeneralizeArg }
+      args := args.push { expr, hName? : GeneralizeArg }
     if (← withMainContext <| args.anyM fun arg => shouldGeneralizeTarget arg.expr <||> pure arg.hName?.isSome) then
       liftMetaTacticAux fun mvarId => do
         let argsToGeneralize ← args.filterM fun arg => shouldGeneralizeTarget arg.expr <||> pure arg.hName?.isSome
         let (fvarIdsNew, mvarId) ← mvarId.generalize argsToGeneralize
+        -- note: fvarIdsNew contains the `x` variables from `args` followed by all the `h` variables
         let mut result := #[]
         let mut j := 0
         for arg in args do
@@ -583,16 +597,18 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
             j := j+1
           else
             result := result.push arg.expr
-        return (result, [mvarId])
+        -- note: `fvarIdsNew[j:]` contains all the `h` variables
+        assert! hIdents.size + j == fvarIdsNew.size
+        return ((result, hIdents.zip fvarIdsNew[j:]), [mvarId])
     else
-      return args.map (·.expr)
+      return (args.map (·.expr), #[])
 
 @[builtin_tactic Lean.Parser.Tactic.cases] def evalCases : Tactic := fun stx =>
   match expandCases? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
     -- leading_parser nonReservedSymbol "cases " >> sepBy1 (group majorPremise) ", " >> usingRec >> optInductionAlts
-    let targets ← elabCasesTargets stx[1].getSepArgs
+    let (targets, toTag) ← elabCasesTargets stx[1].getSepArgs
     let optInductionAlts := stx[3]
     let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
     let alts :=  getAltsOfOptInductionAlts optInductionAlts
@@ -613,7 +629,8 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
       mvarId.withContext do
         ElimApp.setMotiveArg mvarId elimArgs[elimInfo.motivePos]!.mvarId! targetsNew
         mvarId.assign result.elimApp
-        ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo (numEqs := targets.size) (toClear := targetsNew)
+        ElimApp.evalAlts elimInfo result.alts optPreTac alts initInfo
+          (numEqs := targets.size) (toClear := targetsNew) (toTag := toTag)
 
 builtin_initialize
   registerTraceClass `Elab.cases

src/Lean/Elab/Tactic/Location.lean

@@ -41,13 +41,11 @@ open Meta
 
 /--
 Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`.
-
 * If `loc` is a list of locations, runs at each specified hypothesis (and finally the goal if `⊢` is included),
   and fails if any of the tactic applications fail.
 * If `loc` is `*`, runs at the target first and then the hypotheses in reverse order.
+  If `atTarget` closes the main goal, `withLocation` does not run `atLocal`.
   If all tactic applications fail, `withLocation` with call `failed` with the main goal mvar.
-  If the tactic application closes the main goal, `withLocation` will then fail with `no goals to be solved`
-  upon reaching the first hypothesis.
 -/
 def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit) (failed : MVarId → TacticM Unit) : TacticM Unit := do
   match loc with
@@ -59,7 +57,8 @@ def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget
       withMainContext atTarget
   | Location.wildcard =>
     let worked ← tryTactic <| withMainContext <| atTarget
-    withMainContext do
+    let g ← try getMainGoal catch _ => return () -- atTarget closed the goal
+    g.withContext do
       let mut worked := worked
       -- We must traverse backwards because the given `atLocal` may use the revert/intro idiom
       for fvarId in (← getLCtx).getFVarIds.reverse do

src/Lean/Elab/Tactic/Simp.lean

@@ -264,7 +264,14 @@ register_builtin_option tactic.simp.trace : Bool := {
   descr    := "When tracing is enabled, calls to `simp` or `dsimp` will print an equivalent `simp only` call."
 }
 
-def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
+/--
+If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
+`usedSimps` is the set of simp lemmas used by this invocation, then `mkSimpOnly`
+creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
+invocation.
+-/
+def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
+  let isSimpAll := stx.isOfKind ``Parser.Tactic.simpAll
   let mut stx := stx
   if stx[3].isNone then
     stx := stx.setArg 3 (mkNullNode #[mkAtom "only"])
@@ -281,6 +288,12 @@ def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
         else
           (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident)))
     | .fvar fvarId => -- local hypotheses in the context
+      -- `simp_all` always uses all propositional hypotheses (and it can't use
+      -- any others). So `simp_all only [h]`, where `h` is a hypothesis, would
+      -- be redundant. It would also be confusing since it suggests that only
+      -- `h` is used.
+      if isSimpAll then
+        continue
       if let some ldecl := lctx.find? fvarId then
         localsOrStar := localsOrStar.bind fun locals =>
           if !ldecl.userName.isInaccessibleUserName && !ldecl.userName.hasMacroScopes &&
@@ -299,8 +312,10 @@ def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
   else
     args := args.push (← `(Parser.Tactic.simpStar| *))
   let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
-  stx := stx.setArg 4 (mkNullNode argsStx)
-  logInfoAt stx[0] m!"Try this: {stx}"
+  return stx.setArg 4 (mkNullNode argsStx)
+
+def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
+  logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"
 
 /--
 `simpLocation ctx discharge? varIdToLemmaId loc`

src/Lean/Expr.lean

@@ -947,6 +947,37 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
   let nargs := e.getAppNumArgs
   withAppAux k e (mkArray nargs dummy) (nargs-1)
 
+/--
+Given `f a_1 ... a_n`, returns `#[a_1, ..., a_n]`.
+Note that `f` may be an application.
+The resulting array has size `n` even if `f.getAppNumArgs < n`.
+-/
+@[inline] def getAppArgsN (e : Expr) (n : Nat) : Array Expr :=
+  let dummy := mkSort levelZero
+  loop n e (mkArray n dummy)
+where
+  loop : Nat → Expr → Array Expr → Array Expr
+    | 0,   _,        as => as
+    | i+1, .app f a, as => loop i f (as.set! i a)
+    | _,   _,        _  => panic! "too few arguments at"
+
+/--
+Given `e` of the form `f a_1 ... a_n`, return `f`.
+If `n` is greater than the number of arguments, then return `e.getAppFn`.
+-/
+def stripArgsN (e : Expr) (n : Nat) : Expr :=
+  match n, e with
+  | 0,   _        => e
+  | n+1, .app f _ => stripArgsN f n
+  | _,   _        => e
+
+/--
+Given `e` of the form `f a_1 ... a_n ... a_m`, return `f a_1 ... a_n`.
+If `n` is greater than the arity, then return `e`.
+-/
+def getAppPrefix (e : Expr) (n : Nat) : Expr :=
+  e.stripArgsN (e.getAppNumArgs - n)
+
 /-- Given `e = fn a₁ ... aₙ`, runs `f` on `fn` and each of the arguments `aᵢ` and
 makes a new function application with the results. -/
 def traverseApp {M} [Monad M]
@@ -1653,6 +1684,47 @@ def setAppPPExplicitForExposingMVars (e : Expr) : Expr :=
     mkAppN f args |>.setPPExplicit true
   | _      => e
 
+/--
+Returns true if `e` is a `let_fun` expression, which is an expression of the form `letFun v f`.
+Ideally `f` is a lambda, but we do not require that here.
+Warning: if the `let_fun` is applied to additional arguments (such as in `(let_fun f := id; id) 1`), this function returns `false`.
+-/
+def isLetFun (e : Expr) : Bool := e.isAppOfArity ``letFun 4
+
+/--
+Recognizes a `let_fun` expression.
+For `let_fun n : t := v; b`, returns `some (n, t, v, b)`, which are the first four arguments to `Lean.Expr.letE`.
+Warning: if the `let_fun` is applied to additional arguments (such as in `(let_fun f := id; id) 1`), this function returns `none`.
+
+`let_fun` expressions are encoded as `letFun v (fun (n : t) => b)`.
+They can be created using `Lean.Meta.mkLetFun`.
+
+If in the encoding of `let_fun` the last argument to `letFun` is eta reduced, this returns `Name.anonymous` for the binder name.
+-/
+def letFun? (e : Expr) : Option (Name × Expr × Expr × Expr) :=
+  match e with
+  | .app (.app (.app (.app (.const ``letFun _) t) _β) v) f =>
+    match f with
+    | .lam n _ b _ => some (n, t, v, b)
+    | _ => some (.anonymous, t, v, .app f (.bvar 0))
+  | _ => none
+
+/--
+Like `Lean.Expr.letFun?`, but handles the case when the `let_fun` expression is possibly applied to additional arguments.
+Returns those arguments in addition to the values returned by `letFun?`.
+-/
+def letFunAppArgs? (e : Expr) : Option (Array Expr × Name × Expr × Expr × Expr) := do
+  guard <| 4 ≤ e.getAppNumArgs
+  guard <| e.isAppOf ``letFun
+  let args := e.getAppArgs
+  let t := args[0]!
+  let v := args[2]!
+  let f := args[3]!
+  let rest := args.extract 4 args.size
+  match f with
+  | .lam n _ b _ => some (rest, n, t, v, b)
+  | _ => some (rest, .anonymous, t, v, .app f (.bvar 0))
+
 end Expr
 
 /--
@@ -1670,28 +1742,6 @@ def annotation? (kind : Name) (e : Expr) : Option Expr :=
   | .mdata d b => if d.size == 1 && d.getBool kind false then some b else none
   | _          => none
 
-/--
-Annotate `e` with the `let_fun` annotation. This annotation is used as hint for the delaborator.
-If `e` is of the form `(fun x : t => b) v`, then `mkLetFunAnnotation e` is delaborated at
-`let_fun x : t := v; b`
--/
-def mkLetFunAnnotation (e : Expr) : Expr :=
-  mkAnnotation `let_fun e
-
-/--
-Return `some e'` if `e = mkLetFunAnnotation e'`
--/
-def letFunAnnotation? (e : Expr) : Option Expr :=
-  annotation? `let_fun e
-
-/--
-Return true if `e = mkLetFunAnnotation e'`, and `e'` is of the form `(fun x : t => b) v`
--/
-def isLetFun (e : Expr) : Bool :=
-  match letFunAnnotation? e with
-  | none   => false
-  | some e => e.isApp && e.appFn!.isLambda
-
 /--
 Auxiliary annotation used to mark terms marked with the "inaccessible" annotation `.(t)` and
 `_` in patterns.

src/Lean/Linter/UnusedVariables.lean

@@ -179,10 +179,17 @@ def unusedVariables : Linter where
           | _ =>
             assignments)
 
+    -- collect fvars from mvar assignments
     let tacticFVarUses : HashSet FVarId ←
-      tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do
-        let (_, s) ← StateT.run (s := uses) <| expr.forEach fun e => do if e.isFVar then modify (·.insert e.fvarId!)
-        return s
+      Elab.Command.liftIO <|  -- no need to carry around other state here
+      StateT.run' (s := HashSet.empty) do
+      -- use one big cache for all `ForEachExpr.visit` invocations
+      MonadCacheT.run do
+        tacticMVarAssignments.forM fun _ e =>
+          ForEachExpr.visit (e := e) fun e => do
+            if e.isFVar then modify (·.insert e.fvarId!)
+            return e.hasFVar
+        get
 
     -- collect ignore functions
     let ignoreFns := (← getUnusedVariablesIgnoreFns)

src/Lean/Meta/AppBuilder.lean

@@ -24,6 +24,19 @@ def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : MetaM Expr := do
   let u ← getLevel expectedType
   return mkApp2 (mkConst ``id [u]) expectedType e
 
+/--
+`mkLetFun x v e` creates the encoding for the `let_fun x := v; e` expression.
+The expression `x` can either be a free variable or a metavariable, and the function suitably abstracts `x` in `e`.
+-/
+def mkLetFun (x : Expr) (v : Expr) (e : Expr) : MetaM Expr := do
+  let f ← mkLambdaFVars #[x] e
+  let ety ← inferType e
+  let α ← inferType x
+  let β ← mkLambdaFVars #[x] ety
+  let u1 ← getLevel α
+  let u2 ← getLevel ety
+  return mkAppN (.const ``letFun [u1, u2]) #[α, β, v, f]
+
 /-- Return `a = b`. -/
 def mkEq (a b : Expr) : MetaM Expr := do
   let aType ← inferType a
@@ -337,7 +350,7 @@ def mkAppOptM (constName : Name) (xs : Array (Option Expr)) : MetaM Expr := do
     let (f, fType) ← mkFun constName
     mkAppOptMAux f xs 0 #[] 0 #[] fType
 
-/-- Similar to `mkAppOptM`, but takes an `Expr` instead of a constant name -/
+/-- Similar to `mkAppOptM`, but takes an `Expr` instead of a constant name. -/
 def mkAppOptM' (f : Expr) (xs : Array (Option Expr)) : MetaM Expr := do
   let fType ← inferType f
   withAppBuilderTrace f xs do withNewMCtxDepth do
@@ -396,7 +409,7 @@ def mkPure (monad : Expr) (e : Expr) : MetaM Expr :=
   mkAppOptM ``Pure.pure #[monad, none, none, e]
 
 /--
-  `mkProjection s fieldName` return an expression for accessing field `fieldName` of the structure `s`.
+  `mkProjection s fieldName` returns an expression for accessing field `fieldName` of the structure `s`.
   Remark: `fieldName` may be a subfield of `s`. -/
 partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
   let type ← inferType s

src/Lean/Meta/ExprDefEq.lean

@@ -1491,10 +1491,16 @@ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM
     else
       pure false
 
-/-- Remove unnecessary let-decls -/
-private def consumeLet : Expr → Expr
+/--
+Removes unnecessary let-decls (both true `let`s and `let_fun`s).
+-/
+private partial def consumeLet : Expr → Expr
   | e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b
-  | e                       => e
+  | e =>
+    if let some (_, _, _, b) := e.letFun? then
+      if b.hasLooseBVars then e else consumeLet b
+    else
+      e
 
 mutual
 

src/Lean/Meta/IndPredBelow.lean

@@ -169,6 +169,7 @@ where
       let fail _ := do
         throwError "only trivial inductive applications supported in premises:{indentExpr t}"
 
+      let t ← whnf t
       t.withApp fun f args => do
         if let some name := f.constName? then
           if let some idx := ctx.typeInfos.findIdx?
@@ -190,6 +191,7 @@ where
       (domain : Expr)
       {α : Type} (k : Expr → MetaM α) : MetaM α := do
     forallTelescopeReducing domain fun xs t => do
+      let t ← whnf t
       t.withApp fun _ args => do
         let hApp := mkAppN binder xs
         let t := mkAppN vars.motives[indValIdx]! $ args[ctx.numParams:] ++ #[hApp]

src/Lean/Meta/InferType.lean

@@ -246,7 +246,7 @@ partial def isPropQuick : Expr → MetaM LBool
   | .mvar mvarId      => do let mvarType  ← inferMVarType mvarId;  isArrowProp mvarType 0
   | .app f ..         => isPropQuickApp f 1
 
-/-- `isProp whnf e` return `true` if `e` is a proposition.
+/-- `isProp e` returns `true` if `e` is a proposition.
 
      If `e` contains metavariables, it may not be possible
      to decide whether is a proposition or not. We return `false` in this
@@ -371,7 +371,6 @@ def isType (e : Expr) : MetaM Bool := do
     | .sort .. => return true
     | _        => return false
 
-
 @[inline] private def withLocalDecl' {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α := do
   let fvarId ← mkFreshFVarId
   withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do

src/Lean/Meta/Tactic/AC/Main.lean

@@ -150,7 +150,7 @@ def rewriteUnnormalized (mvarId : MVarId) : MetaM Unit := do
   newGoal.refl
 where
   post (e : Expr) : SimpM Simp.Step := do
-    let ctx ← read
+    let ctx ← Simp.getContext
     match e, ctx.parent? with
     | bin op₁ l r, some (bin op₂ _ _) =>
       if ←isDefEq op₁ op₂ then

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

@@ -7,6 +7,7 @@ import Lean.Meta.ACLt
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.AppBuilder
 import Lean.Meta.SynthInstance
+import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.LinearArith.Simp
 
@@ -37,13 +38,18 @@ def synthesizeArgs (thmId : Origin) (xs : Array Expr) (bis : Array BinderInfo) (
         if (← synthesizeInstance x type) then
           continue
       if (← isProp type) then
+        -- We save the state, so that `UsedTheorems` does not accumulate
+        -- `simp` lemmas used during unsuccessful discharging.
+        let usedTheorems := (← get).usedTheorems
         match (← discharge? type) with
         | some proof =>
           unless (← isDefEq x proof) do
             trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign proof{indentExpr type}"
+            modify fun s => { s with usedTheorems }
             return false
         | none =>
           trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to discharge hypotheses{indentExpr type}"
+          modify fun s => { s with usedTheorems }
           return false
   return true
 where
@@ -111,7 +117,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
   | some { expr := eNew, proof? := some proof, .. } =>
     let mut proof := proof
     for extraArg in extraArgs do
-      proof ← mkCongrFun proof extraArg
+      proof ← Meta.mkCongrFun proof extraArg
     if (← hasAssignableMVar eNew) then
       trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, resulting expression has unassigned metavariables"
       return none
@@ -175,6 +181,13 @@ where
   inErasedSet (thm : SimpTheorem) : Bool :=
     erased.contains thm.origin
 
+@[inline] def andThen' (s : Step) (f? : Expr → SimpM Step) : SimpM Step := do
+  match s with
+  | Step.done _  => return s
+  | Step.visit r =>
+    let s' ← f? r.expr
+    return s'.updateResult (← mkEqTrans r s'.result)
+
 @[inline] def andThen (s : Step) (f? : Expr → SimpM (Option Step)) : SimpM Step := do
   match s with
   | Step.done _  => return s
@@ -222,7 +235,7 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
       return none
 
 @[inline] def tryRewriteUsingDecide? (e : Expr) : SimpM (Option Step) := do
-  if (← read).config.decide then
+  if (← getConfig).decide then
     match (← rewriteUsingDecide? e) with
     | some r => return Step.done r
     | none => return none
@@ -230,12 +243,48 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
     return none
 
 def simpArith? (e : Expr) : SimpM (Option Step) := do
-  if !(← read).config.arith then return none
-  let some (e', h) ← Linear.simp? e (← read).parent? | return none
+  if !(← getConfig).arith then return none
+  let some (e', h) ← Linear.simp? e (← getContext).parent? | return none
   return Step.visit { expr := e', proof? := h }
 
-def simpMatchCore? (app : MatcherApp) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Step) := do
-  for matchEq in (← Match.getEquationsFor app.matcherName).eqnNames do
+/--
+Given a match-application `e` with `MatcherInfo` `info`, return `some result`
+if at least of one of the discriminants has been simplified.
+-/
+def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) := do
+  let numArgs := e.getAppNumArgs
+  if numArgs < info.arity then
+    return none
+  let prefixSize := info.numParams + 1 /- motive -/
+  let n     := numArgs - prefixSize
+  let f     := e.stripArgsN n
+  let infos := (← getFunInfoNArgs f n).paramInfo
+  let args  := e.getAppArgsN n
+  let mut r : Result := { expr := f }
+  let mut modified := false
+  for i in [0 : info.numDiscrs] do
+    let arg := args[i]!
+    if i < infos.size && !infos[i]!.hasFwdDeps then
+      let argNew ← simp arg
+      if argNew.expr != arg then modified := true
+      r ← mkCongr r argNew
+    else if (← whnfD (← inferType r.expr)).isArrow then
+      let argNew ← simp arg
+      if argNew.expr != arg then modified := true
+      r ← mkCongr r argNew
+    else
+      let argNew ← dsimp arg
+      if argNew != arg then modified := true
+      r ← mkCongrFun r argNew
+  unless modified do
+    return none
+  for i in [info.numDiscrs : args.size] do
+    let arg := args[i]!
+    r ← mkCongrFun r arg
+  return some r
+
+def simpMatchCore? (matcherName : Name) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Step) := do
+  for matchEq in (← Match.getEquationsFor matcherName).eqnNames do
     -- Try lemma
     match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) } discharge?) with
     | none   => pure ()
@@ -243,33 +292,142 @@ def simpMatchCore? (app : MatcherApp) (e : Expr) (discharge? : Expr → SimpM (O
   return none
 
 def simpMatch? (discharge? : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (Option Step) := do
-  if (← read).config.iota then
-    let some app ← matchMatcherApp? e | return none
-    simpMatchCore? app e discharge?
+  if (← getConfig).iota then
+    if let some e ← reduceRecMatcher? e then
+      return some (.visit { expr := e })
+    let .const declName _ := e.getAppFn
+      | return none
+    if let some info ← getMatcherInfo? declName then
+      if let some r ← simpMatchDiscrs? info e then
+        return some (.visit r)
+      simpMatchCore? declName e discharge?
+    else
+      return none
   else
     return none
 
 def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
-  for thms in (← read).simpTheorems do
+  for thms in (← getContext).simpTheorems do
     if let some r ← rewrite? e thms.pre thms.erased discharge? (tag := "pre") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 
 def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (rflOnly := false) : SimpM Step := do
-  for thms in (← read).simpTheorems do
+  for thms in (← getContext).simpTheorems do
     if let some r ← rewrite? e thms.post thms.erased discharge? (tag := "post") (rflOnly := rflOnly) then
       return Step.visit r
   return Step.visit { expr := e }
 
-def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
+partial def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
   let s ← rewritePre e discharge?
-  andThen s tryRewriteUsingDecide?
+  let s ← andThen s (simpMatch? discharge?)
+  let s ← andThen s tryRewriteUsingDecide?
+  if s.result.expr == e then
+    return s
+  else
+    andThen s (preDefault · discharge?)
 
 def postDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
   let s ← rewritePost e discharge?
-  let s ← andThen s (simpMatch? discharge?)
   let s ← andThen s simpArith?
   let s ← andThen s tryRewriteUsingDecide?
   andThen s tryRewriteCtorEq?
 
+/--
+  Return true if `e` is of the form `(x : α) → ... → s = t → ... → False`
+
+  Recall that this kind of proposition is generated by Lean when creating equations for
+  functions and match-expressions with overlapping cases.
+  Example: the following `match`-expression has overlapping cases.
+  ```
+  def f (x y : Nat) :=
+    match x, y with
+    | Nat.succ n, Nat.succ m => ...
+    | _, _ => 0
+  ```
+  The second equation is of the form
+  ```
+  (x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
+  ```
+  The hypothesis `(n m : Nat) → x = Nat.succ n → y = Nat.succ m → False` is essentially
+  saying the first case is not applicable.
+-/
+partial def isEqnThmHypothesis (e : Expr) : Bool :=
+  e.isForall && go e
+where
+  go (e : Expr) : Bool :=
+    match e with
+    | .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
+    | _ => e.consumeMData.isConstOf ``False
+
+def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
+  (← getLCtx).findDeclRevM? fun localDecl => do
+    if localDecl.isImplementationDetail then
+      return none
+    else if (← isDefEq e localDecl.type) then
+      return some localDecl.toExpr
+    else
+      return none
+
+/--
+  Tries to solve `e` using `unifyEq?`.
+  It assumes that `isEqnThmHypothesis e` is `true`.
+-/
+partial def dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option Expr) := do
+  assert! isEqnThmHypothesis e
+  let mvar ← mkFreshExprSyntheticOpaqueMVar e
+  withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
+    if let .none ← go? mvar.mvarId! then
+      instantiateMVars mvar
+    else
+      return none
+where
+  go? (mvarId : MVarId) : MetaM (Option MVarId) :=
+    try
+      let (fvarId, mvarId) ← mvarId.intro1
+      mvarId.withContext do
+        let localDecl ← fvarId.getDecl
+        if localDecl.type.isEq || localDecl.type.isHEq then
+          if let some { mvarId, .. } ← unifyEq? mvarId fvarId {} then
+            go? mvarId
+          else
+            return none
+        else
+          go? mvarId
+    catch _  =>
+      return some mvarId
+
+def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
+  if isEqnThmHypothesis e then
+    if let some r ← dischargeUsingAssumption? e then
+      return some r
+    if let some r ← dischargeEqnThmHypothesis? e then
+      return some r
+  let ctx ← getContext
+  trace[Meta.Tactic.simp.discharge] ">> discharge?: {e}"
+  if ctx.dischargeDepth >= ctx.config.maxDischargeDepth then
+    trace[Meta.Tactic.simp.discharge] "maximum discharge depth has been reached"
+    return none
+  else
+    withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
+      let r ← simp e
+      if r.expr.consumeMData.isConstOf ``True then
+        try
+          return some (← mkOfEqTrue (← r.getProof))
+        catch _ =>
+          return none
+      else
+        return none
+
+abbrev Discharge := Expr → SimpM (Option Expr)
+
+def mkMethods (discharge? : Discharge) : Methods := {
+  pre        := (preDefault · discharge?)
+  post       := (postDefault · discharge?)
+  discharge? := discharge?
+}
+
+def methodsDefault : Methods :=
+  mkMethods dischargeDefault?
+
 end Lean.Meta.Simp

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

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.AppBuilder
 import Lean.Meta.CongrTheorems
+import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.SimpCongrTheorems
 
@@ -43,7 +44,19 @@ structure State where
   usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
 
-abbrev SimpM := ReaderT Context $ StateRefT State MetaM
+private opaque MethodsRefPointed : NonemptyType.{0}
+
+private def MethodsRef : Type := MethodsRefPointed.type
+
+instance : Nonempty MethodsRef := MethodsRefPointed.property
+
+abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
+
+@[extern "lean_simp"]
+opaque simp (e : Expr) : SimpM Result
+
+@[extern "lean_dsimp"]
+opaque dsimp (e : Expr) : SimpM Expr
 
 inductive Step where
   | visit : Result → Step
@@ -64,31 +77,46 @@ structure Methods where
   discharge? : Expr → SimpM (Option Expr) := fun _ => return none
   deriving Inhabited
 
-/- Internal monad -/
-abbrev M := ReaderT Methods SimpM
+unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
+  unsafeCast m
 
-def pre (e : Expr) : M Step := do
-  (← read).pre e
+@[implemented_by Methods.toMethodsRefImpl]
+opaque Methods.toMethodsRef (m : Methods) : MethodsRef
 
-def post (e : Expr) : M Step := do
-  (← read).post e
+unsafe def MethodsRef.toMethodsImpl (m : MethodsRef) : Methods :=
+  unsafeCast m
 
-def discharge? (e : Expr) : M (Option Expr) := do
-  (← read).discharge? e
+@[implemented_by MethodsRef.toMethodsImpl]
+opaque MethodsRef.toMethods (m : MethodsRef) : Methods
+
+def getMethods : SimpM Methods :=
+  return MethodsRef.toMethods (← read)
+
+def pre (e : Expr) : SimpM Step := do
+  (← getMethods).pre e
+
+def post (e : Expr) : SimpM Step := do
+  (← getMethods).post e
+
+def discharge? (e : Expr) : SimpM (Option Expr) := do
+  (← getMethods).discharge? e
+
+@[inline] def getContext : SimpM Context :=
+  readThe Context
 
 def getConfig : SimpM Config :=
-  return (← read).config
+  return (← getContext).config
 
-@[inline] def withParent (parent : Expr) (f : M α) : M α :=
+@[inline] def withParent (parent : Expr) (f : SimpM α) : SimpM α :=
   withTheReader Context (fun ctx => { ctx with parent? := parent }) f
 
-def getSimpTheorems : M SimpTheoremsArray :=
+def getSimpTheorems : SimpM SimpTheoremsArray :=
   return (← readThe Context).simpTheorems
 
-def getSimpCongrTheorems : M SimpCongrTheorems :=
+def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
   return (← readThe Context).congrTheorems
 
-@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : M α) : M α := do
+@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
   let cacheSaved := (← get).cache
   modify fun s => { s with cache := {} }
   try
@@ -101,8 +129,219 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
     let n := s.usedTheorems.size
     { s with usedTheorems := s.usedTheorems.insert thmId n }
 
+def Result.getProof (r : Result) : MetaM Expr := do
+  match r.proof? with
+  | some p => return p
+  | none   => mkEqRefl r.expr
+
+/--
+  Similar to `Result.getProof`, but adds a `mkExpectedTypeHint` if `proof?` is `none`
+  (i.e., result is definitionally equal to input), but we cannot establish that
+  `source` and `r.expr` are definitionally when using `TransparencyMode.reducible`. -/
+def Result.getProof' (source : Expr) (r : Result) : MetaM Expr := do
+  match r.proof? with
+  | some p => return p
+  | none   =>
+    if (← isDefEq source r.expr) then
+      mkEqRefl r.expr
+    else
+      /- `source` and `r.expr` must be definitionally equal, but
+         are not definitionally equal at `TransparencyMode.reducible` -/
+      mkExpectedTypeHint (← mkEqRefl r.expr) (← mkEq source r.expr)
+
+def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
+  match r.proof? with
+  | none   => return { expr := mkApp r.expr a, proof? := none }
+  | some h => return { expr := mkApp r.expr a, proof? := (← Meta.mkCongrFun h a) }
+
+def mkCongr (r₁ r₂ : Result) : MetaM Result :=
+  let e := mkApp r₁.expr r₂.expr
+  match r₁.proof?, r₂.proof? with
+  | none,     none   => return { expr := e, proof? := none }
+  | some h,  none    => return { expr := e, proof? := (← Meta.mkCongrFun h r₂.expr) }
+  | none,    some h  => return { expr := e, proof? := (← Meta.mkCongrArg r₁.expr h) }
+  | some h₁, some h₂ => return { expr := e, proof? := (← Meta.mkCongr h₁ h₂) }
+
+def mkImpCongr (src : Expr) (r₁ r₂ : Result) : MetaM Result := do
+  let e := src.updateForallE! r₁.expr r₂.expr
+  match r₁.proof?, r₂.proof? with
+  | none,     none   => return { expr := e, proof? := none }
+  | _,        _      => return { expr := e, proof? := (← Meta.mkImpCongr (← r₁.getProof) (← r₂.getProof)) } -- TODO specialize if bottleneck
+
+/-- Given the application `e`, remove unnecessary casts of the form `Eq.rec a rfl` and `Eq.ndrec a rfl`. -/
+partial def removeUnnecessaryCasts (e : Expr) : MetaM Expr := do
+  let mut args := e.getAppArgs
+  let mut modified := false
+  for i in [:args.size] do
+    let arg := args[i]!
+    if isDummyEqRec arg then
+      args := args.set! i (elimDummyEqRec arg)
+      modified := true
+  if modified then
+    return mkAppN e.getAppFn args
+  else
+    return e
+where
+  isDummyEqRec (e : Expr) : Bool :=
+    (e.isAppOfArity ``Eq.rec 6 || e.isAppOfArity ``Eq.ndrec 6) && e.appArg!.isAppOf ``Eq.refl
+
+  elimDummyEqRec (e : Expr) : Expr :=
+    if isDummyEqRec e then
+      elimDummyEqRec e.appFn!.appFn!.appArg!
+    else
+      e
+
+/--
+Given a simplified function result `r` and arguments `args`, simplify arguments using `simp` and `dsimp`.
+The resulting proof is built using `congr` and `congrFun` theorems.
+-/
+def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
+  if args.isEmpty then
+    return r
+  else
+    let infos := (← getFunInfoNArgs r.expr args.size).paramInfo
+    let mut r := r
+    let mut i := 0
+    for arg in args do
+      trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i]!.hasFwdDeps}"
+      if i < infos.size && !infos[i]!.hasFwdDeps then
+        r ← mkCongr r (← simp arg)
+      else if (← whnfD (← inferType r.expr)).isArrow then
+        r ← mkCongr r (← simp arg)
+      else
+        r ← mkCongrFun r (← dsimp arg)
+      i := i + 1
+    return r
+
+/--
+Retrieve auto-generated congruence lemma for `f`.
+
+Remark: If all argument kinds are `fixed` or `eq`, it returns `none` because
+using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof.
+-/
+def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
+  if f.isConst then if (← isMatcher f.constName!) then
+    -- We always use simple congruence theorems for auxiliary match applications
+    return none
+  let info ← getFunInfo f
+  let kinds ← getCongrSimpKinds f info
+  if kinds.all fun k => match k with | CongrArgKind.fixed => true | CongrArgKind.eq => true | _ => false then
+    /- See remark above. -/
+    return none
+  match (← get).congrCache.find? f with
+  | some thm? => return thm?
+  | none =>
+    let thm? ← mkCongrSimpCore? f info kinds
+    modify fun s => { s with congrCache := s.congrCache.insert f thm? }
+    return thm?
+
+/--
+Try to use automatically generated congruence theorems. See `mkCongrSimp?`.
+-/
+def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
+  let f := e.getAppFn
+  -- TODO: cache
+  let some cgrThm ← mkCongrSimp? f | return none
+  if cgrThm.argKinds.size != e.getAppNumArgs then return none
+  let mut simplified := false
+  let mut hasProof   := false
+  let mut hasCast    := false
+  let mut argsNew    := #[]
+  let mut argResults := #[]
+  let args := e.getAppArgs
+  for arg in args, kind in cgrThm.argKinds do
+    match kind with
+    | CongrArgKind.fixed => argsNew := argsNew.push (← dsimp arg)
+    | CongrArgKind.cast  => hasCast := true; argsNew := argsNew.push arg
+    | CongrArgKind.subsingletonInst => argsNew := argsNew.push arg
+    | CongrArgKind.eq =>
+      let argResult ← simp arg
+      argResults := argResults.push argResult
+      argsNew    := argsNew.push argResult.expr
+      if argResult.proof?.isSome then hasProof := true
+      if arg != argResult.expr then simplified := true
+    | _ => unreachable!
+  if !simplified then return some { expr := e }
+  /-
+    If `hasProof` is false, we used to return `mkAppN f argsNew` with `proof? := none`.
+    However, this created a regression when we started using `proof? := none` for `rfl` theorems.
+    Consider the following goal
+    ```
+    m n : Nat
+    a : Fin n
+    h₁ : m < n
+    h₂ : Nat.pred (Nat.succ m) < n
+    ⊢ Fin.succ (Fin.mk m h₁) = Fin.succ (Fin.mk m.succ.pred h₂)
+    ```
+    The term `m.succ.pred` is simplified to `m` using a `Nat.pred_succ` which is a `rfl` theorem.
+    The auto generated theorem for `Fin.mk` has casts and if used here at `Fin.mk m.succ.pred h₂`,
+    it produces the term `Fin.mk m (id (Eq.refl m) ▸ h₂)`. The key property here is that the
+    proof `(id (Eq.refl m) ▸ h₂)` has type `m < n`. If we had just returned `mkAppN f argsNew`,
+    the resulting term would be `Fin.mk m h₂` which is type correct, but later we would not be
+    able to apply `eq_self` to
+    ```lean
+    Fin.succ (Fin.mk m h₁) = Fin.succ (Fin.mk m h₂)
+    ```
+    because we would not be able to establish that `m < n` and `Nat.pred (Nat.succ m) < n` are definitionally
+    equal using `TransparencyMode.reducible` (`Nat.pred` is not reducible).
+    Thus, we decided to return here only if the auto generated congruence theorem does not introduce casts.
+  -/
+  if !hasProof && !hasCast then return some { expr := mkAppN f argsNew }
+  let mut proof := cgrThm.proof
+  let mut type  := cgrThm.type
+  let mut j := 0 -- index at argResults
+  let mut subst := #[]
+  for arg in args, kind in cgrThm.argKinds do
+    proof := mkApp proof arg
+    subst := subst.push arg
+    type := type.bindingBody!
+    match kind with
+    | CongrArgKind.fixed => pure ()
+    | CongrArgKind.cast  => pure ()
+    | CongrArgKind.subsingletonInst =>
+      let clsNew := type.bindingDomain!.instantiateRev subst
+      let instNew ← if (← isDefEq (← inferType arg) clsNew) then
+        pure arg
+      else
+        match (← trySynthInstance clsNew) with
+        | LOption.some val => pure val
+        | _ =>
+          trace[Meta.Tactic.simp.congr] "failed to synthesize instance{indentExpr clsNew}"
+          return none
+      proof := mkApp proof instNew
+      subst := subst.push instNew
+      type := type.bindingBody!
+    | CongrArgKind.eq =>
+      let argResult := argResults[j]!
+      let argProof ← argResult.getProof' arg
+      j := j + 1
+      proof := mkApp2 proof argResult.expr argProof
+      subst := subst.push argResult.expr |>.push argProof
+      type := type.bindingBody!.bindingBody!
+    | _ => unreachable!
+  let some (_, _, rhs) := type.instantiateRev subst |>.eq? | unreachable!
+  let rhs ← if hasCast then removeUnnecessaryCasts rhs else pure rhs
+  if hasProof then
+    return some { expr := rhs, proof? := proof }
+  else
+    /- See comment above. This is reachable if `hasCast == true`. The `rhs` is not structurally equal to `mkAppN f argsNew` -/
+    return some { expr := rhs }
+
 end Simp
 
 export Simp (SimpM)
 
+/--
+  Auxiliary method.
+  Given the current `target` of `mvarId`, apply `r` which is a new target and proof that it is equal to the current one.
+-/
+def applySimpResultToTarget (mvarId : MVarId) (target : Expr) (r : Simp.Result) : MetaM MVarId := do
+  match r.proof? with
+  | some proof => mvarId.replaceTargetEq r.expr proof
+  | none =>
+    if target != r.expr then
+      mvarId.replaceTargetDefEq r.expr
+    else
+      return mvarId
+
 end Lean.Meta

src/Lean/Meta/Tactic/Split.lean

@@ -22,12 +22,14 @@ def simpMatch (e : Expr) : MetaM Simp.Result := do
   (·.1) <$> Simp.main e (← getSimpMatchContext) (methods := { pre })
 where
   pre (e : Expr) : SimpM Simp.Step := do
-    let some app ← matchMatcherApp? e | return Simp.Step.visit { expr := e }
+    unless (← isMatcherApp e) do
+      return Simp.Step.visit { expr := e }
+    let matcherDeclName := e.getAppFn.constName!
     -- First try to reduce matcher
     match (← reduceRecMatcher? e) with
     | some e' => return Simp.Step.done { expr := e' }
     | none    =>
-      match (← Simp.simpMatchCore? app e SplitIf.discharge?) with
+      match (← Simp.simpMatchCore? matcherDeclName e SplitIf.discharge?) with
       | some r => return r
       | none => return Simp.Step.visit { expr := e }
 

src/Lean/Meta/WHNF.lean

@@ -560,6 +560,10 @@ where
       | .const ..  => pure e
       | .letE _ _ v b _ => if config.zeta then go <| b.instantiate1 v else return e
       | .app f ..       =>
+        if config.zeta then
+          if let some (args, _, _, v, b) := e.letFunAppArgs? then
+            -- When zeta reducing enabled, always reduce `letFun` no matter the current reducibility level
+            return (← go <| mkAppN (b.instantiate1 v) args)
         let f := f.getAppFn
         let f' ← go f
         if config.beta && f'.isLambda then

src/Lean/MetavarContext.lean

@@ -15,76 +15,79 @@ assignments. It is used in the elaborator, tactic framework, unifier
 the requirements imposed by these modules.
 
 - We may invoke TC while executing `isDefEq`. We need this feature to
-be able to solve unification problems such as:
-```
-f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m
-```
-where `(?a : Type) (?s : Ring ?a) (?x ?y : ?a)`
-During `isDefEq` (i.e., unification), it will need to solve the constrain
-```
-ringAdd ?s =?= intAdd
-```
-We say `ringAdd ?s` is stuck because it cannot be reduced until we
-synthesize the term `?s : Ring ?a` using TC. This can be done since we
-have assigned `?a := Int` when solving `?a =?= Int`.
+  WellFoundedRelationbe able to solve unification problems such as:
+  ```
+  f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m
+  ```
+  where `(?a : Type) (?s : Ring ?a) (?x ?y : ?a)`.
+
+  During `isDefEq` (i.e., unification), it will need to solve the constrain
+  ```
+  ringAdd ?s =?= intAdd
+  ```
+  We say `ringAdd ?s` is stuck because it cannot be reduced until we
+  synthesize the term `?s : Ring ?a` using TC. This can be done since we
+  have assigned `?a := Int` when solving `?a =?= Int`.
 
 - TC uses `isDefEq`, and `isDefEq` may create TC problems as shown
-above. Thus, we may have nested TC problems.
+  above. Thus, we may have nested TC problems.
 
 - `isDefEq` extends the local context when going inside binders. Thus,
-the local context for nested TC may be an extension of the local
-context for outer TC.
+  the local context for nested TC may be an extension of the local
+  context for outer TC.
 
 - TC should not assign metavariables created by the elaborator, simp,
-tactic framework, and outer TC problems. Reason: TC commits to the
-first solution it finds. Consider the TC problem `Coe Nat ?x`,
-where `?x` is a metavariable created by the caller. There are many
-solutions to this problem (e.g., `?x := Int`, `?x := Real`, ...),
-and it doesn’t make sense to commit to the first one since TC does
-not know the constraints the caller may impose on `?x` after the
-TC problem is solved.
-Remark: we claim it is not feasible to make the whole system backtrackable,
-and allow the caller to backtrack back to TC and ask it for another solution
-if the first one found did not work. We claim it would be too inefficient.
+  tactic framework, and outer TC problems. Reason: TC commits to the
+  first solution it finds. Consider the TC problem `Coe Nat ?x`,
+  where `?x` is a metavariable created by the caller. There are many
+  solutions to this problem (e.g., `?x := Int`, `?x := Real`, ...),
+  and it doesn’t make sense to commit to the first one since TC does
+  not know the constraints the caller may impose on `?x` after the
+  TC problem is solved.
+
+  Remark: we claim it is not feasible to make the whole system backtrackable,
+  and allow the caller to backtrack back to TC and ask it for another solution
+  if the first one found did not work. We claim it would be too inefficient.
 
 - TC metavariables should not leak outside of TC. Reason: we want to
-get rid of them after we synthesize the instance.
+  get rid of them after we synthesize the instance.
 
 - `simp` invokes `isDefEq` for matching the left-hand-side of
-equations to terms in our goal. Thus, it may invoke TC indirectly.
+  equations to terms in our goal. Thus, it may invoke TC indirectly.
 
 - In Lean3, we didn’t have to create a fresh pattern for trying to
-match the left-hand-side of equations when executing `simp`. We had a
-mechanism called "tmp" metavariables. It avoided this overhead, but it
-created many problems since `simp` may indirectly call TC which may
-recursively call TC. Moreover, we may want to allow TC to invoke
-tactics in the future. Thus, when `simp` invokes `isDefEq`, it may indirectly invoke
-a tactic and `simp` itself.  The Lean3 approach assumed that
-metavariables were short-lived, this is not true in Lean4, and to some
-extent was also not true in Lean3 since `simp`, in principle, could
-trigger an arbitrary number of nested TC problems.
+  match the left-hand-side of equations when executing `simp`. We had a
+  mechanism called "tmp" metavariables. It avoided this overhead, but it
+  created many problems since `simp` may indirectly call TC which may
+  recursively call TC. Moreover, we may want to allow TC to invoke
+  tactics in the future. Thus, when `simp` invokes `isDefEq`, it may indirectly invoke
+  a tactic and `simp` itself.  The Lean3 approach assumed that
+  metavariables were short-lived, this is not true in Lean4, and to some
+  extent was also not true in Lean3 since `simp`, in principle, could
+  trigger an arbitrary number of nested TC problems.
 
 - Here are some possible call stack traces we could have in Lean3 (and Lean4).
-```
-Elaborator (-> TC -> isDefEq)+
-Elaborator -> isDefEq (-> TC -> isDefEq)*
-Elaborator -> simp -> isDefEq (-> TC -> isDefEq)*
-```
-In Lean4, TC may also invoke tactics in the future.
+  ```
+  Elaborator (-> TC -> isDefEq)+
+  Elaborator -> isDefEq (-> TC -> isDefEq)*
+  Elaborator -> simp -> isDefEq (-> TC -> isDefEq)*
+  ```
+  In Lean4, TC may also invoke tactics in the future.
 
 - In Lean3 and Lean4, TC metavariables are not really short-lived. We
-solve an arbitrary number of unification problems, and we may have
-nested TC invocations.
+  solve an arbitrary number of unification problems, and we may have
+  nested TC invocations.
 
 - TC metavariables do not share the same local context even in the
-same invocation. In the C++ and Lean implementations we use a trick to
-ensure they do:
-https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L3583-L3594
+  same invocation. In the C++ and Lean implementations we use a trick to
+  ensure they do:
+  <https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L3583-L3594>
 
 - Metavariables may be natural, synthetic or syntheticOpaque.
-  a) Natural metavariables may be assigned by unification (i.e., `isDefEq`).
 
-  b) Synthetic metavariables may still be assigned by unification,
+  1. Natural metavariables may be assigned by unification (i.e., `isDefEq`).
+
+  2. Synthetic metavariables may still be assigned by unification,
      but whenever possible `isDefEq` will avoid the assignment. For example,
      if we have the unification constraint `?m =?= ?n`, where `?m` is synthetic,
      but `?n` is not, `isDefEq` solves it by using the assignment `?n := ?m`.
@@ -94,7 +97,7 @@ https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379
      them, and check whether the synthesized result is compatible with the one
      assigned by `isDefEq`.
 
-  c) SyntheticOpaque metavariables are never assigned by `isDefEq`.
+  3. SyntheticOpaque metavariables are never assigned by `isDefEq`.
      That is, the constraint `?n =?= Nat.succ Nat.zero` always fail
      if `?n` is a syntheticOpaque metavariable. This kind of metavariable
      is created by tactics such as `intro`. Reason: in the tactic framework,
@@ -104,78 +107,80 @@ https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379
   This distinction was not precise in Lean3 and produced
   counterintuitive behavior. For example, the following hack was added
   in Lean3 to work around one of these issues:
-  https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L2751
+  <https://github.com/leanprover/lean/blob/92826917a252a6092cffaf5fc5f1acb1f8cef379/src/library/type_context.cpp#L2751>
 
 - When creating lambda/forall expressions, we need to convert/abstract
-free variables and convert them to bound variables. Now, suppose we are
-trying to create a lambda/forall expression by abstracting free
-variable `xs` and a term `t[?m]` which contains a metavariable `?m`,
-and the local context of `?m` contains `xs`. The term
-```
-fun xs => t[?m]
-```
-will be ill-formed if we later assign a term `s` to `?m`, and
-`s` contains free variables in `xs`. We address this issue by changing
-the free variable abstraction procedure. We consider two cases: `?m`
-is natural or synthetic, or `?m` is syntheticOpaque. Assume the type of `?m` is
-`A[xs]`. Then, in both cases we create an auxiliary metavariable `?n` with
-type `forall xs => A[xs]`, and local context := local context of `?m` - `xs`.
-In both cases, we produce the term `fun xs => t[?n xs]`
-
-  1- If `?m` is natural or synthetic, then we assign `?m := ?n xs`, and we produce
-  the term `fun xs => t[?n xs]`
-
-  2- If `?m` is syntheticOpaque, then we mark `?n` as a syntheticOpaque variable.
-  However, `?n` is managed by the metavariable context itself.
-  We say we have a "delayed assignment" `?n xs := ?m`.
-  That is, after a term `s` is assigned to `?m`, and `s`
-  does not contain metavariables, we replace any occurrence
-  `?n ts` with `s[xs := ts]`.
-
-Gruesome details:
-
-  - When we create the type `forall xs => A` for `?n`, we may
-  encounter the same issue if `A` contains metavariables. So, the
-  process above is recursive. We claim it terminates because we keep
-  creating new metavariables with smaller local contexts.
-
-  - Suppose, we have `t[?m]` and we want to create a let-expression by
-  abstracting a let-decl free variable `x`, and the local context of
-  `?m` contains `x`. Similarly to the previous case
+  free variables and convert them to bound variables. Now, suppose we are
+  trying to create a lambda/forall expression by abstracting free
+  variable `xs` and a term `t[?m]` which contains a metavariable `?m`,
+  and the local context of `?m` contains `xs`. The term
   ```
-  let x : T := v; t[?m]
+  fun xs => t[?m]
   ```
   will be ill-formed if we later assign a term `s` to `?m`, and
-  `s` contains free variable `x`. Again, assume the type of `?m` is `A[x]`.
+  `s` contains free variables in `xs`. We address this issue by changing
+  the free variable abstraction procedure. We consider two cases: `?m`
+  is natural or synthetic, or `?m` is syntheticOpaque. Assume the type of `?m` is
+  `A[xs]`. Then, in both cases we create an auxiliary metavariable `?n` with
+  type `forall xs => A[xs]`, and local context := local context of `?m` - `xs`.
+  In both cases, we produce the term `fun xs => t[?n xs]`
 
-    1- If `?m` is natural or synthetic, then we create `?n : (let x : T := v; A[x])` with
-    and local context := local context of `?m` - `x`, we assign `?m := ?n`,
-    and produce the term `let x : T := v; t[?n]`. That is, we are just making
-    sure `?n` must never be assigned to a term containing `x`.
+  1. If `?m` is natural or synthetic, then we assign `?m := ?n xs`, and we produce
+     the term `fun xs => t[?n xs]`
 
-    2- If `?m` is syntheticOpaque, we create a fresh syntheticOpaque `?n`
-    with type `?n : T -> (let x : T := v; A[x])` and local context := local context of `?m` - `x`,
-    create the delayed assignment `?n #[x] := ?m`, and produce the term `let x : T := v; t[?n x]`.
-    Now suppose we assign `s` to `?m`. We do not assign the term `fun (x : T) => s` to `?n`, since
-    `fun (x : T) => s` may not even be type correct. Instead, we just replace applications `?n r`
-    with `s[x/r]`. The term `r` may not necessarily be a bound variable. For example, a tactic
-    may have reduced `let x : T := v; t[?n x]` into `t[?n v]`.
-    We are essentially using the pair "delayed assignment + application" to implement a delayed
-    substitution.
+  2. If `?m` is syntheticOpaque, then we mark `?n` as a syntheticOpaque variable.
+     However, `?n` is managed by the metavariable context itself.
+     We say we have a "delayed assignment" `?n xs := ?m`.
+     That is, after a term `s` is assigned to `?m`, and `s`
+     does not contain metavariables, we replace any occurrence
+     `?n ts` with `s[xs := ts]`.
+
+  Gruesome details:
+
+  - When we create the type `forall xs => A` for `?n`, we may
+    encounter the same issue if `A` contains metavariables. So, the
+    process above is recursive. We claim it terminates because we keep
+    creating new metavariables with smaller local contexts.
+
+  - Suppose, we have `t[?m]` and we want to create a let-expression by
+    abstracting a let-decl free variable `x`, and the local context of
+    `?m` contains `x`. Similarly to the previous case
+    ```
+    let x : T := v; t[?m]
+    ```
+    will be ill-formed if we later assign a term `s` to `?m`, and
+    `s` contains free variable `x`. Again, assume the type of `?m` is `A[x]`.
+
+    1. If `?m` is natural or synthetic, then we create `?n : (let x : T := v; A[x])` with
+       and local context := local context of `?m` - `x`, we assign `?m := ?n`,
+       and produce the term `let x : T := v; t[?n]`. That is, we are just making
+       sure `?n` must never be assigned to a term containing `x`.
+
+    2. If `?m` is syntheticOpaque, we create a fresh syntheticOpaque `?n`
+       with type `?n : T -> (let x : T := v; A[x])` and local context := local context of `?m` - `x`,
+       create the delayed assignment `?n #[x] := ?m`, and produce the term `let x : T := v; t[?n x]`.
+
+       Now suppose we assign `s` to `?m`. We do not assign the term `fun (x : T) => s` to `?n`, since
+       `fun (x : T) => s` may not even be type correct. Instead, we just replace applications `?n r`
+       with `s[x/r]`. The term `r` may not necessarily be a bound variable. For example, a tactic
+       may have reduced `let x : T := v; t[?n x]` into `t[?n v]`.
+
+       We are essentially using the pair "delayed assignment + application" to implement a delayed
+       substitution.
 
 - We use TC for implementing coercions. Both Joe Hendrix and Reid Barton
-reported a nasty limitation. In Lean3, TC will not be used if there are
-metavariables in the TC problem. For example, the elaborator will not try
-to synthesize `Coe Nat ?x`. This is good, but this constraint is too
-strict for problems such as `Coe (Vector Bool ?n) (BV ?n)`. The coercion
-exists independently of `?n`. Thus, during TC, we want `isDefEq` to throw
-an exception instead of return `false` whenever it tries to assign
-a metavariable owned by its caller. The idea is to sign to the caller that
-it cannot solve the TC problem at this point, and more information is needed.
-That is, the caller must make progress an assign its metavariables before
-trying to invoke TC again.
+  reported a nasty limitation. In Lean3, TC will not be used if there are
+  metavariables in the TC problem. For example, the elaborator will not try
+  to synthesize `Coe Nat ?x`. This is good, but this constraint is too
+  strict for problems such as `Coe (Vector Bool ?n) (BV ?n)`. The coercion
+  exists independently of `?n`. Thus, during TC, we want `isDefEq` to throw
+  an exception instead of return `false` whenever it tries to assign
+  a metavariable owned by its caller. The idea is to sign to the caller that
+  it cannot solve the TC problem at this point, and more information is needed.
+  That is, the caller must make progress an assign its metavariables before
+  trying to invoke TC again.
 
-In Lean4, we are using a simpler design for the `MetavarContext`.
+  In Lean4, we are using a simpler design for the `MetavarContext`.
 
 - No distinction between temporary and regular metavariables.
 
@@ -184,6 +189,7 @@ In Lean4, we are using a simpler design for the `MetavarContext`.
 - MetavarContext also has a `depth` field.
 
 - We bump the `MetavarContext` depth when we create a nested problem.
+
   Example: Elaborator (depth = 0) -> Simplifier matcher (depth = 1) -> TC (level = 2) -> TC (level = 3) -> ...
 
 - When `MetavarContext` is at depth N, `isDefEq` does not assign variables from `depth < N`.
@@ -192,11 +198,12 @@ In Lean4, we are using a simpler design for the `MetavarContext`.
 
 - New design even allows us to invoke tactics from TC.
 
-* Main concern
-We don't have tmp metavariables anymore in Lean4. Thus, before trying to match
-the left-hand-side of an equation in `simp`. We first must bump the level of the `MetavarContext`,
-create fresh metavariables, then create a new pattern by replacing the free variable on the left-hand-side with
-these metavariables. We are hoping to minimize this overhead by
+- Main concern
+
+  We don't have tmp metavariables anymore in Lean4. Thus, before trying to match
+  the left-hand-side of an equation in `simp`. We first must bump the level of the `MetavarContext`,
+  create fresh metavariables, then create a new pattern by replacing the free variable on the left-hand-side with
+  these metavariables. We are hoping to minimize this overhead by
 
   - Using better indexing data structures in `simp`. They should reduce the number of time `simp` must invoke `isDefEq`.
 
@@ -480,7 +487,8 @@ def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (mvar
   modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, mvarIdPending } }
 
 /-!
-Notes on artificial eta-expanded terms due to metavariables.
+## Notes on artificial eta-expanded terms due to metavariables.
+
 We try avoid synthetic terms such as `((fun x y => t) a b)` in the output produced by the elaborator.
 This kind of term may be generated when instantiating metavariable assignments.
 This module tries to avoid their generation because they often introduce unnecessary dependencies and
@@ -491,9 +499,11 @@ all free variables that may be used to "fill" the hole. Suppose, we create a met
 containing `(x : Nat) (y : Nat) (b : Bool)`, then we can assign terms such as `x + y` to `?m` since `x` and `y`
 are in the context used to create `?m`. Now, suppose we have the term `?m + 1` and we want to create the lambda expression
 `fun x => ?m + 1`. This term is not correct since we may assign to `?m` a term containing `x`.
+
 We address this issue by create a synthetic metavariable `?n : Nat → Nat` and adding the delayed assignment
 `?n #[x] := ?m`, and the term `fun x => ?n x + 1`. When we later assign a term `t[x]` to `?m`, `fun x => t[x]` is assigned to
 `?n`, and if we substitute it at `fun x => ?n x + 1`, we produce `fun x => ((fun x => t[x]) x) + 1`.
+
 To avoid this term eta-expanded term, we apply beta-reduction when instantiating metavariable assignments in this module.
 This operation is performed at `instantiateExprMVars`, `elimMVarDeps`, and `levelMVarToParam`.
 -/
@@ -923,7 +933,8 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr)
   Remark: We used to throw an `Exception.revertFailure` exception when an auxiliary declaration
   had to be reversed. Recall that auxiliary declarations are created when compiling (mutually)
   recursive definitions. The `revertFailure` due to auxiliary declaration dependency was originally
-  introduced in Lean3 to address issue https://github.com/leanprover/lean/issues/1258.
+  introduced in Lean3 to address issue <https://github.com/leanprover/lean/issues/1258>.
+
   In Lean4, this solution is not satisfactory because all definitions/theorems are potentially
   recursive. So, even a simple (incomplete) definition such as
   ```
@@ -939,11 +950,13 @@ private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr)
   we create the metavariable `?n : {α : Type} → (a : α) → (f : α → List α) → List α`,
   add the delayed assignment `?n #[α, a, f] := ?m`, and create the lambda
   `fun {α : Type} (a : α) => ?n α a f`.
+
   See `elimMVarDeps` for more information.
+
   If we kept using the Lean3 approach, we would get the `Exception.revertFailure` exception because we are
   reverting the auxiliary definition `f`.
 
-  Note that https://github.com/leanprover/lean/issues/1258 is not an issue in Lean4 because
+  Note that <https://github.com/leanprover/lean/issues/1258> is not an issue in Lean4 because
   we have changed how we compile recursive definitions.
 -/
 def collectForwardDeps (lctx : LocalContext) (toRevert : Array Expr) : M (Array Expr) := do

src/Lean/Parser/Basic.lean

@@ -564,7 +564,40 @@ def hexDigitFn : ParserFn := fun c s =>
     if curr.isDigit || ('a' <= curr && curr <= 'f') || ('A' <= curr && curr <= 'F') then s.setPos i
     else s.mkUnexpectedError "invalid hexadecimal numeral"
 
-def quotedCharCoreFn (isQuotable : Char → Bool) : ParserFn := fun c s =>
+/--
+Parses the whitespace after the `\` when there is a string gap.
+Raises an error if the whitespace does not contain exactly one newline character.
+Processes `\r\n` as a newline.
+-/
+partial def stringGapFn (seenNewline afterCR : Bool) : ParserFn := fun c s =>
+  let i := s.pos
+  if h : c.input.atEnd i then s -- let strLitFnAux handle the EOI error if !seenNewline
+  else
+    let curr := c.input.get' i h
+    if curr == '\n' then
+      if seenNewline then
+        -- Having more than one newline in a string gap is visually confusing
+        s.mkUnexpectedError "unexpected additional newline in string gap"
+      else
+        stringGapFn true false c (s.next' c.input i h)
+    else if curr == '\r' then
+      stringGapFn seenNewline true c (s.next' c.input i h)
+    else if afterCR then
+      s.mkUnexpectedError "expecting newline after carriage return"
+    else if curr.isWhitespace then
+      stringGapFn seenNewline false c (s.next' c.input i h)
+    else if seenNewline then
+      s
+    else
+      s.mkUnexpectedError "expecting newline in string gap"
+
+/--
+Parses a string quotation after a `\`.
+- `isQuotable` determines which characters are valid escapes
+- `inString` enables features that are only valid within strings,
+  in particular `"\" newline whitespace*` gaps.
+-/
+def quotedCharCoreFn (isQuotable : Char → Bool) (inString : Bool) : ParserFn := fun c s =>
   let input := c.input
   let i     := s.pos
   if h : input.atEnd i then s.mkEOIError
@@ -576,6 +609,8 @@ def quotedCharCoreFn (isQuotable : Char → Bool) : ParserFn := fun c s =>
       andthenFn hexDigitFn hexDigitFn c (s.next' input i h)
     else if curr == 'u' then
       andthenFn hexDigitFn (andthenFn hexDigitFn (andthenFn hexDigitFn hexDigitFn)) c (s.next' input i h)
+    else if inString && (curr == '\n' || curr == '\r') then
+      stringGapFn false false c s
     else
       s.mkUnexpectedError "invalid escape sequence"
 
@@ -583,7 +618,14 @@ def isQuotableCharDefault (c : Char) : Bool :=
   c == '\\' || c == '\"' || c == '\'' || c == 'r' || c == 'n' || c == 't'
 
 def quotedCharFn : ParserFn :=
-  quotedCharCoreFn isQuotableCharDefault
+  quotedCharCoreFn isQuotableCharDefault false
+
+/--
+Like `quotedCharFn` but enables escapes that are only valid inside strings.
+In particular, string gaps (`"\" newline whitespace*`).
+-/
+def quotedStringFn : ParserFn :=
+  quotedCharCoreFn isQuotableCharDefault true
 
 /-- Push `(Syntax.node tk <new-atom>)` onto syntax stack if parse was successful. -/
 def mkNodeToken (n : SyntaxNodeKind) (startPos : String.Pos) : ParserFn := fun c s => Id.run do
@@ -624,9 +666,93 @@ partial def strLitFnAux (startPos : String.Pos) : ParserFn := fun c s =>
     let s    := s.setPos (input.next' i h)
     if curr == '\"' then
       mkNodeToken strLitKind startPos c s
-    else if curr == '\\' then andthenFn quotedCharFn (strLitFnAux startPos) c s
+    else if curr == '\\' then andthenFn quotedStringFn (strLitFnAux startPos) c s
     else strLitFnAux startPos c s
 
+/--
+Raw strings have the syntax `r##...#"..."#...##` with zero or more `#`'s.
+If we are looking at a valid start to a raw string (`r##...#"`),
+returns true.
+We assume `i` begins at the position immediately after `r`.
+-/
+partial def isRawStrLitStart (input : String) (i : String.Pos) : Bool :=
+  if h : input.atEnd i then false
+  else
+    let curr := input.get' i h
+    if curr == '#' then
+      isRawStrLitStart input (input.next' i h)
+    else
+      curr == '"'
+
+/--
+Parses a raw string literal assuming `isRawStrLitStart` has returned true.
+The `startPos` is the start of the raw string (at the `r`).
+The parser state is assumed to be immediately after the `r`.
+-/
+partial def rawStrLitFnAux (startPos : String.Pos) : ParserFn := initState 0
+where
+  /--
+  Gives the "unterminated raw string literal" error.
+  -/
+  errorUnterminated (s : ParserState) := s.mkUnexpectedErrorAt "unterminated raw string literal" startPos
+  /--
+  Parses the `#`'s and `"` at the beginning of the raw string.
+  The `num` variable counts the number of `#`s after the `r`.
+  -/
+  initState (num : Nat) : ParserFn := fun c s =>
+    let input := c.input
+    let i     := s.pos
+    if h : input.atEnd i then errorUnterminated s
+    else
+      let curr := input.get' i h
+      let s    := s.setPos (input.next' i h)
+      if curr == '#' then
+        initState (num + 1) c s
+      else if curr == '"' then
+        normalState num c s
+      else
+        -- This should not occur, since we assume `isRawStrLitStart` succeeded.
+        errorUnterminated s
+  /--
+  Parses characters after the first `"`. If we need to start counting `#`'s to decide if we are closing
+  the raw string literal, we switch to `closingState`.
+  -/
+  normalState (num : Nat) : ParserFn := fun c s =>
+    let input := c.input
+    let i     := s.pos
+    if h : input.atEnd i then errorUnterminated s
+    else
+      let curr := input.get' i h
+      let s    := s.setPos (input.next' i h)
+      if curr == '\"' then
+        if num == 0 then
+          mkNodeToken strLitKind startPos c s
+        else
+          closingState num 0 c s
+      else
+        normalState num c s
+  /--
+  Parses `#` characters immediately after a `"`.
+  The `closingNum` variable counts the number of `#`s seen after the `"`.
+  Note: `num > 0` since the `num = 0` case is entirely handled by `normalState`.
+  -/
+  closingState (num : Nat) (closingNum : Nat) : ParserFn := fun c s =>
+    let input := c.input
+    let i     := s.pos
+    if h : input.atEnd i then errorUnterminated s
+    else
+      let curr := input.get' i h
+      let s    := s.setPos (input.next' i h)
+      if curr == '#' then
+        if closingNum + 1 == num then
+          mkNodeToken strLitKind startPos c s
+        else
+          closingState num (closingNum + 1) c s
+      else if curr == '\"' then
+        closingState num 0 c s
+      else
+        normalState num c s
+
 def decimalNumberFn (startPos : String.Pos) (c : ParserContext) : ParserState → ParserState := fun s =>
   let s     := takeWhileFn (fun c => c.isDigit) c s
   let input := c.input
@@ -820,6 +946,8 @@ private def tokenFnAux : ParserFn := fun c s =>
     numberFnAux c s
   else if curr == '`' && isIdFirstOrBeginEscape (getNext input i) then
     nameLitAux i c s
+  else if curr == 'r' && isRawStrLitStart input (input.next i) then
+    rawStrLitFnAux i c (s.next input i)
   else
     let tk := c.tokens.matchPrefix input i
     identFnAux i tk .anonymous c s

src/Lean/Parser/Command.lean

@@ -28,32 +28,27 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
-/-
-A mutual block may be broken in different cliques,
-we identify them using an `ident` (an element of the clique).
-We provide two kinds of hints to the termination checker:
-1- A wellfounded relation (`p` is `termParser`)
-2- A tactic for proving the recursive applications are "decreasing" (`p` is `tacticSeq`)
+/--
+A decreasing_by clause can either be a single tactic (for all functions), or
+a list of tactics labeled with the function they apply to.
 -/
-def terminationHintMany (p : Parser) := leading_parser
-  atomic (lookahead (ident >> " => ")) >>
-  many1Indent (group (ppLine >> ppIndent (ident >> " => " >> p >> optional ";")))
-def terminationHint1 (p : Parser) := leading_parser p
-def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p
+def decreasingByElement := leading_parser
+  ppLine >> ppIndent (ident >> " => " >> Tactic.tacticSeq >> patternIgnore (optional ";"))
+def decreasingByMany := leading_parser
+  atomic (lookahead (ident >> " => ")) >> many1Indent decreasingByElement
+def decreasingBy1  := leading_parser Tactic.tacticSeq
 
-def terminationByCore := leading_parser
-  ppDedent ppLine >> "termination_by' " >> terminationHint termParser
 def decreasingBy := leading_parser
-  ppDedent ppLine >> "decreasing_by " >> terminationHint Tactic.tacticSeq
+  ppDedent ppLine >> "decreasing_by " >> (decreasingByMany <|> decreasingBy1)
 
 def terminationByElement   := leading_parser
   ppLine >> (ident <|> Term.hole) >> many (ppSpace >> (ident <|> Term.hole)) >>
-  " => " >> termParser >> optional ";"
+  " => " >> termParser >> patternIgnore (optional ";")
 def terminationBy          := leading_parser
   ppDedent ppLine >> "termination_by" >> many1Indent terminationByElement
 
 def terminationSuffix :=
-  optional (terminationBy <|> terminationByCore) >> optional decreasingBy
+  optional terminationBy >> optional decreasingBy
 
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|

src/Lean/Parser/StrInterpolation.lean

@@ -24,7 +24,7 @@ partial def interpolatedStrFn (p : ParserFn) : ParserFn := fun c s =>
         let s := mkNodeToken interpolatedStrLitKind startPos c s
         s.mkNode interpolatedStrKind stackSize
       else if curr == '\\' then
-        andthenFn (quotedCharCoreFn isQuotableCharForStrInterpolant) (parse startPos) c s
+        andthenFn (quotedCharCoreFn isQuotableCharForStrInterpolant true) (parse startPos) c s
       else if curr == '{' then
         let s := mkNodeToken interpolatedStrLitKind startPos c s
         let s := p c s

src/Lean/Parser/Term.lean

@@ -669,7 +669,8 @@ def isIdent (stx : Syntax) : Bool :=
   checkStackTop isIdent "expected preceding identifier" >>
   checkNoWsBefore "no space before '.{'" >> ".{" >>
   sepBy1 levelParser ", " >> "}"
-/-- `x@e` matches the pattern `e` and binds its value to the identifier `x`. -/
+/-- `x@e` or `x:h@e` matches the pattern `e` and binds its value to the identifier `x`.
+If present, the identifier `h` is bound to a proof of `x = e`. -/
 @[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser
   checkStackTop isIdent "expected preceding identifier" >>
   checkNoWsBefore "no space before '@'" >> "@" >>

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -277,17 +277,6 @@ end Delaborator
 open SubExpr (Pos PosMap)
 open Delaborator (OptionsPerPos topDownAnalyze)
 
-/-- Custom version of `Lean.Core.betaReduce` to beta reduce expressions for the `pp.beta` option.
-We do not want to beta reduce the application in `let_fun` annotations. -/
-private partial def betaReduce' (e : Expr) : CoreM Expr :=
-  Core.transform e (pre := fun e => do
-    if isLetFun e then
-      return .done <| e.updateMData! (.app (← betaReduce' e.mdataExpr!.appFn!) (← betaReduce' e.mdataExpr!.appArg!))
-    else if e.isHeadBetaTarget then
-      return .visit e.headBeta
-    else
-      return .continue)
-
 def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × PosMap Elab.Info) := do
   /- Using `erasePatternAnnotations` here is a bit hackish, but we do it
      `Expr.mdata` affects the delaborator. TODO: should we fix that? -/
@@ -302,7 +291,7 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delabor
     catch _ => pure ()
   withOptions (fun _ => opts) do
     let e ← if getPPInstantiateMVars opts then instantiateMVars e else pure e
-    let e ← if getPPBeta opts then betaReduce' e else pure e
+    let e ← if getPPBeta opts then Core.betaReduce e else pure e
     let optionsPerPos ←
       if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then
         topDownAnalyze e

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -395,19 +395,34 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
     return Syntax.mkApp stx st.moreArgs
 
 /--
-  Delaborate applications of the form `(fun x => b) v` as `let_fun x := v; b`
+Annotation key to use in hack for overapplied `let_fun` notation.
 -/
-def delabLetFun : Delab := do
-  let stxV ← withAppArg delab
-  withAppFn do
-    let Expr.lam n _ b _ ← getExpr | unreachable!
-    let n ← getUnusedName n b
-    let stxB ← withBindingBody n delab
-    if ← getPPOption getPPLetVarTypes <||> getPPOption getPPAnalysisLetVarType then
-      let stxT ← withBindingDomain delab
-      `(let_fun $(mkIdent n) : $stxT := $stxV; $stxB)
-    else
-      `(let_fun $(mkIdent n) := $stxV; $stxB)
+def delabLetFunKey : Name := `_delabLetFun
+
+/--
+Delaborates applications of the form `letFun v (fun x => b)` as `let_fun x := v; b`.
+-/
+@[builtin_delab app.letFun]
+def delabLetFun : Delab := whenPPOption getPPNotation do
+  let e ← getExpr
+  let nargs := e.getAppNumArgs
+  if 4 < nargs then
+    -- It's overapplied. Hack: insert metadata around the first four arguments and delaborate again.
+    -- This will cause the app delaborator to delaborate `(letFun v f) x1 ... xn` with `letFun v f` as the function.
+    let args := e.getAppArgs
+    let f := mkAppN e.getAppFn (args.extract 0 4)
+    let e' := mkAppN (mkAnnotation delabLetFunKey f) (args.extract 4 args.size)
+    return (← withTheReader SubExpr ({· with expr := e'}) delab)
+  guard <| e.getAppNumArgs == 4
+  let Expr.lam n _ b _ := e.appArg! | failure
+  let n ← getUnusedName n b
+  let stxV ← withAppFn <| withAppArg delab
+  let stxB ← withAppArg <| withBindingBody n delab
+  if ← getPPOption getPPLetVarTypes <||> getPPOption getPPAnalysisLetVarType then
+    let stxT ← SubExpr.withNaryArg 0 delab
+    `(let_fun $(mkIdent n) : $stxT := $stxV; $stxB)
+  else
+    `(let_fun $(mkIdent n) := $stxV; $stxB)
 
 @[builtin_delab mdata]
 def delabMData : Delab := do
@@ -417,8 +432,6 @@ def delabMData : Delab := do
       `(.($s)) -- We only include the inaccessible annotation when we are delaborating patterns
     else
       return s
-  else if isLetFun (← getExpr) && getPPNotation (← getOptions) then
-    withMDataExpr <| delabLetFun
   else if let some _ := isLHSGoal? (← getExpr) then
     withMDataExpr <| withAppFn <| withAppArg <| delab
   else

src/Lean/Server/Rpc/Basic.lean

@@ -62,18 +62,28 @@ def rpcReleaseRef (r : Lsp.RpcRef) : StateM RpcObjectStore Bool := do
   else
     return false
 
-/--
-`RpcEncodable α` means that `α` can be serialized in the RPC system of the Lean server.
-This is required when `α` contains fields which should be serialized as an RPC reference
-instead of being sent in full.
-The type wrapper `WithRpcRef` is used for these fields which should be sent as
-a reference.
+/-- `RpcEncodable α` means that `α` can be deserialized from and serialized into JSON
+for the purpose of receiving arguments to and sending return values from
+Remote Procedure Calls (RPCs).
 
-- Any type with `FromJson` and `ToJson` instance is automatically `RpcEncodable`.
-- If a type has an `Dynamic` instance, then `WithRpcRef` can be used for its references.
-- `deriving RpcEncodable` acts like `FromJson`/`ToJson` but marshalls any `WithRpcRef` fields
-  as `Lsp.RpcRef`s.
--/
+Any type with `FromJson` and `ToJson` instances is `RpcEncodable`.
+
+Furthermore, types that do not have these instances may still be `RpcEncodable`.
+Use `deriving RpcEncodable` to automatically derive instances for such types.
+
+This occurs when `α` contains data that should not or cannot be serialized:
+for instance, heavy objects such as `Lean.Environment`, or closures.
+For such data, we use the `WithRpcRef` marker.
+Note that for `WithRpcRef α` to be `RpcEncodable`,
+`α` must have a `TypeName` instance
+
+On the server side, `WithRpcRef α` is just a structure
+containing a value of type `α`.
+On the client side, it is an opaque reference of (structural) type `Lsp.RpcRef`.
+Thus, `WithRpcRef α` is cheap to transmit over the network
+but may only be accessed on the server side.
+In practice, it is used by the client to pass data
+between various RPC methods provided by the server. -/
 -- TODO(WN): for Lean.js, compile `WithRpcRef` to "opaque reference" on the client
 class RpcEncodable (α : Type) where
   rpcEncode : α → StateM RpcObjectStore Json
@@ -103,7 +113,15 @@ instance [RpcEncodable α] [RpcEncodable β] : RpcEncodable (α × β) where
     let (a, b) ← fromJson? j
     return (← rpcDecode a, ← rpcDecode b)
 
-/-- Marks fields to encode as opaque references in LSP packets. -/
+instance [RpcEncodable α] : RpcEncodable (StateM RpcObjectStore α) where
+  rpcEncode fn := fn >>= rpcEncode
+  rpcDecode j := do
+    let a : α ← rpcDecode j
+    return return a
+
+/-- Marks values to be encoded as opaque references in RPC packets.
+
+See the docstring for `RpcEncodable`. -/
 structure WithRpcRef (α : Type u) where
   val : α
   deriving Inhabited

src/Lean/Server/Rpc/Deriving.lean

@@ -42,7 +42,10 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
 
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
 
-  `(structure RpcEncodablePacket where
+  let indName := mkIdent indVal.name
+  `(-- Workaround for https://github.com/leanprover/lean4/issues/2044
+    namespace $indName
+    structure RpcEncodablePacket where
       $[($fieldIds : $fieldTys)]*
       deriving FromJson, ToJson
 
@@ -55,6 +58,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
       dec j := do
         let a : RpcEncodablePacket ← fromJson? j
         return { $[$decInits],* }
+    end $indName
   )
 
 private def matchAltTerm := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser)
@@ -92,7 +96,10 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
   let typeId ← `(@$(mkIdent indVal.name) $paramIds*)
 
-  `(inductive RpcEncodablePacket where
+  let indName := mkIdent indVal.name
+  `(-- Workaround for https://github.com/leanprover/lean4/issues/2044
+    namespace $indName
+    inductive RpcEncodablePacket where
       $[$ctors:ctor]*
       deriving FromJson, ToJson
 
@@ -107,6 +114,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
         have inst : RpcEncodable $typeId := { rpcEncode := enc, rpcDecode := dec }
         let pkt : RpcEncodablePacket ← fromJson? j
         id <| match pkt with $[$decodes:matchAlt]*
+    end $indName
   )
 
 /-- Creates an `RpcEncodablePacket` for `typeName`. For structures, the packet is a structure

src/Lean/SubExpr.lean

@@ -84,7 +84,7 @@ The first coordinate in the array corresponds to the root of the expression tree
 def ofArray (ps : Array Nat) : Pos :=
   ps.foldl push root
 
-/-- Decodes a subexpression `Pos` as a sequence of coordinates `cs : Array Nat`. See `Pos.fromArray` for details.
+/-- Decodes a subexpression `Pos` as a sequence of coordinates `cs : Array Nat`. See `Pos.ofArray` for details.
 `cs[0]` is the coordinate for the root expression. -/
 def toArray (p : Pos) : Array Nat :=
   foldl Array.push #[] p

src/Lean/Util.lean

@@ -23,6 +23,7 @@ import Lean.Util.ForEachExprWhere
 import Lean.Util.ReplaceLevel
 import Lean.Util.FoldConsts
 import Lean.Util.SCC
+import Lean.Util.TestExtern
 import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
 import Lean.Util.FileSetupInfo

src/Lean/Util/TestExtern.lean

@@ -0,0 +1,25 @@
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Command
+import Lean.Meta.Tactic.Unfold
+import Lean.Meta.Eval
+
+open Lean Elab Meta Command Term
+
+syntax (name := testExternCmd) "test_extern " term : command
+
+@[command_elab testExternCmd] unsafe def elabTestExtern : CommandElab
+  | `(test_extern $t:term) => liftTermElabM do
+    let t ← elabTermAndSynthesize t none
+    match t.getAppFn with
+    | .const f _ =>
+      if isExtern (← getEnv) f then
+        let t' := (← unfold t f).expr
+        let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[t, t'])
+        if ! (← evalExpr Bool (.const ``Bool []) r) then
+          throwError
+            ("native implementation did not agree with reference implementation!\n" ++
+            m!"Compare the outputs of:\n#eval {t}\n and\n#eval {t'}")
+      else
+        throwError "test_extern: {f} does not have an @[extern] attribute"
+    | _ => throwError "test_extern: expects a function application"
+  | _ => throwUnsupportedSyntax

src/Lean/Util/Trace.lean

@@ -16,7 +16,7 @@ usually as `[class.name] message ▸`.
 Every trace node has a class name, a message, and an array of children.
 This module provides the API to produce trace messages,
 the key entry points are:
-- ``registerTraceMessage `class.name`` registers a trace class
+- ``registerTraceClass `class.name`` registers a trace class
 - ``withTraceNode `class.name (fun result => return msg) do body`
   produces a trace message containing the trace messages in `body` as children
 - `trace[class.name] msg` produces a trace message without children

src/Lean/Widget/Basic.lean

@@ -2,6 +2,7 @@ import Lean.Elab.InfoTree
 import Lean.Message
 import Lean.Server.Rpc.Basic
 import Lean.Server.InfoUtils
+import Lean.Widget.Types
 
 namespace Lean.Widget
 

src/Lean/Widget/Types.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2023 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Wojciech Nawrocki
+-/
+import Lean.Server.Rpc.Basic
+
+namespace Lean.Widget
+
+/-- An instance of a widget component:
+the identifier of a widget module and the hash of its JS source code
+together with props.
+
+See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html)
+for more information about widgets. -/
+structure WidgetInstance where
+  /-- Name of the `@[widget_module]`. -/
+  id : Name
+  /-- Hash of the JS source of the widget module. -/
+  javascriptHash : UInt64
+  /-- Arguments to be passed to the component's default exported function.
+
+  Props may contain RPC references,
+  so must be stored as a computation
+  with access to the RPC object store. -/
+  props : StateM Server.RpcObjectStore Json
+
+end Lean.Widget

src/Lean/Widget/UserWidget.lean

@@ -2,29 +2,296 @@
 Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Authors: E.W.Ayers
+Authors: E.W.Ayers, Wojciech Nawrocki
 -/
 import Lean.Elab.Eval
 import Lean.Server.Rpc.RequestHandling
 
-open Lean
-
 namespace Lean.Widget
+open Meta Elab
 
-/-- A custom piece of code that is run on the editor client.
+/-- A widget module is a unit of source code that can execute in the infoview.
 
-The editor can use the `Lean.Widget.getWidgetSource` RPC method to
-get this object.
+Every module definition must either be annotated with `@[widget_module]`,
+or use a value of `javascript` identical to that of another definition
+annotated with `@[widget_module]`.
+This makes it possible for the infoview to load the module.
 
-See the [manual entry](doc/widgets.md) above this declaration for more information on
-how to use the widgets system.
+See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html)
+for more information on how to use the widgets system. -/
+structure Module where
+  /-- A JS [module](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)
+  intended for use in user widgets.
+
+  The JS environment in which modules execute
+  provides a fixed set of libraries accessible via direct `import`,
+  notably [`@leanprover/infoview`](https://www.npmjs.com/package/@leanprover/infoview)
+  and [`react`](https://www.npmjs.com/package/react).
+
+  To initialize this field from an external JS file,
+  you may use `include_str "path"/"to"/"file.js"`.
+  However **beware** that this does not register a dependency with Lake,
+  so your Lean module will not automatically be rebuilt
+  when the `.js` file changes. -/
+  javascript : String
+  /-- The hash is cached to avoid recomputing it whenever the `Module` is used. -/
+  javascriptHash : { x : UInt64 // x = hash javascript } := ⟨hash javascript, rfl⟩
+
+private unsafe def evalModuleUnsafe (e : Expr) : MetaM Module :=
+  evalExpr' Module ``Module e
+
+@[implemented_by evalModuleUnsafe]
+opaque evalModule (e : Expr) : MetaM Module
+
+private unsafe def evalWidgetInstanceUnsafe (e : Expr) : MetaM WidgetInstance :=
+  evalExpr' WidgetInstance ``WidgetInstance e
+
+@[implemented_by evalWidgetInstanceUnsafe]
+opaque evalWidgetInstance (e : Expr) : MetaM WidgetInstance
+
+/-! ## Storage of widget modules -/
+
+class ToModule (α : Type u) where
+  toModule : α → Module
+
+instance : ToModule Module := ⟨id⟩
+
+/-- Every constant `c : α` marked with `@[widget_module]` is registered here.
+The registry maps `hash (toModule c).javascript` to ``(`c, `(@toModule α inst c))``
+where `inst : ToModule α` is synthesized during registration time
+and stored thereafter. -/
+private abbrev ModuleRegistry := SimplePersistentEnvExtension
+  (UInt64 × Name × Expr)
+  (RBMap UInt64 (Name × Expr) compare)
+
+builtin_initialize moduleRegistry : ModuleRegistry ←
+  registerSimplePersistentEnvExtension {
+    addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅
+    addEntryFn    := fun s n => s.insert n.1 n.2
+    toArrayFn     := fun es => es.toArray
+  }
+
+private def widgetModuleAttrImpl : AttributeImpl where
+  name := `widget_module
+  descr := "Registers a widget module. Its type must implement Lean.Widget.ToModule."
+  applicationTime := AttributeApplicationTime.afterCompilation
+  add decl _stx _kind := Prod.fst <$> MetaM.run do
+    let e ← mkAppM ``ToModule.toModule #[.const decl []]
+    let mod ← evalModule e
+    let env ← getEnv
+    if let some (n, _) := moduleRegistry.getState env |>.find? mod.javascriptHash then
+      logWarning m!"A widget module with the same hash(JS source code) was already registered at {Expr.const n []}."
+    setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e)
+
+builtin_initialize registerBuiltinAttribute widgetModuleAttrImpl
+
+/-! ## Retrieval of widget modules -/
+
+structure GetWidgetSourceParams where
+  /-- Hash of the JS module to retrieve. -/
+  hash : UInt64
+  pos : Lean.Lsp.Position
+  deriving ToJson, FromJson
 
--/
 structure WidgetSource where
-  /-- Sourcetext of the code to run.-/
+  /-- Sourcetext of the JS module to run. -/
   sourcetext : String
   deriving Inhabited, ToJson, FromJson
 
+open Server RequestM in
+@[server_rpc_method]
+def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do
+  let doc ← readDoc
+  let pos := doc.meta.text.lspPosToUtf8Pos args.pos
+  let notFound := throwThe RequestError ⟨.invalidParams, s!"No widget module with hash {args.hash} registered"⟩
+  withWaitFindSnap doc (notFoundX := notFound)
+    (fun s => s.endPos >= pos || (moduleRegistry.getState s.env).contains args.hash)
+    fun snap => do
+      if let some (_, e) := moduleRegistry.getState snap.env |>.find? args.hash then
+        runTermElabM snap do
+          return { sourcetext := (← evalModule e).javascript }
+      else
+        notFound
+
+/-! ## Storage of panel widget instances -/
+
+inductive PanelWidgetsExtEntry where
+  | «global» (n : Name)
+  | «local» (wi : WidgetInstance)
+
+/-- Keeps track of panel widget instances that should be displayed.
+
+Instances can be registered for display global
+(i.e., persisted in `.olean`s) and locally (not persisted)
+
+For globally displayed widgets
+we cannot store a `WidgetInstance` in the persistent state
+because it contains a `StateM` closure.
+Instead, we add a global constant of type `WidgetInstance`
+to the environment, and store its name in the extension.
+
+For locally displayed ones, we just store a `WidgetInstance`
+in the extension directly.
+This is okay because it is never persisted.
+
+The (persistent) entries are then of the form `(h, n)`
+where `h` is a hash stored in the `moduleRegistry`
+and `n` is the name of a `WidgetInstance` global constant.
+
+The extension state maps each `h` as above
+to a list of entries that can be either global or local ones.
+Each element of the state indicates that the widget module `h`
+should be displayed with the given `WidgetInstance` as its arguments.
+
+This is similar to a parametric attribute, except that:
+- parametric attributes map at most one parameter to one tagged declaration,
+  whereas we may display multiple instances of a single widget module; and
+- parametric attributes use the same type for local and global entries,
+  which we cannot do owing to the closure. -/
+private abbrev PanelWidgetsExt := SimpleScopedEnvExtension
+  (UInt64 × Name)
+  (RBMap UInt64 (List PanelWidgetsExtEntry) compare)
+
+builtin_initialize panelWidgetsExt : PanelWidgetsExt ←
+  registerSimpleScopedEnvExtension {
+    addEntry := fun s (h, n) => s.insert h (.global n :: s.findD h [])
+    initial  := .empty
+  }
+
+def evalPanelWidgets : MetaM (Array WidgetInstance) := do
+  let mut ret := #[]
+  for (_, l) in panelWidgetsExt.getState (← getEnv) do
+    for e in l do
+      match e with
+      | .global n =>
+        let wi ← evalWidgetInstance (mkConst n)
+        ret := ret.push wi
+      | .local wi => ret := ret.push wi
+  return ret
+
+def addPanelWidgetGlobal [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64) (n : Name) : m Unit := do
+  panelWidgetsExt.add (h, n)
+
+def addPanelWidgetScoped [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64) (n : Name) : m Unit := do
+  panelWidgetsExt.add (h, n) .scoped
+
+def addPanelWidgetLocal [Monad m] [MonadEnv m] (wi : WidgetInstance) : m Unit := do
+  modifyEnv fun env => panelWidgetsExt.modifyState env fun s =>
+    s.insert wi.javascriptHash (.local wi :: s.findD wi.javascriptHash [])
+
+def erasePanelWidget [Monad m] [MonadEnv m] (h : UInt64) : m Unit := do
+  modifyEnv fun env => panelWidgetsExt.modifyState env fun st => st.erase h
+
+/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.
+`hash` must be `hash (toModule c).javascript`
+where `c` is some global constant annotated with `@[widget_module]`. -/
+def savePanelWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m]
+    (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) : m Unit := do
+  let env ← getEnv
+  let some (id, _) := moduleRegistry.getState env |>.find? hash
+    | throwError s!"No widget module with hash {hash} registered"
+  pushInfoLeaf <| .ofUserWidgetInfo { id, javascriptHash := hash, props, stx }
+
+/-! ## `show_panel_widgets` command -/
+
+syntax widgetInstanceSpec := ident ("with " term)?
+
+def elabWidgetInstanceSpecAux (mod : Ident) (props : Term) : TermElabM Expr := do
+  Term.elabTerm (expectedType? := mkConst ``WidgetInstance) <| ← `(
+    { id := $(quote mod.getId)
+      javascriptHash := (ToModule.toModule $mod).javascriptHash
+      props := Server.RpcEncodable.rpcEncode $props })
+
+def elabWidgetInstanceSpec : TSyntax ``widgetInstanceSpec → TermElabM Expr
+  | `(widgetInstanceSpec| $mod:ident) => do
+    elabWidgetInstanceSpecAux mod (← ``(Json.mkObj []))
+  | `(widgetInstanceSpec| $mod:ident with $props:term) => do
+    elabWidgetInstanceSpecAux mod props
+  | _ => throwUnsupportedSyntax
+
+syntax addWidgetSpec := Parser.Term.attrKind widgetInstanceSpec
+syntax eraseWidgetSpec := "-" ident
+syntax showWidgetSpec := addWidgetSpec <|> eraseWidgetSpec
+/-- Use `show_panel_widgets [<widget>]` to mark that `<widget>`
+should always be displayed, including in downstream modules.
+
+The type of `<widget>` must implement `Widget.ToModule`,
+and the type of `<props>` must implement `Server.RpcEncodable`.
+In particular, `<props> : Json` works.
+
+Use `show_panel_widgets [<widget> with <props>]`
+to specify the `<props>` that the widget should be given
+as arguments.
+
+Use `show_panel_widgets [local <widget> (with <props>)?]` to mark it
+for display in the current section, namespace, or file only.
+
+Use `show_panel_widgets [scoped <widget> (with <props>)?]` to mark it
+for display only when the current namespace is open.
+
+Use `show_panel_widgets [-<widget>]` to temporarily hide a previously shown widget
+in the current section, namespace, or file.
+Note that persistent erasure is not possible, i.e.,
+`-<widget>` has no effect on downstream modules. -/
+syntax (name := showPanelWidgetsCmd) "show_panel_widgets " "[" sepBy1(showWidgetSpec, ", ") "]" : command
+
+open Command in
+@[command_elab showPanelWidgetsCmd] def elabShowPanelWidgetsCmd : CommandElab
+  | `(show_panel_widgets [ $ws ,*]) => liftTermElabM do
+    for w in ws.getElems do
+      match w with
+      | `(showWidgetSpec| - $mod:ident) =>
+        let mod : Term ← ``(ToModule.toModule $mod)
+        let mod : Expr ← Term.elabTerm (expectedType? := mkConst ``Module) mod
+        let mod : Module ← evalModule mod
+        erasePanelWidget mod.javascriptHash
+      | `(showWidgetSpec| $attr:attrKind $spec:widgetInstanceSpec) =>
+        let attr ← liftMacroM <| toAttributeKind attr
+        let wiExpr ← elabWidgetInstanceSpec spec
+        let wi ← evalWidgetInstance wiExpr
+        if let .local := attr then
+          addPanelWidgetLocal wi
+        else
+          let name ← mkFreshUserName (wi.id ++ `_instance)
+          let wiExpr ← instantiateMVars wiExpr
+          if wiExpr.hasMVar then
+            throwError "failed to compile expression, it contains metavariables{indentExpr wiExpr}"
+          addAndCompile <| Declaration.defnDecl {
+            name
+            levelParams := []
+            type := mkConst ``WidgetInstance
+            value := wiExpr
+            hints := .opaque
+            safety := .safe
+          }
+          if let .global := attr then
+            addPanelWidgetGlobal wi.javascriptHash name
+          else
+            addPanelWidgetScoped wi.javascriptHash name
+      | _ => throwUnsupportedSyntax
+  | _ => throwUnsupportedSyntax
+
+/-! ## `#widget` command -/
+
+/-- Use `#widget <widget>` to display a panel widget,
+and `#widget <widget> with <props>` to display it with the given props.
+Useful for debugging widgets.
+
+The type of `<widget>` must implement `Widget.ToModule`,
+and the type of `<props>` must implement `Server.RpcEncodable`.
+In particular, `<props> : Json` works. -/
+syntax (name := widgetCmd) "#widget " widgetInstanceSpec : command
+
+open Command in
+@[command_elab widgetCmd] def elabWidgetCmd : CommandElab
+  | stx@`(#widget $s) => liftTermElabM do
+    let wi : Expr ← elabWidgetInstanceSpec s
+    let wi : WidgetInstance ← evalWidgetInstance wi
+    savePanelWidgetInfo wi.javascriptHash wi.props stx
+  | _ => throwUnsupportedSyntax
+
+/-! ## Deprecated definitions -/
+
 /-- Use this structure and the `@[widget]` attribute to define your own widgets.
 
 ```lean
@@ -42,149 +309,101 @@ structure UserWidgetDefinition where
   javascript: String
   deriving Inhabited, ToJson, FromJson
 
-structure UserWidget where
-  id : Name
-  /-- Pretty name of widget to display to the user.-/
-  name : String
-  javascriptHash: UInt64
-  deriving Inhabited, ToJson, FromJson
+instance : ToModule UserWidgetDefinition where
+  toModule uwd := { uwd with }
 
-private abbrev WidgetSourceRegistry := SimplePersistentEnvExtension
-    (UInt64 × Name)
-    (RBMap UInt64 Name compare)
-
--- Mapping widgetSourceId to hash of sourcetext
-builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension
-builtin_initialize widgetSourceRegistry : WidgetSourceRegistry ←
-  registerSimplePersistentEnvExtension {
-    addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅
-    addEntryFn    := fun s n => s.insert n.1 n.2
-    toArrayFn     := fun es => es.toArray
-  }
-
-private unsafe def getUserWidgetDefinitionUnsafe
-  (decl : Name) : CoreM UserWidgetDefinition :=
-  evalConstCheck UserWidgetDefinition ``UserWidgetDefinition decl
-
-@[implemented_by getUserWidgetDefinitionUnsafe]
-private opaque getUserWidgetDefinition
-  (decl : Name) : CoreM UserWidgetDefinition
-
-private def attributeImpl : AttributeImpl where
+private def widgetAttrImpl : AttributeImpl where
   name := `widget
-  descr := "Mark a string as static code that can be loaded by a widget handler."
+  descr := "The `@[widget]` attribute has been deprecated, use `@[widget_module]` instead."
   applicationTime := AttributeApplicationTime.afterCompilation
-  add decl _stx _kind := do
-    let env ← getEnv
-    let defn ← getUserWidgetDefinition decl
-    let javascriptHash := hash defn.javascript
-    let env := userWidgetRegistry.insert env decl {id := decl, name := defn.name, javascriptHash}
-    let env := widgetSourceRegistry.addEntry env (javascriptHash, decl)
-    setEnv <| env
+  add := widgetModuleAttrImpl.add
 
-builtin_initialize registerBuiltinAttribute attributeImpl
+builtin_initialize registerBuiltinAttribute widgetAttrImpl
 
-/-- Input for `getWidgetSource` RPC. -/
-structure GetWidgetSourceParams where
-  /-- The hash of the sourcetext to retrieve. -/
-  hash: UInt64
-  pos : Lean.Lsp.Position
-  deriving ToJson, FromJson
+private unsafe def evalUserWidgetDefinitionUnsafe [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
+    (id : Name) : m UserWidgetDefinition := do
+  ofExcept <| (← getEnv).evalConstCheck UserWidgetDefinition (← getOptions) ``UserWidgetDefinition id
 
-open Server RequestM in
-@[server_rpc_method]
-def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do
-  let doc ← readDoc
-  let pos := doc.meta.text.lspPosToUtf8Pos args.pos
-  let notFound := throwThe RequestError ⟨.invalidParams, s!"No registered user-widget with hash {args.hash}"⟩
-  withWaitFindSnap doc (notFoundX := notFound)
-    (fun s => s.endPos >= pos || (widgetSourceRegistry.getState s.env).contains args.hash)
-    fun snap => do
-      if let some id := widgetSourceRegistry.getState snap.env |>.find? args.hash then
-        runCoreM snap do
-          return {sourcetext := (← getUserWidgetDefinition id).javascript}
-      else
-        notFound
+@[implemented_by evalUserWidgetDefinitionUnsafe]
+opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadError m]
+    (id : Name) : m UserWidgetDefinition
 
-open Lean Elab
+/-- Save a user-widget instance to the infotree.
+    The given `widgetId` should be the declaration name of the widget definition. -/
+@[deprecated savePanelWidgetInfo] def saveWidgetInfo
+    [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [MonadInfoTree m]
+    (widgetId : Name) (props : Json) (stx : Syntax) : m Unit := do
+  let uwd ← evalUserWidgetDefinition widgetId
+  savePanelWidgetInfo (ToModule.toModule uwd).javascriptHash (pure props) stx
 
-/--
-  Try to retrieve the `UserWidgetInfo` at a particular position.
--/
-def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List UserWidgetInfo :=
+/-! ## Retrieving panel widget instances -/
+
+deriving instance Server.RpcEncodable for WidgetInstance
+
+/-- Retrieve all the `UserWidgetInfo`s that intersect a given line. -/
+def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverLine : Nat) : List UserWidgetInfo :=
   t.deepestNodes fun
     | _ctx, i@(Info.ofUserWidgetInfo wi), _cs => do
       if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
-        let trailSize := i.stx.getTrailingSize
-        -- show info at EOF even if strictly outside token + trail
-        let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx
-        guard <| pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + trailSize || atEOF)
+        -- Does the widget's line range contain `hoverLine`?
+        guard <| (text.utf8PosToLspPos pos).line ≤ hoverLine ∧ hoverLine ≤ (text.utf8PosToLspPos tailPos).line
         return wi
       else
         failure
     | _, _, _ => none
 
-/-- UserWidget accompanied by component props. -/
-structure UserWidgetInstance extends UserWidget where
-  /-- Arguments to be fed to the widget's main component. -/
-  props : Json
-  /-- The location of the widget instance in the Lean file. -/
-  range? : Option Lsp.Range
-  deriving ToJson, FromJson
+structure PanelWidgetInstance extends WidgetInstance where
+  /-- The syntactic span in the Lean file at which the panel widget is displayed. -/
+  range? : Option Lsp.Range := none
+  /-- When present, the infoview will wrap the widget
+  in `<details><summary>{name}</summary>...</details>`.
+  This functionality is deprecated
+  but retained for backwards compatibility
+  with `UserWidgetDefinition`. -/
+  name? : Option String := none
+  deriving Server.RpcEncodable
 
 /-- Output of `getWidgets` RPC.-/
 structure GetWidgetsResponse where
-  widgets : Array UserWidgetInstance
-  deriving ToJson, FromJson
+  widgets : Array PanelWidgetInstance
+  deriving Server.RpcEncodable
 
 open Lean Server RequestM in
-/-- Get the `UserWidget`s present at a particular position. -/
+/-- Get the panel widgets present around a particular position. -/
 @[server_rpc_method]
-def getWidgets (args : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
+def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
   let doc ← readDoc
   let filemap := doc.meta.text
-  let pos := filemap.lspPosToUtf8Pos args
-  withWaitFindSnap doc (·.endPos >= pos) (notFoundX := return ⟨∅⟩) fun snap => do
-    let env := snap.env
-    let ws := widgetInfosAt? filemap snap.infoTree pos
-    let ws ← ws.toArray.mapM (fun (w : UserWidgetInfo) => do
-      let some widget := userWidgetRegistry.find? env w.widgetId
-        | throw <| RequestError.mk .invalidParams s!"No registered user-widget with id {w.widgetId}"
-      return {
-        widget with
-        props := w.props
-        range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx
-      })
-    return {widgets := ws}
+  let nextLine := { line := pos.line + 1, character := 0 }
+  let t := doc.cmdSnaps.waitUntil fun snap => filemap.lspPosToUtf8Pos nextLine ≤ snap.endPos
+  mapTask t fun (snaps, _) => do
+    let some snap := snaps.getLast?
+      | return ⟨∅⟩
+    runTermElabM snap do
+      let env ← getEnv
+      /- Panels from the environment. -/
+      let ws' ← evalPanelWidgets
+      let ws' : Array PanelWidgetInstance ← ws'.mapM fun wi => do
+        -- Check if the definition uses the deprecated `UserWidgetDefinition`
+        -- on a best-effort basis.
+        -- If it does, also send the `name` field.
+        let name? ← env.find? wi.id
+          |>.filter (·.type.isConstOf ``UserWidgetDefinition)
+          |>.mapM fun _ => do
+            let uwd ← evalUserWidgetDefinition wi.id
+            return uwd.name
+        return { wi with name? }
+      /- Panels from the infotree. -/
+      let ws := widgetInfosAt? filemap snap.infoTree pos.line
+      let ws : Array PanelWidgetInstance ← ws.toArray.mapM fun (wi : UserWidgetInfo) => do
+        let name? ← env.find? wi.id
+          |>.filter (·.type.isConstOf ``UserWidgetDefinition)
+          |>.mapM fun _ => do
+            let uwd ← evalUserWidgetDefinition wi.id
+            return uwd.name
+        return { wi with range? := String.Range.toLspRange filemap <$> Syntax.getRange? wi.stx, name? }
+      return { widgets := ws' ++ ws }
 
-/-- Save a user-widget instance to the infotree.
-    The given `widgetId` should be the declaration name of the widget definition. -/
-def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetId : Name) (props : Json) (stx : Syntax):  m Unit := do
-  let info := Info.ofUserWidgetInfo {
-    widgetId := widgetId
-    props := props
-    stx := stx
-  }
-  pushInfoLeaf info
-
-/-!  # Widget command -/
-
-/-- Use `#widget <widgetname> <props>` to display a widget. Useful for debugging widgets. -/
-syntax (name := widgetCmd) "#widget " ident ppSpace term : command
-
-open Lean Lean.Meta Lean.Elab Lean.Elab.Term in
-private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json :=
-  Lean.Elab.Term.evalTerm Json (mkConst ``Json) stx
-
-@[implemented_by evalJsonUnsafe]
-private opaque evalJson (stx : Syntax) : TermElabM Json
-
-open Elab Command in
-
-@[command_elab widgetCmd] def elabWidgetCmd : CommandElab := fun
-  | stx@`(#widget $id:ident $props) => do
-    let props : Json ← runTermElabM fun _ => evalJson props
-    saveWidgetInfo id.getId props stx
-  | _ => throwUnsupportedSyntax
+attribute [deprecated Module] UserWidgetDefinition
 
 end Lean.Widget

src/lake/Lake/CLI/Main.lean

@@ -226,7 +226,7 @@ protected def list : CliM PUnit := do
         IO.println script.name
 
 protected nonrec def run : CliM PUnit := do
-  processOptions lakeOption
+  processLeadingOptions lakeOption  -- between `lake [script] run` and `<name>`
   let config ← mkLoadConfig (← getThe LakeOptions)
   let ws ← loadWorkspace config
   if let some spec ← takeArg? then

src/lake/Lake/Load/Elab.lean

@@ -183,7 +183,8 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
       let contents ← h.readToEnd; h.rewind
       let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson?
         | error "compiled configuration is invalid; run with `-R` to reconfigure"
-      let upToDate := trace.platform = platformDescriptor ∧
+      let upToDate :=
+        (← olean.pathExists) ∧ trace.platform = platformDescriptor ∧
         trace.leanHash = Lean.githash ∧ trace.configHash = configHash
       if upToDate then
         return .olean h
@@ -209,11 +210,25 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String)
     h.unlock
     return env
   | .lean h lakeOpts =>
-    let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile
-    Lean.writeModule env olean
-    h.putStrLn <| Json.pretty <| toJson
-      {platform := platformDescriptor, leanHash := Lean.githash,
-        configHash, options := lakeOpts : ConfigTrace}
-    h.truncate
-    h.unlock
-    return env
+    /-
+    NOTE: We write the trace before elaborating the configuration file
+    to enable automatic reconfiguration on the next `lake` invocation if
+    elaboration fails. To ensure a failure triggers a reconfigure, we must also
+    remove any previous out-of-date `.olean`. Otherwise, Lake will treat the
+    older `.olean` as matching the new trace.
+    -/
+    match (← IO.FS.removeFile olean |>.toBaseIO) with
+    | .ok _ | .error (.noFileOrDirectory ..) =>
+      h.putStrLn <| Json.pretty <| toJson
+        {platform := platformDescriptor, leanHash := Lean.githash,
+          configHash, options := lakeOpts : ConfigTrace}
+      h.truncate
+      let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile
+      Lean.writeModule env olean
+      h.unlock
+      return env
+    | .error e =>
+      logError <| toString e
+      h.unlock
+      IO.FS.removeFile traceFile
+      failure

src/lake/examples/scripts/expected.out

@@ -3,6 +3,7 @@ scripts/dismiss
 scripts/greet
 Hello, world!
 Hello, me!
+Hello, --me!
 Display a greeting
 
 USAGE:

src/lake/examples/scripts/test.sh

@@ -11,6 +11,7 @@ $LAKE update
 $LAKE script list | tee produced.out
 $LAKE run /greet | tee -a produced.out
 $LAKE script run greet me | tee -a produced.out
+$LAKE script run greet --me | tee -a produced.out
 $LAKE script doc greet | tee -a produced.out
 $LAKE script run hello | tee -a produced.out
 $LAKE script run dep/hello | tee -a produced.out

src/runtime/io.cpp

@@ -506,7 +506,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_ar
 
 /* monoMsNow : BaseIO Nat */
 extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now(obj_arg /* w */) {
-    static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64));
+    static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64), "size of std::chrono::nanoseconds::rep may not exceed 64");
     auto now = std::chrono::steady_clock::now();
     auto tm = std::chrono::duration_cast<std::chrono::milliseconds>(now.time_since_epoch());
     return io_result_mk_ok(uint64_to_nat(tm.count()));
@@ -514,7 +514,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now(obj_arg /* w */) {
 
 /* monoNanosNow : BaseIO Nat */
 extern "C" LEAN_EXPORT obj_res lean_io_mono_nanos_now(obj_arg /* w */) {
-    static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64));
+    static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64), "size of std::chrono::nanoseconds::rep may not exceed 64");
     auto now = std::chrono::steady_clock::now();
     auto tm = std::chrono::duration_cast<std::chrono::nanoseconds>(now.time_since_epoch());
     return io_result_mk_ok(uint64_to_nat(tm.count()));

src/runtime/mpz.cpp

@@ -327,7 +327,7 @@ void mpz::init_uint64(uint64 v) {
         allocate(1);
         m_digits[0] = v;
     } else {
-        static_assert(sizeof(uint64) == 2 * sizeof(unsigned));
+        static_assert(sizeof(uint64) == 2 * sizeof(unsigned), "unsigned should be half the size of an uint64");
         allocate(2);
         m_digits[0] = static_cast<mpn_digit>(v);
         m_digits[1] = static_cast<mpn_digit>(v >> 8*sizeof(mpn_digit));

src/runtime/object.cpp

@@ -714,8 +714,12 @@ class task_manager {
             resolve_core(t, v);
         } else {
             // `bind` task has not finished yet, re-add as dependency of nested task
+            // NOTE: closure MUST be extracted before unlocking the mutex as otherwise
+            // another thread could deactivate the task and empty `m_clousure` in
+            // between.
+            object * c = t->m_imp->m_closure;
             lock.unlock();
-            add_dep(lean_to_task(closure_arg_cptr(t->m_imp->m_closure)[0]), t);
+            add_dep(lean_to_task(closure_arg_cptr(c)[0]), t);
             lock.lock();
         }
     }

src/stdlib.make.in

@@ -18,7 +18,7 @@ LEANMAKE_OPTS=\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\
 	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
-	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -DwarningAsError=true"\
+	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS}"\
 	LEANC_OPTS+="${LEANC_OPTS}"\
 	LEAN_AR="${CMAKE_AR}"\
 	MORE_DEPS+="${PREV_STAGE}/bin/lean${PREV_STAGE_CMAKE_EXECUTABLE_SUFFIX}"\