feat: add simp configuration option Simp.Config.instances

When `instances := false`, instance implicit arguments are not visited
during `simp`. `Std` does not seem affected by this change.

.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/nix-ci.yml

@@ -87,6 +87,8 @@ jobs:
         run: |
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,test,inked} -o push-doc
           nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
+          # https://github.com/netlify/cli/issues/1809
+          cp -r --dereference ./result ./dist
         if: matrix.name == 'Nix Linux'
       - name: Push to Cachix
         run: |
@@ -95,13 +97,35 @@ jobs:
         run: |
           rm -rf nix-store-cache || true
           nix copy ./push-* --to file://$PWD/nix-store-cache?compression=none
-      - name: Publish manual
+      - name: Publish manual to GH Pages
         uses: peaceiris/actions-gh-pages@v3
         with:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           publish_dir: ./result
           destination_dir: ./doc
         if: matrix.name == 'Nix Linux' && github.ref == 'refs/heads/master' && github.event_name == 'push'
+      - id: deploy-info
+        name: Compute Deployment Metadata
+        run: |
+          set -e
+          python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
+          echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
+      - name: Publish manual to Netlify
+        uses: nwtgck/actions-netlify@v2.0
+        with:
+          publish-dir: ./dist
+          production-branch: master
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          deploy-message: |
+            ${{ github.event_name == 'pull_request' && format('pr#{0}: {1}', github.event.number, github.event.pull_request.title) || format('ref/{0}: {1}', github.ref_name, steps.deploy-info.outputs.message) }}
+          alias: ${{ steps.deploy-info.outputs.alias }}
+          enable-commit-comment: false
+          enable-pull-request-comment: false
+          github-deployment-environment: "lean-lang.org/lean4/doc"
+          fails-without-credentials: false
+        env:
+          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
+          NETLIFY_SITE_ID: "b8e805d2-7e9b-4f80-91fb-a84d72fc4a68"
       - name: Fixup CCache Cache
         run: |
           sudo chown -R $USER /nix/var/cache

.github/workflows/pr-release.yml

@@ -82,11 +82,14 @@ jobs:
             })
 
       # 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: |
-          git ls-remote https://github.com/leanprover/lean4-nightly.git 'refs/tags/nightly-*' --sort version:refname |tail -n1| sed 's,.*refs/tags/nightly-,MOST_RECENT_NIGHTLY=,' >> $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 != '' }}
@@ -97,8 +100,8 @@ jobs:
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: ready
         run: |
-          echo "Most recent nightly: $MOST_RECENT_NIGHTLY"
-          NIGHTLY_SHA=$(git ls-remote https://github.com/leanprover/lean4-nightly.git "nightly-$MOST_RECENT_NIGHTLY"|cut -f1)
+          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 -C lean4.git merge-base origin/master "${{ steps.workflow-info.outputs.sourceHeadSha }}")
           echo "SHA of merge-base: $MERGE_BASE_SHA"

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,11 @@ 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.:
@@ -36,6 +44,51 @@ v4.5.0 (development in progress)
   +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/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/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/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.
 

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

@@ -23,4 +23,5 @@ import Init.NotationExtra
 import Init.SimpLemmas
 import Init.Hints
 import Init.Conv
+import Init.Simproc
 import Init.SizeOfLemmas

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/Fin/Basic.lean

@@ -100,7 +100,7 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
-instance : OfNat (Fin (no_index (n+1))) i where
+instance instOfNat : OfNat (Fin (no_index (n+1))) i where
   ofNat := Fin.ofNat i
 
 instance : Inhabited (Fin (no_index (n+1))) where

src/Init/Data/Int/Basic.lean

@@ -49,7 +49,7 @@ attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc
 
 instance : Coe Nat Int := ⟨Int.ofNat⟩
 
-instance : OfNat Int n where
+instance instOfNat : OfNat Int n where
   ofNat := Int.ofNat n
 
 namespace Int

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⟩
 

src/Init/Data/UInt/Basic.lean

@@ -39,7 +39,7 @@ def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
 def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
 def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
 
-instance : OfNat UInt8 n   := ⟨UInt8.ofNat n⟩
+instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
@@ -110,8 +110,7 @@ def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
 def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
 def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
 
-
-instance : OfNat UInt16 n   := ⟨UInt16.ofNat n⟩
+instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
@@ -184,7 +183,7 @@ def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32
 @[extern "lean_uint16_to_uint32"]
 def UInt16.toUInt32 (a : UInt16) : UInt32 := a.toNat.toUInt32
 
-instance : OfNat UInt32 n   := ⟨UInt32.ofNat n⟩
+instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
@@ -244,7 +243,7 @@ def UInt16.toUInt64 (a : UInt16) : UInt64 := a.toNat.toUInt64
 @[extern "lean_uint32_to_uint64"]
 def UInt32.toUInt64 (a : UInt32) : UInt64 := a.toNat.toUInt64
 
-instance : OfNat UInt64 n   := ⟨UInt64.ofNat n⟩
+instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
@@ -322,7 +321,7 @@ def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 def USize.lt (a b : USize) : Prop := a.val < b.val
 def USize.le (a b : USize) : Prop := a.val ≤ b.val
 
-instance : OfNat USize n   := ⟨USize.ofNat n⟩
+instance USize.instOfNat : OfNat USize n := ⟨USize.ofNat n⟩
 instance : Add USize       := ⟨USize.add⟩
 instance : Sub USize       := ⟨USize.sub⟩
 instance : Mul USize       := ⟨USize.mul⟩

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

@@ -95,6 +95,8 @@ structure Config where
   /-- If `unfoldPartialApp := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will unfold even partial applications of `f` when we request `f` to be unfolded. -/
   unfoldPartialApp  : Bool := false
+  /-- If `instances := true`, then calls to `simp` will (try to) simplify instance implicit arguments. -/
+  instances         : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

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

src/Init/SimpLemmas.lean

@@ -10,6 +10,7 @@ import Init.Core
 set_option linter.missingDocs true -- keep it documented
 
 theorem of_eq_true (h : p = True) : p := h ▸ trivial
+theorem of_eq_false (h : p = False) : ¬ p := fun hp => False.elim (h.mp hp)
 
 theorem eq_true (h : p) : p = True :=
   propext ⟨fun _ => trivial, fun _ => h⟩
@@ -84,6 +85,13 @@ 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
+section SimprocHelperLemmas
+set_option simprocs false
+theorem ite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = True) : (if c then a else b) = a := by simp [h]
+theorem ite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} (a b : α) (h : c = False) : (if c then a else b) = b := by simp [h]
+theorem dite_cond_eq_true {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = True) : (dite c t e) = t (of_eq_true h) := by simp [h]
+theorem dite_cond_eq_false {α : Sort u} {c : Prop} {_ : Decidable c} {t : c → α} {e : ¬ c → α} (h : c = False) : (dite c t e) = e (of_eq_false h) := by simp [h]
+end SimprocHelperLemmas
 @[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/Init/Simproc.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.NotationExtra
+
+namespace Lean.Parser
+/--
+A user-defined simplification procedure used by the `simp` tactic, and its variants.
+Here is an example.
+```lean
+simproc reduce_add (_ + _) := fun e => do
+  unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
+  let some n ← getNatValue? (e.getArg! 4) | return none
+  let some m ← getNatValue? (e.getArg! 5) | return none
+  return some (.done { expr := mkNatLit (n+m) })
+```
+The `simp` tactic invokes `reduce_add` whenever it finds a term of the form `_ + _`.
+The simplification procedures are stored in an (imperfect) discrimination tree.
+The procedure should **not** assume the term `e` perfectly matches the given pattern.
+The body of a simplification procedure must have type `Simproc`, which is an alias for
+`Expr → SimpM (Option Step)`.
+You can instruct the simplifier to apply the procedure before its sub-expressions
+have been simplified by using the modifier `↓` before the procedure name. Example.
+```lean
+simproc ↓ reduce_add (_ + _) := fun e => ...
+```
+Simplification procedures can be also scoped or local.
+-/
+syntax (docComment)? attrKind "simproc " (Tactic.simpPre <|> Tactic.simpPost)? ident " (" term ")" " := " term : command
+
+/--
+A user-defined simplification procedure declaration. To activate this procedure in `simp` tactic,
+we must provide it as an argument, or use the command `attribute` to set its `[simproc]` attribute.
+-/
+syntax (docComment)? "simproc_decl " ident " (" term ")" " := " term : command
+
+/--
+A builtin simplification procedure.
+-/
+syntax (docComment)? attrKind "builtin_simproc " (Tactic.simpPre <|> Tactic.simpPost)? ident " (" term ")" " := " term : command
+
+/--
+A builtin simplification procedure declaration.
+-/
+syntax (docComment)? "builtin_simproc_decl " ident " (" term ")" " := " term : command
+
+/--
+Auxiliary command for associating a pattern with a simplification procedure.
+-/
+syntax (name := simprocPattern) "simproc_pattern% " term " => " ident : command
+
+/--
+Auxiliary command for associating a pattern with a builtin simplification procedure.
+-/
+syntax (name := simprocPatternBuiltin) "builtin_simproc_pattern% " term " => " ident : command
+
+namespace Attr
+/--
+Auxiliary attribute for simplification procedures.
+-/
+syntax (name := simprocAttr) "simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+
+/--
+Auxiliary attribute for builtin simplification procedures.
+-/
+syntax (name := simprocBuiltinAttr) "builtin_simproc" (Tactic.simpPre <|> Tactic.simpPost)? : attr
+end Attr
+
+macro_rules
+  | `($[$doc?:docComment]? simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Simp.Simproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? builtin_simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Simp.Simproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      builtin_simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
+    `(simproc_decl $n ($pattern) := $body
+      attribute [$kind simproc $[$pre?]?] $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind builtin_simproc $[$pre?]? $n:ident ($pattern:term) := $body) => do
+    `(builtin_simproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_simproc $[$pre?]?] $n)
+
+end Lean.Parser

