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/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/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

RELEASES.md

@@ -8,7 +8,10 @@ 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*`.
@@ -20,6 +23,72 @@ v4.5.0 (development in progress)
   ```
   [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
 ---------
 

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/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
 ```
 
@@ -94,6 +94,22 @@ So the complete syntax is:
    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
 =============
 

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/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

@@ -48,5 +48,10 @@
 				}
 			}
 		]
+	},
+	"extensions": {
+		"recommendations": [
+			"leanprover.lean4"
+		]
 	}
 }

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

@@ -800,9 +800,40 @@ partial def decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Optio
   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

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/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/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/GuessLex.lean

@@ -14,6 +14,7 @@ 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
 
 
@@ -32,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
@@ -264,39 +264,6 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext
           return (false, true)
     return (true, true)
 
-/-- 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)
-
 /-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive
 call site.
 -/
@@ -590,7 +557,7 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
         declName, vars, body,
         implicit := true
       }
-  return .ext termByElements
+  return termByElements
 
 
 /--

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,44 +5,46 @@ 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
 
 open Parser.Command in
 /--
-This function takes a user-specified `decreasing_by` or `termination_by'` clause (as `Sytnax`).
-If it is a `terminathionHintMany` (a set of clauses guarded by the function name) then
+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 expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationHint := do
-  let some terminationHint := terminationHint? | return TerminationHint.none
-  let ref := terminationHint
-  match terminationHint with
-  | `(terminationByCore|termination_by' $hint1:terminationHint1)
-  | `(decreasingBy|decreasing_by $hint1:terminationHint1) =>
-    return TerminationHint.one { ref, value := hint1.raw[0] }
-  | `(terminationByCore|termination_by' $hints:terminationHintMany)
-  | `(decreasingBy|decreasing_by $hints:terminationHintMany) => do
-    let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg =>
+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 arg[0].getId.isSuffixOf declName then some declName else none
+        if declId.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] }
+      | 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
@@ -50,69 +52,65 @@ def expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (A
           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
+    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` and `termination_by'` notation -/
+/-! # 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
 
-/-- `terminatoin_by` clauses, grouped by clique -/
+/-- `termination_by` clauses, grouped by clique -/
 structure TerminationByClique where
   elements : Array TerminationByElement
   used     : Bool := false
 
 /--
-A `termination_by'` or `termination_by` hint, as specified by the user
+A `termination_by` hint, as specified by the user
 -/
-inductive TerminationBy where
-  /-- `termination_by'` -/
-  | core (hint : TerminationHint)
-  /-- `termination_by` -/
-  | ext  (cliques : Array TerminationByClique)
+structure TerminationBy where
+  cliques : Array TerminationByClique
   deriving Inhabited
 
 /--
-A `termination_by'` or `termination_by` hint, as applicable to a single clique
+A `termination_by` hint, as applicable to a single clique
 -/
-inductive TerminationWF where
-  | core (stx : Syntax)
-  | ext  (clique : Array TerminationByElement)
+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
@@ -125,8 +123,9 @@ def terminationByElement   := leading_parser ppLine >> (ident <|> hole) >> many
 def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
 ```
 -/
-open Parser.Command in
-private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy := do
+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
@@ -170,51 +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
-
-/--
-Expands the syntax for a `termination_by` or `termination_by'` clause, using the appropriate function
--/
-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
+  return ⟨result⟩
 
 open Parser.Command in
-def TerminationWF.unexpand : TerminationWF → MetaM Syntax
-  | .ext elements => do
-    let elementStxs ← elements.mapM fun element => do
-      let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
-      let body : Term := ⟨element.body⟩
-      let vars : Array Ident := element.vars.map TSyntax.mk
-      `(terminationByElement|$fn $vars* => $body)
-    `(terminationBy|termination_by $elementStxs*)
-  | .core _ => unreachable! -- we don't synthetize termination_by' syntax
+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
@@ -222,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/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/Parser/Basic.lean

@@ -669,6 +669,90 @@ partial def strLitFnAux (startPos : String.Pos) : ParserFn := fun 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
@@ -862,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,23 +28,18 @@ 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 >> patternIgnore (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)) >>
@@ -53,7 +48,7 @@ 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/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/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/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();
         }
     }