Update Trace.lean

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

.gitattributes

@@ -1,3 +1,4 @@
+*.lean text eol=lf
 *.expected.out -text
 RELEASES.md merge=union
 stage0/** binary linguist-generated

.github/workflows/ci.yml

@@ -67,13 +67,13 @@ jobs:
             os: ubuntu-latest
             CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Debug
             # exclude seriously slow tests
-            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest'
+            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest'
           - name: Linux fsanitize
             os: ubuntu-latest
             # turn off custom allocator & symbolic functions to make LSAN do its magic
             CMAKE_OPTIONS: -DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined -DLEANC_EXTRA_FLAGS='-fsanitize=address,undefined -fsanitize-link-c++-runtime' -DSMALL_ALLOCATOR=OFF -DBSYMBOLIC=OFF
             # exclude seriously slow/problematic tests (laketests crash)
-            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest'
+            CTEST_OPTIONS: -E 'interactivetest|leanpkgtest|laketest|benchtest'
           - name: macOS
             os: macos-latest
             release: true
@@ -105,7 +105,7 @@ jobs:
             binary-check: ldd
           - name: Linux aarch64
             os: ubuntu-latest
-            CMAKE_OPTIONS: -DCMAKE_PREFIX_PATH=$GMP -DLEAN_INSTALL_SUFFIX=-linux_aarch64
+            CMAKE_OPTIONS: -DUSE_GMP=OFF -DLEAN_INSTALL_SUFFIX=-linux_aarch64
             release: true
             cross: true
             shell: nix-shell --arg pkgsDist "import (fetchTarball \"channel:nixos-19.03\") {{ localSystem.config = \"aarch64-unknown-linux-gnu\"; }}" --run "bash -euxo pipefail {0}"

.gitmodules

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

README.md

@@ -1,5 +1,5 @@
-This is the repository for **Lean 4**, which is currently being released as milestone releases towards a first stable release.
-[Lean 3](https://github.com/leanprover/lean) is still the latest stable release.
+This is the repository for **Lean 4**, which is being actively developed and published as nightly releases.
+Stable point releases are planned for a later date after establishing a robust release process.
 
 # About
 

RELEASES.md

@@ -1,6 +1,37 @@
 Unreleased
 ---------
 
+* [New `have this` implementation](https://github.com/leanprover/lean4/pull/2247).
+
+  `this` is now a regular identifier again that is implicitly introduced by anonymous `have :=` for the remainder of the tactic block. It used to be a keyword that was visible in all scopes and led to unexpected behavior when explicitly used as a binder name.
+
+* [Show typeclass and tactic names in profile output](https://github.com/leanprover/lean4/pull/2170).
+
+* [Make `calc` require the sequence of relation/proof-s to have the same indentation](https://github.com/leanprover/lean4/pull/1844),
+  and [add `calc` alternative syntax allowing underscores `_` in the first relation](https://github.com/leanprover/lean4/pull/1844).
+
+  The flexible indentation in `calc` was often used to align the relation symbols:
+  ```lean
+  example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
+    calc
+        (x + y) * (x + y) = (x + y) * x + (x + y) * y       := by rw [Nat.mul_add]
+                        -- improper indentation
+                        _ = x * x + y * x + (x + y) * y     := by rw [Nat.add_mul]
+                        _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
+                        _ = x * x + y * x + x * y + y * y   := by rw [←Nat.add_assoc]
+  ```
+
+  This is no longer legal.  The new syntax puts the first term right after the `calc` and each step has the same indentation:
+  ```lean
+  example (x y : Nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
+    calc (x + y) * (x + y)
+      _ = (x + y) * x + (x + y) * y       := by rw [Nat.mul_add]
+      _ = x * x + y * x + (x + y) * y     := by rw [Nat.add_mul]
+      _ = x * x + y * x + (x * y + y * y) := by rw [Nat.add_mul]
+      _ = x * x + y * x + x * y + y * y   := by rw [←Nat.add_assoc]
+  ```
+
+
 * Update Lake to latest prerelease.
 
 * [Make go-to-definition on a typeclass projection application go to the instance(s)](https://github.com/leanprover/lean4/pull/1767).
@@ -9,7 +40,7 @@ Unreleased
 
 * [Pretty-print signatures in hover and `#check <ident>`](https://github.com/leanprover/lean4/pull/1943).
 
-* [Introduce parser memoization to avoid exponentional behavior](https://github.com/leanprover/lean4/pull/1799).
+* [Introduce parser memoization to avoid exponential behavior](https://github.com/leanprover/lean4/pull/1799).
 
 * [feat: allow `doSeq` in `let x <- e | seq`](https://github.com/leanprover/lean4/pull/1809).
 
@@ -622,7 +653,7 @@ v4.0.0-m5 (07 August 2022)
     ...
   ```
 
-* Remove support for `{}` annotation from inductive datatype contructors. This annotation was barely used, and we can control the binder information for parameter bindings using the new inductive family indices to parameter promotion. Example: the following declaration using `{}`
+* Remove support for `{}` annotation from inductive datatype constructors. This annotation was barely used, and we can control the binder information for parameter bindings using the new inductive family indices to parameter promotion. Example: the following declaration using `{}`
   ```lean
   inductive LE' (n : Nat) : Nat → Prop where
     | refl {} : LE' n n -- Want `n` to be explicit
@@ -787,7 +818,7 @@ v4.0.0-m4 (23 March 2022)
 
   initialize my_ext : SimpExtension ← registerSimpAttr `my_simp "my own simp attribute"
   ```
-  If you don't neet to acces `my_ext`, you can also use the macro
+  If you don't need to access `my_ext`, you can also use the macro
   ```lean
   import Lean
 

doc/SUMMARY.md

@@ -4,6 +4,7 @@
 - [Tour of Lean](./tour.md)
 - [Setting Up Lean](./quickstart.md)
   - [Extended Setup Notes](./setup.md)
+  - [Nix Setup](./setup/nix.md)
 - [Theorem Proving in Lean](./tpil.md)
 - [Functional Programming in Lean](fplean.md)
 - [Examples](./examples.md)

doc/declarations.md

@@ -60,7 +60,7 @@ a b c : Nat
 
 Here ``a b c : Nat`` indicates the local context, and the second ``Nat`` indicates the expected type of the result.
 
-A *context* is sometimes called a *telescope*, but the latter is used more generally to include a sequence of declarations occuring relative to a given context. For example, relative to the context ``(a₁ : α₁) (a₂ : α₂) ... (aₙ : αₙ)``, the types ``βᵢ`` in a telescope ``(b₁ : β₁) (b₂ : β₂) ... (bₙ : βₙ)`` can refer to ``a₁, ..., aₙ``. Thus a context can be viewed as a telescope relative to the empty context.
+A *context* is sometimes called a *telescope*, but the latter is used more generally to include a sequence of declarations occurring relative to a given context. For example, relative to the context ``(a₁ : α₁) (a₂ : α₂) ... (aₙ : αₙ)``, the types ``βᵢ`` in a telescope ``(b₁ : β₁) (b₂ : β₂) ... (bₙ : βₙ)`` can refer to ``a₁, ..., aₙ``. Thus a context can be viewed as a telescope relative to the empty context.
 
 Telescopes are often used to describe a list of arguments, or parameters, to a declaration. In such cases, it is often notationally convenient to let ``(a : α)`` stand for a telescope rather than just a single argument. In general, the annotations described in [Implicit Arguments](expressions.md#implicit_arguments) can be used to mark arguments as implicit.
 
@@ -76,7 +76,7 @@ Lean provides ways of adding new objects to the environment. The following provi
 * ``theorem c : p := v`` : similar to ``def``, but intended to be used when ``p`` is a proposition.
 * ``opaque c : α (:= v)?`` : declares a opaque constant named ``c`` of type ``α``, the optional value `v` is must have type `α`
   and can be viewed as a certificate that ``α`` is not an empty type. If the value is not provided, Lean tries to find one
-  using a proceture based on type class resolution. The value `v` is hidden from the type checker. You can assume that
+  using a procedure based on type class resolution. The value `v` is hidden from the type checker. You can assume that
   Lean "forgets" `v` after type checking this kind of declaration.
 
 It is sometimes useful to be able to simulate a definition or theorem without naming it or adding it to the environment.

doc/dev/index.md

@@ -57,3 +57,10 @@ You might find that debugging through elan, e.g. via `gdb lean`, disables some
 things like symbol autocompletion because at first only the elan proxy binary
 is loaded. You can instead pass the explicit path to `bin/lean` in your build
 folder to gdb, or use `gdb $(elan which lean)`.
+
+It is also possible to generate releases that others can use,
+simply by pushing a tag to your fork of the Lean 4 github repository
+(and waiting about an hour; check the `Actions` tab for completion).
+If you push `my-tag` to a fork in your github account `my_name`,
+you can then put `my_name/lean4:my-tag` in your `lean-toolchain` file in a project using `lake`.
+(You must use a tag name that does not start with a numeral, or contain `_`).

doc/expressions.md

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

doc/flake.nix

@@ -4,15 +4,15 @@
   inputs.lean.url = path:../.;
   inputs.flake-utils.follows = "lean/flake-utils";
   inputs.mdBook = {
-    url = github:leanprover/mdBook;
+    url = "github:leanprover/mdBook";
     flake = false;
   };
   inputs.alectryon = {
-    url = github:Kha/alectryon/typeid;
+    url = "github:Kha/alectryon/typeid";
     flake = false;
   };
   inputs.leanInk = {
-    url = github:leanprover/LeanInk;
+    url = "github:leanprover/LeanInk";
     flake = false;
   };
 

doc/latex/lstlean.tex

@@ -201,6 +201,7 @@ literate=
 
 {ₙ}{{\ensuremath{_n}}}1
 {ₘ}{{\ensuremath{_m}}}1
+{ₚ}{{\ensuremath{_p}}}1
 {↑}{{\ensuremath{\uparrow}}}1
 {↓}{{\ensuremath{\downarrow}}}1
 

doc/lean3changes.md

@@ -85,7 +85,7 @@ def id5 : {α : Type} → α → α :=
 
 ## Sugar for simple functions
 
-In Lean 3, we can create simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` As a placeholder. Here are a few examples:
+In Lean 3, we can create simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` as a placeholder. Here are a few examples:
 
 ```lean
 # namespace ex3
@@ -196,6 +196,8 @@ example (f : Nat → Nat) (a b c : Nat) : f (a + b + c) = f (a + (b + c)) :=
   congrArg f (Nat.add_assoc ..)
 ```
 
+In Lean 4, writing `f(x)` in place of `f x` is no longer allowed, you must use whitespace between the function and its arguments (e.g., `f (x)`).
+
 ## Dependent function types
 
 Given `α : Type` and `β : α → Type`, `(x : α) → β x` denotes the type of functions `f` with the property that,

doc/macro_overview.md

@@ -1,7 +1,7 @@
 
 # Macro Overview
 
-The offical paper describing the mechanics behind Lean 4's macro system can be
+The official paper describing the mechanics behind Lean 4's macro system can be
 found in [Beyond Notations: Hygienic Macro Expansion for Theorem Proving
 Languages](https://arxiv.org/abs/2001.10490) by Sebastian Ullrich and Leonardo
 de Moura, and the accompanying repo with example code can be found in the
@@ -257,7 +257,7 @@ pretty printed output.
 ## Syntax expansions with `macro_rules`, and how it desugars.
 
 `macro_rules` lets you declare expansions for a given `Syntax` element using a
-syntax simlar to a `match` statement. The left-hand side of a match arm is a
+syntax similar to a `match` statement. The left-hand side of a match arm is a
 quotation (with a leading `<cat>|` for categories other than `term` and
 `command`) in which users can specify the pattern they'd like to write an
 expansion for. The right-hand side returns a syntax quotation which is the

doc/make/nix.md

@@ -83,7 +83,7 @@ Work on two adjacent stages at the same time without the need for repeatedly upd
 ```bash
 # open an editor that will use only committed changes (so first commit them when changing files)
 nix run .#HEAD-as-stage1.emacs-dev&
-# open a second editor that will use those commited changes as stage 0
+# open a second editor that will use those committed changes as stage 0
 # (so don't commit changes done here until you are done and ran a final `update-stage0-commit`)
 nix run .#HEAD-as-stage0.emacs-dev&
 ```

doc/monads/applicatives.lean

@@ -212,7 +212,7 @@ so you get a nice zipped list like this:
 -- [(1, 4), (2, 5), (3, 6)]
 /-!
 
-And of couse, as you would expect, there is an `unzip` also:
+And of course, as you would expect, there is an `unzip` also:
 
 -/
 #eval List.unzip (List.zip [1, 2, 3] [4, 5, 6])
@@ -286,7 +286,7 @@ But you will need to understand full Monads before this will make sense.
 Diving a bit deeper, (you can skip this and jump to the [Applicative
 Laws](laws.lean.md#what-are-the-applicative-laws) if don't want to dive into this implementation detail right
 now). But, if you write a simple `Option` example `(.*.) <$> some 4 <*> some 5` that produces `some 20`
-using `Seq.seq` you will see somthing interesting:
+using `Seq.seq` you will see something interesting:
 
 -/
 #eval Seq.seq ((.*.) <$> some 4) (fun (_ : Unit) => some 5) -- some 20

doc/quickstart.md

@@ -18,9 +18,11 @@ See quick [walkthrough demo video](https://www.youtube.com/watch?v=yZo6k48L0VY).
 
     ```
     info: syncing channel updates for 'nightly'
-    info: latest update on nightly, lean version nightly-2021-12-05
+    info: latest update on nightly, lean version nightly-2023-06-27
     info: downloading component 'lean'
     ```
+    If there is no popup, you probably have Elan installed already.
+    You may want to make sure that your default toolchain is Lean 4 in this case by running `elan default leanprover/lean4:nightly` and reopen the file, as the next step will fail otherwise.
 
 1. While it is installing, you can paste the following Lean program into the new file:
 
@@ -37,6 +39,8 @@ You are set up!
 
 ## Create a Lean Project
 
+*If your goal is to contribute to [mathlib4](https://github.com/leanprover-community/mathlib4) or use it as a depdency, please see its readme for specific instructions on how to do that.*
+
 You can now create a Lean project in a new folder. Run `lake init foo` from "View > Terminal" to create a package, followed by `lake build` to get an executable version of your Lean program.
 On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.
 

doc/setup.md

@@ -2,7 +2,7 @@
 
 ### Tier 1
 
-Platforms built & tested by our CI, available as nightly & stable releases via elan (see above)
+Platforms built & tested by our CI, available as nightly releases via elan (see below)
 
 * x86-64 Linux with glibc 2.27+
 * x86-64 macOS 10.15+
@@ -10,13 +10,13 @@ Platforms built & tested by our CI, available as nightly & stable releases via e
 
 ### Tier 2
 
-Platforms cross-compiled but not tested by our CI, available as nightly & stable releases
+Platforms cross-compiled but not tested by our CI, available as nightly releases
 
 Releases may be silently broken due to the lack of automated testing.
 Issue reports and fixes are welcome.
 
 * aarch64 Linux with glibc 2.27+
-* aarch64 (M1) macOS
+* aarch64 (Apple Silicon) macOS
 
 <!--
 ### Tier 3
@@ -26,28 +26,17 @@ Platforms that are known to work from manual testing, but do not come with CI or
 
 # Setting Up Lean
 
-There are currently two ways to set up a Lean 4 development environment:
-
-* [basic setup](./setup.md#basic-setup) (Linux/macOS/Windows): uses [`elan`](https://github.com/leanprover/elan) + your preinstalled editor
-* [Nix setup](./setup.md#nix-setup) (Linux/macOS/WSL): uses the [Nix](https://nixos.org/nix/) package manager for installing all dependencies localized to your project
-
-See also the [quickstart](./quickstart.md) instructions for using the basic setup with VS Code as the editor.
-
-## Basic Setup
+See also the [quickstart](./quickstart.md) instructions for a standard setup with VS Code as the editor.
 
 Release builds for all supported platforms are available at <https://github.com/leanprover/lean4/releases>.
 Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager [`elan`](https://github.com/leanprover/elan) instead:
 ```sh
 $ elan self update  # in case you haven't updated elan in a while
-# download & activate latest Lean 4 release (https://github.com/leanprover/lean4/releases)
-$ elan default leanprover/lean4:stable
-# alternatively, use the latest nightly build (https://github.com/leanprover/lean4-nightly/releases)
+# download & activate latest Lean 4 nightly release (https://github.com/leanprover/lean4-nightly/releases)
 $ elan default leanprover/lean4:nightly
-# alternatively, activate Lean 4 in current directory only
-$ elan override set leanprover/lean4:stable
 ```
 
-### `lake`
+## `lake`
 
 Lean 4 comes with a package manager named `lake`.
 Use `lake init foo` to initialize a Lean package `foo` in the current directory, and `lake build` to typecheck and build it as well as all its dependencies. Use `lake help` to learn about further commands.
@@ -67,80 +56,8 @@ After running `lake build` you will see a binary named `./build/bin/foo` and whe
 Hello, world!
 ```
 
-### Editing
+## Editing
 
 Lean implements the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) that can be used for interactive development in [Emacs](https://github.com/leanprover/lean4-mode), [VS Code](https://github.com/leanprover-community/vscode-lean4), and possibly other editors.
 
 Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).
-
-## Nix Setup
-
-The alternative setup based on Nix provides a perfectly reproducible development environment for your project from the Lean version down to the editor and Lean extension.
-However, it is still experimental and subject to change; in particular, it is heavily based on an unreleased version of Nix enabling [Nix Flakes](https://www.tweag.io/blog/2020-05-25-flakes/). The setup has been tested on NixOS, other Linux distributions, and macOS.
-
-After installing (any version of) Nix (<https://nixos.org/download.html>), you can easily open a shell with the particular pre-release version of Nix needed by and tested with our setup (called the "Lean shell" from here on):
-```bash
-$ nix-shell https://github.com/leanprover/lean4/archive/master.tar.gz -A nix
-```
-While this shell is sufficient for executing the steps below, it is recommended to also set the following options in `/etc/nix/nix.conf` (`nix.extraOptions` in NixOS):
-```
-max-jobs = auto  # Allow building multiple derivations in parallel
-keep-outputs = true  # Do not garbage-collect build time-only dependencies (e.g. clang)
-# Allow fetching build results from the Lean Cachix cache
-trusted-substituters = https://lean4.cachix.org/
-trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= lean4.cachix.org-1:mawtxSxcaiWE24xCXXgh3qnvlTkyU7evRRnGeAhD4Wk=
-```
-On a multi-user installation of Nix (the default), you need to restart the Nix daemon afterwards:
-```bash
-sudo pkill nix-daemon
-```
-
-The [Cachix](https://cachix.org/) integration will magically beam any build steps already executed by the CI right onto your machine when calling Nix commands in the shell opened above.
-It can be set up analogously as a cache for your own project.
-
-Note: Your system Nix might print warnings about not knowing some of the settings used by the Lean shell Nix, which can be ignored.
-
-### Basic Commands
-
-From a Lean shell, run
-```bash
-$ nix flake new mypkg -t github:leanprover/lean4
-```
-to create a new Lean package in directory `mypkg` using the latest commit of Lean 4.
-Such packages follow the same directory layout as described in the basic setup above, except for a `lakefile.lean` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
-```bash
-$ nix build  # build package and all dependencies
-$ nix build .#executable  # compile `main` definition into executable (after you've added one)
-$ nix run .#emacs-dev  # open a pinned version of Emacs with lean4-mode fully set up
-$ nix run .#emacs-dev MyPackage.lean  # arguments can be passed as well, e.g. the file to open
-$ nix run .#vscode-dev MyPackage.lean  # ditto, using VS Code
-```
-Note that if you rename `MyPackage.lean`, you also have to adjust the `name` attribute in `flake.nix` accordingly.
-Also note that if you turn the package into a Git repository, only tracked files will be visible to Nix.
-
-As in the basic setup, changes need to be saved to be visible in other files, which have then to be invalidated via an editor command.
-
-If you don't want to or cannot start the pinned editor from Nix, e.g. because you're running Lean inside WSL/a container/on a different machine, you can manually point your editor at the `lean` wrapper script the commands above use internally:
-```bash
-$ nix build .#lean-dev -o result-lean-dev
-```
-The resulting `./result-lean-dev/bin/lean` script essentially runs `nix run .#lean` in the current project's root directory when you open a Lean file or use the "refresh dependencies" command such that the correct Lean version for that project is executed.
-This includes selecting the correct stage of Lean (which it will compile on the fly, though without progress output) if you are [working on Lean itself](./make/nix.md#editor-integration).
-
-Package dependencies can be added as further input flakes and passed to the `deps` list of `buildLeanPackage`. Example: <https://github.com/Kha/testpkg2/blob/master/flake.nix#L5>
-
-For hacking, it can be useful to temporarily override an input with a local checkout/different version of a dependency:
-```bash
-$ nix build --override-input somedep path/to/somedep
-```
-
-On a build error, Nix will show the last 10 lines of the output by default. You can pass `-L` to `nix build` to show all lines, or pass the shown `*.drv` path to `nix log` to show the full log after the fact.
-
-Keeping all outputs ever built on a machine alive can accumulate to quite impressive amounts of disk space, so you might want to trigger the Nix GC when `/nix/store/` has grown too large:
-```bash
-nix-collect-garbage
-```
-This will remove everything not reachable from "GC roots" such as the `./result` symlink created by `nix build`.
-
-Note that the package information in `flake.nix` is currently completely independent from `lakefile.lean` used in the basic setup.
-Unifying the two formats is TBD.

doc/setup/nix.md

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

doc/tactics.md

@@ -224,7 +224,7 @@ example (n : Nat) : (binToChar n).isSome -> n = 0 ∨ n = 1 := by
   next => exact fun _ => Or.inr rfl
   next => intro h; cases h
 
-/- Hypotheses about previous cases can be accessesd by assigning them a
+/- Hypotheses about previous cases can be accessed by assigning them a
    name, like `ne_zero` below. Information about the matched term can also
    be preserved using the `generalizing` tactic: -/
 example (n : Nat) : (n = 0) -> (binToChar n = some '0') := by

flake.lock

@@ -18,11 +18,11 @@
     "lean4-mode": {
       "flake": false,
       "locked": {
-        "lastModified": 1659020985,
-        "narHash": "sha256-+dRaXB7uvN/weSZiKcfSKWhcdJVNg9Vg8k0pJkDNjpc=",
+        "lastModified": 1676498134,
+        "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
         "owner": "leanprover",
         "repo": "lean4-mode",
-        "rev": "37d5c99b7b29c80ab78321edd6773200deb0bca6",
+        "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
         "type": "github"
       },
       "original": {

flake.nix

@@ -1,11 +1,11 @@
 {
   description = "Lean interactive theorem prover";
 
-  inputs.nixpkgs.url = github:NixOS/nixpkgs/nixpkgs-unstable;
-  inputs.flake-utils.url = github:numtide/flake-utils;
-  inputs.nix.url = github:NixOS/nix;
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
+  inputs.nix.url = "github:NixOS/nix";
   inputs.lean4-mode = {
-    url = github:leanprover/lean4-mode;
+    url = "github:leanprover/lean4-mode";
     flake = false;
   };
   # used *only* by `stage0-from-input` below
@@ -29,8 +29,8 @@
       packages = lean-packages // rec {
         debug = lean-packages.override { debug = true; };
         stage0debug = lean-packages.override { stage0debug = true; };
-        sanitized = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" "-DSYMBOLIC=OFF" ]; };
-        sandebug = sanitized.override { debug = true; };
+        asan = lean-packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address" "-DLEANC_EXTRA_FLAGS=-fsanitize=address" "-DSMALL_ALLOCATOR=OFF" "-DSYMBOLIC=OFF" ]; };
+        asandebug = asan.override { debug = true; };
         tsan = lean-packages.override {
           extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=thread" "-DLEANC_EXTRA_FLAGS=-fsanitize=thread" "-DCOMPRESSED_OBJECT_HEADER=OFF" ];
           stage0 = (lean-packages.override {

nix/bootstrap.nix

@@ -1,5 +1,5 @@
 { src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
+  stdenv, lib, cmake, gmp, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
   ... } @ args:
 with builtins;
 rec {
@@ -88,7 +88,7 @@ rec {
         src = src + "/src";
         roots = [ { mod = args.name; glob = "andSubmodules"; } ];
         fullSrc = src;
-        srcPrefix = "src";
+        srcPath = "$PWD/src:$PWD/src/lake";
         inherit debug;
       } // args);
       Init' = build { name = "Init"; deps = []; };
@@ -101,13 +101,25 @@ rec {
       inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
       Init = attachSharedLib leanshared Init';
       Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Init ]; };
-      stdlib = [ Init Lean ];
+      Lake = build {
+        name = "Lake";
+        src = src + "/src/lake";
+        deps = [ Init Lean ];
+      };
+      Lake-Main = build {
+        name = "Lake.Main";
+        roots = [ "Lake.Main" ];
+        executableName = "lake";
+        deps = [ Lake ];
+        linkFlags = lib.optional stdenv.isLinux "-rdynamic";
+        src = src + "/src/lake";
+      };
+      stdlib = [ Init Lean Lake ];
       modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
       depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
-      extlib = stdlib;  # TODO: add Lake
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${leancpp}/lib/lean";
+      stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
         LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
@@ -116,7 +128,8 @@ rec {
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';
-      mods = Init.mods // Lean.mods;
+      mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
+      print-paths = Lean.makePrintPathsFor [] mods;
       leanc = writeShellScriptBin "leanc" ''
         LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@"
       '';
@@ -129,9 +142,9 @@ rec {
         name = "lean-${desc}";
         buildCommand = ''
           mkdir -p $out/bin $out/lib/lean
-          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList extlib)} ${leanshared}/* $out/lib/lean/
+          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${leanshared}/* $out/lib/lean/
           # put everything in a single final derivation so `IO.appDir` references work
-          cp ${lean}/bin/lean ${leanc}/bin/leanc $out/bin
+          cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
           # NOTE: `lndir` will not override existing `bin/leanc`
           ${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
         '';
@@ -140,30 +153,30 @@ rec {
       cacheRoots = linkFarmFromDrvs "cacheRoots" [
         stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
         # .o files are not a runtime dependency on macOS because of lack of thin archives
-        Lean.oTree
+        Lean.oTree Lake.oTree
       ];
       test = buildCMake {
         name = "lean-test-${desc}";
         realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
-        buildInputs = [ gmp perl ];
+        buildInputs = [ gmp perl git ];
         preConfigure = ''
           cd src
         '';
         extraCMakeFlags = [ "-DLLVM=OFF" ];
         postConfigure = ''
-          patchShebangs ../../tests
+          patchShebangs ../../tests ../lake
           rm -r bin lib include share
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)|laketest|leanpkgtest' -j$NIX_BUILD_CORES
+          ctest --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
           touch $out
         '';
       };
       update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = map (l: l.cTree) stdlib; }; in
+        let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Lean.cTree ]; }; in
         writeShellScriptBin "update-stage0" ''
           CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/update-stage0"}
         '';

nix/buildLeanPackage.nix

@@ -3,7 +3,7 @@
   runCommand, darwin, mkShell, ... }:
 let lean-final' = lean-final; in
 lib.makeOverridable (
-{ name, src, fullSrc ? src, srcPrefix ? "",
+{ name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
   # Lean dependencies. Each entry should be an output of buildLeanPackage.
   deps ? [ lean.Lean ],
   # Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
@@ -69,12 +69,14 @@ with builtins; let
     name = "${name}-depRoot";
     inherit deps;
     depRoots = map (drv: drv.LEAN_PATH) deps;
+
+    passAsFile = [ "deps" "depRoots" ];
     buildCommand = ''
       mkdir -p $out
-      for i in $depRoots; do
+      for i in $(cat $depRootsPath); do
         cp -dru --no-preserve=mode $i/. $out
       done
-      for i in $deps; do
+      for i in $(cat $depsPath); do
         cp -drsu --no-preserve=mode $i/. $out
       done
     '';
@@ -208,7 +210,6 @@ with builtins; let
       loadDynlibPaths = map pathOfSharedLib (loadDynlibsOfDeps deps);
     }}'
   '';
-  makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods;
   expandGlob = g:
     if typeOf g == "string" then [g]
     else if g.glob == "one" then [g.mod]
@@ -268,6 +269,7 @@ in rec {
     ln -sf ${iTree}/* $dest/build/lib
   '';
 
+  makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods;
   print-paths = makePrintPathsFor [] (mods' // externalModMap);
   # `lean` wrapper that dynamically runs Nix for the actual `lean` executable so the same editor can be
   # used for multiple projects/after upgrading the `lean` input/for editing both stage 1 and the tests
@@ -295,7 +297,7 @@ in rec {
   devShell = mkShell {
     buildInputs = [ nix ];
     shellHook = ''
-      export LEAN_SRC_PATH="$PWD/${srcPrefix}"
+      export LEAN_SRC_PATH="${srcPath}"
     '';
   };
 })

nix/packages.nix

@@ -52,7 +52,10 @@ let
     src = args.lean4-mode;
     packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash f flycheck magit-section lsp-mode s ];
     recipe = pkgs.writeText "recipe" ''
-      (lean4-mode :repo "leanprover/lean4-mode" :fetcher github)
+      (lean4-mode
+       :repo "leanprover/lean4-mode"
+       :fetcher github
+       :files ("*.el" "data"))
     '';
   };
   lean-emacs = emacsWithPackages [ lean4-mode ];

nix/templates/pkg/flake.nix

@@ -1,8 +1,8 @@
 {
   description = "My Lean package";
 
-  inputs.lean.url = github:leanprover/lean4;
-  inputs.flake-utils.url = github:numtide/flake-utils;
+  inputs.lean.url = "github:leanprover/lean4";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
 
   outputs = { self, lean, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
     let

script/prepare-llvm-macos.sh

@@ -34,8 +34,11 @@ $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
 (cd llvm; $CP --parents lib/clang/*/lib/*/libclang_rt.osx.a ../stage1)
 # libSystem stub, includes libc
 cp $SDK/usr/lib/libSystem.tbd stage1/lib/libc
-# use for linking, use system libs for running
-gcp llvm/lib/lib{c++,c++abi,unwind}.dylib stage1/lib/libc
+# use for linking, use system lib for running
+gcp llvm/lib/libc++.dylib stage1/lib/libc
+# make sure we search for the library in /usr/lib instead of the rpath, which should not contain `/usr/lib`
+# and apparently since Sonoma does not do so implicitly either
+install_name_tool -id /usr/lib/libc++.dylib stage1/lib/libc/libc++.dylib
 echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm-host/bin/llvm-config" # manually point to `llvm-config` location
 echo -n " -DLEAN_STANDALONE=ON"
 # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts,

script/update-stage0

@@ -3,8 +3,8 @@ set -euo pipefail
 
 rm -r stage0 || true
 # don't copy untracked files
-for f in $(git ls-files src); do
-    [[ $f != src/lake && $f != src/Leanc.lean ]] || continue
+# `:!` is git glob flavor for exclude patterns
+for f in $(git ls-files src ':!:src/lake/*' ':!:src/Leanc.lean'); do
     if [[ $f == *.lean ]]; then
         f=${f#src/}
         f=${f%.lean}.c

src/CMakeLists.txt

@@ -293,7 +293,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
     find_package(ZLIB REQUIRED)
     message(STATUS "ZLIB_LIBRARY: ${ZLIB_LIBRARY}")
     cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH)
-    string(APPEND LEAN_EXTRA_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
+    string(APPEND LEANSHARED_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
   endif()
   string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
@@ -301,6 +301,7 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
 else()
   string(APPEND LEANC_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
 endif()
+string(APPEND LEANC_STATIC_LINKER_FLAGS " -lLake")
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
 

src/Init/Coe.lean

@@ -101,8 +101,9 @@ These classes should be implemented for coercions:
   `f` does not have a function type.
   `CoeFun` instances apply to `CoeOut` as well.
 
-* `CoeSort α β` is a coercion to a sort. `β` must be a universe, and if
-  `a : α` appears in a place where a type is expected, like `(x : a)` or `a → a`.
+* `CoeSort α β` is a coercion to a sort. `β` must be a universe, and this is
+  triggered when `a : α` appears in a place where a type is expected, like
+  `(x : a)` or `a → a`.
   `CoeSort` instances apply to `CoeOut` as well.
 
 On top of these instances this file defines several auxiliary type classes:
@@ -122,7 +123,7 @@ chained with other `Coe` instances, and coercion is automatically used when
 `x` has type `α` but it is used in a context where `β` is expected.
 You can use the `↑x` operator to explicitly trigger coercion.
 -/
-class Coe (α : Sort u) (β : Sort v) where
+class Coe (α : semiOutParam (Sort u)) (β : Sort v) where
   /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
   or by double type ascription `((x : α) : β)`. -/
   coe : α → β
@@ -145,7 +146,7 @@ instance : CoeTC α α where coe a := a
 /--
 `CoeOut α β` is for coercions that are applied from left-to-right.
 -/
-class CoeOut (α : Sort u) (β : Sort v) where
+class CoeOut (α : Sort u) (β : semiOutParam (Sort v)) where
   /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
   or by double type ascription `((x : α) : β)`. -/
   coe : α → β
@@ -173,7 +174,7 @@ instance : CoeOTC α α where coe a := a
 `CoeHead α β` is for coercions that are applied from left-to-right at most once
 at beginning of the coercion chain.
 -/
-class CoeHead (α : Sort u) (β : Sort v) where
+class CoeHead (α : Sort u) (β : semiOutParam (Sort v)) where
   /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
   or by double type ascription `((x : α) : β)`. -/
   coe : α → β
@@ -198,7 +199,7 @@ instance : CoeHTC α α where coe a := a
 sequence of coercions. That is, `α` can be further coerced via `Coe σ α` and
 `CoeHead τ σ` instances but `β` will only be the expected type of the expression.
 -/
-class CoeTail (α : Sort u) (β : Sort v) where
+class CoeTail (α : semiOutParam (Sort u)) (β : Sort v) where
   /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
   or by double type ascription `((x : α) : β)`. -/
   coe : α → β
@@ -254,8 +255,9 @@ instance : CoeT α a α where coe := a
 /--
 `CoeFun α (γ : α → Sort v)` is a coercion to a function. `γ a` should be a
 (coercion-to-)function type, and this is triggered whenever an element
-`f : α` appears in an application like `f x` which would not make sense since
-`f` does not have a function type. This is automatically turned into `CoeFun.coe f x`.
+`f : α` appears in an application like `f x`, which would not make sense since
+`f` does not have a function type.
+`CoeFun` instances apply to `CoeOut` as well.
 -/
 class CoeFun (α : Sort u) (γ : outParam (α → Sort v)) where
   /-- Coerces a value `f : α` to type `γ f`, which should be either be a
@@ -267,9 +269,10 @@ attribute [coe_decl] CoeFun.coe
 instance [CoeFun α fun _ => β] : CoeOut α β where coe a := CoeFun.coe a
 
 /--
-`CoeSort α β` is a coercion to a sort. `β` must be a universe, and if
-`a : α` appears in a place where a type is expected, like `(x : a)` or `a → a`,
-then it will be turned into `(x : CoeSort.coe a)`.
+`CoeSort α β` is a coercion to a sort. `β` must be a universe, and this is
+triggered when `a : α` appears in a place where a type is expected, like
+`(x : a)` or `a → a`.
+`CoeSort` instances apply to `CoeOut` as well.
 -/
 class CoeSort (α : Sort u) (β : outParam (Sort v)) where
   /-- Coerces a value of type `α` to `β`, which must be a universe. -/

src/Init/Control/Basic.lean

@@ -186,7 +186,7 @@ This is the same as [`MonadBaseControl`](https://hackage.haskell.org/package/mon
 To learn about `MonadControl`, see the comment above this docstring.
 
 -/
-class MonadControl (m : Type u → Type v) (n : Type u → Type w) where
+class MonadControl (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where
   stM      : Type u → Type u
   liftWith : {α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α
   restoreM : {α : Type u} → m (stM α) → n α

src/Init/Conv.lean

@@ -79,7 +79,7 @@ syntax (name := arg) "arg " "@"? num : conv
 
 /-- `ext x` traverses into a binder (a `fun x => e` or `∀ x, e` expression)
 to target `e`, introducing name `x` in the process. -/
-syntax (name := ext) "ext" (colGt ident)* : conv
+syntax (name := ext) "ext" (ppSpace colGt ident)* : conv
 
 /-- `change t'` replaces the target `t` with `t'`,
 assuming `t` and `t'` are definitionally equal. -/
@@ -89,7 +89,7 @@ syntax (name := change) "change " term : conv
 Like the `delta` tactic, this ignores any definitional equations and uses
 primitive delta-reduction instead, which may result in leaking implementation details.
 Users should prefer `unfold` for unfolding definitions. -/
-syntax (name := delta) "delta " (colGt ident)+ : conv
+syntax (name := delta) "delta" (ppSpace colGt ident)+ : conv
 
 /--
 * `unfold foo` unfolds all occurrences of `foo` in the target.
@@ -97,7 +97,7 @@ syntax (name := delta) "delta " (colGt ident)+ : conv
 Like the `unfold` tactic, this uses equational lemmas for the chosen definition
 to rewrite the target. For recursive definitions,
 only one layer of unfolding is performed. -/
-syntax (name := unfold) "unfold " (colGt ident)+ : conv
+syntax (name := unfold) "unfold" (ppSpace colGt ident)+ : conv
 
 /--
 * `pattern pat` traverses to the first subterm of the target that matches `pat`.
@@ -139,8 +139,8 @@ example (a : Nat): (0 + 0) = a - a := by
     rw [← Nat.sub_self a]
 ```
 -/
-syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")?
-  ("[" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
+syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
+  (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
 
 /-- `simp_match` simplifies match expressions. For example,
 ```
@@ -214,7 +214,7 @@ macro (name := case') tk:"case' " args:sepBy1(caseArg, " | ") arr:" => " s:convS
 `next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
 inaccessible names to the given names.
 -/
-macro "next " args:binderIdent* " => " tac:convSeq : conv => `(conv| case _ $args* => $tac)
+macro "next" args:(ppSpace binderIdent)* " => " tac:convSeq : conv => `(conv| case _ $args* => $tac)
 
 /--
 `focus tac` focuses on the main goal, suppressing all other goals, and runs `tac` on it.
@@ -250,7 +250,7 @@ macro "left" : conv => `(conv| lhs)
 /-- `right` traverses into the right argument. Synonym for `rhs`. -/
 macro "right" : conv => `(conv| rhs)
 /-- `intro` traverses into binders. Synonym for `ext`. -/
-macro "intro" xs:(colGt ident)* : conv => `(conv| ext $xs*)
+macro "intro" xs:(ppSpace colGt ident)* : conv => `(conv| ext $xs*)
 
 syntax enterArg := ident <|> ("@"? num)
 
@@ -261,7 +261,7 @@ It is a shorthand for other conv tactics as follows:
 * `enter [x]` (where `x` is an identifier) is equivalent to `ext x`.
 For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]`
 will traverse to the subterm `b`. -/
-syntax "enter" " [" (colGt enterArg),+ "]": conv
+syntax "enter" " [" withoutPosition(enterArg,+) "]" : conv
 macro_rules
   | `(conv| enter [$i:num]) => `(conv| arg $i)
   | `(conv| enter [@$i]) => `(conv| arg @$i)
@@ -275,7 +275,7 @@ cannot be reasonably interpreted as proving one equality from a list of others.
 macro "apply " e:term : conv => `(conv| tactic => apply $e)
 
 /-- `first | conv | ...` runs each `conv` until one succeeds, or else fails. -/
-syntax (name := first) "first " withPosition((colGe "|" convSeq)+) : conv
+syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "| " convSeq)+) : conv
 
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
 macro "try " t:convSeq : conv => `(conv| first | $t | skip)
@@ -284,7 +284,7 @@ macro:1 x:conv tk:" <;> " y:conv:0 : conv =>
   `(conv| tactic' => (conv' => $x:conv) <;>%$tk (conv' => $y:conv))
 
 /-- `repeat convs` runs the sequence `convs` repeatedly until it fails to apply. -/
-syntax "repeat" convSeq : conv
+syntax "repeat " convSeq : conv
 macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | rfl)
 
@@ -301,6 +301,6 @@ Basic forms:
 -/
 -- HACK: put this at the end so that references to `conv` above
 -- refer to the syntax category instead of this syntax
-syntax (name := conv) "conv " (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
+syntax (name := conv) "conv" (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
 
 end Lean.Parser.Tactic.Conv

src/Init/Core.lean

@@ -797,6 +797,13 @@ theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α}
   | isTrue hc   => absurd hc hnc
   | isFalse _   => rfl
 
+/-- Split an if-then-else into cases. The `split` tactic is generally easier to use than this theorem. -/
+def iteInduction {c} [inst : Decidable c] {motive : α → Sort _} {t e : α}
+    (hpos : c → motive t) (hneg : ¬c → motive e) : motive (ite c t e) :=
+  match inst with
+  | isTrue h => hpos h
+  | isFalse h => hneg h
+
 theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬ c → α} : (dite c t e) = t hc :=
   match h with
   | isTrue  _   => rfl
@@ -1344,7 +1351,8 @@ then it lifts to a function on `Quotient s` such that `lift f h (mk a) = f a`.
 protected abbrev lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : α → β) : ((a b : α) → a ≈ b → f a = f b) → Quotient s → β :=
   Quot.lift f
 
-protected theorem ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} : ((a : α) → motive (Quotient.mk s a)) → (q : Quot Setoid.r) → motive q :=
+/-- The analogue of `Quot.ind`: every element of `Quotient s` is of the form `Quotient.mk s a`. -/
+protected theorem ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} : ((a : α) → motive (Quotient.mk s a)) → (q : Quotient s) → motive q :=
   Quot.ind
 
 /--
@@ -1354,6 +1362,7 @@ then it lifts to a function on `Quotient s` such that `lift (mk a) f h = f a`.
 protected abbrev liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : α → β) (c : (a b : α) → a ≈ b → f a = f b) : β :=
   Quot.liftOn q f c
 
+/-- The analogue of `Quot.inductionOn`: every element of `Quotient s` is of the form `Quotient.mk s a`. -/
 @[elab_as_elim]
 protected theorem inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop}
     (q : Quotient s)
@@ -1471,7 +1480,7 @@ end
 
 section Exact
 
-variable   {α : Sort u}
+variable {α : Sort u}
 
 private def rel {s : Setoid α} (q₁ q₂ : Quotient s) : Prop :=
   Quotient.liftOn₂ q₁ q₂

src/Init/Data/Array/Basic.lean

@@ -269,7 +269,15 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
 /-- Reference implementation for `mapM` -/
 @[implemented_by mapMUnsafe]
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
-  as.foldlM (fun bs a => do let b ← f a; pure (bs.push b)) (mkEmpty as.size)
+  -- Note: we cannot use `foldlM` here for the reference implementation because this calls
+  -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
+  let rec map (i : Nat) (r : Array β) : m (Array β) := do
+    if hlt : i < as.size then
+      map (i+1) (r.push (← f as[i]))
+    else
+      pure r
+  map 0 (mkEmpty as.size)
+termination_by map => as.size - i
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=

src/Init/Data/Hashable.lean

@@ -58,3 +58,7 @@ instance : Hashable Int where
 
 instance (P : Prop) : Hashable P where
   hash _ := 0
+
+/-- An opaque (low-level) hash operation used to implement hashing for pointers. -/
+@[always_inline, inline] def hash64 (u : UInt64) : UInt64 :=
+  mixHash u 11

src/Init/Data/Int/Basic.lean

@@ -9,12 +9,39 @@ prelude
 import Init.Coe
 import Init.Data.Nat.Div
 import Init.Data.List.Basic
+set_option linter.missingDocs true -- keep it documented
 open Nat
 
-/-! # the Type, coercions, and notation -/
+/-! # Integer Type, Coercions, and Notation
 
+This file defines the `Int` type as well as
+
+* coercions, conversions, and compatibility with numeric literals,
+* basic arithmetic operations add/sub/mul/div/mod/pow,
+* a few `Nat`-related operations such as `negOfNat` and `subNatNat`,
+* relations `<`/`≤`/`≥`/`>`, the `NonNeg` property and `min`/`max`,
+* decidability of equality, relations and `NonNeg`.
+-/
+
+/--
+The type of integers. It is defined as an inductive type based on the
+natural number type `Nat` featuring two constructors: "a natural
+number is an integer", and "the negation of a successor of a natural
+number is an integer". The former represents integers between `0`
+(inclusive) and `∞`, and the latter integers between `-∞` and `-1`
+(inclusive).
+
+This type is special-cased by the compiler. The runtime has a special
+representation for `Int` which stores "small" signed numbers directly,
+and larger numbers use an arbitrary precision "bignum" library
+(usually [GMP](https://gmplib.org/)). A "small number" is an integer
+that can be encoded with 63 bits (31 bits on 32-bits architectures).
+-/
 inductive Int : Type where
+  /-- A natural number is an integer (`0` to `∞`). -/
   | ofNat   : Nat → Int
+  /-- The negation of the successor of a natural number is an integer
+    (`-1` to `-∞`). -/
   | negSucc : Nat → Int
 
 attribute [extern "lean_nat_to_int"] Int.ofNat
@@ -28,32 +55,69 @@ instance : OfNat Int n where
 namespace Int
 instance : Inhabited Int := ⟨ofNat 0⟩
 
+/-- Negation of a natural number. -/
 def negOfNat : Nat → Int
   | 0      => 0
   | succ m => negSucc m
 
 set_option bootstrap.genMatcherCode false in
+/-- Negation of an integer.
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_neg"]
 protected def neg (n : @& Int) : Int :=
   match n with
   | ofNat n   => negOfNat n
   | negSucc n => succ n
 
+/-
+  The `Neg Int` default instance must have priority higher than `low`
+  since the default instance `OfNat Nat n` has `low` priority.
+
+  ```
+  #check -42
+  ```
+-/
+@[default_instance mid]
+instance : Neg Int where
+  neg := Int.neg
+
+/-- Subtraction of two natural numbers. -/
 def subNatNat (m n : Nat) : Int :=
   match (n - m : Nat) with
   | 0        => ofNat (m - n)  -- m ≥ n
   | (succ k) => negSucc k
 
 set_option bootstrap.genMatcherCode false in
+/-- Addition of two integers.
+
+  ```
+  #eval (7 : Int) + (6 : Int) -- 13
+  #eval (6 : Int) + (-6 : Int) -- 0
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_add"]
-  protected def add (m n : @& Int) : Int :=
+protected def add (m n : @& Int) : Int :=
   match m, n with
   | ofNat m,   ofNat n   => ofNat (m + n)
   | ofNat m,   negSucc n => subNatNat m (succ n)
   | negSucc m, ofNat n   => subNatNat n (succ m)
   | negSucc m, negSucc n => negSucc (succ (m + n))
 
+instance : Add Int where
+  add := Int.add
+
 set_option bootstrap.genMatcherCode false in
+/-- Multiplication of two integers.
+
+  ```
+  #eval (63 : Int) * (6 : Int) -- 378
+  #eval (6 : Int) * (-6 : Int) -- -36
+  #eval (7 : Int) * (0 : Int) -- 0
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_mul"]
 protected def mul (m n : @& Int) : Int :=
   match m, n with
@@ -62,21 +126,18 @@ protected def mul (m n : @& Int) : Int :=
   | negSucc m, ofNat n   => negOfNat (succ m * n)
   | negSucc m, negSucc n => ofNat (succ m * succ n)
 
-/--
-  The `Neg Int` default instance must have priority higher than `low` since
-  the default instance `OfNat Nat n` has `low` priority.
-  ```
-  #check -42
-  ```
--/
-@[default_instance mid]
-instance : Neg Int where
-  neg := Int.neg
-instance : Add Int where
-  add := Int.add
 instance : Mul Int where
   mul := Int.mul
 
+/-- Subtraction of two integers.
+
+  ```
+  #eval (63 : Int) - (6 : Int) -- 57
+  #eval (7 : Int) - (0 : Int) -- 7
+  #eval (0 : Int) - (7 : Int) -- -7
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_sub"]
 protected def sub (m n : @& Int) : Int :=
   m + (- n)
@@ -84,20 +145,33 @@ protected def sub (m n : @& Int) : Int :=
 instance : Sub Int where
   sub := Int.sub
 
+/-- A proof that an `Int` is non-negative. -/
 inductive NonNeg : Int → Prop where
+  /-- Sole constructor, proving that `ofNat n` is positive. -/
   | mk (n : Nat) : NonNeg (ofNat n)
 
+/-- Definition of `a ≤ b`, encoded as `b - a ≥ 0`. -/
 protected def le (a b : Int) : Prop := NonNeg (b - a)
 
 instance : LE Int where
   le := Int.le
 
+/-- Definition of `a < b`, encoded as `a + 1 ≤ b`. -/
 protected def lt (a b : Int) : Prop := (a + 1) ≤ b
 
 instance : LT Int where
   lt := Int.lt
 
 set_option bootstrap.genMatcherCode false in
+/-- Decides equality between two `Int`s.
+
+  ```
+  #eval (7 : Int) = (3 : Int) + (4 : Int) -- true
+  #eval (6 : Int) = (3 : Int) * (2 : Int) -- true
+  #eval ¬ (6 : Int) = (3 : Int) -- true
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_dec_eq"]
 protected def decEq (a b : @& Int) : Decidable (a = b) :=
   match a, b with
@@ -113,27 +187,93 @@ protected def decEq (a b : @& Int) : Decidable (a = b) :=
 instance : DecidableEq Int := Int.decEq
 
 set_option bootstrap.genMatcherCode false in
+/-- Decides whether an integer is negative.
+
+  ```
+  #eval (7 : Int).decNonneg.decide -- true
+  #eval (0 : Int).decNonneg.decide -- true
+  #eval ¬ (-7 : Int).decNonneg.decide -- true
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_dec_nonneg"]
 private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
   match m with
   | ofNat m   => isTrue <| NonNeg.mk m
   | negSucc _ => isFalse <| fun h => nomatch h
 
+/-- Decides whether `a ≤ b`.
+
+  ```
+  #eval ¬ ( (7 : Int) ≤ (0 : Int) ) -- true
+  #eval (0 : Int) ≤ (0 : Int) -- true
+  #eval (7 : Int) ≤ (10 : Int) -- true
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_dec_le"]
 instance decLe (a b : @& Int) : Decidable (a ≤ b) :=
   decNonneg _
 
+/-- Decides whether `a < b`.
+
+  ```
+  #eval `¬ ( (7 : Int) < 0 )` -- true
+  #eval `¬ ( (0 : Int) < 0 )` -- true
+  #eval `(7 : Int) < 10` -- true
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_dec_lt"]
 instance decLt (a b : @& Int) : Decidable (a < b) :=
   decNonneg _
 
 set_option bootstrap.genMatcherCode false in
+/-- Absolute value (`Nat`) of an integer.
+
+  ```
+  #eval (7 : Int).natAbs -- 7
+  #eval (0 : Int).natAbs -- 0
+  #eval (-11 : Int).natAbs -- 11
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_nat_abs"]
 def natAbs (m : @& Int) : Nat :=
   match m with
   | ofNat m   => m
   | negSucc m => m.succ
 
+/-- Integer division. This function uses the
+  [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention,
+  meaning that it rounds toward zero. Also note that division by zero
+  is defined to equal zero.
+
+  The relation between integer division and modulo is found in [the
+  `Int.mod_add_div` theorem in std][theo mod_add_div] which states
+  that `a % b + b * (a / b) = a`, unconditionally.
+
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
+  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+
+  Examples:
+
+  ```
+  #eval (7 : Int) / (0 : Int) -- 0
+  #eval (0 : Int) / (7 : Int) -- 0
+
+  #eval (12 : Int) / (6 : Int) -- 2
+  #eval (12 : Int) / (-6 : Int) -- -2
+  #eval (-12 : Int) / (6 : Int) -- -2
+  #eval (-12 : Int) / (-6 : Int) -- 2
+
+  #eval (12 : Int) / (7 : Int) -- 1
+  #eval (12 : Int) / (-7 : Int) -- -1
+  #eval (-12 : Int) / (7 : Int) -- -1
+  #eval (-12 : Int) / (-7 : Int) -- 1
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_div"]
 def div : (@& Int) → (@& Int) → Int
   | ofNat m,   ofNat n   => ofNat (m / n)
@@ -141,6 +281,36 @@ def div : (@& Int) → (@& Int) → Int
   | negSucc m, ofNat n   => -ofNat (succ m / n)
   | negSucc m, negSucc n => ofNat (succ m / succ n)
 
+instance : Div Int where
+  div := Int.div
+
+/-- Integer modulo. This function uses the
+  [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
+  to pair with `Int.div`, meaning that `a % b + b * (a / b) = a`
+  unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
+  particular, `a % 0 = a`.
+
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
+  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+
+  Examples:
+
+  ```
+  #eval (7 : Int) % (0 : Int) -- 7
+  #eval (0 : Int) % (7 : Int) -- 0
+
+  #eval (12 : Int) % (6 : Int) -- 0
+  #eval (12 : Int) % (-6 : Int) -- 0
+  #eval (-12 : Int) % (6 : Int) -- 0
+  #eval (-12 : Int) % (-6 : Int) -- 0
+
+  #eval (12 : Int) % (7 : Int) -- 5
+  #eval (12 : Int) % (-7 : Int) -- 5
+  #eval (-12 : Int) % (7 : Int) -- 2
+  #eval (-12 : Int) % (-7 : Int) -- 2
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_mod"]
 def mod : (@& Int) → (@& Int) → Int
   | ofNat m,   ofNat n   => ofNat (m % n)
@@ -148,16 +318,31 @@ def mod : (@& Int) → (@& Int) → Int
   | negSucc m, ofNat n   => -ofNat (succ m % n)
   | negSucc m, negSucc n => -ofNat (succ m % succ n)
 
-instance : Div Int where
-  div := Int.div
-
 instance : Mod Int where
   mod := Int.mod
 
+/-- Turns an integer into a natural number, negative numbers become
+  `0`.
+
+  ```
+  #eval (7 : Int).toNat -- 7
+  #eval (0 : Int).toNat -- 0
+  #eval (-7 : Int).toNat -- 0
+  ```
+-/
 def toNat : Int → Nat
   | ofNat n   => n
   | negSucc _ => 0
 
+/-- Power of an integer to some natural number.
+
+  ```
+  #eval (2 : Int) ^ 4 -- 16
+  #eval (10 : Int) ^ 0 -- 1
+  #eval (0 : Int) ^ 10 -- 0
+  #eval (-7 : Int) ^ 3 -- -343
+  ```
+-/
 protected def pow (m : Int) : Nat → Int
   | 0      => 1
   | succ n => Int.pow m n * m

src/Init/Data/List/Basic.lean

@@ -98,7 +98,7 @@ instance : Append (List α) := ⟨List.append⟩
 
 @[simp] theorem cons_append (a : α) (as bs : List α) : (a::as) ++ bs = a::(as ++ bs) := rfl
 
-@[simp] theorem List.append_eq (as bs : List α) : List.append as bs = as ++ bs := rfl
+@[simp] theorem append_eq (as bs : List α) : List.append as bs = as ++ bs := rfl
 
 theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
   induction as with
@@ -285,7 +285,7 @@ def dropWhile (p : α → Bool) : List α → List α
   | []   => []
   | a::l => match p a with
     | true  => dropWhile p l
-    | false =>  a::l
+    | false => a::l
 
 /--
 `O(|l|)`. `find? p l` returns the first element for which `p` returns true,
@@ -524,7 +524,7 @@ def takeWhile (p : α → Bool) : (xs : List α) → List α
 
 /--
 `O(|l|)`. Returns true if `p` is true for every element of `l`.
-* `any p [a, b, c] = p a && p b && p c`
+* `all p [a, b, c] = p a && p b && p c`
 -/
 @[inline] def all (l : List α) (p : α → Bool) : Bool :=
   foldr (fun a r => p a && r) true l

src/Init/Data/Nat/Basic.lean

@@ -620,6 +620,12 @@ theorem le_add_of_sub_le {a b c : Nat} (h : a - b ≤ c) : a ≤ c + b := by
     have hd := Nat.eq_add_of_sub_eq (Nat.le_trans hge (Nat.le_add_left ..)) hd
     rw [Nat.add_comm, hd]
 
+protected theorem sub_lt_sub_left : ∀ {k m n : Nat}, k < m → k < n → m - n < m - k
+  | 0, m+1, n+1, _, _ => by rw [Nat.add_sub_add_right]; exact lt_succ_of_le (Nat.sub_le _ _)
+  | k+1, m+1, n+1, h1, h2 => by
+    rw [Nat.add_sub_add_right, Nat.add_sub_add_right]
+    exact Nat.sub_lt_sub_left (Nat.lt_of_succ_lt_succ h1) (Nat.lt_of_succ_lt_succ h2)
+
 @[simp] protected theorem zero_sub (n : Nat) : 0 - n = 0 := by
   induction n with
   | zero => rfl

src/Init/Data/String/Basic.lean

@@ -44,7 +44,7 @@ def append : String → (@& String) → String
 def toList (s : String) : List Char :=
   s.data
 
-private def utf8GetAux : List Char → Pos → Pos → Char
+def utf8GetAux : List Char → Pos → Pos → Char
   | [],    _, _ => default
   | c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
 
@@ -58,9 +58,9 @@ def get (s : @& String) (p : @& Pos) : Char :=
   match s with
   | ⟨s⟩ => utf8GetAux s 0 p
 
-private def utf8GetAux? : List Char → Pos → Pos → Option Char
+def utf8GetAux? : List Char → Pos → Pos → Option Char
   | [],    _, _ => none
-  | c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
+  | c::cs, i, p => if i = p then c else utf8GetAux? cs (i + c) p
 
 @[extern "lean_string_utf8_get_opt"]
 def get? : (@& String) → (@& Pos) → Option Char
@@ -74,7 +74,7 @@ def get! (s : @& String) (p : @& Pos) : Char :=
   match s with
   | ⟨s⟩ => utf8GetAux s 0 p
 
-private def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
+def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char
   | [],    _, _ => []
   | c::cs, i, p =>
     if i = p then (c'::cs) else c::(utf8SetAux c' cs (i + c) p)
@@ -91,7 +91,7 @@ def next (s : @& String) (p : @& Pos) : Pos :=
   let c := get s p
   p + c
 
-private def utf8PrevAux : List Char → Pos → Pos → Pos
+def utf8PrevAux : List Char → Pos → Pos → Pos
   | [],    _, _ => 0
   | c::cs, i, p =>
     let i' := i + c
@@ -119,62 +119,106 @@ def get' (s : @& String) (p : @& Pos) (h : ¬ s.atEnd p) : Char :=
   match s with
   | ⟨s⟩ => utf8GetAux s 0 p
 
+/--
+Similar to `next` but runtime does not perform bounds check.
+-/
 @[extern "lean_string_utf8_next_fast"]
 def next' (s : @& String) (p : @& Pos) (h : ¬ s.atEnd p) : Pos :=
   let c := get s p
   p + c
 
-/- TODO: remove `partial` keywords after we restore the tactic
-  framework and wellfounded recursion support -/
+theorem one_le_csize (c : Char) : 1 ≤ csize c := by
+  repeat first | apply iteInduction (motive := (1 ≤ UInt32.toNat ·)) <;> intros | decide
 
-partial def posOfAux (s : String) (c : Char) (stopPos : Pos) (pos : Pos) : Pos :=
-  if pos >= stopPos then pos
-  else if s.get pos == c then pos
-       else posOfAux s c stopPos (s.next pos)
+@[simp] theorem pos_lt_eq (p₁ p₂ : Pos) : (p₁ < p₂) = (p₁.1 < p₂.1) := rfl
+
+@[simp] theorem pos_add_char (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + csize c := rfl
+
+theorem lt_next (s : String) (i : Pos) : i.1 < (s.next i).1 :=
+  Nat.add_lt_add_left (one_le_csize _) _
+
+theorem utf8PrevAux_lt_of_pos : ∀ (cs : List Char) (i p : Pos), p ≠ 0 →
+    (utf8PrevAux cs i p).1 < p.1
+  | [], i, p, h =>
+    Nat.lt_of_le_of_lt (Nat.zero_le _)
+      (Nat.zero_lt_of_ne_zero (mt (congrArg Pos.mk) h))
+  | c::cs, i, p, h => by
+    simp [utf8PrevAux]
+    apply iteInduction (motive := (Pos.byteIdx · < _)) <;> intro h'
+    next => exact h' ▸ Nat.add_lt_add_left (one_le_csize _) _
+    next => exact utf8PrevAux_lt_of_pos _ _ _ h
+
+theorem prev_lt_of_pos (s : String) (i : Pos) (h : i ≠ 0) : (s.prev i).1 < i.1 := by
+  simp [prev, h]
+  exact utf8PrevAux_lt_of_pos _ _ _ h
+
+def posOfAux (s : String) (c : Char) (stopPos : Pos) (pos : Pos) : Pos :=
+  if h : pos < stopPos then
+    if s.get pos == c then pos
+    else
+      have := Nat.sub_lt_sub_left h (lt_next s pos)
+      posOfAux s c stopPos (s.next pos)
+  else pos
+termination_by _ => stopPos.1 - pos.1
 
 @[inline] def posOf (s : String) (c : Char) : Pos :=
   posOfAux s c s.endPos 0
 
-partial def revPosOfAux (s : String) (c : Char) (pos : Pos) : Option Pos :=
- if s.get pos == c then some pos
- else if pos == 0 then none
- else revPosOfAux s c (s.prev pos)
+def revPosOfAux (s : String) (c : Char) (pos : Pos) : Option Pos :=
+  if h : pos = 0 then none
+  else
+    have := prev_lt_of_pos s pos h
+    let pos := s.prev pos
+    if s.get pos == c then some pos
+    else revPosOfAux s c pos
+termination_by _ => pos.1
 
 def revPosOf (s : String) (c : Char) : Option Pos :=
-  if s.endPos == 0 then none
-  else revPosOfAux s c (s.prev s.endPos)
+  revPosOfAux s c s.endPos
 
-partial def findAux (s : String) (p : Char → Bool) (stopPos : Pos) (pos : Pos) : Pos :=
-  if pos >= stopPos then pos
-  else if p (s.get pos) then pos
-       else findAux s p stopPos (s.next pos)
+def findAux (s : String) (p : Char → Bool) (stopPos : Pos) (pos : Pos) : Pos :=
+  if h : pos < stopPos then
+    if p (s.get pos) then pos
+    else
+      have := Nat.sub_lt_sub_left h (lt_next s pos)
+      findAux s p stopPos (s.next pos)
+  else pos
+termination_by _ => stopPos.1 - pos.1
 
 @[inline] def find (s : String) (p : Char → Bool) : Pos :=
   findAux s p s.endPos 0
 
-partial def revFindAux (s : String) (p : Char → Bool) (pos : Pos) : Option Pos :=
- if p (s.get pos) then some pos
- else if pos == 0 then none
- else revFindAux s p (s.prev pos)
+def revFindAux (s : String) (p : Char → Bool) (pos : Pos) : Option Pos :=
+  if h : pos = 0 then none
+  else
+    have := prev_lt_of_pos s pos h
+    let pos := s.prev pos
+    if p (s.get pos) then some pos
+    else revFindAux s p pos
+termination_by _ => pos.1
 
 def revFind (s : String) (p : Char → Bool) : Option Pos :=
-  if s.endPos == 0 then none
-  else revFindAux s p (s.prev s.endPos)
+  revFindAux s p s.endPos
 
 abbrev Pos.min (p₁ p₂ : Pos) : Pos :=
   { byteIdx := p₁.byteIdx.min p₂.byteIdx }
 
 /-- Returns the first position where the two strings differ. -/
-partial def firstDiffPos (a b : String) : Pos :=
+def firstDiffPos (a b : String) : Pos :=
   let stopPos := a.endPos.min b.endPos
   let rec loop (i : Pos) : Pos :=
-    if i >= stopPos || a.get i != b.get i then i
-    else loop (a.next i)
+    if h : i < stopPos then
+      if a.get i != b.get i then i
+      else
+        have := Nat.sub_lt_sub_left h (lt_next a i)
+        loop (a.next i)
+    else i
   loop 0
+termination_by loop => stopPos.1 - i.1
 
 @[extern "lean_string_utf8_extract"]
 def extract : (@& String) → (@& Pos) → (@& Pos) → String
-  | ⟨s⟩, b, e => if b.byteIdx ≥ e.byteIdx then ⟨[]⟩ else ⟨go₁ s 0 b e⟩
+  | ⟨s⟩, b, e => if b.byteIdx ≥ e.byteIdx then "" else ⟨go₁ s 0 b e⟩
 where
   go₁ : List Char → Pos → Pos → Pos → List Char
     | [],        _, _, _ => []
@@ -185,32 +229,38 @@ where
     | c::cs, i, e => if i = e then [] else c :: go₂ cs (i + c) e
 
 
-@[specialize] partial def splitAux (s : String) (p : Char → Bool) (b : Pos) (i : Pos) (r : List String) : List String :=
-  if s.atEnd i then
+@[specialize] def splitAux (s : String) (p : Char → Bool) (b : Pos) (i : Pos) (r : List String) : List String :=
+  if h : s.atEnd i then
     let r := (s.extract b i)::r
     r.reverse
-  else if p (s.get i) then
-    let i := s.next i
-    splitAux s p i i (s.extract b { byteIdx := i.byteIdx - 1 } :: r)
   else
-    splitAux s p b (s.next i) r
+    have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
+    if p (s.get i) then
+      let i' := s.next i
+      splitAux s p i' i' (s.extract b i :: r)
+    else
+      splitAux s p b (s.next i) r
+termination_by _ => s.endPos.1 - i.1
 
 @[specialize] def split (s : String) (p : Char → Bool) : List String :=
   splitAux s p 0 0 []
 
-partial def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String) : List String :=
-  if s.atEnd i then
-    let r := if sep.atEnd j then ""::(s.extract b (i - j))::r else (s.extract b i)::r
+def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String) : List String :=
+  if h : s.atEnd i then
+    let r := (s.extract b i)::r
     r.reverse
-  else if s.get i == sep.get j then
-    let i := s.next i
-    let j := sep.next j
-    if sep.atEnd j then
-      splitOnAux s sep i i 0 (s.extract b (i - j)::r)
-    else
-      splitOnAux s sep b i j r
   else
-    splitOnAux s sep b (s.next i) 0 r
+    have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
+    if s.get i == sep.get j then
+      let i := s.next i
+      let j := sep.next j
+      if sep.atEnd j then
+        splitOnAux s sep i i 0 (s.extract b (i - j)::r)
+      else
+        splitOnAux s sep b i j r
+    else
+      splitOnAux s sep b (s.next i) 0 r
+termination_by _ => s.endPos.1 - i.1
 
 def splitOn (s : String) (sep : String := " ") : List String :=
   if sep == "" then [s] else splitOnAux s sep 0 0 0 []
@@ -312,55 +362,108 @@ def prevn : Iterator → Nat → Iterator
   | it, i+1 => prevn it.prev i
 end Iterator
 
-partial def offsetOfPosAux (s : String) (pos : Pos) (i : Pos) (offset : Nat) : Nat :=
-  if i >= pos || s.atEnd i then
+def offsetOfPosAux (s : String) (pos : Pos) (i : Pos) (offset : Nat) : Nat :=
+  if i >= pos then offset
+  else if h : s.atEnd i then
     offset
   else
+    have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
     offsetOfPosAux s pos (s.next i) (offset+1)
+termination_by _ => s.endPos.1 - i.1
 
 def offsetOfPos (s : String) (pos : Pos) : Nat :=
   offsetOfPosAux s pos 0 0
 
-@[specialize] partial def foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : Pos) (i : Pos) (a : α) : α :=
-  let rec loop (i : Pos) (a : α) :=
-    if i >= stopPos then a
-    else loop (s.next i) (f a (s.get i))
-  loop i a
+@[specialize] def foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : Pos) (i : Pos) (a : α) : α :=
+  if h : i < stopPos then
+    have := Nat.sub_lt_sub_left h (lt_next s i)
+    foldlAux f s stopPos (s.next i) (f a (s.get i))
+  else a
+termination_by _ => stopPos.1 - i.1
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α :=
   foldlAux f s s.endPos 0 init
 
-@[specialize] partial def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (stopPos : Pos) (i : Pos) : α :=
-  let rec loop (i : Pos) :=
-    if i >= stopPos then a
-    else f (s.get i) (loop (s.next i))
-  loop i
+@[specialize] def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (i begPos : Pos) : α :=
+  if h : begPos < i then
+    have := String.prev_lt_of_pos s i <| mt (congrArg String.Pos.byteIdx) <|
+      Ne.symm <| Nat.ne_of_lt <| Nat.lt_of_le_of_lt (Nat.zero_le _) h
+    let i := s.prev i
+    let a := f (s.get i) a
+    foldrAux f a s i begPos
+  else a
+termination_by _ => i.1
 
 @[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α :=
   foldrAux f init s s.endPos 0
 
-@[specialize] partial def anyAux (s : String) (stopPos : Pos) (p : Char → Bool) (i : Pos) : Bool :=
-  let rec loop (i : Pos) :=
-    if i >= stopPos then false
-    else if p (s.get i) then true
-    else loop (s.next i)
-  loop i
+@[specialize] def anyAux (s : String) (stopPos : Pos) (p : Char → Bool) (i : Pos) : Bool :=
+  if h : i < stopPos then
+    if p (s.get i) then true
+    else
+      have := Nat.sub_lt_sub_left h (lt_next s i)
+      anyAux s stopPos p (s.next i)
+  else false
+termination_by _ => stopPos.1 - i.1
 
 @[inline] def any (s : String) (p : Char → Bool) : Bool :=
-anyAux s s.endPos p 0
+  anyAux s s.endPos p 0
 
 @[inline] def all (s : String) (p : Char → Bool) : Bool :=
-!s.any (fun c => !p c)
+  !s.any (fun c => !p c)
 
 def contains (s : String) (c : Char) : Bool :=
 s.any (fun a => a == c)
 
-@[specialize] partial def mapAux (f : Char → Char) (i : Pos) (s : String) : String :=
-  if s.atEnd i then s
+theorem utf8SetAux_of_gt (c' : Char) : ∀ (cs : List Char) {i p : Pos}, i > p → utf8SetAux c' cs i p = cs
+  | [],    _, _, _ => rfl
+  | c::cs, i, p, h => by
+    rw [utf8SetAux, if_neg (mt (congrArg (·.1)) (Ne.symm <| Nat.ne_of_lt h)), utf8SetAux_of_gt c' cs]
+    exact Nat.lt_of_lt_of_le h (Nat.le_add_right ..)
+
+theorem set_next_add (s : String) (i : Pos) (c : Char) (b₁ b₂)
+    (h : (s.next i).1 + b₁ = s.endPos.1 + b₂) :
+    ((s.set i c).next i).1 + b₁ = (s.set i c).endPos.1 + b₂ := by
+  simp [next, get, set, endPos, utf8ByteSize] at h ⊢
+  rw [Nat.add_comm i.1, Nat.add_assoc] at h ⊢
+  let rec foo : ∀ cs a b₁ b₂,
+    csize (utf8GetAux cs a i) + b₁ = utf8ByteSize.go cs + b₂ →
+    csize (utf8GetAux (utf8SetAux c cs a i) a i) + b₁ = utf8ByteSize.go (utf8SetAux c cs a i) + b₂
+  | [], _, _, _, h => h
+  | c'::cs, a, b₁, b₂, h => by
+    unfold utf8SetAux
+    apply iteInduction (motive := fun p => csize (utf8GetAux p a i) + b₁ = utf8ByteSize.go p + b₂) <;>
+      intro h' <;> simp [utf8GetAux, h', utf8ByteSize.go] at h ⊢
+    next =>
+      rw [Nat.add_assoc, Nat.add_left_comm] at h ⊢; rw [Nat.add_left_cancel h]
+    next =>
+      rw [Nat.add_assoc] at h ⊢
+      refine foo cs (a + c') b₁ (csize c' + b₂) h
+  exact foo s.1 0 _ _ h
+
+theorem mapAux_lemma (s : String) (i : Pos) (c : Char) (h : ¬s.atEnd i) :
+    (s.set i c).endPos.1 - ((s.set i c).next i).1 < s.endPos.1 - i.1 :=
+  suffices (s.set i c).endPos.1 - ((s.set i c).next i).1 = s.endPos.1 - (s.next i).1 by
+    rw [this]
+    apply Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next ..)
+  Nat.sub.elim (motive := (_ = ·)) _ _
+    (fun _ k e =>
+      have := set_next_add _ _ _ k 0 e.symm
+      Nat.sub_eq_of_eq_add <| this.symm.trans <| Nat.add_comm ..)
+    (fun h => by
+      have ⟨k, e⟩ := Nat.le.dest h
+      rw [Nat.succ_add] at e
+      have : ((s.set i c).next i).1 = _ := set_next_add _ _ c 0 k.succ e.symm
+      exact Nat.sub_eq_zero_of_le (this ▸ Nat.le_add_right ..))
+
+@[specialize] def mapAux (f : Char → Char) (i : Pos) (s : String) : String :=
+  if h : s.atEnd i then s
   else
     let c := f (s.get i)
+    have := mapAux_lemma s i c h
     let s := s.set i c
     mapAux f (s.next i) s
+termination_by _ => s.endPos.1 - i.1
 
 @[inline] def map (f : Char → Char) (s : String) : String :=
   mapAux f 0 s
@@ -377,32 +480,40 @@ def toNat? (s : String) : Option Nat :=
 /--
 Return `true` iff the substring of byte size `sz` starting at position `off1` in `s1` is equal to that starting at `off2` in `s2.`.
 False if either substring of that byte size does not exist. -/
-partial def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) : Bool :=
+def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) : Bool :=
   off1.byteIdx + sz ≤ s1.endPos.byteIdx && off2.byteIdx + sz ≤ s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
 where
   loop (off1 off2 stop1 : Pos) :=
-    if off1.byteIdx >= stop1.byteIdx then
-      true
-    else
+    if h : off1.byteIdx < stop1.byteIdx then
       let c₁ := s1.get off1
       let c₂ := s2.get off2
+      have := Nat.sub_lt_sub_left h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
       c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
+    else true
+termination_by loop => stop1.1 - off1.1
 
 /-- Return true iff `p` is a prefix of `s` -/
 def isPrefixOf (p : String) (s : String) : Bool :=
   substrEq p 0 s 0 p.endPos.byteIdx
 
-/-- Replace all occurrences of `pattern` in `s` with `replacment`. -/
-partial def replace (s pattern replacement : String) : String :=
-  loop "" 0 0
-where
-  loop (acc : String) (accStop pos : String.Pos) :=
-    if pos.byteIdx + pattern.endPos.byteIdx > s.endPos.byteIdx then
-      acc ++ s.extract accStop s.endPos
-    else if s.substrEq pos pattern 0 pattern.endPos.byteIdx then
-      loop (acc ++ s.extract accStop pos ++ replacement) (pos + pattern) (pos + pattern)
-    else
-      loop acc accStop (s.next pos)
+/-- Replace all occurrences of `pattern` in `s` with `replacement`. -/
+def replace (s pattern replacement : String) : String :=
+  if h : pattern.endPos.1 = 0 then s
+  else
+    have hPatt := Nat.zero_lt_of_ne_zero h
+    let rec loop (acc : String) (accStop pos : String.Pos) :=
+      if h : pos.byteIdx + pattern.endPos.byteIdx > s.endPos.byteIdx then
+        acc ++ s.extract accStop s.endPos
+      else
+        have := Nat.lt_of_lt_of_le (Nat.add_lt_add_left hPatt _) (Nat.ge_of_not_lt h)
+        if s.substrEq pos pattern 0 pattern.endPos.byteIdx then
+          have := Nat.sub_lt_sub_left this (Nat.add_lt_add_left hPatt _)
+          loop (acc ++ s.extract accStop pos ++ replacement) (pos + pattern) (pos + pattern)
+        else
+          have := Nat.sub_lt_sub_left this (lt_next s pos)
+          loop acc accStop (s.next pos)
+    loop "" 0 0
+termination_by loop => s.endPos.1 - pos.1
 
 end String
 
@@ -428,6 +539,15 @@ return the offset there of the next codepoint. -/
     let absP := b+p
     if absP = e then p else { byteIdx := (s.next absP).byteIdx - b.byteIdx }
 
+theorem lt_next (s : Substring) (i : String.Pos) (h : i.1 < s.bsize) :
+    i.1 < (s.next i).1 := by
+  simp [next]; rw [if_neg ?a]
+  case a =>
+    refine mt (congrArg String.Pos.byteIdx) (Nat.ne_of_lt ?_)
+    exact (Nat.add_comm .. ▸ Nat.add_lt_of_lt_sub h :)
+  apply Nat.lt_sub_of_add_lt
+  rw [Nat.add_comm]; apply String.lt_next
+
 /-- Given an offset of a codepoint into the substring,
 return the offset there of the previous codepoint. -/
 @[inline] def prev : Substring → String.Pos → String.Pos
@@ -470,27 +590,30 @@ or `s.bsize` if `c` doesn't occur. -/
 @[inline] def extract : Substring → String.Pos → String.Pos → Substring
   | ⟨s, b, e⟩, b', e' => if b' ≥ e' then ⟨"", 0, 0⟩ else ⟨s, e.min (b+b'), e.min (b+e')⟩
 
-partial def splitOn (s : Substring) (sep : String := " ") : List Substring :=
+def splitOn (s : Substring) (sep : String := " ") : List Substring :=
   if sep == "" then
     [s]
   else
     let rec loop (b i j : String.Pos) (r : List Substring) : List Substring :=
-      if i.byteIdx == s.bsize then
+      if h : i.byteIdx < s.bsize then
+        have := Nat.sub_lt_sub_left h (lt_next s i h)
+        if s.get i == sep.get j then
+          let i := s.next i
+          let j := sep.next j
+          if sep.atEnd j then
+            loop i i 0 (s.extract b (i-j) :: r)
+          else
+            loop b i j r
+        else
+          loop b (s.next i) 0 r
+      else
         let r := if sep.atEnd j then
           "".toSubstring :: s.extract b (i-j) :: r
         else
           s.extract b i :: r
         r.reverse
-      else if s.get i == sep.get j then
-        let i := s.next i
-        let j := sep.next j
-        if sep.atEnd j then
-          loop i i 0 (s.extract b (i-j) :: r)
-        else
-          loop b i j r
-      else
-        loop b (s.next i) 0 r
     loop 0 0 0 []
+termination_by loop => s.bsize - i.1
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring) : α :=
   match s with
@@ -510,10 +633,14 @@ partial def splitOn (s : Substring) (sep : String := " ") : List Substring :=
 def contains (s : Substring) (c : Char) : Bool :=
   s.any (fun a => a == c)
 
-@[specialize] private partial def takeWhileAux (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos :=
-  if i >= stopPos then i
-  else if p (s.get i) then takeWhileAux s stopPos p (s.next i)
+@[specialize] def takeWhileAux (s : String) (stopPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos :=
+  if h : i < stopPos then
+    if p (s.get i) then
+      have := Nat.sub_lt_sub_left h (String.lt_next s i)
+      takeWhileAux s stopPos p (s.next i)
+    else i
   else i
+termination_by _ => stopPos.1 - i.1
 
 @[inline] def takeWhile : Substring → (Char → Bool) → Substring
   | ⟨s, b, e⟩, p =>
@@ -525,13 +652,16 @@ def contains (s : Substring) (c : Char) : Bool :=
     let b := takeWhileAux s e p b;
     ⟨s, b, e⟩
 
-@[specialize] private partial def takeRightWhileAux (s : String) (begPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos :=
-  if i == begPos then i
-  else
+@[specialize] def takeRightWhileAux (s : String) (begPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos :=
+  if h : begPos < i then
+    have := String.prev_lt_of_pos s i <| mt (congrArg String.Pos.byteIdx) <|
+      Ne.symm <| Nat.ne_of_lt <| Nat.lt_of_le_of_lt (Nat.zero_le _) h
     let i' := s.prev i
     let c  := s.get i'
     if !p c then i
     else takeRightWhileAux s begPos p i'
+  else i
+termination_by _ => i.1
 
 @[inline] def takeRightWhile : Substring → (Char → Bool) → Substring
   | ⟨s, b, e⟩, p =>

src/Init/Data/String/Extra.lean

@@ -33,40 +33,14 @@ opaque fromUTF8Unchecked (a : @& ByteArray) : String
 @[extern "lean_string_to_utf8"]
 opaque toUTF8 (a : @& String) : ByteArray
 
-theorem one_le_csize (c : Char) : 1 ≤ csize c := by
-  simp [csize, Char.utf8Size]
-  repeat (first | split | decide)
-
-@[simp] theorem pos_lt_eq (p₁ p₂ : Pos) : (p₁ < p₂) = (p₁.1 < p₂.1) := rfl
-
-@[simp] theorem pos_add_char (p : Pos) (c : Char) : (p + c).byteIdx = p.byteIdx + csize c := rfl
-
-theorem eq_empty_of_bsize_eq_zero (h : s.endPos = {}) : s = "" := by
-  match s with
-  | ⟨[]⟩   => rfl
-  | ⟨c::cs⟩ =>
-    injection h with h
-    simp [endPos, utf8ByteSize, utf8ByteSize.go] at h
-    have : utf8ByteSize.go cs + 1 ≤ utf8ByteSize.go cs + csize c := Nat.add_le_add_left (one_le_csize c) _
-    simp_arith [h] at this
-
-theorem lt_next (s : String) (i : String.Pos) : i.1 < (s.next i).1 := by
-  simp_arith [next]; apply one_le_csize
-
 theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext) : sizeOf i.next < sizeOf i := by
   cases i; rename_i s pos; simp [Iterator.next, Iterator.sizeOf_eq]; simp [Iterator.hasNext] at h
-  have := String.lt_next s pos
-  apply Nat.sub.elim (motive := fun k => k < _) (utf8ByteSize s) (String.next s pos).1
-  . intro _ k he
-    simp [he]; rw [Nat.add_comm, Nat.add_sub_assoc (Nat.le_of_lt this)]
-    have := Nat.zero_lt_sub_of_lt this
-    simp_all_arith
-  . intro; apply Nat.zero_lt_sub_of_lt h
+  exact Nat.sub_lt_sub_left h (String.lt_next s pos)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
 
 theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
-  have h : i.hasNext = true := by simp_arith [atEnd] at h; simp_arith [hasNext, h]
+  have h : i.hasNext := decide_eq_true <| Nat.gt_of_not_le <| mt decide_eq_true h
   sizeOf_next_lt_of_hasNext i h
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)

src/Init/Meta.lean

@@ -271,10 +271,11 @@ abbrev CharLit := TSyntax charLitKind
 abbrev NameLit := TSyntax nameLitKind
 abbrev ScientificLit := TSyntax scientificLitKind
 abbrev NumLit := TSyntax numLitKind
+abbrev HygieneInfo := TSyntax hygieneInfoKind
 
 end Syntax
 
-export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit)
+export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit ScientificLit NumLit HygieneInfo)
 
 namespace TSyntax
 
@@ -836,22 +837,30 @@ private partial def splitNameLitAux (ss : Substring) (acc : List Substring) : Li
 def splitNameLit (ss : Substring) : List Substring :=
   splitNameLitAux ss [] |>.reverse
 
+def _root_.Substring.toName (s : Substring) : Name :=
+  match splitNameLitAux s [] with
+  | [] => .anonymous
+  | comps => comps.foldr (init := Name.anonymous)
+    fun comp n =>
+      let comp := comp.toString
+      if isIdBeginEscape comp.front then
+        Name.mkStr n (comp.drop 1 |>.dropRight 1)
+      else if comp.front.isDigit then
+        if let some k := decodeNatLitVal? comp then
+          Name.mkNum n k
+        else
+          unreachable!
+      else
+        Name.mkStr n comp
+
+def _root_.String.toName (s : String) : Name :=
+  s.toSubstring.toName
+
 def decodeNameLit (s : String) : Option Name :=
   if s.get 0 == '`' then
-    match splitNameLitAux (s.toSubstring.drop 1) [] with
-    | [] => none
-    | comps => some <| comps.foldr (init := Name.anonymous)
-      fun comp n =>
-        let comp := comp.toString
-        if isIdBeginEscape comp.front then
-          Name.mkStr n (comp.drop 1 |>.dropRight 1)
-        else if comp.front.isDigit then
-          if let some k := decodeNatLitVal? comp then
-            Name.mkNum n k
-          else
-            unreachable!
-        else
-          Name.mkStr n comp
+    match (s.toSubstring.drop 1).toName with
+    | .anonymous => none
+    | name => some name
   else
     none
 
@@ -913,6 +922,9 @@ def getChar (s : CharLit) : Char :=
 def getName (s : NameLit) : Name :=
   s.raw.isNameLit?.getD .anonymous
 
+def getHygieneInfo (s : HygieneInfo) : Name :=
+  s.raw[0].getId
+
 namespace Compat
 
 scoped instance : CoeTail (Array Syntax) (Syntax.TSepArray k sep) where
@@ -922,12 +934,18 @@ end Compat
 
 end TSyntax
 
+def HygieneInfo.mkIdent (s : HygieneInfo) (val : Name) (canonical := false) : Ident :=
+  let src := s.raw[0]
+  let id := { extractMacroScopes src.getId with name := val.eraseMacroScopes }.review
+  ⟨Syntax.ident (SourceInfo.fromRef src canonical) (toString val).toSubstring id []⟩
+
 /-- Reflect a runtime datum back to surface syntax (best-effort). -/
 class Quote (α : Type) (k : SyntaxNodeKind := `term) where
   quote : α → TSyntax k
 
 export Quote (quote)
 
+set_option synthInstance.checkSynthOrder false in
 instance [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])] : Quote α k' := ⟨fun a => quote (k := k) a⟩
 
 instance : Quote Term := ⟨id⟩
@@ -1271,13 +1289,15 @@ namespace Parser.Tactic
 /-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
 This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
 which only unfolds `@[reducible]` definitions). -/
-macro "erw " s:rwRuleSeq loc:(location)? : tactic =>
+macro "erw" s:rwRuleSeq loc:(location)? : tactic =>
   `(tactic| rw (config := { transparency := .default }) $s $(loc)?)
 
-syntax simpAllKind := atomic("(" &"all") " := " &"true" ")"
-syntax dsimpKind   := atomic("(" &"dsimp") " := " &"true" ")"
+syntax simpAllKind := atomic(" (" &"all") " := " &"true" ")"
+syntax dsimpKind   := atomic(" (" &"dsimp") " := " &"true" ")"
 
-macro (name := declareSimpLikeTactic) doc?:(docComment)? "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?) tacName:ident tacToken:str updateCfg:term : command => do
+macro (name := declareSimpLikeTactic) doc?:(docComment)?
+    "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?)
+    ppSpace tacName:ident ppSpace tacToken:str ppSpace updateCfg:term : command => do
   let (kind, tkn, stx) ←
     if opt.raw.isNone then
       pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))

src/Init/Notation.lean

@@ -363,7 +363,7 @@ namespace Parser.Tactic
 A case tag argument has the form `tag x₁ ... xₙ`; it refers to tag `tag` and renames
 the last `n` hypotheses to `x₁ ... xₙ`.
 -/
-syntax caseArg := binderIdent binderIdent*
+syntax caseArg := binderIdent (ppSpace binderIdent)*
 
 end Parser.Tactic
 end Lean
@@ -479,7 +479,7 @@ The syntax `%[a,b,c|tail]` constructs a value equivalent to `a::b::c::tail`.
 It uses binary partitioning to construct a tree of intermediate let bindings as in
 `let left := [d, e, f]; a :: b :: c :: left` to avoid creating very deep expressions.
 -/
-syntax "%[" withoutPosition(term,* "|" term) "]" : term
+syntax "%[" withoutPosition(term,* " | " term) "]" : term
 
 namespace Lean
 
@@ -496,12 +496,6 @@ macro_rules
     else
       `(%[ $elems,* | List.nil ])
 
--- Declare `this` as a keyword that unhygienically binds to a scope-less `this` assumption (or other binding).
--- The keyword prevents declaring a `this` binding except through metaprogramming, as is done by `have`/`show`.
-/-- Special identifier introduced by "anonymous" `have : ...`, `suffices p ...` etc. -/
-macro tk:"this" : term =>
-  return (⟨(Syntax.ident tk.getHeadInfo "this".toSubstring `this [])⟩ : TSyntax `term)
-
 /--
 Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
 The only accepted parser for this category is an antiquotation.
@@ -521,11 +515,11 @@ existing code. It may be removed in a future version of the library.
 
 `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
 -/
-syntax (name := deprecated) "deprecated " (ident)? : attr
+syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr
 
 /--
 When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
 a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this
 file cannot be read, elaboration fails.
 -/
-syntax (name := includeStr) "include_str" term : term
+syntax (name := includeStr) "include_str " term : term

src/Init/NotationExtra.lean

@@ -16,9 +16,9 @@ macro "Macro.trace[" id:ident "]" s:interpolatedStr(term) : term =>
 
 -- Auxiliary parsers and functions for declaring notation with binders
 
-syntax unbracketedExplicitBinders := binderIdent+ (" : " term)?
-syntax bracketedExplicitBinders   := "(" withoutPosition(binderIdent+ " : " term) ")"
-syntax explicitBinders            := bracketedExplicitBinders+ <|> unbracketedExplicitBinders
+syntax unbracketedExplicitBinders := (ppSpace binderIdent)+ (" : " term)?
+syntax bracketedExplicitBinders   := "(" withoutPosition((binderIdent ppSpace)+ ": " term) ")"
+syntax explicitBinders            := (ppSpace bracketedExplicitBinders)+ <|> unbracketedExplicitBinders
 
 open TSyntax.Compat in
 def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax :=
@@ -64,7 +64,8 @@ def expandBrackedBinders (combinatorDeclName : Name) (bracketedExplicitBinders :
 syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?
 
-syntax (docComment)? attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) patternIgnore("|-" <|> "⊢ ") unifConstraint : command
+syntax (docComment)? attrKind "unif_hint" (ppSpace ident)? (ppSpace bracketedBinder)*
+  " where " withPosition(unifConstraintElem*) patternIgnore(atomic("|" noWs "-") <|> "⊢") unifConstraint : command
 
 macro_rules
   | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁ ≟ $cs₂]* |- $t₁ ≟ $t₂) => do
@@ -79,7 +80,7 @@ open Lean
 
 section
 open TSyntax.Compat
-macro "∃ " xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Exists xs b
+macro "∃" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Exists xs b
 macro "exists" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Exists xs b
 macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Sigma xs b
 macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``PSigma xs b
@@ -91,7 +92,7 @@ end
 syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
 -- enforce indentation of calc steps so we know when to stop parsing them
 syntax calcStep := ppIndent(colGe term " := " term)
-syntax calcSteps := ppLine withPosition(calcFirstStep) ppLine withPosition((calcStep ppLine)*)
+syntax calcSteps := ppLine withPosition(calcFirstStep) withPosition((ppLine calcStep)*)
 
 /-- Step-wise reasoning over transitive relations.
 ```
@@ -372,19 +373,14 @@ macro_rules
     `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
       attribute [instance] $ctor)
 
-section
-open Lean.Parser.Tactic
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
-syntax cdotTk sepBy1IndentSemicolon(tactic) : tactic
-macro_rules
-  | `(tactic| $cdot:cdotTk $tacs*) => `(tactic| {%$cdot $tacs* }%$cdot)
-end
+syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
 
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.
 -/
-syntax (name := solve) "solve " withPosition((colGe "|" tacticSeq)+) : tactic
+syntax (name := solve) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
@@ -421,12 +417,12 @@ syntax "while " termBeforeDo " do " doSeq : doElem
 macro_rules
   | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
 
-syntax "repeat " doSeq " until " term : doElem
+syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
 
 macro_rules
   | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
 
-macro:50 e:term:51 " matches " p:sepBy1(term:51, "|") : term =>
+macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
   `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))
 
 end Lean

src/Init/Prelude.lean

@@ -313,7 +313,7 @@ theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
 /--
 Equality is transitive: if `a = b` and `b = c` then `a = c`.
 
-Because this is in the `Eq` namespace, if you variables or expressions
+Because this is in the `Eq` namespace, if you have variables or expressions
 `h₁ : a = b` and `h₂ : b = c`, you can use `h₁.trans h₂ : a = c` as shorthand
 for `Eq.trans h₁ h₂`.
 
@@ -392,7 +392,7 @@ perform exactly these constructions, and installs this last equation as a
 definitional reduction rule.
 
 Given a type `α` and any binary relation `r` on `α`, `Quot r` is a type. Note
-that `r` is not required to be an equivalance relation. `Quot` is the basic
+that `r` is not required to be an equivalence relation. `Quot` is the basic
 building block used to construct later the type `Quotient`.
 -/
 add_decl_doc Quot
@@ -438,7 +438,7 @@ have all the same properties as `Eq`, because the assumption that the types of
 important non-theorem is the analogue of `congr`: If `HEq f g` and `HEq x y`
 and `f x` and `g y` are well typed it does not follow that `HEq (f x) (g y)`.
 (This does follow if you have `f = g` instead.) However if `a` and `b` have
-the same type then `a = b` and `HEq a b` ae equivalent.
+the same type then `a = b` and `HEq a b` are equivalent.
 -/
 inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
   /-- Reflexivity of heterogeneous equality. -/
@@ -473,7 +473,7 @@ attribute [unbox] Prod
 
 /--
 Similar to `Prod`, but `α` and `β` can be propositions.
-We use this Type internally to automatically generate the `brecOn` recursor.
+We use this type internally to automatically generate the `brecOn` recursor.
 -/
 structure PProd (α : Sort u) (β : Sort v) where
   /-- The first projection out of a pair. if `p : PProd α β` then `p.1 : α`. -/
@@ -594,6 +594,29 @@ the "member" type `α` is determined by looking at the container type.
 -/
 @[reducible] def outParam (α : Sort u) : Sort u := α
 
+/--
+Gadget for marking semi output parameters in type classes.
+
+Semi-output parameters influence the order in which arguments to type class
+instances are processed.  Lean determines an order where all non-(semi-)output
+parameters to the instance argument have to be figured out before attempting to
+synthesize an argument (that is, they do not contain assignable metavariables
+created during TC synthesis). This rules out instances such as `[Mul β] : Add
+α` (because `β` could be anything). Marking a parameter as semi-output is a
+promise that instances of the type class will always fill in a value for that
+parameter.
+
+For example, the `Coe` class is defined as:
+```
+class Coe (α : semiOutParam (Sort u)) (β : Sort v)
+```
+This means that all `Coe` instances should provide a concrete value for `α`
+(i.e., not an assignable metavariable). An instance like `Coe Nat Int` or `Coe
+α (Option α)` is fine, but `Coe α Nat` is not since it does not provide a value
+for `α`.
+-/
+@[reducible] def semiOutParam (α : Sort u) : Sort u := α
+
 set_option linter.unusedVariables.funArgs false in
 /-- Auxiliary declaration used to implement named patterns like `x@h:p`. -/
 @[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a
@@ -1448,7 +1471,7 @@ set_option bootstrap.genMatcherCode false in
 /--
 The power operation on natural numbers.
 
-This definition is overridden in the compiler to efficiently
+This definition is overridden in both the kernel and the compiler to efficiently
 evaluate using the "bignum" representation (see `Nat`). The definition provided
 here is the logical model.
 -/
@@ -2397,7 +2420,7 @@ The `panicCore` definition cannot be specialized since it is an extern.
 When `panic` occurs in monadic code, the `Inhabited α` parameter depends on a
 `[inst : Monad m]` instance. The `inst` parameter will not be eliminated during
 specialization if it occurs inside of a binder (to avoid work duplication), and
-will prevent the the actual monad from being "copied" to the code being specialized.
+will prevent the actual monad from being "copied" to the code being specialized.
 When we reimplement the specializer, we may consider copying `inst` if it also
 occurs outside binders or if it is an instance.
 -/
@@ -2758,7 +2781,7 @@ Alternatively, an implementation of [`MonadLayer`] without `layerInvmap` (so far
   [`MonadTrans`]: https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html
   [`MonadLayer`]: https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer
 -/
-class MonadLift (m : Type u → Type v) (n : Type u → Type w) where
+class MonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where
   /-- Lifts a value from monad `m` into monad `n`. -/
   monadLift : {α : Type u} → m α → n α
 
@@ -2793,7 +2816,7 @@ monad transformers. Alternatively, an implementation of [`MonadTransFunctor`].
   [`MFunctor`]: https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html
   [`MonadTransFunctor`]: http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor
 -/
-class MonadFunctor (m : Type u → Type v) (n : Type u → Type w) where
+class MonadFunctor (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where
   /-- Lifts a monad morphism `f : {β : Type u} → m β → m β` to
   `monadMap f : {α : Type u} → n α → n α`. -/
   monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α
@@ -2846,7 +2869,7 @@ The `try ... catch e => ...` syntax inside `do` blocks is sugar for the
 
   [`MonadError`]: https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError
 -/
-class MonadExceptOf (ε : Type u) (m : Type v → Type w) where
+class MonadExceptOf (ε : semiOutParam (Type u)) (m : Type v → Type w) where
   /-- `throw : ε → m α` "throws an error" of type `ε` to the nearest enclosing
   catch block. -/
   throw {α : Type v} : ε → m α
@@ -2998,7 +3021,7 @@ class MonadReaderOf (ρ : Type u) (n : Type u → Type u) where
 
   [`MonadReader`]: https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader-Class.html#t:MonadReader
 -/
-class MonadReaderOf (ρ : Type u) (m : Type u → Type v) where
+class MonadReaderOf (ρ : semiOutParam (Type u)) (m : Type u → Type v) where
   /-- `(← read) : ρ` reads the state out of monad `m`. -/
   read : m ρ
 
@@ -3033,7 +3056,7 @@ function `f : ρ → ρ`. In addition to `ReaderT` itself, this operation lifts
 over most monad transformers, so it allows us to apply `withReader` to monads
 deeper in the stack.
 -/
-class MonadWithReaderOf (ρ : Type u) (m : Type u → Type v) where
+class MonadWithReaderOf (ρ : semiOutParam (Type u)) (m : Type u → Type v) where
   /-- `withReader (f : ρ → ρ) (x : m α) : m α`  runs the inner `x : m α` inside
   a modified context after applying the function `f : ρ → ρ`.-/
   withReader {α : Type u} : (ρ → ρ) → m α → m α
@@ -3069,7 +3092,7 @@ we use overlapping instances to derive instances automatically from `monadLift`.
 
   [`MonadState`]: https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-State-Class.html
 -/
-class MonadStateOf (σ : Type u) (m : Type u → Type v) where
+class MonadStateOf (σ : semiOutParam (Type u)) (m : Type u → Type v) where
   /-- `(← get) : σ` gets the state out of a monad `m`. -/
   get : m σ
   /-- `set (s : σ)` replaces the state with value `s`. -/
@@ -3355,7 +3378,7 @@ opaque mixHash (u₁ u₂ : UInt64) : UInt64
 instance [Hashable α] {p : α → Prop} : Hashable (Subtype p) where
   hash a := hash a.val
 
-/-- A opaque string hash function. -/
+/-- An opaque string hash function. -/
 @[extern "lean_string_hash"]
 protected opaque String.hash (s : @& String) : UInt64
 
@@ -3578,7 +3601,7 @@ inductive Syntax where
   subexpression corresponding to this node. The parser sets the `info` field
   to `none`.
   The parser sets the `info` field to `none`, with position retrieval continuing recursively.
-  Nodes created by quotatons use the result from `SourceInfo.fromRef` so that they are marked
+  Nodes created by quotations use the result from `SourceInfo.fromRef` so that they are marked
   as synthetic even when the leading/trailing token is not.
   The delaborator uses the `info` field to store the position of the subexpression
   corresponding to this node.
@@ -3656,7 +3679,7 @@ instance : Inhabited Syntax where
 instance : Inhabited (TSyntax ks) where
   default := ⟨default⟩
 
-/-! Builtin kinds -/
+/-! # Builtin kinds -/
 
 /--
 The `choice` kind is used when a piece of syntax has multiple parses, and the
@@ -3698,6 +3721,16 @@ abbrev nameLitKind : SyntaxNodeKind := `name
 /-- `fieldIdx` is the node kind of projection indices like the `2` in `x.2`. -/
 abbrev fieldIdxKind : SyntaxNodeKind := `fieldIdx
 
+/--
+`hygieneInfo` is the node kind of the `hygieneInfo` parser, which is an
+"invisible token" which captures the hygiene information at the current point
+without parsing anything.
+
+They can be used to generate identifiers (with `Lean.HygieneInfo.mkIdent`)
+as if they were introduced by the calling context, not the called macro.
+-/
+abbrev hygieneInfoKind : SyntaxNodeKind := `hygieneInfo
+
 /--
 `interpolatedStrLitKind` is the node kind of interpolated string literal
 fragments like `"value = {` and `}"` in `s!"value = {x}"`.
@@ -3797,7 +3830,7 @@ def isIdent : Syntax → Bool
   | ident .. => true
   | _        => false
 
-/-- If this is a `ident`, return the parsed value, else `.anonymous`. -/
+/-- If this is an `ident`, return the parsed value, else `.anonymous`. -/
 def getId : Syntax → Name
   | ident _ _ val _ => val
   | _               => Name.anonymous
@@ -4100,7 +4133,7 @@ foo.bla._@.Init.Data.List.Basic._hyg.2.5
 ```
 
 We may have to combine scopes from different files/modules.
-The main modules being processed is always the right most one.
+The main modules being processed is always the right-most one.
 This situation may happen when we execute a macro generated in
 an imported file in the current file.
 ```
@@ -4225,7 +4258,7 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
 
 /--
 Append two names that may have macro scopes. The macro scopes in `b` are always erased.
-If `a` has macro scopes, then the are propagated to result of `append a b`
+If `a` has macro scopes, then they are propagated to the result of `append a b`.
 -/
 def Name.append (a b : Name) : Name :=
   match a.hasMacroScopes, b.hasMacroScopes with
@@ -4365,14 +4398,14 @@ def throwUnsupported {α} : MacroM α :=
   throw Exception.unsupportedSyntax
 
 /--
-Throw a error with the given message,
+Throw an error with the given message,
 using the `ref` for the location information.
 -/
 def throwError {α} (msg : String) : MacroM α :=
   bind getRef fun ref =>
   throw (Exception.error ref msg)
 
-/-- Throw a error with the given message and location information. -/
+/-- Throw an error with the given message and location information. -/
 def throwErrorAt {α} (ref : Syntax) (msg : String) : MacroM α :=
   withRef ref (throwError msg)
 
@@ -4407,7 +4440,7 @@ structure Methods where
   hasDecl           : Name → MacroM Bool
   /-- Resolves the given name to an overload list of namespaces. -/
   resolveNamespace  : Name → MacroM (List Name)
-  /-- Resolves the given name to a overload list of global definitions.
+  /-- Resolves the given name to an overload list of global definitions.
   The `List String` in each alternative is the deduced list of projections
   (which are ambiguous with name components). -/
   resolveGlobalName : Name → MacroM (List (Prod Name (List String)))
@@ -4451,7 +4484,7 @@ def resolveNamespace (n : Name) : MacroM (List Name) := do
   (← getMethods).resolveNamespace n
 
 /--
-Resolves the given name to a overload list of global definitions.
+Resolves the given name to an overload list of global definitions.
 The `List String` in each alternative is the deduced list of projections
 (which are ambiguous with name components).
 -/

src/Init/SimpLemmas.lean

@@ -97,6 +97,7 @@ theorem dite_congr {_ : Decidable b} [Decidable c]
 @[simp] theorem false_implies (p : Prop) : (False → p) = True := eq_true False.elim
 @[simp] theorem implies_true (α : Sort u) : (α → True) = True := eq_true fun _ => trivial
 @[simp] theorem true_implies (p : Prop) : (True → p) = p := propext ⟨(· trivial), (fun _ => ·)⟩
+@[simp] theorem not_false_eq_true : (¬ False) = True := eq_true False.elim
 
 @[simp] theorem Bool.or_false (b : Bool) : (b || false) = b  := by cases b <;> rfl
 @[simp] theorem Bool.or_true (b : Bool) : (b || true) = true := by cases b <;> rfl
@@ -155,3 +156,6 @@ theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
 
 @[simp] theorem decide_False : decide False = false := rfl
 @[simp] theorem decide_True : decide True = true := rfl
+
+@[simp] theorem bne_iff_ne [BEq α] [LawfulBEq α] (a b : α) : a != b ↔ a ≠ b := by
+  simp [bne]; rw [← beq_iff_eq a b]; simp [-beq_iff_eq]

src/Init/SizeOfLemmas.lean

@@ -8,26 +8,26 @@ import Init.Meta
 import Init.SizeOf
 import Init.Data.Nat.Linear
 
-@[simp] theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
+@[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
   cases a; simp_arith
 
-@[simp] theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [UInt8.toNat]
 
-@[simp] theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [UInt16.toNat]
 
-@[simp] theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [UInt32.toNat]
 
-@[simp] theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [UInt64.toNat]
 
-@[simp] theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
+@[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 2 := by
   cases a; simp_arith [USize.toNat]
 
-@[simp] theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
+@[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 3 := by
   cases a; simp_arith [Char.toNat]
 
-@[simp] theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
+@[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
   cases s; simp_arith

src/Init/System/IO.lean

@@ -268,21 +268,7 @@ namespace FS
 
 namespace Handle
 
-private def fopenFlags (m : FS.Mode) (b : Bool) : String :=
-  let mode :=
-    match m with
-    | FS.Mode.read      => "r"
-    | FS.Mode.write     => "w"
-    | FS.Mode.readWrite => "r+"
-    | FS.Mode.append    => "a" ;
-  let bin := if b then "b" else "t"
-  mode ++ bin
-
-@[extern "lean_io_prim_handle_mk"] opaque mkPrim (fn : @& FilePath) (mode : @& String) : IO Handle
-
-def mk (fn : FilePath) (Mode : Mode) (bin : Bool := true) : IO Handle :=
-  mkPrim fn (fopenFlags Mode bin)
-
+@[extern "lean_io_prim_handle_mk"] opaque mk (fn : @& FilePath) (mode : FS.Mode) : IO Handle
 @[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit
 /--
 Read up to the given number of bytes from the handle.
@@ -308,6 +294,14 @@ end Handle
 @[extern "lean_io_remove_dir"] opaque removeDir : @& FilePath → IO Unit
 @[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit
 
+/--
+Moves a file or directory `old` to the new location `new`.
+
+This function coincides with the [POSIX `rename` function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/rename.html),
+see there for more information.
+-/
+@[extern "lean_io_rename"] opaque rename (old new : @& FilePath) : IO Unit
+
 end FS
 
 @[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String)
@@ -342,15 +336,15 @@ partial def Handle.readToEnd (h : Handle) : IO String := do
   loop ""
 
 def readBinFile (fname : FilePath) : IO ByteArray := do
-  let h ← Handle.mk fname Mode.read true
+  let h ← Handle.mk fname Mode.read
   h.readBinToEnd
 
 def readFile (fname : FilePath) : IO String := do
-  let h ← Handle.mk fname Mode.read false
+  let h ← Handle.mk fname Mode.read
   h.readToEnd
 
 partial def lines (fname : FilePath) : IO (Array String) := do
-  let h ← Handle.mk fname Mode.read false
+  let h ← Handle.mk fname Mode.read
   let rec read (lines : Array String) := do
     let line ← h.getLine
     if line.length == 0 then
@@ -364,11 +358,11 @@ partial def lines (fname : FilePath) : IO (Array String) := do
   read #[]
 
 def writeBinFile (fname : FilePath) (content : ByteArray) : IO Unit := do
-  let h ← Handle.mk fname Mode.write true
+  let h ← Handle.mk fname Mode.write
   h.write content
 
 def writeFile (fname : FilePath) (content : String) : IO Unit := do
-  let h ← Handle.mk fname Mode.write false
+  let h ← Handle.mk fname Mode.write
   h.putStr content
 
 def Stream.putStrLn (strm : FS.Stream) (s : String) : IO Unit :=
@@ -436,16 +430,18 @@ where
       return ()
     for d in (← p.readDir) do
       modify (·.push d.path)
-      let m ← d.path.metadata
-      match m.type with
-      | FS.FileType.symlink =>
+      match (← d.path.metadata.toBaseIO) with
+      | .ok { type := .symlink, .. } =>
         let p' ← FS.realPath d.path
         if (← p'.isDir) then
           -- do not call `enter` on a non-directory symlink
           if (← enter p) then
             go p'
-      | FS.FileType.dir => go d.path
-      | _ => pure ()
+      | .ok { type := .dir, .. } => go d.path
+      | .ok _ => pure ()
+      -- entry vanished, ignore
+      | .error (.noFileOrDirectory ..) => pure ()
+      | .error e => throw e
 
 end System.FilePath
 
@@ -548,6 +544,8 @@ structure SpawnArgs extends StdioConfig where
   cwd : Option FilePath := none
   /-- Add or remove environment variables for the process. -/
   env : Array (String × Option String) := #[]
+  /-- Start process in new session and process group using `setsid`. Currently a no-op on non-POSIX platforms. -/
+  setsid : Bool := false
 
 -- TODO(Sebastian): constructor must be private
 structure Child (cfg : StdioConfig) where
@@ -559,6 +557,10 @@ structure Child (cfg : StdioConfig) where
 
 @[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
+/-- Terminates the child process using the SIGTERM signal or a platform analogue.
+    If the process was started using `SpawnArgs.setsid`, terminates the entire process group instead. -/
+@[extern "lean_io_process_child_kill"] opaque Child.kill {cfg : @& StdioConfig} : @& Child cfg → IO Unit
+
 /--
 Extract the `stdin` field from a `Child` object, allowing them to be freed independently.
 This operation is necessary for closing the child process' stdin while still holding on to a process handle,

src/Init/Tactics.lean

@@ -36,13 +36,13 @@ be a `let` or function type.
   | ...
   ```
 -/
-syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic
+syntax (name := intro) "intro" notFollowedBy("|") (ppSpace colGt term:max)* : tactic
 
 /--
 `intros x...` behaves like `intro x...`, but then keeps introducing (anonymous)
 hypotheses until goal is not of a function type.
 -/
-syntax (name := intros) "intros " (colGt (ident <|> hole))* : tactic
+syntax (name := intros) "intros" (ppSpace colGt (ident <|> hole))* : tactic
 
 /--
 `rename t => x` renames the most recent hypothesis whose type matches `t`
@@ -54,20 +54,20 @@ syntax (name := rename) "rename " term " => " ident : tactic
 `revert x...` is the inverse of `intro x...`: it moves the given hypotheses
 into the main goal's target type.
 -/
-syntax (name := revert) "revert " (colGt term:max)+ : tactic
+syntax (name := revert) "revert" (ppSpace colGt term:max)+ : tactic
 
 /--
 `clear x...` removes the given hypotheses, or fails if there are remaining
 references to a hypothesis.
 -/
-syntax (name := clear) "clear " (colGt term:max)+ : tactic
+syntax (name := clear) "clear" (ppSpace colGt term:max)+ : tactic
 
 /--
 `subst x...` substitutes each `x` with `e` in the goal if there is a hypothesis
 of type `x = e` or `e = x`.
 If `x` is itself a hypothesis of type `y = e` or `e = y`, `y` is substituted instead.
 -/
-syntax (name := subst) "subst " (colGt term:max)+ : tactic
+syntax (name := subst) "subst" (ppSpace colGt term:max)+ : tactic
 
 /--
 Applies `subst` to all hypotheses of the form `h : x = t` or `h : t = x`.
@@ -220,20 +220,20 @@ In this setting all definitions that are not opaque are unfolded.
 syntax (name := withUnfoldingAll) "with_unfolding_all " tacticSeq : tactic
 
 /-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
-syntax (name := first) "first " withPosition((colGe "|" tacticSeq)+) : tactic
+syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
 /--
 `rotate_left n` rotates goals to the left by `n`. That is, `rotate_left 1`
 takes the main goal and puts it to the back of the subgoal list.
 If `n` is omitted, it defaults to `1`.
 -/
-syntax (name := rotateLeft) "rotate_left" (num)? : tactic
+syntax (name := rotateLeft) "rotate_left" (ppSpace num)? : tactic
 
 /--
 Rotate the goals to the right by `n`. That is, take the goal at the back
 and push it to the front `n` times. If `n` is omitted, it defaults to `1`.
 -/
-syntax (name := rotateRight) "rotate_right" (num)? : tactic
+syntax (name := rotateRight) "rotate_right" (ppSpace num)? : tactic
 
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
 macro "try " t:tacticSeq : tactic => `(tactic| first | $t | skip)
@@ -298,13 +298,13 @@ macro "infer_instance" : tactic => `(tactic| exact inferInstance)
 syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
 
 /-- The `*` location refers to all hypotheses and the goal. -/
-syntax locationWildcard := "*"
+syntax locationWildcard := " *"
 
 /--
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (colGt term:max)+ patternIgnore("⊢" <|> "|-")?
+syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore( atomic("|" noWs "-") <|> "⊢")?
 
 /--
 Location specifications are used by many tactics that can operate on either the
@@ -315,7 +315,7 @@ hypotheses or the goal. It can have one of the forms:
 * `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
 * `at *`: target all hypotheses and the goal
 -/
-syntax location := withPosition(" at " (locationWildcard <|> locationHyp))
+syntax location := withPosition(" at" (locationWildcard <|> locationHyp))
 
 /--
 * `change tgt'` will change the goal from `tgt` to `tgt'`,
@@ -376,13 +376,13 @@ Given `h : a::b = c::d`, the tactic `injection h` adds two new hypothesis with t
 `a = c` and `b = d` to the main goal.
 The tactic `injection h with h₁ h₂` uses the names `h₁` and `h₂` to name the new hypotheses.
 -/
-syntax (name := injection) "injection " term (" with " (colGt (ident <|> hole))+)? : tactic
+syntax (name := injection) "injection " term (" with" (ppSpace colGt (ident <|> hole))+)? : tactic
 
 /-- `injections` applies `injection` to all hypotheses recursively
 (since `injection` can produce new hypotheses). Useful for destructing nested
 constructor equalities like `(a::b::c) = (d::e::f)`. -/
 -- TODO: add with
-syntax (name := injections) "injections" (colGt (ident <|> hole))* : tactic
+syntax (name := injections) "injections" (ppSpace colGt (ident <|> hole))* : tactic
 
 /--
 The discharger clause of `simp` and related tactics.
@@ -448,7 +448,7 @@ syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
 This is a low-level tactic, it will expose how recursive definitions have been
 compiled by Lean.
 -/
-syntax (name := delta) "delta " (colGt ident)+ (location)? : tactic
+syntax (name := delta) "delta" (ppSpace colGt ident)+ (location)? : tactic
 
 /--
 * `unfold id` unfolds definition `id`.
@@ -458,7 +458,7 @@ For non-recursive definitions, this tactic is identical to `delta`.
 For definitions by pattern matching, it uses "equation lemmas" which are
 autogenerated for each match arm.
 -/
-syntax (name := unfold) "unfold " (colGt ident)+ (location)? : tactic
+syntax (name := unfold) "unfold" (ppSpace colGt ident)+ (location)? : tactic
 
 /--
 Auxiliary macro for lifting have/suffices/let/...
@@ -511,7 +511,7 @@ macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_la
 /-- Similar to `have`, but using `refine'` -/
 macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
 /-- Similar to `have`, but using `refine'` -/
-macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x : _ := $p)
+macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
 /-- Similar to `let`, but using `refine'` -/
 macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)
 
@@ -530,7 +530,7 @@ syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> synth
 After `with`, there is an optional tactic that runs on all branches, and
 then a list of alternatives.
 -/
-syntax inductionAlts := "with " (tactic)? withPosition((colGe inductionAlt)+)
+syntax inductionAlts := " with" (ppSpace tactic)? withPosition((colGe inductionAlt)+)
 
 /--
 Assuming `x` is a variable in the local context with an inductive type,
@@ -559,7 +559,7 @@ You can use `with` to provide the variables names for each constructor.
   uses tactic `tac₁` for the `zero` case, and `tac₂` for the `succ` case.
 -/
 syntax (name := induction) "induction " term,+ (" using " ident)?
-  ("generalizing " (colGt term:max)+)? (inductionAlts)? : tactic
+  (" generalizing" (ppSpace colGt term:max)+)? (inductionAlts)? : tactic
 
 /-- A `generalize` argument, of the form `term = x` or `h : term = x`. -/
 syntax generalizeArg := atomic(ident " : ")? term:51 " = " ident
@@ -604,11 +604,12 @@ You can use `with` to provide the variables names for each constructor.
 syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
 
 /-- `rename_i x_1 ... x_n` renames the last `n` inaccessible names using the given names. -/
-syntax (name := renameI) "rename_i " (colGt binderIdent)+ : tactic
+syntax (name := renameI) "rename_i" (ppSpace colGt binderIdent)+ : tactic
 
 /--
-`repeat tac` applies `tac` to main goal. If the application succeeds,
-the tactic is applied recursively to the generated subgoals until it eventually fails.
+`repeat tac` repeatedly applies `tac` to the main goal until it fails.
+That is, if `tac` produces multiple subgoals, only subgoals up to the first failure will be visited.
+The `Std` library provides `repeat'` which repeats separately in each subgoal.
 -/
 syntax "repeat " tacticSeq : tactic
 macro_rules
@@ -636,7 +637,7 @@ renamed used the `case` or `next` tactics.
 - `split` will split the goal (target).
 - `split at h` will split the hypothesis `h`.
 -/
-syntax (name := split) "split " (colGt term)? (location)? : tactic
+syntax (name := split) "split" (ppSpace colGt term)? (location)? : tactic
 
 /-- `dbg_trace "foo"` prints `foo` when elaborated.
 Useful for debugging tactic control flow:
@@ -689,7 +690,7 @@ example : ∀ x : Nat, x = x := by unhygienic
 macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t)
 
 /-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/
-syntax (name := fail) "fail " (str)? : tactic
+syntax (name := fail) "fail" (ppSpace str)? : tactic
 
 /--
 `checkpoint tac` acts the same as `tac`, but it caches the input and output of `tac`,
@@ -720,7 +721,7 @@ macro (name := save) "save" : tactic => `(tactic| skip)
 The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing.
 It is used for debugging purposes only.
 -/
-syntax (name := sleep) "sleep" num : tactic
+syntax (name := sleep) "sleep " num : tactic
 
 /--
 `exists e₁, e₂, ...` is shorthand for `refine ⟨e₁, e₂, ...⟩; try trivial`.
@@ -737,7 +738,7 @@ For example, given `⊢ f (g (x + y)) = f (g (y + x))`,
 `congr` produces the goals `⊢ x = y` and `⊢ y = x`,
 while `congr 2` produces the intended `⊢ x + y = y + x`.
 -/
-syntax (name := congr) "congr " (num)? : tactic
+syntax (name := congr) "congr" (ppSpace num)? : tactic
 
 end Tactic
 
@@ -785,7 +786,7 @@ If there are several with the same priority, it is uses the "most recent one". E
   cases d <;> rfl
 ```
 -/
-syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (prio)? : attr
+syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
 end Attr
 
 end Parser

src/Init/WF.lean

@@ -184,15 +184,9 @@ protected theorem caseStrongInductionOn
 
 end Nat
 
-def Measure {α : Sort u} : (α → Nat) → α → α → Prop :=
-  InvImage (fun a b => a < b)
-
 abbrev measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α :=
   invImage f Nat.lt_wfRel
 
-def SizeOfRef (α : Sort u) [SizeOf α] : α → α → Prop :=
-  Measure sizeOf
-
 abbrev sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α :=
   measure sizeOf
 

src/Lean/Compiler/IR/Checker.lean

@@ -16,6 +16,10 @@ def maxCtorFields := getMaxCtorFields ()
 opaque getMaxCtorScalarsSize : Unit → Nat
 def maxCtorScalarsSize := getMaxCtorScalarsSize ()
 
+@[extern c inline "lean_box(LeanMaxCtorTag)"]
+opaque getMaxCtorTag : Unit → Nat
+def maxCtorTag := getMaxCtorTag ()
+
 @[extern c inline "lean_box(sizeof(size_t))"]
 opaque getUSizeSize : Unit → Nat
 def usizeSize := getUSizeSize ()
@@ -113,6 +117,8 @@ def checkExpr (ty : IRType) : Expr → M Unit
   | Expr.ap x ys            => checkObjVar x *> checkArgs ys
   | Expr.fap f ys           => checkFullApp f ys
   | Expr.ctor c ys          => do
+    if c.cidx > maxCtorTag && (c.size > 0 || c.usize > 0 || c.ssize > 0) then
+      throw s!"tag for constructor '{c.name}' is too big, this is a limitation of the current runtime"
     if c.size > maxCtorFields then
       throw s!"constructor '{c.name}' has too many fields"
     if c.ssize + c.usize * usizeSize > maxCtorScalarsSize then
@@ -175,7 +181,7 @@ end Checker
 def checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit := do
   let env ← getEnv
   match (Checker.checkDecl decl { env := env, decls := decls }).run' {} with
-  | .error msg => throw s!"IR check failed at '{decl.name}', error: {msg}"
+  | .error msg => throw s!"compiler IR check failed at '{decl.name}', error: {msg}"
   | _ => pure ()
 
 def checkDecls (decls : Array Decl) : CompilerM Unit :=

src/Lean/Compiler/IR/EmitC.lean

@@ -687,9 +687,13 @@ def emitDeclInit (d : Decl) : M Unit := do
   let env ← getEnv
   let n := d.name
   if isIOUnitInitFn env n then
+    if isIOUnitBuiltinInitFn env n then
+      emit "if (builtin) {"
     emit "res = "; emitCName n; emitLn "(lean_io_mk_world());"
     emitLn "if (lean_io_result_is_error(res)) return res;"
     emitLn "lean_dec_ref(res);"
+    if isIOUnitBuiltinInitFn env n then
+      emit "}"
   else if d.params.size == 0 then
     match getInitFnNameFor? env d.name with
     | some initFn =>

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -415,24 +415,38 @@ def emitFnDeclAux (mod : LLVM.Module llvmctx)
   let env ← getEnv
   -- bollu: if we have a declaration with no parameters, then we emit it as a global pointer.
   -- bollu: Otherwise, we emit it as a function
+  let global ←
+    if ps.isEmpty then
+        let retty ← (toLLVMType decl.resultType)
+        let global ← LLVM.getOrAddGlobal mod cppBaseName retty
+        if !isExternal then
+          LLVM.setInitializer global (← LLVM.getUndef retty)
+        pure global
+    else
+        let retty ← (toLLVMType decl.resultType)
+        let mut argtys := #[]
+        for p in ps do
+          -- if it is extern, then we must not add irrelevant args
+          if !(isExternC env decl.name) || !p.ty.isIrrelevant then
+            argtys := argtys.push (← toLLVMType p.ty)
+        -- TODO (bollu): simplify this API, this code of `closureMaxArgs` is duplicated in multiple places.
+        if argtys.size > closureMaxArgs && isBoxedName decl.name then
+          argtys := #[← LLVM.pointerType (← LLVM.voidPtrType llvmctx)]
+        let fnty ← LLVM.functionType retty argtys (isVarArg := false)
+        LLVM.getOrAddFunction mod cppBaseName fnty
+  -- we must now set symbol visibility for global.
   if ps.isEmpty then
-      let retty ← (toLLVMType decl.resultType)
-      let global ← LLVM.getOrAddGlobal mod cppBaseName retty
-      if !isExternal then
-        LLVM.setInitializer global (← LLVM.getUndef retty)
-      return global
-  else
-      let retty ← (toLLVMType decl.resultType)
-      let mut argtys := #[]
-      for p in ps do
-        -- if it is extern, then we must not add irrelevant args
-        if !(isExternC env decl.name) || !p.ty.isIrrelevant then
-          argtys := argtys.push (← toLLVMType p.ty)
-      -- TODO (bollu): simplify this API, this code of `closureMaxArgs` is duplicated in multiple places.
-      if argtys.size > closureMaxArgs && isBoxedName decl.name then
-        argtys := #[← LLVM.pointerType (← LLVM.voidPtrType llvmctx)]
-      let fnty ← LLVM.functionType retty argtys (isVarArg := false)
-      LLVM.getOrAddFunction mod cppBaseName fnty
+    if isClosedTermName env decl.name then LLVM.setVisibility global LLVM.Visibility.hidden -- static
+    else if isExternal then pure () -- extern (Recall that C/LLVM funcs are extern linkage by default.)
+    else LLVM.setDLLStorageClass global LLVM.DLLStorageClass.export  -- LEAN_EXPORT
+  else if !isExternal
+    -- An extern decl might be linked in from a different translation unit.
+    -- Thus, we cannot export an external declaration as we do not define it,
+    -- only declare its presence.
+    -- So, we only export non-external definitions.
+    then LLVM.setDLLStorageClass global LLVM.DLLStorageClass.export
+  return global
+
 
 def emitFnDecl (decl : Decl) (isExternal : Bool) : M llvmctx Unit := do
   let cppBaseName ← toCName decl.name
@@ -1137,6 +1151,14 @@ def emitDeclAux (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) (d
           argtys := argtys.push (← toLLVMType x.ty)
       let fnty ← LLVM.functionType retty argtys (isVarArg := false)
       let llvmfn ← LLVM.getOrAddFunction mod name fnty
+      -- set linkage and visibility
+      -- TODO: consider refactoring these into a separate concept (e.g. 'setLinkageAndVisibility')
+      --       Find the spots where this refactor needs to happen by grepping for 'LEAN_EXPORT'
+      --       in the C backend
+      if xs.size == 0 then
+        LLVM.setVisibility llvmfn LLVM.Visibility.hidden -- "static "
+      else
+        LLVM.setDLLStorageClass llvmfn LLVM.DLLStorageClass.export  -- LEAN_EXPORT: make symbol visible to the interpreter
       withReader (fun llvmctx => { llvmctx with mainFn := f, mainParams := xs }) do
         set { var2val := default, jp2bb := default : EmitLLVM.State llvmctx } -- flush variable map
         let bb ← LLVM.appendBasicBlockInContext llvmctx llvmfn "entry"
@@ -1247,10 +1269,12 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
 
   let initFnTy ← LLVM.functionType (← LLVM.voidPtrType llvmctx) #[ (← LLVM.i8Type llvmctx), (← LLVM.voidPtrType llvmctx)] (isVarArg := false)
   let initFn ← LLVM.getOrAddFunction mod (mkModuleInitializationFunctionName modName) initFnTy
+  LLVM.setDLLStorageClass initFn LLVM.DLLStorageClass.export  -- LEAN_EXPORT
   let entryBB ← LLVM.appendBasicBlockInContext llvmctx initFn "entry"
   LLVM.positionBuilderAtEnd builder entryBB
   let ginit?ty := ← LLVM.i1Type llvmctx
   let ginit?slot ← LLVM.getOrAddGlobal mod (modName.mangle ++ "_G_initialized") ginit?ty
+  LLVM.setVisibility ginit?slot LLVM.Visibility.hidden -- static
   LLVM.setInitializer ginit?slot (← LLVM.constFalse llvmctx)
   let ginit?v ← LLVM.buildLoad2 builder ginit?ty ginit?slot "init_v"
   buildIfThen_ builder "isGInitialized" ginit?v

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -294,6 +294,28 @@ opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit
 opaque disposeModule (m : Module ctx) : BaseIO Unit
 
 
+-- https://github.com/llvm/llvm-project/blob/c3e073bcbdc523b0f758d44a89a6333e38bff863/llvm/include/llvm-c/Core.h#L198
+structure Visibility where
+  private mk :: val : UInt64
+
+def Visibility.default   : Visibility := { val := 0 }
+def Visibility.hidden    : Visibility := { val := 1 }
+def Visibility.protected : Visibility := { val := 2 }
+
+@[extern "lean_llvm_set_visibility"]
+opaque setVisibility {ctx : Context} (value : Value ctx) (visibility : Visibility) : BaseIO Unit
+
+-- https://github.com/llvm/llvm-project/blob/c3e073bcbdc523b0f758d44a89a6333e38bff863/llvm/include/llvm-c/Core.h#L210
+structure DLLStorageClass where
+  private mk :: val : UInt64
+
+def DLLStorageClass.default : DLLStorageClass := { val := 0 }
+def DLLStorageClass.import  : DLLStorageClass := { val := 1 }
+def DLLStorageClass.export  : DLLStorageClass := { val := 2 }
+
+@[extern "lean_llvm_set_dll_storage_class"]
+opaque setDLLStorageClass {ctx : Context} (value : Value ctx) (dllStorageClass : DLLStorageClass) : BaseIO Unit
+
 -- Helper to add a function if it does not exist, and to return the function handle if it does.
 def getOrAddFunction(m : Module ctx) (name : String) (type : LLVMType ctx) : BaseIO (Value ctx) :=  do
   match (← getNamedFunction m name) with

src/Lean/Compiler/InitAttr.lean

@@ -54,14 +54,23 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
       let ctx ← read
       if runAfterImport && (← isInitializerExecutionEnabled) then
         for mod in ctx.env.header.moduleNames,
+            modData in ctx.env.header.moduleData,
             modEntries in entries do
           -- any native Lean code reachable by the interpreter (i.e. from shared
           -- libraries with their corresponding module in the Environment) must
           -- first be initialized
-          if !(← runModInit mod) then
-            -- If no native code for the module is available, run `[init]` decls manually.
-            -- All other constants (nullary functions) are lazily initialized by the interpreter.
-            for (decl, initDecl) in modEntries do
+          if (← runModInit mod) then
+            continue
+          -- If no native code for the module is available, run `[init]` decls manually.
+          -- All other constants (nullary functions) are lazily initialized by the interpreter.
+          if modEntries.isEmpty then
+            -- If there are no `[init]` decls, don't bother walking through all module decls.
+            -- We do this after trying `runModInit` as that one may also efficiently initialize
+            -- nullary functions.
+            continue
+          for c in modData.constNames do
+            -- make sure to run initializers in declaration order, not extension state order, to respect dependencies
+            if let some (decl, initDecl) := modEntries.binSearch (c, default) (Name.quickLt ·.1 ·.1) then
               if initDecl.isAnonymous then
                 let initFn ← IO.ofExcept <| ctx.env.evalConst (IO Unit) ctx.opts decl
                 initFn

src/Lean/Compiler/LCNF/Main.lean

@@ -72,8 +72,8 @@ def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDe
   decls := markRecDecls decls
   let manager ← getPassManager
   for pass in manager.passes do
-    trace[Compiler] "Running pass: {pass.name}"
-    decls ← withPhase pass.phase <| pass.run decls
+    decls ← withTraceNode `Compiler (fun _ => return m!"new compiler phase: {pass.phase}, pass: {pass.name}") do
+      withPhase pass.phase <| pass.run decls
     withPhase pass.phaseOut <| checkpoint pass.name decls
   if (← Lean.isTracingEnabledFor `Compiler.result) then
     for decl in decls do
@@ -94,7 +94,8 @@ def showDecl (phase : Phase) (declName : Name) : CoreM Format := do
 @[export lean_lcnf_compile_decls]
 def main (declNames : List Name) : CoreM Unit := do
   profileitM Exception "compilation new" (← getOptions) do
-    CompilerM.run <| discard <| PassManager.run declNames.toArray
+    withTraceNode `Compiler (fun _ => return m!"compiling new: {declNames}") do
+      CompilerM.run <| discard <| PassManager.run declNames.toArray
 
 builtin_initialize
   registerTraceClass `Compiler.init (inherited := true)

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -219,7 +219,10 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
   incVisited
   match code with
   | .let decl k =>
-    let mut decl ← normLetDecl decl
+    let baseDecl := decl
+    let mut decl ← normLetDecl baseDecl
+    if baseDecl != decl then
+      markSimplified
     if let some value ← simpValue? decl.value then
       markSimplified
       decl ← decl.updateValue value

src/Lean/Compiler/Specialize.lean

@@ -79,7 +79,7 @@ inductive SpecArgKind where
 
 structure SpecInfo where
   mutualDecls : List Name
-  argKinds : SpecArgKind
+  argKinds : List SpecArgKind
   deriving Inhabited
 
 structure SpecState where

src/Lean/CoreM.lean

@@ -19,6 +19,8 @@ register_builtin_option maxHeartbeats : Nat := {
   descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit"
 }
 
+builtin_initialize registerTraceClass `Kernel
+
 def getMaxHeartbeats (opts : Options) : Nat :=
   maxHeartbeats.get opts * 1000
 
@@ -271,11 +273,13 @@ def mkArrow (d b : Expr) : CoreM Expr :=
   return Lean.mkForall (← mkFreshUserName `x) BinderInfo.default d b
 
 def addDecl (decl : Declaration) : CoreM Unit := do
-  if !(← MonadLog.hasErrors) && decl.hasSorry then
-    logWarning "declaration uses 'sorry'"
-  match (← getEnv).addDecl decl with
-  | Except.ok    env => setEnv env
-  | Except.error ex  => throwKernelException ex
+  profileitM Exception "type checking" (← getOptions) do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
+      if !(← MonadLog.hasErrors) && decl.hasSorry then
+        logWarning "declaration uses 'sorry'"
+      match (← getEnv).addDecl decl with
+      | Except.ok    env => setEnv env
+      | Except.error ex  => throwKernelException ex
 
 private def supportedRecursors :=
   #[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
@@ -294,13 +298,21 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla
     | some (Expr.const declName ..) => throwError "code generator does not support recursor '{declName}' yet, consider using 'match ... with' and/or structural recursion"
     | _ => pure ()
 
+register_builtin_option compiler.enableNew : Bool := {
+  defValue := true
+  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"
+}
+
 -- Forward declaration
 @[extern "lean_lcnf_compile_decls"]
 opaque compileDeclsNew (declNames : List Name) : CoreM Unit
 
 def compileDecl (decl : Declaration) : CoreM Unit := do
-  compileDeclsNew (Compiler.getDeclNamesForCodeGen decl)
-  match (← getEnv).compileDecl (← getOptions) decl with
+  let opts ← getOptions
+  if compiler.enableNew.get opts then
+    compileDeclsNew (Compiler.getDeclNamesForCodeGen decl)
+  match (← getEnv).compileDecl opts decl with
   | Except.ok env   => setEnv env
   | Except.error (KernelException.other msg) =>
     checkUnsupported decl -- Generate nicer error message for unsupported recursors and axioms
@@ -309,8 +321,10 @@ def compileDecl (decl : Declaration) : CoreM Unit := do
     throwKernelException ex
 
 def compileDecls (decls : List Name) : CoreM Unit := do
-  compileDeclsNew decls
-  match (← getEnv).compileDecls (← getOptions) decls with
+  let opts ← getOptions
+  if compiler.enableNew.get opts then
+    compileDeclsNew decls
+  match (← getEnv).compileDecls opts decls with
   | Except.ok env   => setEnv env
   | Except.error (KernelException.other msg) =>
     throwError msg

src/Lean/Data/HashMap.lean

@@ -38,7 +38,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; rw [Nat.zero_mod]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Data/HashSet.lean

@@ -34,7 +34,7 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
   if h' : u.toNat < sz then
     ⟨u, h'⟩
   else
-    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; rw [Nat.zero_mod]; apply Nat.pos_of_isPowerOfTwo h⟩
+    ⟨0, by simp [USize.toNat, OfNat.ofNat, USize.ofNat, Fin.ofNat']; apply Nat.pos_of_isPowerOfTwo h⟩
 
 @[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
   let ⟨i, h⟩ := mkIdx (hashFn a) data.property

src/Lean/Data/Json/FromToJson.lean

@@ -81,8 +81,8 @@ instance : FromJson Name where
     if s == "[anonymous]" then
       return Name.anonymous
     else
-      let some n := Syntax.decodeNameLit ("`" ++ s)
-        | throw s!"expected a `Name`, got '{j}'"
+      let n := s.toName
+      if n.isAnonymous then throw s!"expected a `Name`, got '{j}'"
       return n
 
 instance : ToJson Name where

src/Lean/Data/Lsp/Internal.lean

@@ -34,9 +34,10 @@ def fromString (s : String) : Except String RefIdent := do
   -- See `FromJson Name`
   let name ← match sName with
     | "[anonymous]" => pure Name.anonymous
-    | _ => match Syntax.decodeNameLit ("`" ++ sName) with
-      | some n => pure n
-      | none => throw s!"expected a Name, got {sName}"
+    | _ =>
+      let n := sName.toName
+      if n.isAnonymous then throw s!"expected a Name, got {sName}"
+      else pure n
   match sPrefix with
     | "c:" => return RefIdent.const name
     | "f:" => return RefIdent.fvar <| FVarId.mk name

src/Lean/Data/Name.lean

@@ -96,16 +96,6 @@ def quickCmp (n₁ n₂ : Name) : Ordering :=
 def quickLt (n₁ n₂ : Name) : Bool :=
   quickCmp n₁ n₂ == Ordering.lt
 
-/-- Alternative HasLt instance. -/
-@[inline] protected def hasLtQuick : LT Name :=
-  ⟨fun a b => Name.quickLt a b = true⟩
-
-@[inline] def Name.decLt : DecidableRel (@LT.lt Name Name.hasLtQuick) :=
-  inferInstanceAs (DecidableRel fun a b => Name.quickLt a b = true)
-
-instance : DecidableRel (@LT.lt Name Name.hasLtQuick) :=
-  Name.decLt
-
 /-- The frontend does not allow user declarations to start with `_` in any of its parts.
    We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
 def isInternal : Name → Bool
@@ -161,7 +151,3 @@ end Name
 end Lean
 
 open Lean
-
-def String.toName (s : String) : Name :=
-  let ps := s.splitOn ".";
-  ps.foldl (fun n p => Name.mkStr n p.trim) Name.anonymous

src/Lean/Data/Options.lean

@@ -62,28 +62,6 @@ def getOptionDescr (name : Name) : IO String := do
   let decl ← getOptionDecl name
   pure decl.descr
 
-def setOptionFromString (opts : Options) (entry : String) : IO Options := do
-  let ps := (entry.splitOn "=").map String.trim
-  let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'"
-  let key := Name.mkSimple key
-  let defValue ← getOptionDefaultValue key
-  match defValue with
-  | DataValue.ofString _ => pure $ opts.setString key val
-  | DataValue.ofBool _   =>
-    if key == `true then pure $ opts.setBool key true
-    else if key == `false then pure $ opts.setBool key false
-    else throw $ IO.userError s!"invalid Bool option value '{val}'"
-  | DataValue.ofName _   => pure $ opts.setName key val.toName
-  | DataValue.ofNat _    =>
-    match val.toNat? with
-    | none   => throw (IO.userError s!"invalid Nat option value '{val}'")
-    | some v => pure $ opts.setNat key v
-  | DataValue.ofInt _    =>
-    match val.toInt? with
-    | none   => throw (IO.userError s!"invalid Int option value '{val}'")
-    | some v => pure $ opts.setInt key v
-  | DataValue.ofSyntax _ => throw (IO.userError s!"invalid Syntax option value")
-
 class MonadOptions (m : Type → Type) where
   getOptions : m Options
 

src/Lean/Elab/AutoBound.lean

@@ -11,7 +11,7 @@ namespace Lean.Elab
 
 register_builtin_option autoImplicit : Bool := {
     defValue := true
-    descr    := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only a lower case or greek letter followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
+    descr    := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only single character followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
   }
 
 register_builtin_option relaxedAutoImplicit : Bool := {
@@ -39,7 +39,7 @@ Therefore, we do consider identifier with macro scopes anymore.
 
 def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool :=
   match n with
-  | .str .anonymous s => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
+  | .str .anonymous s => s.length > 0 && (relaxed || isValidAutoBoundSuffix s)
   | _ => false
 
 def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=

src/Lean/Elab/Binders.lean

@@ -182,7 +182,10 @@ register_builtin_option checkBinderAnnotations : Bool := {
 /-- Throw an error if `type` is not a valid local instance. -/
 private partial def checkLocalInstanceParameters (type : Expr) : TermElabM Unit := do
   let .forallE n d b bi ← whnf type | return ()
-  if !b.hasLooseBVar 0 then
+  -- We allow instance arguments so that local instances of the form
+  -- `variable [∀ (a : α) [P a], Q a]`
+  -- are accepted, per https://github.com/leanprover/lean4/issues/2311
+  if bi != .instImplicit && !b.hasLooseBVar 0 then
     throwError "invalid parametric local instance, parameter with type{indentExpr d}\ndoes not have forward dependencies, type class resolution cannot use this kind of local instance because it will not be able to infer a value for this parameter."
   withLocalDecl n bi d fun x => checkLocalInstanceParameters (b.instantiate1 x)
 
@@ -421,9 +424,8 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat
       let s := { s with lctx }
       match ← isClass? type, kind with
       | some className, .default =>
-        resettingSynthInstanceCache do
-          let localInsts := s.localInsts.push { className, fvar := mkFVar fvarId }
-          elabFunBinderViews binderViews (i+1) { s with localInsts }
+        let localInsts := s.localInsts.push { className, fvar := mkFVar fvarId }
+        elabFunBinderViews binderViews (i+1) { s with localInsts }
       | _, _ => elabFunBinderViews binderViews (i+1) s
   else
     pure s
@@ -445,7 +447,7 @@ def elabFunBinders (binders : Array Syntax) (expectedType? : Option Expr) (x : A
     let lctx ← getLCtx
     let localInsts ← getLocalInstances
     let s ← FunBinders.elabFunBindersAux binders 0 { lctx, localInsts, expectedType? }
-    resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) <| withLCtx s.lctx s.localInsts <|
+    withLCtx s.lctx s.localInsts do
       x s.fvars s.expectedType?
 
 def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
@@ -690,7 +692,7 @@ structure LetIdDeclView where
   value   : Syntax
 
 def mkLetIdDeclView (letIdDecl : Syntax) : LetIdDeclView :=
-  -- `letIdDecl` is of the form `ident >> many bracketedBinder >> optType >> " := " >> termParser
+  -- `letIdDecl` is of the form `binderIdent >> many bracketedBinder >> optType >> " := " >> termParser
   let id      := letIdDecl[0]
   let binders := letIdDecl[1].getArgs
   let optType := letIdDecl[2]
@@ -709,6 +711,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
   let body    := stx[3]
   if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then
     let { id, binders, type, value } := mkLetIdDeclView letDecl
+    let id ← if id.isIdent then pure id else mkFreshIdent id (canonical := true)
     elabLetDeclAux id binders type value body expectedType? useLetExpr elabBodyFirst usedLetOnly
   else if letDecl.getKind == ``Lean.Parser.Term.letPatDecl then
     -- node `Lean.Parser.Term.letPatDecl  $ try (termParser >> pushNone >> optType >> " := ") >> termParser
@@ -718,7 +721,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B
     let optType := letDecl[2]
     let val     := letDecl[4]
     if pat.getKind == ``Parser.Term.hole then
-      -- `let _ := ...` should not be treated at a `letIdDecl`
+      -- `let _ := ...` should not be treated as a `letIdDecl`
       let id   ← mkFreshIdent pat (canonical := true)
       let type := expandOptType id optType
       elabLetDeclAux id #[] type val body expectedType? useLetExpr elabBodyFirst usedLetOnly

src/Lean/Elab/BuiltinCommand.lean

@@ -52,14 +52,19 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
   for _ in [0:numScopes] do
     popScope
 
-private def checkAnonymousScope : List Scope → Bool
-  | { header := "", .. } :: _   => true
-  | _                           => false
+private def checkAnonymousScope : List Scope → Option Name
+  | { header := "", .. } :: _ => none
+  | { header := h, .. }  :: _ => some h
+  | _                         => some .anonymous -- should not happen
 
-private def checkEndHeader : Name → List Scope → Bool
-  | .anonymous, _                             => true
-  | .str p s,   { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
-  | _,          _                             => false
+private def checkEndHeader : Name → List Scope → Option Name
+  | .anonymous, _ => none
+  | .str p s, { header := h, .. } :: scopes =>
+    if h == s then
+      (.str · s) <$> checkEndHeader p scopes
+    else
+      some h
+  | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>
   match stx with
@@ -94,12 +99,12 @@ private def checkEndHeader : Name → List Scope → Bool
     throwError "invalid 'end', insufficient scopes"
   match header? with
   | none        =>
-    unless checkAnonymousScope scopes do
-      throwError "invalid 'end', name is missing"
+    if let some name := checkAnonymousScope scopes then
+      throwError "invalid 'end', name is missing (expected {name})"
   | some header =>
-    unless checkEndHeader header scopes do
+    if let some name := checkEndHeader header scopes then
       addCompletionInfo <| CompletionInfo.endSection stx (scopes.map fun scope => scope.header)
-      throwError "invalid 'end', name mismatch"
+      throwError "invalid 'end', name mismatch (expected {if name == `«» then `nothing else name})"
 
 private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM Unit :=
   if h : i < cmds.size then

src/Lean/Elab/BuiltinNotation.lean

@@ -104,17 +104,25 @@ open Meta
 
 @[builtin_macro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
   match stx with
-  | `(have $x $bs* $[: $type]? := $val; $body)            => `(let_fun $x $bs* $[: $type]? := $val; $body)
-  | `(have%$tk $[: $type]? := $val; $body)                => `(have $(mkIdentFrom tk `this (canonical := true)) $[: $type]? := $val; $body)
-  | `(have $x $bs* $[: $type]? $alts; $body)              => `(let_fun $x $bs* $[: $type]? $alts; $body)
-  | `(have%$tk $[: $type]? $alts:matchAlts; $body)        => `(have $(mkIdentFrom tk `this (canonical := true)) $[: $type]? $alts:matchAlts; $body)
-  | `(have $pattern:term $[: $type]? := $val:term; $body) => `(let_fun $pattern:term $[: $type]? := $val:term ; $body)
-  | _                                                     => Macro.throwUnsupported
+  | `(have $hy:hygieneInfo $bs* $[: $type]? := $val; $body) =>
+    `(have $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $type]? := $val; $body)
+  | `(have $hy:hygieneInfo $bs* $[: $type]? $alts; $body)   =>
+    `(have $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $type]? $alts; $body)
+  | `(have $x:ident $bs* $[: $type]? := $val; $body) => `(let_fun $x $bs* $[: $type]? := $val; $body)
+  | `(have $x:ident $bs* $[: $type]? $alts; $body)   => `(let_fun $x $bs* $[: $type]? $alts; $body)
+  | `(have _%$x     $bs* $[: $type]? := $val; $body) => `(let_fun _%$x $bs* $[: $type]? := $val; $body)
+  | `(have _%$x     $bs* $[: $type]? $alts; $body)   => `(let_fun _%$x $bs* $[: $type]? $alts; $body)
+  | `(have $pattern:term $[: $type]? := $val; $body) => `(let_fun $pattern:term $[: $type]? := $val; $body)
+  | _                                                => Macro.throwUnsupported
 
 @[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices%$tk $[$x :]? $type from $val; $body)            => `(have%$tk $[$x]? : $type := $body; $val)
-  | `(suffices%$tk $[$x :]? $type by%$b $tac:tacticSeq; $body) => `(have%$tk $[$x]? : $type := $body; by%$b $tac)
-  | _                                                          => Macro.throwUnsupported
+  | `(suffices%$tk $x:ident      : $type from $val; $body)            => `(have%$tk $x : $type := $body; $val)
+  | `(suffices%$tk _%$x          : $type from $val; $body)            => `(have%$tk _%$x : $type := $body; $val)
+  | `(suffices%$tk $hy:hygieneInfo $type from $val; $body)            => `(have%$tk $hy:hygieneInfo : $type := $body; $val)
+  | `(suffices%$tk $x:ident      : $type by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac)
+  | `(suffices%$tk _%$x          : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac)
+  | `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac)
+  | _                                                                 => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do

src/Lean/Elab/BuiltinTerm.lean

@@ -157,7 +157,7 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
 
-@[builtin_term_elab cdot] def elabBadCDot : TermElab := fun _ _ =>
+@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun _ _ =>
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
 @[builtin_term_elab str] def elabStrLit : TermElab := fun stx _ => do

src/Lean/Elab/Command.lean

@@ -47,7 +47,9 @@ structure Context where
 abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
 abbrev CommandElabM := CommandElabCoreM Exception
 abbrev CommandElab  := Syntax → CommandElabM Unit
-abbrev Linter := Syntax → CommandElabM Unit
+structure Linter where
+  run : Syntax → CommandElabM Unit
+  name : Name := by exact decl_name%
 
 /-
 Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
@@ -68,6 +70,7 @@ def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options :=
 /- Linters should be loadable as plugins, so store in a global IO ref instead of an attribute managed by the
     environment (which only contains `import`ed objects). -/
 builtin_initialize lintersRef : IO.Ref (Array Linter) ← IO.mkRef #[]
+builtin_initialize registerTraceClass `Elab.lint
 
 def addLinter (l : Linter) : IO Unit := do
   let ls ← lintersRef.get
@@ -157,8 +160,8 @@ def liftCoreM (x : CoreM α) : CommandElabM α := do
   modify fun s => { s with
     env := coreS.env
     ngen := coreS.ngen
-    messages := addTraceAsMessagesCore ctx (s.messages ++ coreS.messages) coreS.traceState
-    traceState := coreS.traceState
+    messages := s.messages ++ coreS.messages
+    traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
     infoState.trees := s.infoState.trees.append coreS.infoState.trees
   }
   match ea with
@@ -195,17 +198,20 @@ instance : MonadLog CommandElabM where
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data }
     modify fun s => { s with messages := s.messages.add msg }
 
-def runLinters (stx : Syntax) : CommandElabM Unit := do profileitM Exception "linting" (← getOptions) do
-  let linters ← lintersRef.get
-  unless linters.isEmpty do
-    for linter in linters do
-      let savedState ← get
-      try
-        linter stx
-      catch ex =>
-        logException ex
-      finally
-        modify fun s => { savedState with messages := s.messages }
+def runLinters (stx : Syntax) : CommandElabM Unit := do
+  profileitM Exception "linting" (← getOptions) do
+    withTraceNode `Elab.lint (fun _ => return m!"running linters") do
+      let linters ← lintersRef.get
+      unless linters.isEmpty do
+        for linter in linters do
+          withTraceNode `Elab.lint (fun _ => return m!"running linter: {linter.name}") do
+            let savedState ← get
+            try
+              linter.run stx
+            catch ex =>
+              logException ex
+            finally
+              modify fun s => { savedState with messages := s.messages }
 
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
@@ -274,8 +280,7 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
         -- list of commands => elaborate in order
         -- The parser will only ever return a single command at a time, but syntax quotations can return multiple ones
         args.forM elabCommand
-      else do
-        trace `Elab.command fun _ => stx;
+      else withTraceNode `Elab.command (fun _ => return stx) do
         let s ← get
         match (← liftMacroM <| expandMacroImpl? s.env stx) with
         | some (decl, stxNew?) =>
@@ -299,8 +304,7 @@ builtin_initialize registerTraceClass `Elab.input
 `elabCommand` wrapper that should be used for the initial invocation, not for recursive calls after
 macro expansion etc.
 -/
-def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do
-  trace[Elab.input] stx
+def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do profileitM Exception "elaboration" (← getOptions) do
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
   let initInfoTrees ← getResetInfoTrees
   -- We should *not* factor out `elabCommand`'s `withLogging` to here since it would make its error
@@ -395,14 +399,15 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   let x : TermElabM _  := withSaveInfoContext x
   let x : MetaM _      := (observing x).run (mkTermContext ctx s) { levelNames := scope.levelNames }
   let x : CoreM _      := x.run mkMetaContext {}
-  let x : EIO _ _      := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled }
+  let x : EIO _ _      := x.run (mkCoreContext ctx s heartbeats) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope, infoState.enabled := s.infoState.enabled, traceState := s.traceState }
   let (((ea, _), _), coreS) ← liftEIO x
   modify fun s => { s with
-    env             := coreS.env
-    nextMacroScope  := coreS.nextMacroScope
-    ngen            := coreS.ngen
-    infoState.trees := s.infoState.trees.append coreS.infoState.trees
-    messages        := addTraceAsMessagesCore ctx (s.messages ++ coreS.messages) coreS.traceState
+    env               := coreS.env
+    nextMacroScope    := coreS.nextMacroScope
+    ngen              := coreS.ngen
+    infoState.trees   := s.infoState.trees.append coreS.infoState.trees
+    traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
+    messages          := s.messages ++ coreS.messages
   }
   match ea with
   | Except.ok a     => pure a

src/Lean/Elab/Do.lean

@@ -49,7 +49,7 @@ private def letDeclArgHasBinders (letDeclArg : Syntax) : Bool :=
   else if k == ``Parser.Term.letEqnsDecl then
     true
   else if k == ``Parser.Term.letIdDecl then
-    -- letIdLhs := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> letIdBinder)) >> optType
+    -- letIdLhs := binderIdent >> checkWsBefore "expected space before binders" >> many (ppSpace >> letIdBinder)) >> optType
     let binders := letDeclArg[1]
     binders.getNumArgs > 0
   else
@@ -584,8 +584,11 @@ def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlo
   let terminal ← liftMacroM <| convertTerminalActionIntoJmp terminal.code jp xs
   return { code  := attachJP jpDecl terminal, uvars := k.uvars }
 
-def getLetIdDeclVar (letIdDecl : Syntax) : Var :=
-  letIdDecl[0]
+def getLetIdDeclVars (letIdDecl : Syntax) : Array Var :=
+  if letIdDecl[0].isIdent then
+    #[letIdDecl[0]]
+  else
+    #[]
 
 -- support both regular and syntax match
 def getPatternVarsEx (pattern : Syntax) : TermElabM (Array Var) :=
@@ -600,17 +603,20 @@ def getLetPatDeclVars (letPatDecl : Syntax) : TermElabM (Array Var) := do
   let pattern := letPatDecl[0]
   getPatternVarsEx pattern
 
-def getLetEqnsDeclVar (letEqnsDecl : Syntax) : Var :=
-  letEqnsDecl[0]
+def getLetEqnsDeclVars (letEqnsDecl : Syntax) : Array Var :=
+  if letEqnsDecl[0].isIdent then
+    #[letEqnsDecl[0]]
+  else
+    #[]
 
 def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var) := do
   let arg := letDecl[0]
   if arg.getKind == ``Parser.Term.letIdDecl then
-    return #[getLetIdDeclVar arg]
+    return getLetIdDeclVars arg
   else if arg.getKind == ``Parser.Term.letPatDecl then
     getLetPatDeclVars arg
   else if arg.getKind == ``Parser.Term.letEqnsDecl then
-    return #[getLetEqnsDeclVar arg]
+    return getLetEqnsDeclVars arg
   else
     throwError "unexpected kind of let declaration"
 
@@ -618,11 +624,11 @@ def getDoLetVars (doLet : Syntax) : TermElabM (Array Var) :=
   -- leading_parser "let " >> optional "mut " >> letDecl
   getLetDeclVars doLet[2]
 
-def getHaveIdLhsVar (optIdent : Syntax) : TermElabM Var :=
-  if optIdent.isNone then
-    `(this)
+def getHaveIdLhsVar (optIdent : Syntax) : Var :=
+  if optIdent.getKind == hygieneInfoKind then
+    HygieneInfo.mkIdent optIdent[0] `this
   else
-    pure optIdent[0]
+    optIdent
 
 def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) := do
   -- doHave := leading_parser "have " >> Term.haveDecl
@@ -630,13 +636,13 @@ def getDoHaveVars (doHave : Syntax) : TermElabM (Array Var) := do
   let arg := doHave[1][0]
   if arg.getKind == ``Parser.Term.haveIdDecl then
     -- haveIdDecl := leading_parser atomic (haveIdLhs >> " := ") >> termParser
-    -- haveIdLhs := optional (ident >> many (ppSpace >> letIdBinder)) >> optType
-    return #[← getHaveIdLhsVar arg[0]]
+    -- haveIdLhs := (binderIdent <|> hygieneInfo) >> many letIdBinder >> optType
+    return #[getHaveIdLhsVar arg[0]]
   else if arg.getKind == ``Parser.Term.letPatDecl then
     getLetPatDeclVars arg
   else if arg.getKind == ``Parser.Term.haveEqnsDecl then
     -- haveEqnsDecl := leading_parser haveIdLhs >> matchAlts
-    return #[← getHaveIdLhsVar arg[0]]
+    return #[getHaveIdLhsVar arg[0]]
   else
     throwError "unexpected kind of have declaration"
 
@@ -672,7 +678,7 @@ def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var) := do
 def getDoReassignVars (doReassign : Syntax) : TermElabM (Array Var) := do
   let arg := doReassign[0]
   if arg.getKind == ``Parser.Term.letIdDecl then
-    return #[getLetIdDeclVar arg]
+    return getLetIdDeclVars arg
   else if arg.getKind == ``Parser.Term.letPatDecl then
     getLetPatDeclVars arg
   else

src/Lean/Elab/Extra.lean

@@ -209,11 +209,11 @@ private structure AnalyzeResult where
   max?            : Option Expr := none
   hasUncomparable : Bool := false -- `true` if there are two types `α` and `β` where we don't have coercions in any direction.
 
-private def isUnknow : Expr → Bool
+private def isUnknown : Expr → Bool
   | .mvar ..        => true
-  | .app f _        => isUnknow f
-  | .letE _ _ _ b _ => isUnknow b
-  | .mdata _ b      => isUnknow b
+  | .app f _        => isUnknown f
+  | .letE _ _ _ b _ => isUnknown b
+  | .mdata _ b      => isUnknown b
   | _               => false
 
 private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM AnalyzeResult := do
@@ -222,7 +222,7 @@ private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM Analyze
     | none => pure none
     | some expectedType =>
       let expectedType ← instantiateMVars expectedType
-      if isUnknow expectedType then pure none else pure (some expectedType)
+      if isUnknown expectedType then pure none else pure (some expectedType)
   (go t *> get).run' { max? }
 where
    go (t : Tree) : StateRefT AnalyzeResult TermElabM Unit := do
@@ -233,7 +233,7 @@ where
        | .unop _ _ arg => go arg
        | .term _ _ val =>
          let type ← instantiateMVars (← inferType val)
-         unless isUnknow type do
+         unless isUnknown type do
            match (← get).max? with
            | none     => modify fun s => { s with max? := type }
            | some max =>
@@ -246,7 +246,10 @@ where
                  trace[Elab.binop] "uncomparable types: {max}, {type}"
                  modify fun s => { s with hasUncomparable := true }
 
-private def mkBinOp (f : Expr) (lhs rhs : Expr) : TermElabM Expr := do
+private def mkBinOp (lazy : Bool) (f : Expr) (lhs rhs : Expr) : TermElabM Expr := do
+  let mut rhs := rhs
+  if lazy then
+    rhs ← mkFunUnit rhs
   elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] (expectedType? := none) (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
 
 private def mkUnOp (f : Expr) (arg : Expr) : TermElabM Expr := do
@@ -258,11 +261,7 @@ private def toExprCore (t : Tree) : TermElabM Expr := do
     modifyInfoState (fun s => { s with trees := s.trees ++ trees }); return e
   | .binop ref lazy f lhs rhs =>
     withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
-      let lhs ← toExprCore lhs
-      let mut rhs ← toExprCore rhs
-      if lazy then
-        rhs ← mkFunUnit rhs
-      mkBinOp f lhs rhs
+      mkBinOp lazy f (← toExprCore lhs) (← toExprCore rhs)
   | .unop ref f arg =>
     withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
       mkUnOp f (← toExprCore arg)
@@ -359,7 +358,7 @@ mutual
           return .binop ref lazy f (← go lhs f true false) (← go rhs f false false)
         else
           let r ← withRef ref do
-            mkBinOp f (← toExpr lhs none) (← toExpr rhs none)
+            mkBinOp lazy f (← toExpr lhs none) (← toExpr rhs none)
           let infoTrees ← getResetInfoTrees
           return .term ref infoTrees r
       | .unop ref f arg =>
@@ -367,7 +366,7 @@ mutual
       | .term ref trees e =>
         let type ← instantiateMVars (← inferType e)
         trace[Elab.binop] "visiting {e} : {type} =?= {maxType}"
-        if isUnknow type then
+        if isUnknown type then
           if let some f := f? then
             if (← hasHeterogeneousDefaultInstances f maxType lhs) then
               -- See comment at `hasHeterogeneousDefaultInstances`

src/Lean/Elab/Frontend.lean

@@ -62,7 +62,7 @@ def processCommand : FrontendM Bool := do
     modify fun s => { s with commands := s.commands.push cmd }
     setParserState ps
     setMessages messages
-    profileitM IO.Error "elaboration" scope.opts <| elabCommandAtFrontend cmd
+    elabCommandAtFrontend cmd
     pure (Parser.isTerminalCommand cmd)
 
 partial def processCommands : FrontendM Unit := do

src/Lean/Elab/LetRec.lean

@@ -37,6 +37,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
     else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
       let declId := decl[0]
+      unless declId.isIdent do
+        throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
       let currDeclName? ← getDeclName?
       let declName := currDeclName?.getD Name.anonymous ++ shortDeclName

src/Lean/Elab/MutualDef.lean

@@ -210,6 +210,7 @@ private def expandWhereStructInst : Macro
         have : Coe (TSyntax ``letIdBinder) (TSyntax ``funBinder) := ⟨(⟨·⟩)⟩
         val ← if binders.size > 0 then `(fun $binders* => $val) else pure val
         `(structInstField|$id:ident := $val)
+      | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
       | _ => Macro.throwUnsupported
     let body ← `({ $structInstFields,* })
     match whereDecls? with

src/Lean/Elab/PreDefinition/Basic.lean

@@ -120,8 +120,7 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List N
     if preDef.modifiers.isNoncomputable then
       modifyEnv fun env => addNoncomputable env preDef.declName
     if compile && shouldGenCodeFor preDef then
-      unless (← compileDecl decl) do
-        return ()
+      discard <| compileDecl decl
     if applyAttrAfterCompilation then
       applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
@@ -157,8 +156,7 @@ def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSaf
       for preDef in preDefs do
         addTermInfo' preDef.ref (← mkConstWithLevelParams preDef.declName) (isBinder := true)
     applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking
-    unless (← compileDecl decl) do
-      return ()
+    discard <| compileDecl decl
     applyAttributesOf preDefs AttributeApplicationTime.afterCompilation
     return ()
 

src/Lean/Elab/PreDefinition/Main.lean

@@ -73,7 +73,7 @@ private def ensureNoUnassignedMVarsAtPreDef (preDef : PreDefinition) : TermElabM
   This method beta-reduces them to make sure they can be eliminated by the well-founded recursion module. -/
 private def betaReduceLetRecApps (preDefs : Array PreDefinition) : MetaM (Array PreDefinition) :=
   preDefs.mapM fun preDef => do
-    let value ← transform preDef.value fun e => do
+    let value ← Core.transform preDef.value fun e => do
       if e.isApp && e.getAppFn.isLambda && e.getAppArgs.all fun arg => arg.getAppFn.isConst && preDefs.any fun preDef => preDef.declName == arg.getAppFn.constName! then
         return .visit e.headBeta
       else
@@ -106,7 +106,12 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
   for preDefs in cliques do
     trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
     if preDefs.size == 1 && isNonRecursive preDefs[0]! then
-      let preDef := preDefs[0]!
+      /-
+      We must erase `recApp` annotations even when `preDef` is not recursive
+      because it may use another recursive declaration in the same mutual block.
+      See issue #2321
+      -/
+      let preDef ← eraseRecAppSyntax preDefs[0]!
       if preDef.modifiers.isNoncomputable then
         addNonRec preDef
       else

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -85,7 +85,14 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
     let preDefNonRec ← eraseRecAppSyntax preDefNonRec
     let preDef ← eraseRecAppSyntax preDefs[0]!
     state.addMatchers.forM liftM
-    registerEqnsInfo preDef recArgPos
+    unless preDef.kind.isTheorem do
+      unless (← isProp preDef.type) do
+        /-
+        Don't save predefinition info for equation generator
+        for theorems and definitions that are propositions.
+        See issue #2327
+        -/
+        registerEqnsInfo preDef recArgPos
     mapError (addNonRec preDefNonRec (applyAttrAfterCompilation := false)) fun msg =>
       m!"structural recursion failed, produced type incorrect term{indentD msg}"
     addAndCompilePartialRec #[preDef]

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

@@ -208,11 +208,18 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
-def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : CoreM Unit := do
-  let declNames := preDefs.map (·.declName)
-  modifyEnv fun env =>
-    preDefs.foldl (init := env) fun env preDef =>
-      eqnInfoExt.insert env preDef.declName { preDef with declNames, declNameNonRec, fixedPrefixSize }
+def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat) : MetaM Unit := do
+  /-
+  See issue #2327.
+  Remark: we could do better for mutual declarations that mix theorems and definitions. However, this is a rare
+  combination, and we would have add support for it in the equation generator. I did not check which assumptions are made there.
+  -/
+  unless preDefs.all fun p => p.kind.isTheorem do
+    unless (← preDefs.allM fun p => isProp p.type) do
+      let declNames := preDefs.map (·.declName)
+      modifyEnv fun env =>
+        preDefs.foldl (init := env) fun env preDef =>
+          eqnInfoExt.insert env preDef.declName { preDef with declNames, declNameNonRec, fixedPrefixSize }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/Quotation.lean

@@ -384,13 +384,15 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
     else if isAntiquotSplice quoted then throwErrorAt quoted "unexpected antiquotation splice"
     else if quoted.getArgs.size == 1 && isAntiquotSuffixSplice quoted[0] then
       let inner := getAntiquotSuffixSpliceInner quoted[0]
-      let anti := getAntiquotTerm (getCanonicalAntiquot inner)
       let ks := antiquotKinds inner |>.map (·.1)
-      unconditionally fun rhs => match antiquotSuffixSplice? quoted[0] with
-        | `optional => `(have $anti := Option.map (@TSyntax.mk $(quote ks)) (Syntax.getOptional? __discr); $rhs)
-        | `many     => `(have $anti := @TSyntaxArray.mk $(quote ks) (Syntax.getArgs __discr); $rhs)
-        | `sepBy    => `(have $anti := @TSepArray.mk $(quote ks) $(quote <| getSepFromSplice quoted[0]) (Syntax.getArgs __discr); $rhs)
-        | k         => throwErrorAt quoted "invalid antiquotation suffix splice kind '{k}'"
+      unconditionally <| match getAntiquotTerm (getCanonicalAntiquot inner) with
+        | `(_)         => pure
+        | `($id:ident) => fun rhs => match antiquotSuffixSplice? quoted[0] with
+          | `optional => `(have $id := Option.map (@TSyntax.mk $(quote ks)) (Syntax.getOptional? __discr); $rhs)
+          | `many     => `(have $id := @TSyntaxArray.mk $(quote ks) (Syntax.getArgs __discr); $rhs)
+          | `sepBy    => `(have $id := @TSepArray.mk $(quote ks) $(quote <| getSepFromSplice quoted[0]) (Syntax.getArgs __discr); $rhs)
+          | k         => throwErrorAt quoted "invalid antiquotation suffix splice kind '{k}'"
+        | anti         => fun _   => throwErrorAt anti "unsupported antiquotation kind in pattern"
     else if quoted.getArgs.size == 1 && isAntiquotSplice quoted[0] then pure {
       check   := other pat,
       onMatch := fun

src/Lean/Elab/Structure.lean

@@ -761,7 +761,6 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
   let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
   withLocalDeclD `self structType fun source => do
     let mut declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType))
-    declType := mkOutParamArgsImplicit declType
     if view.isClass && isClass env parentStructName then
       declType := setSourceInstImplicit declType
     declType := declType.inferImplicit params.size true

src/Lean/Elab/Syntax.lean

@@ -191,26 +191,31 @@ where
     return (stx, stackSz)
 
   processNullaryOrCat (stx : Syntax) := do
-    match (← elabParserName? stx[0]) with
+    let ident := stx[0]
+    let id := ident.getId.eraseMacroScopes
+    -- run when parser is neither a decl nor a cat
+    let default := do
+      if (← Parser.isParserAlias id) then
+        ensureNoPrec stx
+        return (← processAlias ident #[])
+      throwError "unknown parser declaration/category/alias '{id}'"
+    match (← elabParserName? ident) with
     | some (.parser c (isDescr := true)) =>
       ensureNoPrec stx
       -- `syntax _ :=` at least enforces this
       let stackSz := 1
       return (mkIdentFrom stx c, stackSz)
     | some (.parser c (isDescr := false)) =>
+      if (← Parser.getParserAliasInfo id).declName == c then
+        -- prefer parser alias over base declaration because it has more metadata, #2249
+        return (← default)
       ensureNoPrec stx
       -- as usual, we assume that people using `Parser` know what they are doing
       let stackSz := 1
       return (← `(ParserDescr.parser $(quote c)), stackSz)
     | some (.category _) =>
       processParserCategory stx
-    | none =>
-      let id := stx[0].getId.eraseMacroScopes
-      if (← Parser.isParserAlias id) then
-        ensureNoPrec stx
-        processAlias stx[0] #[]
-      else
-        throwError "unknown parser declaration/category/alias '{id}'"
+    | none => default
 
   processSepBy (stx : Syntax) := do
     let p ← ensureUnaryOutput <$> withNestedParser do process stx[1]
@@ -260,7 +265,7 @@ open Lean.Parser.Command
 
 private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
   if let .str _ suffix := catName then
-    let quotSymbol := "`(" ++ suffix ++ "|"
+    let quotSymbol := "`(" ++ suffix ++ "| "
     let name := catName ++ `quot
     let cmd ← `(
       @[term_parser] def $(mkIdent name) : Lean.ParserDescr :=

src/Lean/Elab/Tactic/Basic.lean

@@ -17,7 +17,7 @@ def admitGoal (mvarId : MVarId) : MetaM Unit :=
 def goalsToMessageData (goals : List MVarId) : MessageData :=
   MessageData.joinSep (goals.map MessageData.ofGoal) m!"\n\n"
 
-def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
+def Term.reportUnsolvedGoals (goals : List MVarId) : MetaM Unit := do
   logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{goalsToMessageData goals}"
   goals.forM fun mvarId => admitGoal mvarId
 
@@ -139,14 +139,14 @@ structure EvalTacticFailure where
   exception : Exception
   state : SavedState
 
-partial def evalTactic (stx : Syntax) : TacticM Unit :=
+partial def evalTactic (stx : Syntax) : TacticM Unit := do
+  profileitM Exception "tactic execution" (decl := stx.getKind) (← getOptions) <|
   withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
     | .node _ k _    =>
       if k == nullKind then
         -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
         stx.getArgs.forM evalTactic
-      else do
-        trace[Elab.step] "{stx}"
+      else withTraceNode `Elab.step (fun _ => return stx) do
         let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind
         let macros  := macroAttribute.getEntries (← getEnv) stx.getKind
         if evalFns.isEmpty && macros.isEmpty then

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -69,11 +69,14 @@ Output:
 -/
 -- Note that we need to preserve the separators to show the right goals after semicolons.
 def addCheckpoints (stx : Syntax) : TacticM Syntax := do
-  -- if (← readThe Term.Context).tacticCache? |>.isSome then
   if !(← stx.getSepArgs.anyM isCheckpointableTactic) then return stx
+  -- do not checkpoint checkpointable tactic by itself to prevent infinite recursion
+  -- TODO: rethink approach if we add non-trivial checkpointable tactics
+  if stx.getNumArgs <= 2 then return stx
   let mut currentCheckpointBlock := #[]
   let mut output := #[]
-  for i in [:stx.getArgs.size / 2] do
+  -- `+ 1` to account for optional trailing separator
+  for i in [:(stx.getArgs.size + 1) / 2] do
     let tac := stx[2*i]
     let sep? := stx.getArgs[2*i+1]?
     if (← isCheckpointableTactic tac) then
@@ -83,7 +86,7 @@ def addCheckpoints (stx : Syntax) : TacticM Syntax := do
           mkNode ``tacticSeq #[
             mkNode ``tacticSeq1Indented #[
               -- HACK: null node is not a valid tactic, but prevents infinite loop
-              mkNullNode (currentCheckpointBlock.push tac)
+              mkNullNode (currentCheckpointBlock.push (mkNullNode #[tac]))
             ]
           ]
         ]
@@ -115,6 +118,17 @@ def evalSepByIndentTactic (stx : Syntax) : TacticM Unit := do
     withInfoContext (pure ()) initInfo
     evalSepByIndentTactic stx[1]
 
+@[builtin_tactic cdot] def evalTacticCDot : Tactic := fun stx => do
+  -- adjusted copy of `evalTacticSeqBracketed`; we used to use the macro
+  -- ``| `(tactic| $cdot:cdotTk $tacs) => `(tactic| {%$cdot ($tacs) }%$cdot)``
+  -- but the token antiquotation does not copy trailing whitespace, leading to
+  -- differences in the goal display (#2153)
+  let initInfo ← mkInitialTacticInfo stx[0]
+  withRef stx[0] <| closeUsingOrAdmit do
+    -- save state before/after entering focus on `·`
+    withInfoContext (pure ()) initInfo
+    evalSepByIndentTactic stx[1]
+
 @[builtin_tactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx => do
   let mkInfo ← mkInitialTacticInfo stx[0]
   focus do

src/Lean/Elab/Tactic/Generalize.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Intro
+import Lean.Elab.Binders
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Location
 
@@ -14,15 +15,27 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.generalize] def evalGeneralize : Tactic := fun stx =>
   withMainContext do
-    let args ← stx[1].getSepArgs.mapM fun arg => do
-      let hName? := if arg[0].isNone then none else some arg[0][0].getId
+    let mut xIdents := #[]
+    let mut hIdents := #[]
+    let mut args := #[]
+    for arg in stx[1].getSepArgs do
+      let hName? ← if arg[0].isNone then
+        pure none
+      else
+        hIdents := hIdents.push arg[0][0]
+        pure (some arg[0][0].getId)
       let expr ← elabTerm arg[1] none
-      return { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
+      xIdents := xIdents.push arg[3]
+      args := args.push { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
     let hyps ← match expandOptLocation stx[2] with
     | .targets hyps _ => getFVarIds hyps
     | .wildcard => pure (← getLCtx).getFVarIds
-    liftMetaTactic fun mvarId => do
-      let (_, _, mvarId) ← mvarId.generalizeHyp args hyps
-      return [mvarId]
+    let mvarId ← getMainGoal
+    mvarId.withContext do
+      let (_, newVars, mvarId) ← mvarId.generalizeHyp args hyps
+      mvarId.withContext do
+        for v in newVars, id in xIdents ++ hIdents do
+          Term.addLocalVarInfo id (.fvar v)
+        replaceMainGoal [mvarId]
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Location.lean

@@ -56,6 +56,8 @@ def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget
       let mut worked := worked
       -- We must traverse backwards because the given `atLocal` may use the revert/intro idiom
       for fvarId in (← getLCtx).getFVarIds.reverse do
+        if (← fvarId.getDecl).isImplementationDetail then
+          continue
         worked := worked || (← tryTactic <| withMainContext <| atLocal fvarId)
       unless worked do
         failed (← getMainGoal)

src/Lean/Elab/Tactic/Rewrite.lean

@@ -11,20 +11,16 @@ import Lean.Elab.Tactic.Config
 namespace Lean.Elab.Tactic
 open Meta
 
-def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do
-  Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
-    let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
-    replaceMainGoal (mvarId' :: r.mvarIds)
+def rewriteTarget (e : Expr) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do
+  let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
+  let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
+  replaceMainGoal (mvarId' :: r.mvarIds)
 
-def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do
-  Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    let localDecl ← fvarId.getDecl
-    let rwResult ← (← getMainGoal).rewrite localDecl.type e symm (config := config)
-    let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
-    replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
+def rewriteLocalDecl (e : Expr) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do
+  let localDecl ← fvarId.getDecl
+  let rwResult ← (← getMainGoal).rewrite localDecl.type e symm (config := config)
+  let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
+  replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
 
 def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
   let lbrak := rwRulesSeqStx[0]
@@ -62,9 +58,11 @@ declare_config_elab elabRewriteConfig Rewrite.Config
   let cfg ← elabRewriteConfig stx[1]
   let loc   := expandOptLocation stx[3]
   withRWRulesSeq stx[0] stx[2] fun symm term => do
-    withLocation loc
-      (rewriteLocalDecl term symm · cfg)
-      (rewriteTarget term symm cfg)
-      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
+    Term.withSynthesize <| withMainContext do
+      let e ← elabTerm term none true
+      withLocation loc
+        (rewriteLocalDecl e symm · cfg)
+        (rewriteTarget e symm cfg)
+        (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
 
 end Lean.Elab.Tactic

src/Lean/Elab/Term.lean

@@ -196,9 +196,9 @@ structure Context where
   sectionFVars       : NameMap Expr    := {}
   /-- Enable/disable implicit lambdas feature. -/
   implicitLambda     : Bool            := true
-  /-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for  -/
+  /-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
   isNoncomputableSection : Bool        := false
-  /-- When `true` we skip TC failures. We use this option when processing patterns -/
+  /-- When `true` we skip TC failures. We use this option when processing patterns. -/
   ignoreTCFailures : Bool := false
   /-- `true` when elaborating patterns. It affects how we elaborate named holes. -/
   inPattern        : Bool := false
@@ -367,14 +367,14 @@ opaque mkTermElabAttribute (ref : Name) : IO (KeyedDeclsAttribute TermElab)
 builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute decl_name%
 
 /--
-  Auxiliary datatatype for presenting a Lean lvalue modifier.
-  We represent a unelaborated lvalue as a `Syntax` (or `Expr`) and `List LVal`.
+  Auxiliary datatype for presenting a Lean lvalue modifier.
+  We represent an unelaborated lvalue as a `Syntax` (or `Expr`) and `List LVal`.
   Example: `a.foo.1` is represented as the `Syntax` `a` and the list
   `[LVal.fieldName "foo", LVal.fieldIdx 1]`.
 -/
 inductive LVal where
   | fieldIdx  (ref : Syntax) (i : Nat)
-  /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name.
+  /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name.
   `ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/
   | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax)
 
@@ -398,7 +398,7 @@ def getLetRecsToLift : TermElabM (List LetRecToLift) := return (← get).letRecs
 /-- Return the declaration of the given metavariable -/
 def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := return (← getMCtx).getDecl mvarId
 
-/-- Execute `x` with `declName? := name`. See `getDeclName? -/
+/-- Execute `x` with `declName? := name`. See `getDeclName?`. -/
 def withDeclName (name : Name) (x : TermElabM α) : TermElabM α :=
   withReader (fun ctx => { ctx with declName? := name }) x
 
@@ -426,7 +426,7 @@ def withoutErrToSorryImp (x : TermElabM α) : TermElabM α :=
 
 /--
   Execute `x` without converting errors (i.e., exceptions) to `sorry` applications.
-  Recall that when `errToSorry = true`, the method `elabTerm` catches exceptions and convert them into `sorry` applications.
+  Recall that when `errToSorry = true`, the method `elabTerm` catches exceptions and converts them into `sorry` applications.
 -/
 def withoutErrToSorry [MonadFunctorT TermElabM m] : m α → m α :=
   monadMap (m := TermElabM) withoutErrToSorryImp
@@ -498,7 +498,7 @@ def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData)
   Auxiliary method for reporting errors of the form "... contains metavariables ...".
   This kind of error is thrown, for example, at `Match.lean` where elaboration
   cannot continue if there are metavariables in patterns.
-  We only want to log it if we haven't logged any error so far. -/
+  We only want to log it if we haven't logged any errors so far. -/
 def throwMVarError (m : MessageData) : TermElabM α := do
   if (← MonadLog.hasErrors) then
     throwAbortTerm
@@ -605,7 +605,7 @@ def mkFreshIdent [Monad m] [MonadQuotation m] (ref : Syntax) (canonical := false
 
 private def applyAttributesCore
     (declName : Name) (attrs : Array Attribute)
-    (applicationTime? : Option AttributeApplicationTime) : TermElabM Unit :=
+    (applicationTime? : Option AttributeApplicationTime) : TermElabM Unit := do profileitM Exception "attribute application" (← getOptions) do
   for attr in attrs do
     withRef attr.stx do withLogging do
     let env ← getEnv
@@ -724,7 +724,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
       unless (← isDefEq oldVal val) do
         if (← containsPendingMVar oldVal <||> containsPendingMVar val) then
           /- If `val` or `oldVal` contains metavariables directly or indirectly (e.g., in a let-declaration),
-             we return `false` to indicate we should try again later. This is very course grain since
+             we return `false` to indicate we should try again later. This is very coarse grain since
              the metavariable may not be responsible for the failure. We should refine the test in the future if needed.
              This check has been added to address dependencies between postponed metavariables. The following
              example demonstrates the issue fixed by this test.
@@ -759,7 +759,7 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
       throwError "failed to synthesize instance{indentExpr type}"
 
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
-  trace[Elab.coe] "adding coercion for {e} : {← inferType e} =?= {expectedType}"
+  withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
   try
     withoutMacroStackAtErr do
       match ← coerce? e expectedType with
@@ -797,7 +797,7 @@ private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr :
   mkSyntheticSorry expectedType
 
 /--
-  Log the given exception, and create an synthetic sorry for representing the failed
+  Log the given exception, and create a synthetic sorry for representing the failed
   elaboration step with exception `ex`.
 -/
 def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do
@@ -883,15 +883,15 @@ def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDec
   return (← get).syntheticMVars.find? mvarId
 
 /--
-  Create an auxiliary annotation to make sure we create a `Info` even if `e` is a metavariable.
+  Create an auxiliary annotation to make sure we create an `Info` even if `e` is a metavariable.
   See `mkTermInfo`.
 
-  We use this functions because some elaboration functions elaborate subterms that may not be immediately
+  We use this function because some elaboration functions elaborate subterms that may not be immediately
   part of the resulting term. Example:
   ```
   let_mvar% ?m := b; wait_if_type_mvar% ?m; body
   ```
-  If the type of `b` is not known, then `wait_if_type_mvar% ?m; body` is postponed and just return a fresh
+  If the type of `b` is not known, then `wait_if_type_mvar% ?m; body` is postponed and just returns a fresh
   metavariable `?n`. The elaborator for
   ```
   let_mvar% ?m := b; wait_if_type_mvar% ?m; body
@@ -978,7 +978,7 @@ def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
     postponeElabTermCore stx expectedType?
 
 /--
-  Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
+  Helper function for `elabTerm` that tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
   an error is found. -/
 private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool)
     : List (KeyedDeclsAttribute.AttributeEntry TermElab) → TermElabM Expr
@@ -1049,7 +1049,7 @@ private def isExplicitApp (stx : Syntax) : Bool :=
   stx.getKind == ``Lean.Parser.Term.app && isExplicit stx[0]
 
 /--
-  Return true if `stx` if a lambda abstraction containing a `{}` or `[]` binder annotation.
+  Return true if `stx` is a lambda abstraction containing a `{}` or `[]` binder annotation.
   Example: `fun {α} (a : α) => a` -/
 private def isLambdaWithImplicit (stx : Syntax) : Bool :=
   match stx with
@@ -1134,7 +1134,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
     end
   ```
   In the example above, we have two local declarations named `toString` in the local context, and
-  we want the `toString f` to be resolved to `Foo.toString f`
+  we want the `toString f` to be resolved to `Foo.toString f`.
   -/
   let matchAuxRecDecl? (localDecl : LocalDecl) (fullDeclName : Name) (givenNameView : MacroScopesView) : Option LocalDecl := do
     let fullDeclView := extractMacroScopes fullDeclName
@@ -1165,7 +1165,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
       return localDecl
     else
       /-
-         It is the standard algorithm we using at `resolveGlobalName` for processing namespaces.
+         It is the standard algorithm we are using at `resolveGlobalName` for processing namespaces.
 
          The current solution also has a limitation when using `def _root_` in a mutual block.
          The non `def _root_` declarations may update the namespace. See the following example:
@@ -1215,7 +1215,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   /-
   We use the parameter `globalDeclFound` to decide whether we should skip auxiliary declarations or not.
   We set it to true if we found a global declaration `n` as we iterate over the `loop`.
-  Without this workaround, we would not be able to elaborate example such as
+  Without this workaround, we would not be able to elaborate an example such as
   ```
   def foo.aux := 1
   def foo : Nat → Nat
@@ -1319,7 +1319,7 @@ private def decorateErrorMessageWithLambdaImplicitVars (ex : Exception) (impFVar
         let auxMsg := m!"{impFVar} : {← inferType impFVar}"
         let auxMsg ← addMessageContext auxMsg
         msg := m!"{msg}{indentD auxMsg}"
-      msg := m!"{msg}\nyou can disable implict lambdas using `@` or writing a lambda expression with `\{}` or `[]` binder annotations."
+      msg := m!"{msg}\nyou can disable implicit lambdas using `@` or writing a lambda expression with `\{}` or `[]` binder annotations."
       return Exception.error ref msg
   | _ => return ex
 
@@ -1411,7 +1411,7 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPo
   let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
   withRef stx <| ensureHasType expectedType? e errorMsgHeader?
 
-/-- Execute `x` and return `some` if no new errors were recorded or exceptions was thrown. Otherwise, return `none` -/
+/-- Execute `x` and return `some` if no new errors were recorded or exceptions were thrown. Otherwise, return `none`. -/
 def commitIfNoErrors? (x : TermElabM α) : TermElabM (Option α) := do
   let saved ← saveState
   Core.resetMessageLog
@@ -1434,7 +1434,7 @@ def adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab := fun stx expe
 
 /--
   Create a new metavariable with the given type, and try to synthesize it.
-  It type class resolution cannot be executed (e.g., it is stuck because of metavariables in `type`),
+  If type class resolution cannot be executed (e.g., it is stuck because of metavariables in `type`),
   register metavariable as a pending one.
 -/
 def mkInstMVar (type : Expr) : TermElabM Expr := do
@@ -1445,7 +1445,7 @@ def mkInstMVar (type : Expr) : TermElabM Expr := do
   return mvar
 
 /--
-  Make sure `e` is a type by inferring its type and making sure it is a `Expr.sort`
+  Make sure `e` is a type by inferring its type and making sure it is an `Expr.sort`
   or is unifiable with `Expr.sort`, or can be coerced into one. -/
 def ensureType (e : Expr) : TermElabM Expr := do
   if (← isType e) then
@@ -1506,28 +1506,29 @@ partial def collectUnassignedMVars (type : Expr) (init : Array Expr := #[]) (exc
   if mvarIds.isEmpty then
     return init
   else
-    go mvarIds.toList init
+    go mvarIds.toList init init
 where
-  go (mvarIds : List MVarId) (result : Array Expr) : TermElabM (Array Expr) := do
+  go (mvarIds : List MVarId) (result visited : Array Expr) : TermElabM (Array Expr) := do
     match mvarIds with
     | [] => return result
     | mvarId :: mvarIds => do
+      let visited := visited.push (mkMVar mvarId)
       if (← mvarId.isAssigned) then
-        go mvarIds result
+        go mvarIds result visited
       else if result.contains (mkMVar mvarId) || except mvarId then
-        go mvarIds result
+        go mvarIds result visited
       else
         let mvarType := (← getMVarDecl mvarId).type
         let mvarIdsNew ← getMVars mvarType
-        let mvarIdsNew := mvarIdsNew.filter fun mvarId => !result.contains (mkMVar mvarId)
+        let mvarIdsNew := mvarIdsNew.filter fun mvarId => !visited.contains (mkMVar mvarId)
         if mvarIdsNew.isEmpty then
-          go  mvarIds (result.push (mkMVar mvarId))
+          go mvarIds (result.push (mkMVar mvarId)) visited
         else
-          go (mvarIdsNew.toList ++ mvarId :: mvarIds) result
+          go (mvarIdsNew.toList ++ mvarId :: mvarIds) result visited
 
 /--
   Return `autoBoundImplicits ++ xs`
-  This methoid throws an error if a variable in `autoBoundImplicits` depends on some `x` in `xs`.
+  This method throws an error if a variable in `autoBoundImplicits` depends on some `x` in `xs`.
   The `autoBoundImplicits` may contain free variables created by the auto-implicit feature, and unassigned free variables.
   It avoids the hack used at `autoBoundImplicitsOld`.
 
@@ -1554,9 +1555,9 @@ where
 
 /--
   Similar to `autoBoundImplicits`, but immediately if the resulting array of expressions contains metavariables,
-  it immediately use `mkForallFVars` + `forallBoundedTelescope` to convert them into free variables.
+  it immediately uses `mkForallFVars` + `forallBoundedTelescope` to convert them into free variables.
   The type `type` is modified during the process if type depends on `xs`.
-  We use this method to simplify the conversion of code using `autoBoundImplicitsOld` to `autoBoundImplicits`
+  We use this method to simplify the conversion of code using `autoBoundImplicitsOld` to `autoBoundImplicits`.
 -/
 def addAutoBoundImplicits' (xs : Array Expr) (type : Expr) (k : Array Expr → Expr → TermElabM α) : TermElabM α := do
   let xs ← addAutoBoundImplicits xs

src/Lean/Exception.lean

@@ -159,7 +159,7 @@ The first argument must be a `Syntax` that provides position information for
 the error message.
 `throwErrorAt ref msg` is equivalent to `withRef ref <| throwError msg`
 -/
-syntax "throwErrorAt " term:max (interpolatedStr(term) <|> term) : term
+syntax "throwErrorAt " term:max ppSpace (interpolatedStr(term) <|> term) : term
 
 macro_rules
   | `(throwError $msg:interpolatedStr) => `(Lean.throwError (m! $msg))

src/Lean/Expr.lean

@@ -1400,6 +1400,10 @@ def getAutoParamTactic? (e : Expr) : Option Expr :=
 def isOutParam (e : Expr) : Bool :=
   e.isAppOfArity ``outParam 1
 
+/-- Return `true` if `e` is of the form `semiOutParam _` -/
+def isSemiOutParam (e : Expr) : Bool :=
+  e.isAppOfArity ``semiOutParam 1
+
 /-- Return `true` if `e` is of the form `optParam _ _` -/
 def isOptParam (e : Expr) : Bool :=
   e.isAppOfArity ``optParam 2
@@ -1419,7 +1423,7 @@ Examples:
 partial def consumeTypeAnnotations (e : Expr) : Expr :=
   if e.isOptParam || e.isAutoParam then
     consumeTypeAnnotations e.appFn!.appArg!
-  else if e.isOutParam then
+  else if e.isOutParam || e.isSemiOutParam then
     consumeTypeAnnotations e.appArg!
   else
     e

src/Lean/Linter/Builtin.lean

@@ -10,24 +10,25 @@ register_builtin_option linter.suspiciousUnexpanderPatterns : Bool := {
 
 def getLinterSuspiciousUnexpanderPatterns (o : Options) : Bool := getLinterValue linter.suspiciousUnexpanderPatterns o
 
-def suspiciousUnexpanderPatterns : Linter := fun cmdStx => do
-  unless getLinterSuspiciousUnexpanderPatterns (← getOptions) do
-    return
+def suspiciousUnexpanderPatterns : Linter where
+  run cmdStx := do
+    unless getLinterSuspiciousUnexpanderPatterns (← getOptions) do
+      return
 
-  -- check `[app_unexpander _]` defs defined by pattern matching
-  let `($[$_:docComment]? @[$[$attrs:attr],*] $(_vis)? def $_ : $_ $[| $pats => $_]*) := cmdStx | return
+    -- check `[app_unexpander _]` defs defined by pattern matching
+    let `($[$_:docComment]? @[$[$attrs:attr],*] $(_vis)? def $_ : $_ $[| $pats => $_]*) := cmdStx | return
 
-  unless attrs.any (· matches `(attr| app_unexpander $_)) do
-    return
+    unless attrs.any (· matches `(attr| app_unexpander $_)) do
+      return
 
-  for pat in pats do
-    let patHead ← match pat with
-      | `(`($patHead:ident $_args*)) => pure patHead
-      | `(`($patHead:ident))         => pure patHead
-      | _                            => continue
+    for pat in pats do
+      let patHead ← match pat with
+        | `(`($patHead:ident $_args*)) => pure patHead
+        | `(`($patHead:ident))         => pure patHead
+        | _                            => continue
 
-    logLint linter.suspiciousUnexpanderPatterns patHead
-      "Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name."
+      logLint linter.suspiciousUnexpanderPatterns patHead
+        "Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name."
 
 builtin_initialize addLinter suspiciousUnexpanderPatterns
 

src/Lean/Linter/MissingDocs.lean

@@ -64,9 +64,10 @@ def addHandler (env : Environment) (declName key : Name) (h : Handler) : Environ
 
 def getHandlers (env : Environment) : NameMap Handler := (missingDocsExt.getState env).2
 
-partial def missingDocs : Linter := fun stx => do
-  if let some h := (getHandlers (← getEnv)).find? stx.getKind then
-    h (getLinterMissingDocs (← getOptions)) stx
+partial def missingDocs : Linter where
+  run stx := do
+    if let some h := (getHandlers (← getEnv)).find? stx.getKind then
+      h (getLinterMissingDocs (← getOptions)) stx
 
 builtin_initialize addLinter missingDocs
 
@@ -237,10 +238,10 @@ def handleIn : Handler := fun _ stx => do
   if stx[0].getKind == ``«set_option» then
     let opts ← Elab.elabSetOption stx[0][1] stx[0][2]
     withScope (fun scope => { scope with opts }) do
-      missingDocs stx[2]
+      missingDocs.run stx[2]
   else
-    missingDocs stx[2]
+    missingDocs.run stx[2]
 
 @[builtin_missing_docs_handler «mutual»]
 def handleMutual : Handler := fun _ stx => do
-  stx[1].getArgs.forM missingDocs
+  stx[1].getArgs.forM missingDocs.run

src/Lean/Linter/UnusedVariables.lean

@@ -133,111 +133,112 @@ unsafe def getUnusedVariablesIgnoreFnsImpl : CommandElabM (Array IgnoreFunction)
 opaque getUnusedVariablesIgnoreFns : CommandElabM (Array IgnoreFunction)
 
 
-def unusedVariables : Linter := fun cmdStx => do
-  unless getLinterUnusedVariables (← getOptions) do
-    return
+def unusedVariables : Linter where
+  run cmdStx := do
+    unless getLinterUnusedVariables (← getOptions) do
+      return
 
-  -- NOTE: `messages` is local to the current command
-  if (← get).messages.hasErrors then
-    return
+    -- NOTE: `messages` is local to the current command
+    if (← get).messages.hasErrors then
+      return
 
-  let some cmdStxRange := cmdStx.getRange?
-    | pure ()
+    let some cmdStxRange := cmdStx.getRange?
+      | pure ()
 
-  let infoTrees := (← get).infoState.trees.toArray
-  let fileMap := (← read).fileMap
+    let infoTrees := (← get).infoState.trees.toArray
+    let fileMap := (← read).fileMap
 
-  if (← infoTrees.anyM (·.hasSorry)) then
-    return
+    if (← infoTrees.anyM (·.hasSorry)) then
+      return
 
-  -- collect references
-  let refs := findModuleRefs fileMap infoTrees (allowSimultaneousBinderUse := true)
+    -- collect references
+    let refs := findModuleRefs fileMap infoTrees (allowSimultaneousBinderUse := true)
 
-  let mut vars : HashMap FVarId RefInfo := .empty
-  let mut constDecls : HashSet String.Range := .empty
+    let mut vars : HashMap FVarId RefInfo := .empty
+    let mut constDecls : HashSet String.Range := .empty
 
-  for (ident, info) in refs.toList do
-    match ident with
-    | .fvar id =>
-      vars := vars.insert id info
-    | .const _ =>
-      if let some definition := info.definition then
-        if let some range := definition.stx.getRange? then
-          constDecls := constDecls.insert range
+    for (ident, info) in refs.toList do
+      match ident with
+      | .fvar id =>
+        vars := vars.insert id info
+      | .const _ =>
+        if let some definition := info.definition then
+          if let some range := definition.stx.getRange? then
+            constDecls := constDecls.insert range
 
-  -- collect uses from tactic infos
-  let tacticMVarAssignments : HashMap MVarId Expr :=
-    infoTrees.foldr (init := .empty) fun tree assignments =>
-      tree.foldInfo (init := assignments) (fun _ i assignments => match i with
-        | .ofTacticInfo ti =>
-          ti.mctxAfter.eAssignment.foldl (init := assignments) fun assignments mvar expr =>
-            if assignments.contains mvar then
-              assignments
-            else
-              assignments.insert mvar expr
-        | _ =>
-          assignments)
+    -- collect uses from tactic infos
+    let tacticMVarAssignments : HashMap MVarId Expr :=
+      infoTrees.foldr (init := .empty) fun tree assignments =>
+        tree.foldInfo (init := assignments) (fun _ i assignments => match i with
+          | .ofTacticInfo ti =>
+            ti.mctxAfter.eAssignment.foldl (init := assignments) fun assignments mvar expr =>
+              if assignments.contains mvar then
+                assignments
+              else
+                assignments.insert mvar expr
+          | _ =>
+            assignments)
 
-  let tacticFVarUses : HashSet FVarId ←
-    tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do
-      let (_, s) ← StateT.run (s := uses) <| expr.forEachWhere Expr.isFVar fun e => modify (·.insert e.fvarId!)
-      return s
+    let tacticFVarUses : HashSet FVarId ←
+      tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do
+        let (_, s) ← StateT.run (s := uses) <| expr.forEachWhere Expr.isFVar fun e => modify (·.insert e.fvarId!)
+        return s
 
-  -- collect ignore functions
-  let ignoreFns := (← getUnusedVariablesIgnoreFns)
-    |>.insertAt! 0 (isTopLevelDecl constDecls)
+    -- collect ignore functions
+    let ignoreFns := (← getUnusedVariablesIgnoreFns)
+      |>.insertAt! 0 (isTopLevelDecl constDecls)
 
-  -- determine unused variables
-  let mut unused := #[]
-  for (id, ⟨decl?, uses⟩) in vars.toList do
-    -- process declaration
-    let some decl := decl?
-      | continue
-    let declStx := skipDeclIdIfPresent decl.stx
-    let some range := declStx.getRange?
-      | continue
-    let some localDecl := decl.info.lctx.find? id
-      | continue
-    if !cmdStxRange.contains range.start || localDecl.userName.hasMacroScopes then
-      continue
-
-    -- check if variable is used
-    if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar id => tacticFVarUses.contains id | _ => false) then
+    -- determine unused variables
+    let mut unused := #[]
+    for (id, ⟨decl?, uses⟩) in vars.toList do
+      -- process declaration
+      let some decl := decl?
+        | continue
+      let declStx := skipDeclIdIfPresent decl.stx
+      let some range := declStx.getRange?
+        | continue
+      let some localDecl := decl.info.lctx.find? id
+        | continue
+      if !cmdStxRange.contains range.start || localDecl.userName.hasMacroScopes then
         continue
 
-    -- check linter options
-    let opts := decl.ci.options
-    if !getLinterUnusedVariables opts then
-      continue
+      -- check if variable is used
+      if !uses.isEmpty || tacticFVarUses.contains id || decl.aliases.any (match · with | .fvar id => tacticFVarUses.contains id | _ => false) then
+          continue
 
-    -- evaluate ignore functions on original syntax
-    if let some ((id', _) :: stack) := cmdStx.findStack? (·.getRange?.any (·.includes range)) then
-      if id'.isIdent && ignoreFns.any (· declStx stack opts) then
+      -- check linter options
+      let opts := decl.ci.options
+      if !getLinterUnusedVariables opts then
         continue
-    else
-      continue
 
-    -- evaluate ignore functions on macro expansion outputs
-    if ← infoTrees.anyM fun tree => do
-      if let some macroExpansions ← collectMacroExpansions? range tree then
-        return macroExpansions.any fun expansion =>
-          -- in a macro expansion, there may be multiple leafs whose (synthetic) range includes `range`, so accept strict matches only
-          if let some (_ :: stack) := expansion.output.findStack? (·.getRange?.any (·.includes range)) (fun stx => stx.isIdent && stx.getRange?.any (· == range)) then
-            ignoreFns.any (· declStx stack opts)
-          else
-            false
+      -- evaluate ignore functions on original syntax
+      if let some ((id', _) :: stack) := cmdStx.findStack? (·.getRange?.any (·.includes range)) then
+        if id'.isIdent && ignoreFns.any (· declStx stack opts) then
+          continue
       else
-        return false
-    then
-      continue
+        continue
 
-    -- publish warning if variable is unused and not ignored
-    unused := unused.push (declStx, localDecl)
+      -- evaluate ignore functions on macro expansion outputs
+      if ← infoTrees.anyM fun tree => do
+        if let some macroExpansions ← collectMacroExpansions? range tree then
+          return macroExpansions.any fun expansion =>
+            -- in a macro expansion, there may be multiple leafs whose (synthetic) range includes `range`, so accept strict matches only
+            if let some (_ :: stack) := expansion.output.findStack? (·.getRange?.any (·.includes range)) (fun stx => stx.isIdent && stx.getRange?.any (· == range)) then
+              ignoreFns.any (· declStx stack opts)
+            else
+              false
+        else
+          return false
+      then
+        continue
 
-  for (declStx, localDecl) in unused.qsort (·.1.getPos?.get! < ·.1.getPos?.get!) do
-    logLint linter.unusedVariables declStx m!"unused variable `{localDecl.userName}`"
+      -- publish warning if variable is unused and not ignored
+      unused := unused.push (declStx, localDecl)
 
-  return ()
+    for (declStx, localDecl) in unused.qsort (·.1.getPos?.get! < ·.1.getPos?.get!) do
+      logLint linter.unusedVariables declStx m!"unused variable `{localDecl.userName}`"
+
+    return ()
 where
   skipDeclIdIfPresent (stx : Syntax) : Syntax :=
     if stx.isOfKind ``Lean.Parser.Command.declId then

src/Lean/Message.lean

@@ -103,6 +103,8 @@ def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
 }
 
 def ofSyntax (stx : Syntax) : MessageData :=
+  -- discard leading/trailing whitespace
+  let stx := stx.copyHeadTailInfoFrom .missing
   .ofPPFormat {
     pp := fun
       | some ctx => ppTerm ctx ⟨stx⟩  -- HACK: might not be a term

src/Lean/Meta/AbstractNestedProofs.lean

@@ -8,11 +8,18 @@ import Lean.Meta.Closure
 namespace Lean.Meta
 namespace AbstractNestedProofs
 
+def getLambdaBody (e : Expr) : Expr :=
+  match e with
+  | .lam _ _ b _ => getLambdaBody b
+  | _ => e
+
 def isNonTrivialProof (e : Expr) : MetaM Bool := do
   if !(← isProof e) then
     pure false
   else
-    e.withApp fun f args =>
+    -- We consider proofs such as `fun x => f x a` as trivial.
+    -- For example, we don't want to abstract the body of `def rfl`
+    (getLambdaBody e).withApp fun f args =>
       pure $ !f.isAtomic || args.any fun arg => !arg.isAtomic
 
 structure Context where
@@ -31,7 +38,7 @@ private def mkAuxLemma (e : Expr) : M Expr := do
   /- We turn on zeta-expansion to make sure we don't need to perform an expensive `check` step to
      identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zeta expasion step.
      It a benchmark created by @selsam, The extra `check` step was a bottleneck. -/
-  mkAuxDefinitionFor lemmaName e (zeta := true)
+  mkAuxTheoremFor lemmaName e (zeta := true)
 
 partial def visit (e : Expr) : M Expr := do
   if e.isAtomic then

src/Lean/Meta/AppBuilder.lean

@@ -422,8 +422,8 @@ partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
           pure none
       match r? with
       | some r => pure r
-      | none   => throwAppBuilderException `mkProjectionn ("invalid field name '" ++ toString fieldName ++ "' for" ++ hasTypeMsg s type)
-  | _ => throwAppBuilderException `mkProjectionn ("structure expected" ++ hasTypeMsg s type)
+      | none   => throwAppBuilderException `mkProjection ("invalid field name '" ++ toString fieldName ++ "' for" ++ hasTypeMsg s type)
+  | _ => throwAppBuilderException `mkProjection ("structure expected" ++ hasTypeMsg s type)
 
 private def mkListLitAux (nil : Expr) (cons : Expr) : List Expr → Expr
   | []    => nil

src/Lean/Meta/Basic.lean

@@ -195,7 +195,7 @@ instance : Hashable InfoCacheKey :=
   ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) <| mixHash (hash expr) (hash nargs)⟩
 end InfoCacheKey
 
-abbrev SynthInstanceCache := PersistentHashMap Expr (Option Expr)
+abbrev SynthInstanceCache := PersistentHashMap (LocalInstances × Expr) (Option Expr)
 
 abbrev InferTypeCache := PersistentExprStructMap Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo
@@ -864,47 +864,28 @@ private partial def isClassQuick? : Expr → MetaM (LOption Name)
   | .mdata _ e       => isClassQuick? e
   | .const n _       => isClassQuickConst? n
   | .mvar mvarId     => do
-    match (← getExprMVarAssignment? mvarId) with
-    | some val => isClassQuick? val
-    | none     => return .none
-  | .app f _         =>
+    let some val ← getExprMVarAssignment? mvarId | return .none
+    isClassQuick? val
+  | .app f _         => do
     match f.getAppFn with
-    | .const n .. => isClassQuickConst? n
-    | .lam ..     => return .undef
-    | _           => return .none
-
-def saveAndResetSynthInstanceCache : MetaM SynthInstanceCache := do
-  let savedSythInstance := (← get).cache.synthInstance
-  modifyCache fun c => { c with synthInstance := {} }
-  return savedSythInstance
-
-def restoreSynthInstanceCache (cache : SynthInstanceCache) : MetaM Unit :=
-  modifyCache fun c => { c with synthInstance := cache }
-
-@[inline] private def resettingSynthInstanceCacheImpl (x : MetaM α) : MetaM α := do
-  let savedSythInstance ← saveAndResetSynthInstanceCache
-  try x finally restoreSynthInstanceCache savedSythInstance
-
-/-- Reset `synthInstance` cache, execute `x`, and restore cache -/
-@[inline] def resettingSynthInstanceCache : n α → n α :=
-  mapMetaM resettingSynthInstanceCacheImpl
-
-@[inline] def resettingSynthInstanceCacheWhen (b : Bool) (x : n α) : n α :=
-  if b then resettingSynthInstanceCache x else x
+    | .const n ..  => isClassQuickConst? n
+    | .lam ..      => return .undef
+    | .mvar mvarId =>
+      let some val ← getExprMVarAssignment? mvarId | return .none
+      match val.getAppFn with
+      | .const n .. => isClassQuickConst? n
+      | _ => return .undef
+    | _            => return .none
 
 private def withNewLocalInstanceImp (className : Name) (fvar : Expr) (k : MetaM α) : MetaM α := do
   let localDecl ← getFVarLocalDecl fvar
   if localDecl.isImplementationDetail then
     k
   else
-    resettingSynthInstanceCache <|
-      withReader
-        (fun ctx => { ctx with localInstances := ctx.localInstances.push { className := className, fvar := fvar } })
-        k
+    withReader (fun ctx => { ctx with localInstances := ctx.localInstances.push { className := className, fvar := fvar } }) k
 
 /-- Add entry `{ className := className, fvar := fvar }` to localInstances,
-    and then execute continuation `k`.
-    It resets the type class cache using `resettingSynthInstanceCache`. -/
+    and then execute continuation `k`. -/
 def withNewLocalInstance (className : Name) (fvar : Expr) : n α → n α :=
   mapMetaM <| withNewLocalInstanceImp className fvar
 
@@ -919,9 +900,7 @@ mutual
     using free variables `fvars[j] ... fvars.back`, and execute `k`.
 
     - `isClassExpensive` is defined later.
-    - The type class chache is reset whenever a new local instance is found.
-    - `isClassExpensive` uses `whnf` which depends (indirectly) on the set of local instances.
-      Thus, each new local instance requires a new `resettingSynthInstanceCache`. -/
+    - `isClassExpensive` uses `whnf` which depends (indirectly) on the set of local instances. -/
   private partial def withNewLocalInstancesImp
       (fvars : Array Expr) (i : Nat) (k : MetaM α) : MetaM α := do
     if h : i < fvars.size then
@@ -1005,20 +984,27 @@ mutual
       else
         k #[] type
 
+
+  -- Helper method for isClassExpensive?
+  private partial def isClassApp? (type : Expr) (instantiated := false) : MetaM (Option Name) := do
+    match type.getAppFn with
+    | .const c _ =>
+      let env ← getEnv
+      if isClass env c then
+        return some c
+      else
+        -- Use whnf to make sure abbreviations are unfolded
+        match (← whnf type).getAppFn with
+        | .const c _ => if isClass env c then return some c else return none
+        | _ => return none
+    | .mvar .. =>
+      if instantiated then return none
+      isClassApp? (← instantiateMVars type) true
+    | _ => return none
+
   private partial def isClassExpensive? (type : Expr) : MetaM (Option Name) :=
     withReducible do -- when testing whether a type is a type class, we only unfold reducible constants.
-      forallTelescopeReducingAux type none fun _ type => do
-        let env ← getEnv
-        match type.getAppFn with
-        | .const c _ => do
-          if isClass env c then
-            return some c
-          else
-            -- make sure abbreviations are unfolded
-            match (← whnf type).getAppFn with
-            | .const c _ => return if isClass env c then some c else none
-            | _ => return none
-        | _ => return none
+      forallTelescopeReducingAux type none fun _ type => isClassApp? type
 
   private partial def isClassImp? (type : Expr) : MetaM (Option Name) := do
     match (← isClassQuick? type) with
@@ -1278,7 +1264,7 @@ def withLocalInstancesImp (decls : List LocalDecl) (k : MetaM α) : MetaM α :=
   if localInsts.size == size then
     k
   else
-    resettingSynthInstanceCache <| withReader (fun ctx => { ctx with localInstances := localInsts }) k
+    withReader (fun ctx => { ctx with localInstances := localInsts }) k
 
 /-- Register any local instance in `decls` -/
 def withLocalInstances (decls : List LocalDecl) : n α → n α :=
@@ -1322,12 +1308,8 @@ def withNewMCtxDepth (k : n α) (allowLevelAssignments := false) : n α :=
   mapMetaM (withNewMCtxDepthImp allowLevelAssignments) k
 
 private def withLocalContextImp (lctx : LocalContext) (localInsts : LocalInstances) (x : MetaM α) : MetaM α := do
-  let localInstsCurr ← getLocalInstances
   withReader (fun ctx => { ctx with lctx := lctx, localInstances := localInsts }) do
-    if localInsts == localInstsCurr then
-      x
-    else
-      resettingSynthInstanceCache x
+    x
 
 /--
   `withLCtx lctx localInsts k` replaces the local context and local instances, and then executes `k`.

src/Lean/Meta/Closure.lean

@@ -366,4 +366,39 @@ def mkAuxDefinitionFor (name : Name) (value : Expr) (zeta : Bool := false) : Met
   let type := type.headBeta
   mkAuxDefinition name type value (zeta := zeta)
 
+/--
+  Create an auxiliary theorem with the given name, type and value. It is similar to `mkAuxDefinition`.
+-/
+def mkAuxTheorem (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : MetaM Expr := do
+  let result ← Closure.mkValueTypeClosure type value zeta
+  let env ← getEnv
+  let decl :=
+    if env.hasUnsafe result.type || env.hasUnsafe result.value then
+      -- `result` contains unsafe code, thus we cannot use a theorem.
+      Declaration.defnDecl {
+        name
+        levelParams := result.levelParams.toList
+        type        := result.type
+        value       := result.value
+        hints       := ReducibilityHints.opaque
+        safety      := DefinitionSafety.unsafe
+      }
+    else
+      Declaration.thmDecl {
+        name
+        levelParams := result.levelParams.toList
+        type        := result.type
+        value       := result.value
+      }
+  addDecl decl
+  return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
+
+/--
+  Similar to `mkAuxTheorem`, but infers the type of `value`.
+-/
+def mkAuxTheoremFor (name : Name) (value : Expr) (zeta : Bool := false) : MetaM Expr := do
+  let type ← inferType value
+  let type := type.headBeta
+  mkAuxTheorem name type value zeta
+
 end Lean.Meta

src/Lean/Meta/Coe.lean

@@ -54,18 +54,28 @@ def coerceSimple? (expr expectedType : Expr) : MetaM (LOption Expr) := do
 
 /-- Coerces `expr` to a function type. -/
 def coerceToFunction? (expr : Expr) : MetaM (Option Expr) := do
-  let result ← try mkAppM ``CoeFun.coe #[expr] catch _ => return none
-  let expanded ← expandCoe result
+  -- constructing expression manually because mkAppM wouldn't assign universe mvars
+  let α ← inferType expr
+  let u ← getLevel α
+  let v ← mkFreshLevelMVar
+  let γ ← mkFreshExprMVar (← mkArrow α (mkSort v))
+  let .some inst ← trySynthInstance (mkApp2 (.const ``CoeFun [u,v]) α γ) | return none
+  let expanded ← expandCoe (mkApp4 (.const ``CoeFun.coe [u,v]) α γ inst expr)
   unless (← whnf (← inferType expanded)).isForall do
-    throwError "failed to coerce{indentExpr expr}\nto a function, after applying `CoeFun.coe`, result is still not a function{indentExpr expanded}\nthis is often due to incorrect `CoeFun` instances, the synthesized instance was{indentExpr result.appFn!.appArg!}"
+    throwError "failed to coerce{indentExpr expr}\nto a function, after applying `CoeFun.coe`, result is still not a function{indentExpr expanded}\nthis is often due to incorrect `CoeFun` instances, the synthesized instance was{indentExpr inst}"
   return expanded
 
 /-- Coerces `expr` to a type. -/
 def coerceToSort? (expr : Expr) : MetaM (Option Expr) := do
-  let result ← try mkAppM ``CoeSort.coe #[expr] catch _ => return none
-  let expanded ← expandCoe result
+  -- constructing expression manually because mkAppM wouldn't assign universe mvars
+  let α ← inferType expr
+  let u ← getLevel α
+  let v ← mkFreshLevelMVar
+  let β ← mkFreshExprMVar (mkSort v)
+  let .some inst ← trySynthInstance (mkApp2 (.const ``CoeSort [u,v]) α β) | return none
+  let expanded ← expandCoe (mkApp4 (.const ``CoeSort.coe [u,v]) α β inst expr)
   unless (← whnf (← inferType expanded)).isSort do
-    throwError "failed to coerce{indentExpr expr}\nto a type, after applying `CoeSort.coe`, result is still not a type{indentExpr expanded}\nthis is often due to incorrect `CoeSort` instances, the synthesized instance was{indentExpr result.appFn!.appArg!}"
+    throwError "failed to coerce{indentExpr expr}\nto a type, after applying `CoeSort.coe`, result is still not a type{indentExpr expanded}\nthis is often due to incorrect `CoeSort` instances, the synthesized instance was{indentExpr inst}"
   return expanded
 
 /-- Return `some (m, α)` if `type` can be reduced to an application of the form `m α` using `[reducible]` transparency. -/

src/Lean/Meta/DiscrTree.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.WHNF
+import Lean.Meta.Transform
 import Lean.Meta.DiscrTreeTypes
 
 namespace Lean.Meta.DiscrTree
@@ -181,6 +182,31 @@ private partial def isNumeral (e : Expr) : Bool :=
       else if fName == ``Nat.zero && e.getAppNumArgs == 0 then true
       else false
 
+private partial def toNatLit? (e : Expr) : Option Literal :=
+  if isNumeral e then
+    if let some n := loop e then
+      some (.natVal n)
+    else
+      none
+  else
+    none
+where
+  loop (e : Expr) : OptionT Id Nat := do
+    let f := e.getAppFn
+    match f with
+    | .lit (.natVal n) => return n
+    | .const fName .. =>
+      if fName == ``Nat.succ && e.getAppNumArgs == 1 then
+        let r ← loop e.appArg!
+        return r+1
+      else if fName == ``OfNat.ofNat && e.getAppNumArgs == 3 then
+        loop (e.getArg! 1)
+      else if fName == ``Nat.zero && e.getAppNumArgs == 0 then
+        return 0
+      else
+        failure
+    | _ => failure
+
 private def isNatType (e : Expr) : MetaM Bool :=
   return (← whnf e).isConstOf ``Nat
 
@@ -206,16 +232,14 @@ private def isOffset (fName : Name) (e : Expr) : MetaM Bool := do
   TODO: add hook for users adding their own functions for controlling `shouldAddAsStar`
   Different `DiscrTree` users may populate this set using, for example, attributes.
 
-  Remark: we currently tag `Nat.zero` and "offset" terms to avoid having to add special
-  support for `Expr.lit` and offset terms.
+  Remark: we currently tag "offset" terms as star to avoid having to add special
+  support for offset terms.
   Example, suppose the discrimination tree contains the entry
   `Nat.succ ?m |-> v`, and we are trying to retrieve the matches for `Expr.lit (Literal.natVal 1) _`.
-  In this scenario, we want to retrieve `Nat.succ ?m |-> v` -/
+  In this scenario, we want to retrieve `Nat.succ ?m |-> v`
+-/
 private def shouldAddAsStar (fName : Name) (e : Expr) : MetaM Bool := do
-  if fName == ``Nat.zero then
-    return true
-  else
-    isOffset fName e
+  isOffset fName e
 
 def mkNoindexAnnotation (e : Expr) : Expr :=
   mkAnnotation `noindex e
@@ -252,6 +276,33 @@ private def isBadKey (fn : Expr) : Bool :=
   | .forallE _ _ b _ => b.hasLooseBVars
   | _ => true
 
+/--
+  Try to eliminate loose bound variables by performing beta-reduction.
+  We use this method when processing terms in discrimination trees.
+  These trees distinguish dependent arrows from nondependent ones.
+  Recall that dependent arrows are indexed as `.other`, but nondependent arrows as `.arrow ..`.
+  Motivation: we want to "discriminate" implications and simple arrows in our index.
+
+  Now suppose we add the term `Foo (Nat → Nat)` to our index. The nested arrow appears as
+  `.arrow ..`. Then, suppose we want to check whether the index contains
+  `(x : Nat) → (fun _ => Nat) x`, but it will fail to retrieve `Foo (Nat → Nat)` because
+  it assumes the nested arrow is a dependent one and uses `.other`.
+
+  We use this method to address this issue by beta-reducing terms containing loose bound variables.
+  See issue #2232.
+
+  Remark: we expect the performance impact will be minimal.
+-/
+private def elimLooseBVarsByBeta (e : Expr) : CoreM Expr :=
+  Core.transform e
+    (pre := fun e => do
+      if !e.hasLooseBVars then
+        return .done e
+      else if e.isHeadBetaTarget then
+        return .visit e.headBeta
+      else
+        return .continue)
+
 /--
   Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
   is a bad key (see comment at `isBadKey`).
@@ -285,9 +336,12 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key s
       let todo ← pushArgsAux info.paramInfo (nargs-1) e todo
       return (k, todo)
     match fn with
-    | .lit v         => return (.lit v, todo)
-    | .const c _     =>
+    | .lit v     =>
+      return (.lit v, todo)
+    | .const c _ =>
       unless root do
+        if let some v := toNatLit? e then
+          return (.lit v, todo)
         if (← shouldAddAsStar c e) then
           return (.star, todo)
       let nargs := e.getAppNumArgs
@@ -314,6 +368,8 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key s
       else
         return (.star, todo)
     | .forallE _ d b _ =>
+      -- See comment at elimLooseBVarsByBeta
+      let b ← if b.hasLooseBVars then elimLooseBVarsByBeta b else pure b
       if b.hasLooseBVars then
         return (.other, todo)
       else
@@ -346,8 +402,24 @@ private partial def createNodes (keys : Array (Key s)) (v : α) (i : Nat) : Trie
   else
     .node #[v] #[]
 
+/--
+If `vs` contains an element `v'` such that `v == v'`, then replace `v'` with `v`.
+Otherwise, push `v`.
+See issue #2155
+Recall that `BEq α` may not be Lawful.
+-/
 private def insertVal [BEq α] (vs : Array α) (v : α) : Array α :=
-  if vs.contains v then vs else vs.push v
+  loop 0
+where
+  loop (i : Nat) : Array α :=
+    if h : i < vs.size then
+      if v == vs[i] then
+        vs.set ⟨i,h⟩ v
+      else
+        loop (i+1)
+    else
+      vs.push v
+termination_by loop i => vs.size - i
 
 private partial def insertAux [BEq α] (keys : Array (Key s)) (v : α) : Nat → Trie α s → Trie α s
   | i, .node vs cs =>
@@ -380,6 +452,10 @@ def insert [BEq α] (d : DiscrTree α s) (e : Expr) (v : α) : MetaM (DiscrTree
 
 private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array Expr) := do
   let e ← reduceDT e root (simpleReduce := s)
+  unless root do
+    -- See pushArgs
+    if let some v := toNatLit? e then
+      return (.lit v, #[])
   match e.getAppFn with
   | .lit v         => return (.lit v, #[])
   | .const c _     =>
@@ -445,6 +521,8 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array
     let nargs := e.getAppNumArgs
     return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
   | .forallE _ d b _ =>
+    -- See comment at elimLooseBVarsByBeta
+    let b ← if b.hasLooseBVars then elimLooseBVarsByBeta b else pure b
     if b.hasLooseBVars then
       return (.other, #[])
     else

src/Lean/Meta/ExprDefEq.lean

@@ -9,6 +9,27 @@ import Lean.Util.OccursCheck
 
 namespace Lean.Meta
 
+/--
+  Return `true` if `e` is of the form `fun (x_1 ... x_n) => ?m y_1 ... y_k)`, and `?m` is unassigned.
+  Remark: `n`, `k` may be 0.
+  This function is used to filter unification problems in
+  `isDefEqArgs`/`isDefEqEtaStruct` where we can assign proofs.
+  If one side is of the form described above, then we can likely assign `?m`.
+  But it it's not, we would most likely apply proof irrelevance, which is
+  usually very expensive since it needs to unify the types as well.
+-/
+def isAbstractedUnassignedMVar : Expr → MetaM Bool
+  | .lam _ _ b _ => isAbstractedUnassignedMVar b
+  | .app a _ => isAbstractedUnassignedMVar a
+  | .mvar mvarId => do
+    if (← mvarId.isReadOnlyOrSyntheticOpaque) then
+      pure false
+    else if (← mvarId.isAssigned) then
+      pure false
+    else
+      pure true
+  | _ => pure false
+
 /--
   Return true if `b` is of the form `mk a.1 ... a.n`, and `a` is not a constructor application.
 
@@ -49,6 +70,13 @@ where
           for i in [ctorVal.numParams : args.size] do
             let j := i - ctorVal.numParams
             let proj ← mkProjFn ctorVal us params j a
+            if ← isProof proj then
+              unless ← isAbstractedUnassignedMVar args[i]! do
+                -- Skip expensive unification problem that is likely solved
+                -- using proof irrelevance.  We already know that `proj` and
+                -- `args[i]!` have the same type, so they're defeq in any case.
+                -- See comment at `isAbstractedUnassignedMVar`.
+                continue
             trace[Meta.isDefEq.eta.struct] "{a} =?= {b} @ [{j}], {proj} =?= {args[i]!}"
             unless (← isDefEq proj args[i]!) do
               trace[Meta.isDefEq.eta.struct] "failed, unexpect arg #{i}, projection{indentExpr proj}\nis not defeq to{indentExpr args[i]!}"
@@ -222,12 +250,26 @@ private def isDefEqArgsFirstPass
       trace[Meta.isDefEq] "found messy {a₁} =?= {a₂}"
       postponedHO := postponedHO.push i
     else if info.isExplicit then
+      if info.isProp then
+        unless ← isAbstractedUnassignedMVar a₁ <||> isAbstractedUnassignedMVar a₂ do
+          -- Skip expensive unification problem that is likely solved
+          -- using proof irrelevance.  We already know that `a₁` and
+          -- `a₂` have the same type, so they're defeq in any case.
+          -- See comment at `isAbstractedUnassignedMVar`.
+          continue
       unless (← Meta.isExprDefEqAux a₁ a₂) do
         return .failed
     else if (← isEtaUnassignedMVar a₁ <||> isEtaUnassignedMVar a₂) then
       unless (← Meta.isExprDefEqAux a₁ a₂) do
         return .failed
     else
+      if info.isProp then
+        unless ← isAbstractedUnassignedMVar a₁ <||> isAbstractedUnassignedMVar a₂ do
+          -- Skip expensive unification problem that is likely solved
+          -- using proof irrelevance.  We already know that `a₁` and
+          -- `a₂` have the same type, so they're defeq in any case.
+          -- See comment at `isAbstractedUnassignedMVar`.
+          continue
       postponedImplicit := postponedImplicit.push i
   return .ok postponedImplicit postponedHO
 
@@ -1729,13 +1771,17 @@ private def isDefEqProjInst (t : Expr) (s : Expr) : MetaM LBool := do
 private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   whenUndefDo (isDefEqEta t s) do
   whenUndefDo (isDefEqEta s t) do
-  -- TODO: investigate whether this is the place for putting this check
-  if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then return true
   if (← isDefEqProj t s) then return true
   whenUndefDo (isDefEqNative t s) do
   whenUndefDo (isDefEqNat t s) do
   whenUndefDo (isDefEqOffset t s) do
   whenUndefDo (isDefEqDelta t s) do
+  -- We try structure eta *after* lazy delta reduction;
+  -- otherwise we would end up applying it at every step of a reduction chain
+  -- as soon as one of the sides is a constructor application,
+  -- which is very costly because it requires us to unify the fields.
+  if (← (isDefEqEtaStruct t s <||> isDefEqEtaStruct s t)) then
+    return true
   if t.isConst && s.isConst then
     if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
   else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
@@ -1811,7 +1857,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
 builtin_initialize
   registerTraceClass `Meta.isDefEq
   registerTraceClass `Meta.isDefEq.stuck
-  registerTraceClass `Meta.isDefEq.stuck.mvar (inherited := true)
+  registerTraceClass `Meta.isDefEq.stuckMVar (inherited := true)
   registerTraceClass `Meta.isDefEq.cache
   registerTraceClass `Meta.isDefEq.foApprox (inherited := true)
   registerTraceClass `Meta.isDefEq.onFailure (inherited := true)