src/Init/Tactics.lean

@@ -355,9 +355,9 @@ Using `rw (config := {occs := .pos L}) [e]`,
 where `L : List Nat`, you can control which "occurrences" are rewritten.
 (This option applies to each rule, so usually this will only be used with a single rule.)
 Occurrences count from `1`.
-At the first occurrence, whether allowed or not,
-arguments of the rewrite rule `e` may be instantiated,
+At each allowed occurrence, arguments of the rewrite rule `e` may be instantiated,
 restricting which later rewrites can be found.
+(Disallowed occurrences do not result in instantiation.)
 `{occs := .neg L}` allows skipping specified occurrences.
 -/
 syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
@@ -753,7 +753,7 @@ end Tactic
 
 namespace Attr
 /--
-Theorems tagged with the `simp` attribute are by the simplifier
+Theorems tagged with the `simp` attribute are used by the simplifier
 (i.e., the `simp` tactic, and its variants) to simplify expressions occurring in your goals.
 We call theorems tagged with the `simp` attribute "simp theorems" or "simp lemmas".
 Lean maintains a database/index containing all active simp theorems.

src/Init/WFTactics.lean

@@ -11,7 +11,7 @@ import Init.WF
 /-- Unfold definitions commonly used in well founded relation definitions.
 This is primarily intended for internal use in `decreasing_tactic`. -/
 macro "simp_wf" : tactic =>
-  `(tactic| try simp (config := { unfoldPartialApp := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
+  `(tactic| try simp (config := { unfoldPartialApp := true, instances := true }) [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
 /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
 reasoning after applying lexicographic order lemmas.

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/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/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/Structural/Eqns.lean

@@ -42,7 +42,7 @@ where
       go mvarId
     else if let some mvarId ← whnfReducibleLHS? mvarId then
       go mvarId
-    else match (← simpTargetStar mvarId {}).1 with
+    else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId
       | TacticResultCNM.noChange =>

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 }
 
@@ -169,7 +169,7 @@ private partial def mkProof (declName : Name) (info : EqnInfo) (type : Expr) : M
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else match (← simpTargetStar mvarId { config.dsimp := false }).1 with
+      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

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
 
 
@@ -223,7 +224,7 @@ def SavedLocalContext.run {α} (slc : SavedLocalContext) (k : MetaM α) :
 /-- A `RecCallWithContext` focuses on a single recursive call in a unary predefinition,
 and runs the given action in the context of that call.  -/
 structure RecCallWithContext where
-  /-- Syntax location of reursive call -/
+  /-- Syntax location of recursive call -/
   ref : Syntax
   /-- Function index of caller -/
   caller : Nat
@@ -263,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.
 -/

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

@@ -13,6 +13,7 @@ import Lean.Elab.Tactic.Match
 import Lean.Elab.Tactic.Rewrite
 import Lean.Elab.Tactic.Location
 import Lean.Elab.Tactic.Simp
+import Lean.Elab.Tactic.Simproc
 import Lean.Elab.Tactic.BuiltinTactic
 import Lean.Elab.Tactic.Split
 import Lean.Elab.Tactic.Conv

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/Conv/Simp.lean

@@ -17,9 +17,9 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
     updateLhs result.expr (← result.getProof)
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.simp] def evalSimp : Tactic := fun stx => withMainContext do
-  let { ctx, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
+  let { ctx, simprocs, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
   let lhs ← getLhs
-  let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (discharge? := d?)
+  let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (simprocs := simprocs) (discharge? := d?)
   applySimpResult result
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do

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

@@ -88,7 +88,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.
   | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
   | .dsimp   => return { (← elabDSimpConfigCore optConfig) with }
 
-private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM Meta.SimpTheorems := do
+private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
   if e.isConst then
     let declName := e.constName!
     let info ← getConstInfo declName
@@ -115,7 +115,7 @@ private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (id : Origin) (e
   else
     thms.add id #[] e (post := post) (inv := inv)
 
-private def addSimpTheorem (thms : Meta.SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM Meta.SimpTheorems := do
+private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
   let (levelParams, proof) ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx <| Term.withoutErrToSorry do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
@@ -129,12 +129,14 @@ private def addSimpTheorem (thms : Meta.SimpTheorems) (id : Origin) (stx : Synta
   thms.add id levelParams proof (post := post) (inv := inv)
 
 structure ElabSimpArgsResult where
-  ctx     : Simp.Context
-  starArg : Bool := false
+  ctx      : Simp.Context
+  simprocs : Simprocs
+  starArg  : Bool := false
 
 inductive ResolveSimpIdResult where
   | none
   | expr (e : Expr)
+  | simproc (declName : Name)
   | ext  (ext : SimpExtension)
 
 /--
@@ -142,9 +144,9 @@ inductive ResolveSimpIdResult where
   If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`),
   this option only makes sense for `simp_all` or `*` is used.
 -/
-def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
+def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
   if stx.isNone then
-    return { ctx }
+    return { ctx, simprocs }
   else
     /-
     syntax simpPre := "↓"
@@ -156,6 +158,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
     withMainContext do
       let mut thmsArray := ctx.simpTheorems
       let mut thms      := thmsArray[0]!
+      let mut simprocs  := simprocs
       let mut starArg   := false
       for arg in stx[1].getSepArgs do
         if arg.getKind == ``Lean.Parser.Tactic.simpErase then
@@ -165,7 +168,9 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
             let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
-            if ctx.config.autoUnfold then
+            if (← Simp.isSimproc declName) then
+              simprocs := simprocs.erase declName
+            else if ctx.config.autoUnfold then
               thms := thms.eraseCore (.decl declName)
             else
               thms ← thms.erase (.decl declName)
@@ -177,11 +182,12 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
               arg[0][0].getKind == ``Parser.Tactic.simpPost
           let inv  := !arg[1].isNone
           let term := arg[2]
-
           match (← resolveSimpIdTheorem? term) with
           | .expr e  =>
             let name ← mkFreshId
             thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
+          | .simproc declName =>
+            simprocs ← simprocs.add declName post
           | .ext ext =>
             thmsArray := thmsArray.push (← ext.getTheorems)
           | .none    =>
@@ -191,8 +197,13 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
           starArg := true
         else
           throwUnsupportedSyntax
-      return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, starArg }
+      return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
 where
+  isSimproc? (e : Expr) : MetaM (Option Name) := do
+    let .const declName _ := e | return none
+    unless (← Simp.isSimproc declName) do return none
+    return some declName
+
   resolveSimpIdTheorem? (simpArgTerm : Term) : TacticM ResolveSimpIdResult := do
     let resolveExt (n : Name) : TacticM ResolveSimpIdResult := do
       if let some ext ← getSimpExtension? n then
@@ -203,9 +214,16 @@ where
     | `($id:ident) =>
       try
         if let some e ← Term.resolveId? simpArgTerm (withInfo := true) then
-          return .expr e
+          if let some simprocDeclName ← isSimproc? e then
+            return .simproc simprocDeclName
+          else
+            return .expr e
         else
-          resolveExt id.getId.eraseMacroScopes
+          let name := id.getId.eraseMacroScopes
+          if (← Simp.isBuiltinSimproc name) then
+            return .simproc name
+          else
+            resolveExt name
       catch _ =>
         resolveExt id.getId.eraseMacroScopes
     | _ =>
@@ -218,6 +236,7 @@ where
 
 structure MkSimpContextResult where
   ctx              : Simp.Context
+  simprocs         : Simprocs
   dischargeWrapper : Simp.DischargeWrapper
 
 /--
@@ -238,8 +257,9 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
     simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
   else
     getSimpTheorems
+  let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := simprocs) {
     config      := (← elabSimpConfig stx[1] (kind := kind))
     simpTheorems := #[simpTheorems], congrTheorems
   }
@@ -247,6 +267,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
     return { r with dischargeWrapper }
   else
     let ctx := r.ctx
+    let simprocs := r.simprocs
     let mut simpTheorems := ctx.simpTheorems
     /-
     When using `zeta := false`, we do not expand let-declarations when using `[*]`.
@@ -257,7 +278,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
       unless simpTheorems.isErased (.fvar h) do
         simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
     let ctx := { ctx with simpTheorems }
-    return { ctx, dischargeWrapper }
+    return { ctx, simprocs, dischargeWrapper }
 
 register_builtin_option tactic.simp.trace : Bool := {
   defValue := false
@@ -281,12 +302,21 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
   let env ← getEnv
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
-    | .decl declName inv => -- global definitions in the environment
+    | .decl declName post inv => -- global definitions in the environment
       if env.contains declName && (inv || !simpOnlyBuiltins.contains declName) then
-        args := args.push (if inv then
-          (← `(Parser.Tactic.simpLemma| ← $(mkIdent (← unresolveNameGlobal declName)):ident))
-        else
-          (← `(Parser.Tactic.simpLemma| $(mkIdent (← unresolveNameGlobal declName)):ident)))
+        let decl : Term ← `($(mkIdent (← unresolveNameGlobal declName)):ident)
+        let arg ← match post, inv with
+          | true,  true  => `(Parser.Tactic.simpLemma| ← $decl:term)
+          | true,  false => `(Parser.Tactic.simpLemma| $decl:term)
+          | false, true  => `(Parser.Tactic.simpLemma| ↓ ← $decl:term)
+          | false, false => `(Parser.Tactic.simpLemma| ↓ $decl:term)
+        args := args.push arg
+      else if (← Simp.isBuiltinSimproc declName) then
+        let decl := mkIdent declName
+        let arg ← match post with
+          | true  => `(Parser.Tactic.simpLemma| $decl:term)
+          | false => `(Parser.Tactic.simpLemma| ↓ $decl:term)
+        args := args.push arg
     | .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
@@ -331,7 +361,7 @@ For many tactics other than the simplifier,
 one should use the `withLocation` tactic combinator
 when working with a `location`.
 -/
-def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
+def simpLocation (ctx : Simp.Context) (simprocs : Simprocs) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -343,7 +373,7 @@ def simpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := non
 where
   go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, usedSimps) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some (_, mvarId) => replaceMainGoal [mvarId]
@@ -353,15 +383,15 @@ where
   "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
 -/
 @[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
-  let { ctx, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
+  let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
   let usedSimps ← dischargeWrapper.with fun discharge? =>
-    simpLocation ctx discharge? (expandOptLocation stx[5])
+    simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
   if tactic.simp.trace.get (← getOptions) then
     traceSimpCall stx usedSimps
 
 @[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
-  let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
-  let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
+  let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
+  let (result?, usedSimps) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
   match result? with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [mvarId]

src/Lean/Elab/Tactic/Simproc.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Elab.Binders
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Term
+import Lean.Elab.Command
+
+namespace Lean.Elab
+
+open Lean Meta Simp
+
+def elabSimprocPattern (stx : Syntax) : MetaM Expr := do
+  let go : TermElabM Expr := do
+    let pattern ← Term.elabTerm stx none
+    Term.synthesizeSyntheticMVars
+    return pattern
+  go.run'
+
+def elabSimprocKeys (stx : Syntax) : MetaM (Array Meta.SimpTheoremKey) := do
+  let pattern ← elabSimprocPattern stx
+  DiscrTree.mkPath pattern simpDtConfig
+
+def checkSimprocType (declName : Name) : CoreM Unit := do
+  let decl ← getConstInfo declName
+  match decl.type with
+  | .const ``Simproc _ => pure ()
+  | _ => throwError "unexpected type at '{declName}', 'Simproc' expected"
+
+namespace Command
+
+@[builtin_command_elab Lean.Parser.simprocPattern] def elabSimprocPattern : CommandElab := fun stx => do
+  let `(simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  let declName ← resolveGlobalConstNoOverload declName
+  liftTermElabM do
+    checkSimprocType declName
+    let keys ← elabSimprocKeys pattern
+    registerSimproc declName keys
+
+@[builtin_command_elab Lean.Parser.simprocPatternBuiltin] def elabSimprocPatternBuiltin : CommandElab := fun stx => do
+  let `(builtin_simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  let declName ← resolveGlobalConstNoOverload declName
+  liftTermElabM do
+    checkSimprocType declName
+    let keys ← elabSimprocKeys pattern
+    let val := mkAppN (mkConst ``registerBuiltinSimproc) #[toExpr declName, toExpr keys, mkConst declName]
+    let initDeclName ← mkFreshUserName (declName ++ `declare)
+    declareBuiltin initDeclName val
+
+end Command
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `simprocAttr
+    descr           := "Simplification procedure"
+    erase           := eraseSimprocAttr
+    add             := fun declName stx attrKind => do
+      let go : MetaM Unit := do
+        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+        addSimprocAttr declName attrKind post
+      go.run' {}
+    applicationTime := AttributeApplicationTime.afterCompilation
+  }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `simprocBuiltinAttr
+    descr           := "Builtin simplification procedure"
+    erase           := eraseSimprocAttr
+    add             := fun declName stx _ => do
+      let go : MetaM Unit := do
+        let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
+        let val := mkAppN (mkConst ``addSimprocBuiltinAttr) #[toExpr declName, toExpr post, mkConst declName]
+        let initDeclName ← mkFreshUserName (declName ++ `declare)
+        declareBuiltin initDeclName val
+      go.run' {}
+    applicationTime := AttributeApplicationTime.afterCompilation
+  }
+
+end Lean.Elab

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

@@ -421,20 +421,20 @@ where
       vs.push v
 termination_by loop i => vs.size - i
 
-private partial def insertAux [BEq α] (keys : Array Key) (v : α) (config : WhnfCoreConfig) : Nat → Trie α → Trie α
+private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
   | i, .node vs cs =>
     if h : i < keys.size then
       let k := keys.get ⟨i, h⟩
       let c := Id.run $ cs.binInsertM
           (fun a b => a.1 < b.1)
-          (fun ⟨_, s⟩ => let c := insertAux keys v config (i+1) s; (k, c)) -- merge with existing
+          (fun ⟨_, s⟩ => let c := insertAux keys v (i+1) s; (k, c)) -- merge with existing
           (fun _ => let c := createNodes keys v (i+1); (k, c))
           (k, default)
       .node vs c
     else
       .node (insertVal vs v) cs
 
-def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) (config : WhnfCoreConfig) : DiscrTree α :=
+def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
   if keys.isEmpty then panic! "invalid key sequence"
   else
     let k := keys[0]!
@@ -443,12 +443,12 @@ def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) (config :
       let c := createNodes keys v 1
       { root := d.root.insert k c }
     | some c =>
-      let c := insertAux keys v config 1 c
+      let c := insertAux keys v 1 c
       { root := d.root.insert k c }
 
 def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) : MetaM (DiscrTree α) := do
   let keys ← mkPath e config
-  return d.insertCore keys v config
+  return d.insertCore keys v
 
 private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
   let e ← reduceDT e root config

src/Lean/Meta/DiscrTreeTypes.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Expr
+import Lean.ToExpr
 
 namespace Lean.Meta
 
@@ -34,6 +35,17 @@ protected def Key.hash : Key → UInt64
 
 instance : Hashable Key := ⟨Key.hash⟩
 
+instance : ToExpr Key where
+  toTypeExpr := mkConst ``Key
+  toExpr k   := match k with
+   | .const n a => mkApp2 (mkConst ``Key.const) (toExpr n) (toExpr a)
+   | .fvar id a => mkApp2 (mkConst ``Key.fvar) (toExpr id) (toExpr a)
+   | .lit l => mkApp (mkConst ``Key.lit) (toExpr l)
+   | .star => mkConst ``Key.star
+   | .other => mkConst ``Key.other
+   | .arrow => mkConst ``Key.arrow
+   | .proj n i a => mkApp3 (mkConst ``Key.proj) (toExpr n) (toExpr i) (toExpr a)
+
 /--
 Discrimination tree trie. See `DiscrTree`.
 -/

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

@@ -76,8 +76,8 @@ def tcDtConfig : WhnfCoreConfig := {}
 
 def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances :=
   match e.globalName? with
-  | some n => { d with discrTree := d.discrTree.insertCore e.keys e tcDtConfig, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n }
-  | none   => { d with discrTree := d.discrTree.insertCore e.keys e tcDtConfig }
+  | some n => { d with discrTree := d.discrTree.insertCore e.keys e, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n }
+  | none   => { d with discrTree := d.discrTree.insertCore e.keys e }
 
 def Instances.eraseCore (d : Instances) (declName : Name) : Instances :=
   { d with erased := d.erased.insert declName, instanceNames := d.instanceNames.erase declName }

src/Lean/Meta/KAbstract.lean

@@ -16,9 +16,11 @@ By default, all occurrences are abstracted,
 but this behavior can be controlled using the `occs` parameter.
 
 All matches of `p` in `e` are considered for occurrences,
-but at the first match (whether included in the occurrences or not)
+but for each match that is included by the `occs` parameter,
 metavariables appearing in `p` (or `e`) may become instantiated,
 affecting the possibility of subsequent matches.
+For matches that are not included in the `occs` parameter, the metavariable context is rolled back
+to prevent blocking subsequent matches which require different instantiations.
 -/
 def kabstract (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr := do
   let e ← instantiateMVars e
@@ -41,15 +43,22 @@ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr :=
         visitChildren ()
       else if e.toHeadIndex != pHeadIdx || e.headNumArgs != pNumArgs then
         visitChildren ()
-      else if (← isDefEq e p) then
-        let i ← get
-        set (i+1)
-        if occs.contains i then
-          return mkBVar offset
+      else
+        -- We save the metavariable context here,
+        -- so that it can be rolled back unless `occs.contains i`.
+        let mctx ← getMCtx
+        if (← isDefEq e p) then
+          let i ← get
+          set (i+1)
+          if occs.contains i then
+            return mkBVar offset
+          else
+            -- Revert the metavariable context,
+            -- so that other matches are still possible.
+            setMCtx mctx
+            visitChildren ()
         else
           visitChildren ()
-      else
-        visitChildren ()
     visit e 0 |>.run' 1
 
 end Lean.Meta

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

@@ -37,7 +37,7 @@ where
       let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
       let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
       -- TODO: we only need the `sizeOf` simp theorems
-      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] }).1 with
+      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] } {}).1 with
       | some _ => return false
       | none   =>
         let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)

src/Lean/Meta/Tactic/Simp.lean

@@ -9,6 +9,8 @@ import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Simp.SimpAll
+import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 
 namespace Lean
 

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

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean

@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.Simproc
+
+open Lean Meta Simp
+
+builtin_simproc ↓ reduceIte (ite _ _ _) := fun e => OptionT.run do
+  guard (e.isAppOfArity ``ite 5)
+  let c := e.getArg! 1
+  let r ← simp c
+  if r.expr.isConstOf ``True then
+    let eNew  := e.getArg! 3
+    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
+    return .visit { expr := eNew, proof? := pr }
+  if r.expr.isConstOf ``False then
+    let eNew  := e.getArg! 4
+    let pr    := mkApp (mkAppN (mkConst ``ite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) (← r.getProof)
+    return .visit { expr := eNew, proof? := pr }
+  failure
+
+builtin_simproc ↓ reduceDite (dite _ _ _) := fun e => OptionT.run do
+  guard (e.isAppOfArity ``dite 5)
+  let c := e.getArg! 1
+  let r ← simp c
+  if r.expr.isConstOf ``True then
+    let pr    ← r.getProof
+    let h     := mkApp2 (mkConst ``of_eq_true) c pr
+    let eNew  := mkApp (e.getArg! 3) h |>.headBeta
+    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_true e.getAppFn.constLevels!) e.getAppArgs) pr
+    return .visit { expr := eNew, proof? := prNew }
+  if r.expr.isConstOf ``False then
+    let pr    ← r.getProof
+    let h     := mkApp2 (mkConst ``of_eq_false) c pr
+    let eNew  := mkApp (e.getArg! 4) h |>.headBeta
+    let prNew := mkApp (mkAppN (mkConst ``dite_cond_eq_false e.getAppFn.constLevels!) e.getAppArgs) pr
+    return .visit { expr := eNew, proof? := prNew }
+  failure

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.ToExpr
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+namespace Fin
+open Lean Meta Simp
+
+structure Value where
+  ofNatFn   : Expr
+  size      : Nat
+  value     : Nat
+
+def fromExpr? (e : Expr) : OptionT SimpM Value := do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isAppOfArity ``Fin 1)
+  let size ← Nat.fromExpr? type.appArg!
+  guard (size > 0)
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let value := value % size
+  return { size, value, ofNatFn := e.appFn!.appFn! }
+
+def Value.toExpr (v : Value) : Expr :=
+  let vExpr := mkRawNatLit v.value
+  mkApp2 v.ofNatFn vExpr (mkApp2 (mkConst ``Fin.instOfNat) (Lean.toExpr (v.size - 1)) vExpr)
+
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let v₁ ← fromExpr? e.appFn!.appArg!
+  let v₂ ← fromExpr? e.appArg!
+  guard (v₁.size == v₂.size)
+  let v := { v₁ with value := op v₁.value v₂.value % v₁.size }
+  return .done { expr := v.toExpr }
+
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let v₁ ← fromExpr? e.appFn!.appArg!
+  let v₂ ← fromExpr? e.appArg!
+  let d ← mkDecide e
+  if op v₁.value v₂.value then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+
+/-
+The following code assumes users did not override the `Fin n` instances for the arithmetic operators.
+If they do, they must disable the following `simprocs`.
+-/
+
+builtin_simproc reduceAdd ((_ + _ : Fin _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_simproc reduceMul ((_ * _ : Fin _)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_simproc reduceSub ((_ - _ : Fin _)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_simproc reduceDiv ((_ / _ : Fin _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_simproc reduceMod ((_ % _ : Fin _)) := reduceBin ``HMod.hMod 6 (· % ·)
+
+builtin_simproc reduceLT  (( _ : Fin _) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc reduceLE  (( _ : Fin _) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc reduceGT  (( _ : Fin _) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc reduceGE  (( _ : Fin _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+
+end Fin

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.ToExpr
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+namespace Int
+open Lean Meta Simp
+
+def fromExpr? (e : Expr) : OptionT SimpM Int := do
+  let mut e := e
+  let mut isNeg := false
+  if e.isAppOfArity ``Neg.neg 3 then
+    e := e.appArg!
+    isNeg := true
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isConstOf ``Int)
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let mut value : Int := value
+  if isNeg then value := - value
+  return value
+
+def toExpr (v : Int) : Expr :=
+  let n := v.natAbs
+  let r := mkRawNatLit n
+  let e := mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Int) r (mkApp (mkConst ``instOfNat) r)
+  if v < 0 then
+    mkAppN (mkConst ``Neg.neg [levelZero]) #[mkConst ``Int, mkConst ``instNegInt, e]
+  else
+    e
+
+@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Int → Int) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let n ← fromExpr? e.appArg!
+  return .done { expr := toExpr (op n) }
+
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Int → Int → Int) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let v₁ ← fromExpr? e.appFn!.appArg!
+  let v₂ ← fromExpr? e.appArg!
+  return .done { expr := toExpr (op v₁ v₂) }
+
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : OptionT SimpM Step := OptionT.run do
+  guard (e.isAppOfArity declName arity)
+  let v₁ ← fromExpr? e.appFn!.appArg!
+  let v₂ ← fromExpr? e.appArg!
+  let d ← mkDecide e
+  if op v₁ v₂ then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+
+/-
+The following code assumes users did not override the `Int` instances for the arithmetic operators.
+If they do, they must disable the following `simprocs`.
+-/
+
+builtin_simproc reduceNeg ((- _ : Int)) := fun e => OptionT.run do
+  guard (e.isAppOfArity ``Neg.neg 3)
+  let v ← fromExpr? e.appArg!
+  guard (v < 0)
+  return .done { expr := toExpr (- v) }
+
+builtin_simproc reduceAdd ((_ + _ : Int)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_simproc reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_simproc reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_simproc reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_simproc reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
+
+builtin_simproc reducePow ((_ : Int) ^ (_ : Nat)) := fun e => OptionT.run do
+  guard (e.isAppOfArity ``HPow.hPow 6)
+  let v₁ ← fromExpr? e.appFn!.appArg!
+  let v₂ ← Nat.fromExpr? e.appArg!
+  return .done { expr := toExpr (v₁ ^ v₂) }
+
+builtin_simproc reduceAbs (natAbs _) := fun e => OptionT.run do
+  guard (e.isAppOfArity ``natAbs 1)
+  let v ← fromExpr? e.appArg!
+  return .done { expr := mkNatLit (natAbs v) }
+
+builtin_simproc reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc reduceLE  (( _ : Int) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc reduceGT  (( _ : Int) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc reduceGE  (( _ : Int) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+
+end Int

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Offset
+import Lean.Meta.Tactic.Simp.Simproc
+
+namespace Nat
+open Lean Meta Simp
+
+def fromExpr? (e : Expr) : SimpM (Option Nat) := do
+  let some n ← evalNat e |>.run | return none
+  return n
+
+@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let n ← fromExpr? e.appArg!
+  return .done { expr := mkNatLit (op n) }
+
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let n ← fromExpr? e.appFn!.appArg!
+  let m ← fromExpr? e.appArg!
+  return .done { expr := mkNatLit (op n m) }
+
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let n ← fromExpr? e.appFn!.appArg!
+  let m ← fromExpr? e.appArg!
+  let d ← mkDecide e
+  if op n m then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+
+builtin_simproc reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
+
+/-
+The following code assumes users did not override the `Nat` instances for the arithmetic operators.
+If they do, they must disable the following `simprocs`.
+-/
+
+builtin_simproc reduceAdd ((_ + _ : Nat)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_simproc reduceMul ((_ * _ : Nat)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_simproc reduceSub ((_ - _ : Nat)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_simproc reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_simproc reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_simproc reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPow 6 (· ^ ·)
+builtin_simproc reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
+
+builtin_simproc reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc reduceLE  (( _ : Nat) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc reduceGE  (( _ : Nat) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+
+end Nat

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+open Lean Meta Simp
+
+macro "declare_uint_simprocs" typeName:ident : command =>
+let ofNat := typeName.getId ++ `ofNat
+let fromExpr := mkIdent `fromExpr
+let toExpr := mkIdent `toExpr
+`(
+namespace $typeName
+
+structure Value where
+  ofNatFn : Expr
+  value   : $typeName
+
+def $fromExpr (e : Expr) : OptionT SimpM Value := do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isConstOf $(quote typeName.getId))
+  let value ← Nat.fromExpr? e.appFn!.appArg!
+  let value := $(mkIdent ofNat) value
+  return { value, ofNatFn := e.appFn!.appFn! }
+
+def $toExpr (v : Value) : Expr :=
+  let vExpr := mkRawNatLit v.value.val
+  mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
+
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : $typeName → $typeName → $typeName) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let n ← ($fromExpr e.appFn!.appArg!)
+  let m ← ($fromExpr e.appArg!)
+  let r := { n with value := op n.value m.value }
+  return .done { expr := $toExpr r }
+
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : OptionT SimpM Step := do
+  guard (e.isAppOfArity declName arity)
+  let n ← ($fromExpr e.appFn!.appArg!)
+  let m ← ($fromExpr e.appArg!)
+  let d ← mkDecide e
+  if op n.value m.value then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+
+builtin_simproc $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_simproc $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_simproc $(mkIdent `reduceSub):ident ((_ - _ : $typeName)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_simproc $(mkIdent `reduceDiv):ident ((_ / _ : $typeName)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_simproc $(mkIdent `reduceMod):ident ((_ % _ : $typeName)) := reduceBin ``HMod.hMod 6 (· % ·)
+
+builtin_simproc $(mkIdent `reduceLT):ident  (( _ : $typeName) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc $(mkIdent `reduceLE):ident  (( _ : $typeName) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc $(mkIdent `reduceGT):ident  (( _ : $typeName) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc $(mkIdent `reduceGE):ident  (( _ : $typeName) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+
+end $typeName
+)
+
+declare_uint_simprocs UInt8
+declare_uint_simprocs UInt16
+declare_uint_simprocs UInt32
+declare_uint_simprocs UInt64
+declare_uint_simprocs USize

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

@@ -7,8 +7,10 @@ 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
+import Lean.Meta.Tactic.Simp.Simproc
 
 namespace Lean.Meta.Simp
 
@@ -108,19 +110,11 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf
   extraArgs := extraArgs.reverse
   match (← go e) with
   | none => return none
-  | some { expr := eNew, proof? := none, .. } =>
-    if (← hasAssignableMVar eNew) then
+  | some r =>
+    if (← hasAssignableMVar r.expr) then
       trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, resulting expression has unassigned metavariables"
       return none
-    return some { expr := mkAppN eNew extraArgs }
-  | some { expr := eNew, proof? := some proof, .. } =>
-    let mut proof := proof
-    for extraArg in extraArgs do
-      proof ← mkCongrFun proof extraArg
-    if (← hasAssignableMVar eNew) then
-      trace[Meta.Tactic.simp.rewrite] "{← ppSimpTheorem thm}, resulting expression has unassigned metavariables"
-      return none
-    return some { expr := mkAppN eNew extraArgs, proof? := some proof }
+    r.addExtraArgs extraArgs
 
 def tryTheoremWithExtraArgs? (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Result) :=
   withNewMCtxDepth do
@@ -148,18 +142,6 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt
       else
         return none
 
-/--
-Return a WHNF configuration for retrieving `[simp]` from the discrimination tree.
-If user has disabled `zeta` and/or `beta` reduction in the simplifier, we must also
-disable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281
--/
-def getDtConfig (cfg : Config) : WhnfCoreConfig :=
-  match cfg.beta, cfg.zeta with
-  | true, true => simpDtConfig
-  | true, false => { simpDtConfig with zeta := false }
-  | false, true => { simpDtConfig with beta := false }
-  | false, false => { simpDtConfig with beta := false, zeta := false }
-
 /--
 Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
 -/
@@ -180,6 +162,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
@@ -227,7 +216,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
@@ -235,12 +224,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 ()
@@ -248,33 +273,151 @@ 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 preSimproc?
+  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 postSimproc?
   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 (simprocs : Simprocs) (discharge? : Discharge) : Methods := {
+  pre        := (preDefault · discharge?)
+  post       := (postDefault · discharge?)
+  discharge? := discharge?
+  simprocs   := simprocs
+}
+
+def mkDefaultMethodsCore (simprocs : Simprocs) : Methods :=
+  mkMethods simprocs dischargeDefault?
+
+def mkDefaultMethods : CoreM Methods := do
+  if simprocs.get (← getOptions) then
+    return mkDefaultMethodsCore (← getSimprocs)
+  else
+    return mkDefaultMethodsCore {}
+
 end Lean.Meta.Simp

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

@@ -27,6 +27,7 @@ structure State where
   mvarId    : MVarId
   entries   : Array Entry := #[]
   ctx       : Simp.Context
+  simprocs  : Simprocs
   usedSimps : UsedSimps := {}
 
 abbrev M := StateRefT State MetaM
@@ -52,6 +53,7 @@ private abbrev getSimpTheorems : M SimpTheoremsArray :=
 
 private partial def loop : M Bool := do
   modify fun s => { s with modified := false }
+  let simprocs := (← get).simprocs
   -- simplify entries
   for i in [:(← get).entries.size] do
     let entry := (← get).entries[i]!
@@ -59,7 +61,7 @@ private partial def loop : M Bool := do
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
     let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
-    let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx (usedSimps := (← get).usedSimps)
+    let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (usedSimps := (← get).usedSimps)
     modify fun s => { s with usedSimps }
     match r with
     | none => return true -- closed the goal
@@ -99,7 +101,7 @@ private partial def loop : M Bool := do
         }
   -- simplify target
   let mvarId := (← get).mvarId
-  let (r, usedSimps) ← simpTarget mvarId (← get).ctx (usedSimps := (← get).usedSimps)
+  let (r, usedSimps) ← simpTarget mvarId (← get).ctx simprocs (usedSimps := (← get).usedSimps)
   modify fun s => { s with usedSimps }
   match r with
   | none => return true
@@ -140,9 +142,9 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {}) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   mvarId.withContext do
-    let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps }
+    let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
     if let .some mvarIdNew := r then
       if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
         throwError "simp_all made no progress"

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

@@ -18,7 +18,7 @@ what action the user took which lead to this theorem existing in the simp set.
 -/
 inductive Origin where
   /-- A global declaration in the environment. -/
-  | decl (declName : Name) (inv := false)
+  | decl (declName : Name) (post := true) (inv := false)
   /--
   A local hypothesis.
   When `contextual := true` is enabled, this fvar may exist in an extension
@@ -42,7 +42,7 @@ inductive Origin where
 
 /-- A unique identifier corresponding to the origin. -/
 def Origin.key : Origin → Name
-  | .decl declName _ => declName
+  | .decl declName _ _ => declName
   | .fvar fvarId => fvarId.name
   | .stx id _ => id
   | .other name => name
@@ -137,7 +137,13 @@ instance : ToFormat SimpTheorem where
     name ++ prio ++ perm
 
 def ppOrigin [Monad m] [MonadEnv m] [MonadError m] : Origin → m MessageData
-  | .decl n inv => do let r ← mkConstWithLevelParams n; if inv then return m!"← {r}" else return r
+  | .decl n post inv => do
+    let r ← mkConstWithLevelParams n;
+    match post, inv with
+    | true,  true  => return m!"← {r}"
+    | true,  false => return r
+    | false, true  => return m!"↓ ← {r}"
+    | false, false => return m!"↓ {r}"
   | .fvar n => return mkFVar n
   | .stx _ ref => return ref
   | .other n => return n
@@ -171,9 +177,9 @@ def simpDtConfig : WhnfCoreConfig := { iota := false, proj := .no }
 
 def addSimpTheoremEntry (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems :=
   if e.post then
-    { d with post := d.post.insertCore e.keys e simpDtConfig, lemmaNames := updateLemmaNames d.lemmaNames }
+    { d with post := d.post.insertCore e.keys e, lemmaNames := updateLemmaNames d.lemmaNames }
   else
-    { d with pre := d.pre.insertCore e.keys e simpDtConfig, lemmaNames := updateLemmaNames d.lemmaNames }
+    { d with pre := d.pre.insertCore e.keys e, lemmaNames := updateLemmaNames d.lemmaNames }
 where
   updateLemmaNames (s : PHashSet Origin) : PHashSet Origin :=
     s.insert e.origin
@@ -201,10 +207,11 @@ def SimpTheorems.registerDeclToUnfoldThms (d : SimpTheorems) (declName : Name) (
 
 partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpTheorems :=
   let d := { d with erased := d.erased.insert thmId, lemmaNames := d.lemmaNames.erase thmId }
-  if let .decl declName := thmId then
+  if let .decl declName .. := thmId then
     let d := { d with toUnfold := d.toUnfold.erase declName }
     if let some thms := d.toUnfoldThms.find? declName then
-      thms.foldl (init := d) (eraseCore · <| .decl ·)
+      let dummy := true
+      thms.foldl (init := d) (eraseCore · <| .decl · dummy dummy)
     else
       d
   else
@@ -213,7 +220,7 @@ partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpThe
 def SimpTheorems.erase [Monad m] [MonadError m] (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
   unless d.isLemma thmId ||
     match thmId with
-    | .decl declName => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
+    | .decl declName .. => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
     | _ => false
   do
     throwError "'{thmId.key}' does not have [simp] attribute"
@@ -333,10 +340,10 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
       let mut r := #[]
       for (val, type) in (← preprocess val type inv (isGlobal := true)) do
         let auxName ← mkAuxLemma cinfo.levelParams type val
-        r := r.push <| (← mkSimpTheoremCore (.decl declName inv) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio)
+        r := r.push <| (← mkSimpTheoremCore (.decl declName post inv) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio)
       return r
     else
-      return #[← mkSimpTheoremCore (.decl declName) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio]
+      return #[← mkSimpTheoremCore (.decl declName post inv) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio]
 
 inductive SimpEntry where
   | thm      : SimpTheorem → SimpEntry
@@ -418,7 +425,7 @@ def getSimpTheorems : CoreM SimpTheorems :=
 
 /-- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure. -/
 def SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do
-  let s := { s with erased := s.erased.erase (.decl declName inv) }
+  let s := { s with erased := s.erased.erase (.decl declName post inv) }
   let simpThms ← mkSimpTheoremsFromConst declName post inv prio
   return simpThms.foldl addSimpTheoremEntry s
 

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

@@ -0,0 +1,198 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.ScopedEnvExtension
+import Lean.Meta.DiscrTree
+import Lean.Meta.Tactic.Simp.Types
+
+namespace Lean.Meta.Simp
+
+structure BuiltinSimprocs where
+  keys  : HashMap Name (Array SimpTheoremKey) := {}
+  procs : HashMap Name Simproc := {}
+  deriving Inhabited
+
+builtin_initialize builtinSimprocDeclsRef : IO.Ref BuiltinSimprocs ← IO.mkRef {}
+
+structure SimprocDecl where
+  declName : Name
+  keys     : Array SimpTheoremKey
+  deriving Inhabited
+
+structure SimprocDeclExtState where
+  builtin    : HashMap Name (Array SimpTheoremKey)
+  newEntries : PHashMap Name (Array SimpTheoremKey) := {}
+  deriving Inhabited
+
+def SimprocDecl.lt (decl₁ decl₂ : SimprocDecl) : Bool :=
+  Name.quickLt decl₁.declName decl₂.declName
+
+builtin_initialize simprocDeclExt : PersistentEnvExtension SimprocDecl SimprocDecl SimprocDeclExtState ←
+  registerPersistentEnvExtension {
+    mkInitial       := return { builtin := (← builtinSimprocDeclsRef.get).keys }
+    addImportedFn   := fun _ => return { builtin := (← builtinSimprocDeclsRef.get).keys }
+    addEntryFn      := fun s d => { s with newEntries := s.newEntries.insert d.declName d.keys }
+    exportEntriesFn := fun s =>
+      let result := s.newEntries.foldl (init := #[]) fun result declName keys => result.push { declName, keys }
+      result.qsort SimprocDecl.lt
+  }
+
+def getSimprocDeclKeys? (declName : Name) : CoreM (Option (Array SimpTheoremKey)) := do
+  let env ← getEnv
+  let keys? ← match env.getModuleIdxFor? declName with
+    | some modIdx => do
+      let some decl := (simprocDeclExt.getModuleEntries env modIdx).binSearch { declName, keys := #[] } SimprocDecl.lt
+        | pure none
+      pure (some decl.keys)
+    | none        => pure ((simprocDeclExt.getState env).newEntries.find? declName)
+  if let some keys := keys? then
+    return some keys
+  else
+    return (simprocDeclExt.getState env).builtin.find? declName
+
+def isBuiltinSimproc (declName : Name) : CoreM Bool := do
+  let s := simprocDeclExt.getState (← getEnv)
+  return s.builtin.contains declName
+
+def isSimproc (declName : Name) : CoreM Bool :=
+  return (← getSimprocDeclKeys? declName).isSome
+
+def registerBuiltinSimproc (declName : Name) (key : Array SimpTheoremKey) (proc : Simproc) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError s!"invalid builtin simproc declaration, it can only be registered during initialization")
+  if (← builtinSimprocDeclsRef.get).keys.contains declName then
+    throw (IO.userError s!"invalid builtin simproc declaration '{declName}', it has already been declared")
+  builtinSimprocDeclsRef.modify fun { keys, procs } =>
+    { keys := keys.insert declName key, procs := procs.insert declName proc }
+
+def registerSimproc (declName : Name) (keys : Array SimpTheoremKey) : CoreM Unit := do
+  let env ← getEnv
+  unless (env.getModuleIdxFor? declName).isNone do
+    throwError "invalid simproc declaration '{declName}', function declaration is in an imported module"
+  if (← isSimproc declName) then
+    throwError "invalid simproc declaration '{declName}', it has already been declared"
+  modifyEnv fun env => simprocDeclExt.modifyState env fun s => { s with newEntries := s.newEntries.insert declName keys }
+
+instance : BEq SimprocEntry where
+  beq e₁ e₂ := e₁.declName == e₂.declName
+
+instance : ToFormat SimprocEntry where
+  format e := format e.declName
+
+def Simprocs.erase (s : Simprocs) (declName : Name) : Simprocs :=
+  { s with erased := s.erased.insert declName, simprocNames := s.simprocNames.erase declName }
+
+builtin_initialize builtinSimprocsRef : IO.Ref Simprocs ← IO.mkRef {}
+
+abbrev SimprocExtension := ScopedEnvExtension SimprocOLeanEntry SimprocEntry Simprocs
+
+unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM Simproc := do
+  let ctx ← read
+  match ctx.env.evalConstCheck Simproc ctx.opts ``Lean.Meta.Simp.Simproc declName with
+  | .ok proc  => return proc
+  | .error ex => throw (IO.userError ex)
+
+@[implemented_by getSimprocFromDeclImpl]
+opaque getSimprocFromDecl (declName: Name) : ImportM Simproc
+
+def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do
+  return { toSimprocOLeanEntry := e, proc := (← getSimprocFromDecl e.declName) }
+
+builtin_initialize simprocExtension : SimprocExtension ←
+  registerScopedEnvExtension {
+    name          := `simproc
+    mkInitial     := builtinSimprocsRef.get
+    ofOLeanEntry  := fun _ => toSimprocEntry
+    toOLeanEntry  := fun e => e.toSimprocOLeanEntry
+    addEntry      := fun s e =>
+      if e.post then
+        { s with post := s.post.insertCore e.keys e }
+      else
+        { s with pre := s.pre.insertCore e.keys e }
+  }
+
+def eraseSimprocAttr (declName : Name) : AttrM Unit := do
+  let s := simprocExtension.getState (← getEnv)
+  unless s.simprocNames.contains declName do
+    throwError "'{declName}' does not have [simproc] attribute"
+  modifyEnv fun env => simprocExtension.modifyState env fun s => s.erase declName
+
+def addSimprocAttr (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do
+  let proc ← getSimprocFromDecl declName
+  let some keys ← getSimprocDeclKeys? declName |
+    throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
+  simprocExtension.add { declName, post, keys, proc } kind
+
+def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc) : IO Unit := do
+  let some keys := (← builtinSimprocDeclsRef.get).keys.find? declName |
+    throw (IO.userError "invalid [builtin_simproc] attribute, '{declName}' is not a builtin simproc")
+  if post then
+    builtinSimprocsRef.modify fun s => { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+  else
+    builtinSimprocsRef.modify fun s => { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+
+def getSimprocs : CoreM Simprocs :=
+  return simprocExtension.getState (← getEnv)
+
+def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs := do
+  let proc ←
+    try
+      getSimprocFromDecl declName
+    catch e =>
+      if (← isBuiltinSimproc declName) then
+        let some proc := (← builtinSimprocDeclsRef.get).procs.find? declName
+          | throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
+        pure proc
+      else
+        throw e
+  let some keys ← getSimprocDeclKeys? declName |
+    throwError "invalid [simproc] attribute, '{declName}' is not a simproc"
+  if post then
+    return { s with post := s.post.insertCore keys { declName, keys, post, proc } }
+  else
+    return { s with pre := s.pre.insertCore keys { declName, keys, post, proc } }
+
+def SimprocEntry.try? (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM (Option Step) := do
+  let mut extraArgs := #[]
+  let mut e := e
+  for _ in [:numExtraArgs] do
+    extraArgs := extraArgs.push e.appArg!
+    e := e.appFn!
+  extraArgs := extraArgs.reverse
+  match (← s.proc e) with
+  | none => return none
+  | some step => return some (← step.addExtraArgs extraArgs)
+
+def simproc? (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM (Option Step) := do
+  let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+  if candidates.isEmpty then
+    let tag := if post then "post" else "pre"
+    trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"
+    return none
+  else
+    for (simprocEntry, numExtraArgs) in candidates do
+      unless erased.contains simprocEntry.declName do
+        if let some step ← simprocEntry.try? numExtraArgs e then
+          trace[Debug.Meta.Tactic.simp] "simproc result {e} => {step.result.expr}"
+          recordSimpTheorem (.decl simprocEntry.declName post)
+          return some step
+    return none
+
+register_builtin_option simprocs : Bool := {
+  defValue := true
+  descr    := "Enable/disable `simproc`s (simplification procedures)."
+}
+
+def preSimproc? (e : Expr) : SimpM (Option Step) := do
+  unless simprocs.get (← getOptions) do return none
+  let s := (← getMethods).simprocs
+  simproc? (post := false) s.pre s.erased e
+
+def postSimproc? (e : Expr) : SimpM (Option Step) := do
+  unless simprocs.get (← getOptions) do return none
+  let s := (← getMethods).simprocs
+  simproc? (post := true) s.post s.erased e
+
+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
@@ -58,37 +71,84 @@ def Step.updateResult : Step → Result → Step
   | Step.visit _, r => Step.visit r
   | Step.done _, r  => Step.done r
 
+abbrev Simproc := Expr → SimpM (Option Step)
+
+/--
+`Simproc` .olean entry.
+-/
+structure SimprocOLeanEntry where
+  /-- Name of a declaration stored in the environment which has type `Simproc`. -/
+  declName : Name
+  post     : Bool := true
+  keys     : Array SimpTheoremKey := #[]
+  deriving Inhabited
+
+/--
+`Simproc` entry. It is the .olean entry plus the actual function.
+-/
+structure SimprocEntry extends SimprocOLeanEntry where
+  /--
+  Recall that we cannot store `Simproc` into .olean files because it is a closure.
+  Given `SimprocOLeanEntry.declName`, we convert it into a `Simproc` by using the unsafe function `evalConstCheck`.
+  -/
+  proc : Simproc
+
+abbrev SimprocTree := DiscrTree SimprocEntry
+
+structure Simprocs where
+  pre          : SimprocTree   := DiscrTree.empty
+  post         : SimprocTree   := DiscrTree.empty
+  simprocNames : PHashSet Name := {}
+  erased       : PHashSet Name := {}
+  deriving Inhabited
+
 structure Methods where
   pre        : Expr → SimpM Step          := fun e => return Step.visit { expr := e }
   post       : Expr → SimpM Step          := fun e => return Step.done { expr := e }
   discharge? : Expr → SimpM (Option Expr) := fun _ => return none
+  simprocs   : Simprocs                   := {}
   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 +161,264 @@ 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 config ← getConfig
+    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 h : i < infos.size then
+        let info := infos[i]
+        if !config.instances && info.isInstImplicit then
+          r ← mkCongrFun r arg
+        else if !info.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)
+      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 args := e.getAppArgs
+  let config ← getConfig
+  let infos := (← getFunInfoNArgs f args.size).paramInfo
+  let mut simplified := false
+  let mut hasProof   := false
+  let mut hasCast    := false
+  let mut argsNew    := #[]
+  let mut argResults := #[]
+  let mut i          := 0 -- index at args
+  for arg in args, kind in cgrThm.argKinds do
+    if h : !config.instances ∧ i < infos.size then
+      if (infos[i]'h.2).isInstImplicit then
+        -- Do not visit instance implict argument
+        argsNew := argsNew.push arg
+        i := i + 1
+        continue
+    i := i + 1
+    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 }
+
+/--
+Return a WHNF configuration for retrieving `[simp]` from the discrimination tree.
+If user has disabled `zeta` and/or `beta` reduction in the simplifier, we must also
+disable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281
+-/
+def getDtConfig (cfg : Config) : WhnfCoreConfig :=
+  match cfg.beta, cfg.zeta with
+  | true, true => simpDtConfig
+  | true, false => { simpDtConfig with zeta := false }
+  | false, true => { simpDtConfig with beta := false }
+  | false, false => { simpDtConfig with beta := false, zeta := false }
+
+def Result.addExtraArgs (r : Result) (extraArgs : Array Expr) : MetaM Result := do
+  match r.proof? with
+  | none => return { expr := mkAppN r.expr extraArgs }
+  | some proof =>
+    let mut proof := proof
+    for extraArg in extraArgs do
+      proof ← Meta.mkCongrFun proof extraArg
+    return { expr := mkAppN r.expr extraArgs, proof? := some proof }
+
+def Step.addExtraArgs (s : Step) (extraArgs : Array Expr) : MetaM Step := do
+  match s with
+  | .visit r => return .visit (← r.addExtraArgs extraArgs)
+  | .done r => return .done (← r.addExtraArgs extraArgs)
+
 end Simp
 
-export Simp (SimpM)
+export Simp (SimpM Simprocs)
+
+/--
+  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/Tactic/SplitIf.lean

@@ -82,14 +82,14 @@ open SplitIf
 
 def simpIfTarget (mvarId : MVarId) (useDecide := false) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let (some mvarId', _) ← simpTarget mvarId ctx (discharge? useDecide) (mayCloseGoal := false) then
+  if let (some mvarId', _) ← simpTarget mvarId ctx {} (discharge? useDecide) (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!
 
 def simpIfLocalDecl (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId := do
   let mut ctx ← getSimpContext
-  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx discharge? (mayCloseGoal := false) then
+  if let (some (_, mvarId'), _) ← simpLocalDecl mvarId fvarId ctx {} discharge? (mayCloseGoal := false) then
     return mvarId'
   else
     unreachable!

src/Lean/Meta/UnificationHint.lean

@@ -29,7 +29,7 @@ instance : ToFormat UnificationHints where
 def UnificationHints.config : WhnfCoreConfig := { iota := false, proj := .no }
 
 def UnificationHints.add (hints : UnificationHints) (e : UnificationHintEntry) : UnificationHints :=
-  { hints with discrTree := hints.discrTree.insertCore e.keys e.val config }
+  { hints with discrTree := hints.discrTree.insertCore e.keys e.val }
 
 builtin_initialize unificationHintExtension : SimpleScopedEnvExtension UnificationHintEntry UnificationHints ←
   registerSimpleScopedEnvExtension {

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
@@ -823,12 +827,17 @@ def reduceNative? (e : Expr) : MetaM (Option Expr) :=
   | _ =>
     return none
 
-@[inline] def withNatValue {α} (a : Expr) (k : Nat → MetaM (Option α)) : MetaM (Option α) := do
+@[inline] def withNatValue (a : Expr) (k : Nat → MetaM (Option α)) : MetaM (Option α) := do
+  if !a.hasExprMVar && a.hasFVar then
+    return none
+  let a ← instantiateMVars a
+  if a.hasExprMVar || a.hasFVar then
+    return none
   let a ← whnf a
   match a with
-  | Expr.const `Nat.zero _      => k 0
-  | Expr.lit (Literal.natVal v) => k v
-  | _                           => return none
+  | .const ``Nat.zero _ => k 0
+  | .lit (.natVal v)    => k v
+  | _                   => return none
 
 def reduceUnaryNatOp (f : Nat → Nat) (a : Expr) : MetaM (Option Expr) :=
   withNatValue a fun a =>
@@ -846,27 +855,26 @@ def reduceBinNatPred (f : Nat → Nat → Bool) (a b : Expr) : MetaM (Option Exp
   return toExpr <| f a b
 
 def reduceNat? (e : Expr) : MetaM (Option Expr) :=
-  if e.hasFVar || e.hasMVar then
-    return none
-  else match e with
-    | .app (.const fn _) a                =>
-      if fn == ``Nat.succ then
-        reduceUnaryNatOp Nat.succ a
-      else
-        return none
-    | .app (.app (.const fn _) a1) a2 =>
-      if fn == ``Nat.add then reduceBinNatOp Nat.add a1 a2
-      else if fn == ``Nat.sub then reduceBinNatOp Nat.sub a1 a2
-      else if fn == ``Nat.mul then reduceBinNatOp Nat.mul a1 a2
-      else if fn == ``Nat.div then reduceBinNatOp Nat.div a1 a2
-      else if fn == ``Nat.mod then reduceBinNatOp Nat.mod a1 a2
-      else if fn == ``Nat.pow then reduceBinNatOp Nat.pow a1 a2
-      else if fn == ``Nat.gcd then reduceBinNatOp Nat.gcd a1 a2
-      else if fn == ``Nat.beq then reduceBinNatPred Nat.beq a1 a2
-      else if fn == ``Nat.ble then reduceBinNatPred Nat.ble a1 a2
-      else return none
-    | _ =>
+  match e with
+  | .app (.const fn _) a =>
+    if fn == ``Nat.succ then
+      reduceUnaryNatOp Nat.succ a
+    else
       return none
+  | .app (.app (.const fn _) a1) a2 =>
+    match fn with
+    | ``Nat.add => reduceBinNatOp Nat.add a1 a2
+    | ``Nat.sub => reduceBinNatOp Nat.sub a1 a2
+    | ``Nat.mul => reduceBinNatOp Nat.mul a1 a2
+    | ``Nat.div => reduceBinNatOp Nat.div a1 a2
+    | ``Nat.mod => reduceBinNatOp Nat.mod a1 a2
+    | ``Nat.pow => reduceBinNatOp Nat.pow a1 a2
+    | ``Nat.gcd => reduceBinNatOp Nat.gcd a1 a2
+    | ``Nat.beq => reduceBinNatPred Nat.beq a1 a2
+    | ``Nat.ble => reduceBinNatPred Nat.ble a1 a2
+    | _ => return none
+  | _ =>
+    return none
 
 
 @[inline] private def useWHNFCache (e : Expr) : MetaM Bool := do

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/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
@@ -740,6 +753,16 @@ partial def delabDoElems : DelabM (List Syntax) := do
       let b := b.instantiate1 fvar
       descend b 2 $
         prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
+  else if e.isLetFun then
+    -- letFun.{u, v} : {α : Sort u} → {β : α → Sort v} → (v : α) → ((x : α) → β x) → β v
+    let stxT ← withNaryArg 0 delab
+    let stxV ← withNaryArg 2 delab
+    withAppArg do
+      match (← getExpr) with
+      | Expr.lam .. =>
+        withBindingBodyUnusedName fun n => do
+          prependAndRec `(doElem|have $n:term : $stxT := $stxV)
+      | _ => failure
   else
     let stx ← delab
     return [← `(doElem|$stx:term)]

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

@@ -100,6 +100,16 @@ instance [ToExpr α] [ToExpr β] : ToExpr (α × β) :=
   { toExpr     := fun ⟨a, b⟩ => mkApp4 (mkConst ``Prod.mk [levelZero, levelZero]) αType βType (toExpr a) (toExpr b),
     toTypeExpr := mkApp2 (mkConst ``Prod [levelZero, levelZero]) αType βType }
 
+instance : ToExpr Literal where
+  toTypeExpr := mkConst ``Literal
+  toExpr l   := match l with
+   | .natVal _ => mkApp (mkConst ``Literal.natVal) (.lit l)
+   | .strVal _ => mkApp (mkConst ``Literal.strVal) (.lit l)
+
+instance : ToExpr FVarId where
+  toTypeExpr    := mkConst ``FVarId
+  toExpr fvarId := mkApp (mkConst ``FVarId.mk) (toExpr fvarId.name)
+
 def Expr.toCtorIfLit : Expr → Expr
   | .lit (.natVal v) =>
     if v == 0 then mkConst ``Nat.zero

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/Load/Elab.lean

@@ -210,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