fix: code duplication at liftCoreM and liftTermElabM at Command.lean

This PR also
- Fields caching specific `Options` at `CoreM` are properly set.
- `nextMacroScope` was not being propagated at `liftCoreM`.

.github/workflows/ci.yml

@@ -54,7 +54,10 @@ jobs:
         with:
           script: |
             const quick = ${{ steps.set-quick.outputs.quick }};
-            console.log(`quick: ${quick}`)
+            console.log(`quick: ${quick}`);
+            // use large runners outside PRs where available (original repo)
+            // disabled for now as this mostly just speeds up the test suite which is not a bottleneck
+            // let large = ${{ github.event_name != 'pull_request' && github.repository == 'leanprover/lean4' }} ? "-large" : "";
             let matrix = [
               {
                 // portable release build: use channel with older glibc (2.27)

README.md

@@ -22,4 +22,4 @@ Please read our [Contribution Guidelines](CONTRIBUTING.md) first.
 
 # Building from Source
 
-See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html).
+See [Building Lean](https://lean-lang.org/lean4/doc/make/index.html) (documentation source: [doc/make/index.md](doc/make/index.md)).

RELEASES.md

@@ -8,7 +8,10 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
-v4.8.0 (development in progress)
+v4.9.0 (development in progress)
+---------
+
+v4.8.0 
 ---------
 
 * **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
@@ -85,6 +88,8 @@ v4.8.0 (development in progress)
   [#3798](https://github.com/leanprover/lean4/pull/3798) and
   [#3978](https://github.com/leanprover/lean4/pull/3978).
 
+* Hovers for terms in `match` expressions in the Infoview now reliably show the correct term.
+
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators
   for the `induction` and `cases` tactics, replacing the `@[eliminator]` attribute.
   Gives custom eliminators for `Nat` so that `induction` and `cases` put goal states into terms of `0` and `n + 1`

doc/dev/bootstrap.md

@@ -84,10 +84,12 @@ gh workflow run update-stage0.yml
 Leaving stage0 updates to the CI automation is preferable, but should you need
 to do it locally, you can use `make update-stage0-commit` in `build/release` to
 update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
-update from another stage.
+update from another stage. This command will automatically stage the updated files
+and introduce a commit,so make sure to commit your work before that.
 
-This command will automatically stage the updated files and introduce a commit,
-so make sure to commit your work before that.
+If you rebased the branch (either onto a newer version of `master`, or fixing
+up some commits prior to the stage0 update, recreate the stage0 update commits.
+The script `script/rebase-stage0.sh` can be used for that.
 
 The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
 from entering `master` through the (squashing!) merge queue, and label such PRs
@@ -95,6 +97,7 @@ with the `changes-stage0` label. Such PRs should have a cleaned up history,
 with separate stage0 update commits; then coordinate with the admins to merge
 your PR using rebase merge, bypassing the merge queue.
 
+
 ## Further Bootstrapping Complications
 
 As written above, changes in meta code in the current stage usually will only

doc/dev/ffi.md

@@ -53,10 +53,59 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`).
 * A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
-  Its runtime value is a pointer to an object of a subtype of `lean_object` (see respective declarations in `lean.h`) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
+  Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
   Example: the runtime value of `u : Unit` is always `lean_box(0)`.
 
+#### Inductive types
+
+For inductive types which are in the fallback `lean_object *` case above and not trivial constructors, the type is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true. A `lean_ctor_object` stores the constructor index in the header, and the fields are stored in the `m_objs` portion of the object.
+
+The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
+
+* Non-scalar fields stored as `lean_object *`
+* Fields of type `USize`
+* Other scalar fields, in decreasing order by size
+
+Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
+
+* To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
+* To access `USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
+* To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
+
+For example, a structure such as
+```lean
+structure S where
+  ptr_1 : Array Nat
+  usize_1 : USize
+  sc64_1 : UInt64
+  ptr_2 : { x : UInt64 // x > 0 } -- wrappers don't count as scalars
+  sc64_2 : Float -- `Float` is 64 bit
+  sc8_1 : Bool
+  sc16_1 : UInt16
+  sc8_2 : UInt8
+  sc64_3 : UInt64
+  usize_2 : USize
+  ptr_3 : Char -- trivial wrapper around `UInt32`
+  sc32_1 : UInt32
+  sc16_2 : UInt16
+```
+would get re-sorted into the following memory order:
+
+* `S.ptr_1` - `lean_ctor_get(val, 0)`
+* `S.ptr_2` - `lean_ctor_get(val, 1)`
+* `S.ptr_3` - `lean_ctor_get(val, 2)`
+* `S.usize_1` - `lean_ctor_get_usize(val, 3)`
+* `S.usize_2` - `lean_ctor_get_usize(val, 4)`
+* `S.sc64_1` - `lean_ctor_get_uint64(val, sizeof(void*)*5)`
+* `S.sc64_2` - `lean_ctor_get_float(val, sizeof(void*)*5 + 8)`
+* `S.sc64_3` - `lean_ctor_get_uint64(val, sizeof(void*)*5 + 16)`
+* `S.sc32_1` - `lean_ctor_get_uint32(val, sizeof(void*)*5 + 24)`
+* `S.sc16_1` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 28)`
+* `S.sc16_2` - `lean_ctor_get_uint16(val, sizeof(void*)*5 + 30)`
+* `S.sc8_1` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 32)`
+* `S.sc8_2` - `lean_ctor_get_uint8(val, sizeof(void*)*5 + 33)`
+
 ### Borrowing
 
 By default, all `lean_object *` parameters of an `@[extern]` function are considered *owned*, i.e. the external code is passed a "virtual RC token" and is responsible for passing this token along to another consuming function (exactly once) or freeing it via `lean_dec`.

nix/bootstrap.nix

@@ -180,7 +180,7 @@ rec {
       update-stage0 =
         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"}
+          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
         '';
       update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
         set -euo pipefail

script/lib/README.md

@@ -0,0 +1,2 @@
+This directory contains various scripts that are *not* meant to be called
+directly, but through other scripts or makefiles.

script/lib/rebase-editor.sh

@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+
+# Script internal to `./script/rebase-stage0.sh`
+
+# Determine OS type for sed in-place editing
+SED_CMD=("sed" "-i")
+if [[ "$OSTYPE" == "darwin"* ]]
+then
+    # macOS requires an empty string argument with -i for in-place editing
+    SED_CMD=("sed" "-i" "")
+fi
+
+if [ "$STAGE0_WITH_NIX" = true ]
+then
+  "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x nix run .#update-stage0-commit,' "$1"
+else
+  "${SED_CMD[@]}" '/chore: update stage0/ s,.*,x make -j32 -C build/release update-stage0 \&\& git commit -m "chore: update stage0",' "$1"
+fi

script/rebase-stage0.sh

@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+# This script rebases onto the given branch/commit, and updates
+# all `chore: update stage0` commits along the way.
+
+# Whether to use nix or make to update stage0
+if [ "$1" = "-nix" ]
+then
+   export STAGE0_WITH_NIX=true
+   shift
+fi
+
+# Check if an argument is provided
+if [ "$#" -eq 0 ]; then
+    echo "Usage: $0 [-nix] <options to git rebase -i>"
+    exit 1
+fi
+
+REPO_ROOT=$(git rev-parse --show-toplevel)
+
+# Run git rebase in interactive mode, but automatically edit the todo list
+# using the defined GIT_SEQUENCE_EDITOR command
+GIT_SEQUENCE_EDITOR="$REPO_ROOT/script/lib/rebase-editor.sh" git rebase -i "$@"
+

src/CMakeLists.txt

@@ -9,7 +9,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 8)
+set(LEAN_VERSION_MINOR 9)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -591,7 +591,7 @@ endif()
 
 if(PREV_STAGE)
   add_custom_target(update-stage0
-    COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/update-stage0'
+    COMMAND bash -c 'CSRCS=${CMAKE_BINARY_DIR}/lib/temp script/lib/update-stage0'
     DEPENDS make_stdlib
     WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/..")
 

src/Init/Data/BitVec/Lemmas.lean

@@ -103,7 +103,13 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
     have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
-@[simp] theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+-- This cannot be a `@[simp]` lemma, as it would be tried at every term.
+theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
+
+@[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
+@[simp] theorem getLsb_zero_length (x : BitVec 0) : x.getLsb i = false := by simp [of_length_zero]
+@[simp] theorem getMsb_zero_length (x : BitVec 0) : x.getMsb i = false := by simp [of_length_zero]
+@[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
@@ -336,7 +342,7 @@ theorem nat_eq_toNat (x : BitVec w) (y : Nat)
 @[simp] theorem getMsb_zeroExtend_add {x : BitVec w} (h : k ≤ i) :
     (x.zeroExtend (w + k)).getMsb i = x.getMsb (i - k) := by
   by_cases h : w = 0
-  · subst h; simp
+  · subst h; simp [of_length_zero]
   simp only [getMsb, getLsb_zeroExtend]
   by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
     <;> simp [h₁, h₂, h₃]

src/Init/Notation.lean

@@ -687,4 +687,27 @@ syntax (name := checkSimp) "#check_simp " term "~>" term : command
 -/
 syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
 
+/--
+The `seal foo` command ensures that the definition of `foo` is sealed, meaning it is marked as `[irreducible]`.
+This command is particularly useful in contexts where you want to prevent the reduction of `foo` in proofs.
+
+In terms of functionality, `seal foo` is equivalent to `attribute [local irreducible] foo`.
+This attribute specifies that `foo` should be treated as irreducible only within the local scope,
+which helps in maintaining the desired abstraction level without affecting global settings.
+-/
+syntax "seal " (ppSpace ident)+ : command
+
+/--
+The `unseal foo` command ensures that the definition of `foo` is unsealed, meaning it is marked as `[semireducible]`, the
+default reducibility setting. This command is useful when you need to allow some level of reduction of `foo` in proofs.
+
+Functionally, `unseal foo` is equivalent to `attribute [local semireducible] foo`.
+Applying this attribute makes `foo` semireducible only within the local scope.
+-/
+syntax "unseal " (ppSpace ident)+ : command
+
+macro_rules
+  | `(seal $fs:ident*) => `(attribute [local irreducible] $fs:ident*)
+  | `(unseal $fs:ident*) => `(attribute [local semireducible] $fs:ident*)
+
 end Parser

src/Init/Prelude.lean

@@ -4372,7 +4372,7 @@ def defaultMaxRecDepth := 512
 
 /-- The message to display on stack overflow. -/
 def maxRecDepthErrorMessage : String :=
-  "maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)"
+  "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
 
 namespace Syntax
 

src/Init/System/IO.lean

@@ -625,7 +625,13 @@ partial def FS.removeDirAll (p : FilePath) : IO Unit := do
 
 namespace Process
 
-/-- Returns the process ID of the current process. -/
+/-- Returns the current working directory of the calling process. -/
+@[extern "lean_io_process_get_current_dir"] opaque getCurrentDir : IO FilePath
+
+/-- Sets the current working directory of the calling process. -/
+@[extern "lean_io_process_set_current_dir"] opaque setCurrentDir (path : @& FilePath) : IO Unit
+
+/-- Returns the process ID of the calling process. -/
 @[extern "lean_io_process_get_pid"] opaque getPID : BaseIO UInt32
 
 inductive Stdio where

src/Init/Tactics.lean

@@ -368,7 +368,7 @@ for new reflexive relations.
 Remark: `rfl` is an extensible tactic. We later add `macro_rules` to try different
 reflexivity theorems (e.g., `Iff.rfl`).
 -/
-macro "rfl" : tactic => `(tactic| fail "The rfl tactic failed. Possible reasons:
+macro "rfl" : tactic => `(tactic| case' _ => fail "The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
 - The arguments of the relation are not equal.
 Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")

src/Lean/Compiler/ExternAttr.lean

@@ -156,7 +156,7 @@ private def getExternConstArity (declName : Name) : CoreM Nat := do
 @[export lean_get_extern_const_arity]
 def getExternConstArityExport (env : Environment) (declName : Name) : IO (Option Nat) := do
   try
-    let (arity, _) ← (getExternConstArity declName).toIO { fileName := "<compiler>", fileMap := default, diag := false } { env := env }
+    let (arity, _) ← (getExternConstArity declName).toIO { fileName := "<compiler>", fileMap := default } { env := env }
     return some arity
   catch
    | IO.Error.userError _   => return none

src/Lean/CoreM.lean

@@ -121,7 +121,19 @@ instance : MonadOptions CoreM where
   getOptions := return (← read).options
 
 instance : MonadWithOptions CoreM where
-  withOptions f x := withReader (fun ctx => { ctx with options := f ctx.options }) x
+  withOptions f x :=
+    withReader
+      (fun ctx =>
+        let options := f ctx.options
+        { ctx with
+          options
+          diag := diagnostics.get options
+          maxRecDepth := maxRecDepth.get options })
+      x
+
+-- Helper function for ensuring fields that depend on `options` have the correct value.
+@[inline] private def withConsistentCtx (x : CoreM α) : CoreM α := do
+  withOptions id x
 
 instance : AddMessageContext CoreM where
   addMessageContext := addMessageContextPartial
@@ -209,7 +221,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
   mkFreshNameImp n
 
 @[inline] def CoreM.run (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
-  (x ctx).run s
+  ((withConsistentCtx x) ctx).run s
 
 @[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
   Prod.fst <$> x.run ctx s
@@ -223,7 +235,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 instance [MetaEval α] : MetaEval (CoreM α) where
   eval env opts x _ := do
     let x : CoreM α := do try x finally printTraces
-    let (a, s) ← x.toIO { maxRecDepth := maxRecDepth.get opts, options := opts, fileName := "<CoreM>", fileMap := default, diag := diagnostics.get opts } { env := env }
+    let (a, s) ← (withConsistentCtx x).toIO { fileName := "<CoreM>", fileMap := default, options := opts } { env := env }
     MetaEval.eval s.env opts a (hideUnit := true)
 
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
@@ -236,7 +248,7 @@ protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m
     throw <| Exception.error .missing "elaboration interrupted"
 
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let msg := s!"(deterministic) timeout at '{moduleName}', maximum number of heartbeats ({max/1000}) has been reached (use 'set_option {optionName} <num>' to set the limit)"
+  let msg := s!"(deterministic) timeout at `{moduleName}`, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
   throw <| Exception.error (← getRef) (MessageData.ofFormat (Std.Format.text msg))
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do
@@ -398,8 +410,7 @@ def isDiagnosticsEnabled : CoreM Bool :=
 
 def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let ctx ← read
-  let opts := ctx.opts
-  let (a, _) ← x.toIO { options := opts, fileName := "<ImportM>", fileMap := default, diag := getDiag opts } { env := ctx.env }
+  let (a, _) ← (withOptions (fun _ => ctx.opts) x).toIO { fileName := "<ImportM>", fileMap := default } { env := ctx.env }
   return a
 
 /-- Return `true` if the exception was generated by one our resource limits. -/

src/Lean/Declaration.lean

@@ -135,6 +135,11 @@ structure TheoremVal extends ConstantVal where
   all : List Name := [name]
   deriving Inhabited, BEq
 
+@[export lean_mk_theorem_val]
+def mkTheoremValEx (name : Name) (levelParams : List Name) (type : Expr) (value : Expr) (all : List Name) : TheoremVal := {
+  name, levelParams, type, value, all
+}
+
 /-- Value for an opaque constant declaration `opaque x : t := e` -/
 structure OpaqueVal extends ConstantVal where
   value : Expr

src/Lean/Elab/Binders.lean

@@ -70,30 +70,34 @@ def kindOfBinderName (binderName : Name) : LocalDeclKind :=
   else
     .default
 
-partial def quoteAutoTactic : Syntax → TermElabM Syntax
-  | stx@(.ident ..) => throwErrorAt stx "invalid auto tactic, identifier is not allowed"
+partial def quoteAutoTactic : Syntax → CoreM Expr
+  | .ident _ _ val preresolved =>
+    return mkApp4 (.const ``Syntax.ident [])
+      (.const ``SourceInfo.none [])
+      (.app (.const ``String.toSubstring []) (mkStrLit (toString val)))
+      (toExpr val)
+      (toExpr preresolved)
   | stx@(.node _ k args) => do
     if stx.isAntiquot then
       throwErrorAt stx "invalid auto tactic, antiquotation is not allowed"
     else
-      let mut quotedArgs ← `(Array.empty)
+      let ty := .const ``Syntax []
+      let mut quotedArgs := mkApp (.const ``Array.empty [.zero]) ty
       for arg in args do
         if k == nullKind && (arg.isAntiquotSuffixSplice || arg.isAntiquotSplice) then
           throwErrorAt arg "invalid auto tactic, antiquotation is not allowed"
         else
           let quotedArg ← quoteAutoTactic arg
-          quotedArgs ← `(Array.push $quotedArgs $quotedArg)
-      `(Syntax.node SourceInfo.none $(quote k) $quotedArgs)
-  | .atom _ val => `(mkAtom $(quote val))
+          quotedArgs := mkApp3 (.const ``Array.push [.zero]) ty quotedArgs quotedArg
+      return mkApp3 (.const ``Syntax.node []) (.const ``SourceInfo.none []) (toExpr k) quotedArgs
+  | .atom _ val => return .app (.const ``mkAtom []) (toExpr val)
   | .missing    => throwError "invalid auto tactic, tactic is missing"
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
   withFreshMacroScope do
     let name ← MonadQuotation.addMacroScope `_auto
     let type := Lean.mkConst `Lean.Syntax
-    let tactic ← quoteAutoTactic tactic
-    let value ← elabTerm tactic type
-    let value ← instantiateMVars value
+    let value ← quoteAutoTactic tactic
     trace[Elab.autoParam] value
     let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := .opaque,
                                        safety := DefinitionSafety.safe }

src/Lean/Elab/BuiltinNotation.lean

@@ -388,7 +388,7 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
                return (← mkEqRec motive h (← mkEqSymm heq), none)
          let motive ← mkMotive lhs expectedAbst
          if badMotive?.isSome || !(← isTypeCorrect motive) then
-           -- Before failing try tos use `subst`
+           -- Before failing try to use `subst`
            if ← (isSubstCandidate lhs rhs <||> isSubstCandidate rhs lhs) then
              withLocalIdentFor heqStx heq fun heqStx => do
                let h ← instantiateMVars h
@@ -408,9 +408,13 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
        | none =>
          let h ← elabTerm hStx none
          let hType ← inferType h
-         let hTypeAbst ← kabstract hType lhs
+         let mut hTypeAbst ← kabstract hType lhs
          unless hTypeAbst.hasLooseBVars do
-           throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut its left hand side is not mentioned in the type{indentExpr hType}"
+           hTypeAbst ← kabstract hType rhs
+           unless hTypeAbst.hasLooseBVars do
+             throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut neither side of the equality is mentioned in the type{indentExpr hType}"
+           heq ← mkEqSymm heq
+           (lhs, rhs) := (rhs, lhs)
          let motive ← mkMotive lhs hTypeAbst
          unless (← isTypeCorrect motive) do
            throwError "invalid `▸` notation, failed to compute motive for the substitution"

src/Lean/Elab/BuiltinTerm.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Elab.Open
 import Lean.Elab.SetOption
 import Lean.Elab.Eval
@@ -313,8 +314,12 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
 
 @[builtin_term_elab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options, diag := getDiag options }) do
-    elabTerm stx[5] expectedType?
+  withOptions (fun _ => options) do
+    try
+      elabTerm stx[5] expectedType?
+    finally
+      if stx[1].getId == `diagnostics then
+        reportDiag
 
 @[builtin_term_elab withAnnotateTerm] def elabWithAnnotateTerm : TermElab := fun stx expectedType? => do
   match stx with

src/Lean/Elab/Command.lean

@@ -128,20 +128,6 @@ def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severit
   let endPos := ref.getTailPos?.getD pos
   mkMessageCore ctx.fileName ctx.fileMap msgData severity pos endPos
 
-private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.Context :=
-  let scope        := s.scopes.head!
-  { fileName       := ctx.fileName
-    fileMap        := ctx.fileMap
-    options        := scope.opts
-    currRecDepth   := ctx.currRecDepth
-    maxRecDepth    := s.maxRecDepth
-    ref            := ctx.ref
-    currNamespace  := scope.currNamespace
-    openDecls      := scope.openDecls
-    initHeartbeats := heartbeats
-    currMacroScope := ctx.currMacroScope
-    diag           := getDiag scope.opts }
-
 private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
   if traceState.traces.isEmpty then return log
   let mut traces : HashMap (String.Pos × String.Pos) (Array MessageData) := ∅
@@ -167,31 +153,49 @@ private def addTraceAsMessages : CommandElabM Unit := do
       traceState.traces := {}
     }
 
-def liftCoreM (x : CoreM α) : CommandElabM α := do
+private def runCore (x : CoreM α) : CommandElabM α := do
   let s ← get
   let ctx ← read
   let heartbeats ← IO.getNumHeartbeats
-  let Eα := Except Exception α
-  let x : CoreM Eα := try let a ← x; pure <| Except.ok a catch ex => pure <| Except.error ex
-  let x : EIO Exception (Eα × Core.State) := (ReaderT.run x (mkCoreContext ctx s heartbeats)).run { env := s.env, ngen := s.ngen, traceState := s.traceState, messages := {}, infoState.enabled := s.infoState.enabled }
+  let env := s.env
+  let scope := s.scopes.head!
+  let coreCtx : Core.Context := {
+    fileName       := ctx.fileName
+    fileMap        := ctx.fileMap
+    currRecDepth   := ctx.currRecDepth
+    maxRecDepth    := s.maxRecDepth
+    ref            := ctx.ref
+    currNamespace  := scope.currNamespace
+    openDecls      := scope.openDecls
+    initHeartbeats := heartbeats
+    currMacroScope := ctx.currMacroScope
+    options        := scope.opts
+  }
+  let x : EIO _ _ := x.run coreCtx {
+    env
+    ngen := s.ngen
+    nextMacroScope := s.nextMacroScope
+    infoState.enabled := s.infoState.enabled
+    traceState := s.traceState
+  }
   let (ea, coreS) ← liftM x
   modify fun s => { s with
-    env := coreS.env
-    ngen := coreS.ngen
-    messages := s.messages ++ coreS.messages
+    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 }
-    infoState.trees := s.infoState.trees.append coreS.infoState.trees
+    messages          := s.messages ++ coreS.messages
   }
-  match ea with
-  | Except.ok a    => pure a
-  | Except.error e => throw e
+  return ea
+
+def liftCoreM (x : CoreM α) : CommandElabM α := do
+  MonadExcept.ofExcept (← runCore (observing x))
 
 private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message :=
   let ref := getBetterRef ref ctx.macroStack
   mkMessageAux ctx ref (toString err) MessageSeverity.error
 
-@[inline] def liftEIO {α} (x : EIO Exception α) : CommandElabM α := liftM x
-
 @[inline] def liftIO {α} (x : IO α) : CommandElabM α := do
   let ctx ← read
   IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
@@ -271,7 +275,7 @@ private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttrib
       (fun _ => do set s; elabCommandUsing s stx elabFns)
 
 /-- Elaborate `x` with `stx` on the macro stack -/
-def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
+def withMacroExpansion (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
   withInfoContext (mkInfo := pure <| .ofMacroExpansionInfo { stx := beforeStx, output := afterStx, lctx := .empty }) do
     withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
 
@@ -404,7 +408,6 @@ def printExpr (e : Expr) : MetaM Unit := do
 def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   let ctx ← read
   let s   ← get
-  let heartbeats ← IO.getNumHeartbeats
   -- dbg_trace "heartbeats: {heartbeats}"
   let scope := s.scopes.head!
   -- We execute `x` with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands.
@@ -413,18 +416,9 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   -- make sure `observing` below also catches runtime exceptions (like we do by default in
   -- `CommandElabM`)
   let _ := MonadAlwaysExcept.except (m := TermElabM)
-  let x : MetaM _      := (observing (try x finally Meta.reportDiag)).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, 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
-    traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref }
-    messages          := s.messages ++ coreS.messages
-  }
+  let x : MetaM _ := (observing (try x finally Meta.reportDiag)).run (mkTermContext ctx s) { levelNames := scope.levelNames }
+  let x : CoreM _ := x.run mkMetaContext {}
+  let ((ea, _), _) ← runCore x
   MonadExcept.ofExcept ea
 
 /--

src/Lean/Elab/InfoTree/Main.lean

@@ -102,9 +102,10 @@ def ContextInfo.runCoreM (info : ContextInfo) (x : CoreM α) : IO α := do
     have been used in `lctx` and `info.mctx`.
   -/
   (·.1) <$>
-    x.toIO { options := info.options, currNamespace := info.currNamespace, openDecls := info.openDecls
-             fileName := "<InfoTree>", fileMap := default, diag := getDiag info.options }
-           { env := info.env, ngen := info.ngen }
+    (withOptions (fun _ => info.options) x).toIO
+      { currNamespace := info.currNamespace, openDecls := info.openDecls
+        fileName := "<InfoTree>", fileMap := default }
+      { env := info.env, ngen := info.ngen }
 
 def ContextInfo.runMetaM (info : ContextInfo) (lctx : LocalContext) (x : MetaM α) : IO α := do
   (·.1) <$> info.runCoreM (x.run { lctx := lctx } { mctx := info.mctx })

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -228,20 +228,23 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
             throwThe Unit ()
   return (← (find e).run) matches .error _
 
-partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
+partial def mkEqnTypes (tryRefl : Bool) (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]
   return eqnTypes
 where
   go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
     trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
-    if (← tryURefl mvarId) then
-      saveEqn mvarId
-      return ()
+    if tryRefl then
+      if (← tryURefl mvarId) then
+        saveEqn mvarId
+        return ()
 
     if let some mvarId ← expandRHS? mvarId then
       return (← go mvarId)
---  The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it if we want to apply `splitMatch` on the body of the lambda
-/-    if let some mvarId ← funext? mvarId then
+
+    --  The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it
+    --  if we want to apply `splitMatch` on the body of the lambda
+    /- if let some mvarId ← funext? mvarId then
         return (← go mvarId) -/
 
     if (← shouldUseSimpMatch (← mvarId.getType')) then

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

@@ -62,7 +62,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes #[info.declName] goal.mvarId!
+    mkEqnTypes (tryRefl := true) #[info.declName] goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do

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

@@ -114,7 +114,8 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes info.declNames goal.mvarId!
+    withReducible do
+      mkEqnTypes (tryRefl := false) info.declNames goal.mvarId!
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Diagnostics
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Contradiction
@@ -163,8 +164,12 @@ private def getOptRotation (stx : Syntax) : Nat :=
 
 @[builtin_tactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
   let options ← Elab.elabSetOption stx[1] stx[3]
-  withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options, diag := getDiag options }) do
-    evalTactic stx[5]
+  withOptions (fun _ => options) do
+    try
+      evalTactic stx[5]
+    finally
+      if stx[1].getId == `diagnostics then
+        reportDiag
 
 @[builtin_tactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
   let mvarIds ← getGoals

src/Lean/Elab/Tactic/NormCast.lean

@@ -146,7 +146,9 @@ It tries to rewrite an expression using the elim and move lemmas.
 On failure, it calls the splitting procedure heuristic.
 -/
 partial def upwardAndElim (up : SimpTheorems) (e : Expr) : SimpM Simp.Step := do
-  let r ← withDischarger prove do
+  -- Remark: we set `wellBehavedDischarge := false` because `prove` may access arbitrary elements in the local context.
+  -- See comment at `Methods.wellBehavedDischarge`
+  let r ← withDischarger prove (wellBehavedDischarge := false) do
     Simp.rewrite? e up.post up.erased (tag := "squash") (rflOnly := false)
   let r := r.getD { expr := e }
   let r ← r.mkEqTrans (← splittingProcedure r.expr)

src/Lean/Elab/Tactic/Simp.lean

@@ -15,7 +15,6 @@ import Lean.Elab.Tactic.Config
 namespace Lean.Elab.Tactic
 open Meta
 open TSyntax.Compat
-open Simp (UsedSimps)
 
 declare_config_elab elabSimpConfigCore    Meta.Simp.Config
 declare_config_elab elabSimpConfigCtxCore Meta.Simp.ConfigCtx
@@ -327,7 +326,7 @@ If `stx` is the syntax of a `simp`, `simp_all` or `dsimp` tactic invocation, and
 creates the syntax of an equivalent `simp only`, `simp_all only` or `dsimp only`
 invocation.
 -/
-def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
+def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
   let isSimpAll := stx.isOfKind ``Parser.Tactic.simpAll
   let mut stx := stx
   if stx[3].isNone then
@@ -379,7 +378,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : UsedSimps) : MetaM Syntax := do
   let argsStx := if args.isEmpty then #[] else #[mkAtom "[", (mkAtom ",").mkSep args, mkAtom "]"]
   return stx.setArg 4 (mkNullNode argsStx)
 
-def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
+def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
   logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"
 
 /--
@@ -396,7 +395,7 @@ For many tactics other than the simplifier,
 one should use the `withLocation` tactic combinator
 when working with a `location`.
 -/
-def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM UsedSimps := do
+def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge? : Option Simp.Discharge := none) (loc : Location) : TacticM Simp.Stats := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -406,33 +405,39 @@ def simpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (discharge
     withMainContext do
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM UsedSimps := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, stats) ← simpGoal mvarId ctx (simprocs := simprocs) (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some (_, mvarId) => replaceMainGoal [mvarId]
-    return usedSimps
+    return stats
+
+def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
+  let stats ← x
+  Simp.reportDiag stats
 
 /-
   "simp" (config)? (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
   (location)?
 -/
-@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
+@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
-  let usedSimps ← dischargeWrapper.with fun discharge? =>
+  let stats ← dischargeWrapper.with fun discharge? =>
     simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
   if tactic.simp.trace.get (← getOptions) then
-    traceSimpCall stx usedSimps
+    traceSimpCall stx stats.usedTheorems
+  return stats.diag
 
-@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
+@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
-  let (result?, usedSimps) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
+  let (result?, stats) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
   match result? with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [mvarId]
   if tactic.simp.trace.get (← getOptions) then
-    traceSimpCall stx usedSimps
+    traceSimpCall stx stats.usedTheorems
+  return stats.diag
 
 def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Location) : TacticM Unit := do
   match loc with
@@ -444,14 +449,15 @@ def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Lo
     withMainContext do
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := withSimpDiagnostics do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
+    let (result?, stats) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
     if tactic.simp.trace.get (← getOptions) then
-      mvarId.withContext <| traceSimpCall (← getRef) usedSimps
+      mvarId.withContext <| traceSimpCall (← getRef) stats.usedTheorems
+    return stats.diag
 
 @[builtin_tactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
   let { ctx, simprocs, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -25,39 +25,41 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
 @[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
   match stx with
   | `(tactic|
-      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do
+      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
     let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
-    let usedSimps ← dischargeWrapper.with fun discharge? =>
+    let stats ← dischargeWrapper.with fun discharge? =>
       simpLocation ctx (simprocs := simprocs) discharge? <|
         (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx usedSimps
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
   match stx with
-  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => do
+  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
     else
       `(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
     let { ctx, .. } ← mkSimpContext stx (eraseLocal := true)
       (kind := .simpAll) (ignoreStarArg := true)
-    let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
+    let (result?, stats) ← simpAll (← getMainGoal) ctx
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
-    let stx ← mkSimpCallStx stx usedSimps
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax
 
 /-- Implementation of `dsimp?`. -/
 def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Location) :
-    TacticM Simp.UsedSimps := do
+    TacticM Simp.Stats := do
   match loc with
   | Location.targets hyps simplifyTarget =>
     withMainContext do
@@ -68,25 +70,26 @@ def dsimpLocation' (ctx : Simp.Context) (simprocs : SimprocsArray) (loc : Locati
       go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
 where
   /-- Implementation of `dsimp?`. -/
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
+  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.Stats := do
     let mvarId ← getMainGoal
-    let (result?, usedSimps) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
+    let (result?, stats) ← dsimpGoal mvarId ctx simprocs (simplifyTarget := simplifyTarget)
       (fvarIdsToSimp := fvarIdsToSimp)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
-    pure usedSimps
+    pure stats
 
 @[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
   match stx with
-  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
+  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
     let stx ← if bang.isSome then
       `(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
     else
       `(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
     let { ctx, simprocs, .. } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-    let usedSimps ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx usedSimps
+    let stats ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
+    let stx ← mkSimpCallStx stx stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
+    return stats.diag
   | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Simpa.lean

@@ -31,7 +31,7 @@ deriving instance Repr for UseImplicitLambdaResult
 @[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
   match stx with
   | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
-        $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do
+        $[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
     let stx ← `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
     let { ctx, simprocs, dischargeWrapper } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false)
@@ -39,12 +39,13 @@ deriving instance Repr for UseImplicitLambdaResult
     -- TODO: have `simpa` fail if it doesn't use `simp`.
     let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
     dischargeWrapper.with fun discharge? => do
-      let (some (_, g), usedSimps) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
+      let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)
         | if getLinterUnnecessarySimpa (← getOptions) then
             logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
+          return {}
       g.withContext do
-      let usedSimps ← if let some stx := usingArg then
+      let stats ← if let some stx := usingArg then
         setGoals [g]
         g.withContext do
         let e ← Tactic.elabTerm stx none (mayPostpone := true)
@@ -52,8 +53,8 @@ deriving instance Repr for UseImplicitLambdaResult
           pure (h, g)
         else
           (← g.assert `h (← inferType e) e).intro1
-        let (result?, usedSimps) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
-          (simplifyTarget := false) (usedSimps := usedSimps) (discharge? := discharge?)
+        let (result?, stats) ← simpGoal g ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
+          (simplifyTarget := false) (stats := stats) (discharge? := discharge?)
         match result? with
         | some (xs, g) =>
           let h := match xs with | #[h] | #[] => h | _ => unreachable!
@@ -66,18 +67,18 @@ deriving instance Repr for UseImplicitLambdaResult
             if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
               logLint linter.unnecessarySimpa (← getRef)
                 m!"try 'simp at {Expr.fvar h}' instead of 'simpa using {Expr.fvar h}'"
-        pure usedSimps
+        pure stats
       else if let some ldecl := (← getLCtx).findFromUserName? `this then
-        if let (some (_, g), usedSimps) ← simpGoal g ctx (simprocs := simprocs)
-            (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (usedSimps := usedSimps)
+        if let (some (_, g), stats) ← simpGoal g ctx (simprocs := simprocs)
+            (fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
             (discharge? := discharge?) then
-          g.assumption; pure usedSimps
+          g.assumption; pure stats
         else
-          pure usedSimps
+          pure stats
       else
-        g.assumption; pure usedSimps
+        g.assumption; pure stats
       if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
-        let stx ← match ← mkSimpOnly stx usedSimps with
+        let stx ← match ← mkSimpOnly stx stats.usedTheorems with
           | `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
             if unfold.isSome then
               `(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
@@ -85,6 +86,7 @@ deriving instance Repr for UseImplicitLambdaResult
               `(tactic| simpa $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
           | _ => unreachable!
         TryThis.addSuggestion tk stx (origSpan? := ← getRef)
+      return stats.diag
     | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic.Simpa

src/Lean/Meta/Diagnostics.lean

@@ -10,57 +10,79 @@ import Lean.Meta.Instances
 
 namespace Lean.Meta
 
-private def collectAboveThreshold (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool) : Array (Name × Nat) := Id.run do
+def collectAboveThreshold [BEq α] [Hashable α] (counters : PHashMap α Nat) (threshold : Nat) (p : α → Bool) (lt : α → α → Bool) : Array (α × Nat) := Id.run do
   let mut r := #[]
   for (declName, counter) in counters do
     if counter > threshold then
     if p declName then
       r := r.push (declName, counter)
-  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then d₁.lt d₂ else c₁ > c₂
+  return r.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then lt d₁ d₂ else c₁ > c₂
 
-private def mkMessageBodyFor? (counters : PHashMap Name Nat) (threshold : Nat) (p : Name → Bool := fun _ => true) : MetaM (Option MessageData) := do
-  let entries := collectAboveThreshold counters threshold p
-  if entries.isEmpty then
-    return none
-  else
-    let mut m := MessageData.nil
-    for (declName, counter) in entries do
-      unless m matches .nil do
-        m := m ++ "\n"
-      m := m ++ m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
-    return some m
-
-private def appendOptMessageData (m : MessageData) (header : String) (m? : Option MessageData) : MessageData :=
-  if let some m' := m? then
-    if m matches .nil then
-      header ++ indentD m'
+def subCounters [BEq α] [Hashable α] (newCounters oldCounters : PHashMap α Nat) : PHashMap α Nat := Id.run do
+  let mut result := {}
+  for (a, counterNew) in newCounters do
+    if let some counterOld := oldCounters.find? a then
+      result := result.insert a (counterNew - counterOld)
     else
-      m ++ "\n" ++ header ++ indentD m'
+      result := result.insert a counterNew
+  return result
+
+structure DiagSummary where
+  data  : Array MessageData := #[]
+  max   : Nat := 0
+  deriving Inhabited
+
+def DiagSummary.isEmpty (s : DiagSummary) : Bool :=
+  s.data.isEmpty
+
+def mkDiagSummary (counters : PHashMap Name Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
+  let entries := collectAboveThreshold counters threshold p Name.lt
+  if entries.isEmpty then
+    return {}
   else
+    let mut data := #[]
+    for (declName, counter) in entries do
+      data := data.push m!"{if data.isEmpty then "  " else "\n"}{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}"
+    return { data, max := entries[0]!.2 }
+
+def mkDiagSummaryForUnfolded (counters : PHashMap Name Nat) (instances := false) : MetaM DiagSummary := do
+  let env ← getEnv
+  mkDiagSummary counters fun declName =>
+    getReducibilityStatusCore env declName matches .semireducible
+    && isInstanceCore env declName == instances
+
+def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM DiagSummary := do
+  let env ← getEnv
+  mkDiagSummary counters fun declName =>
+    getReducibilityStatusCore env declName matches .reducible
+
+def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
+  mkDiagSummary (← get).diag.instanceCounter
+
+def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData :=
+  if s.isEmpty then
     m
+  else
+    let header := s!"{header} (max: {s.max}, num: {s.data.size}):"
+    m ++ .trace { cls } header s.data
 
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
-    let threshold := diagnostics.threshold.get (← getOptions)
-    let mut m := MessageData.nil
-    let env ← getEnv
-    let unfoldDefault? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
-      getReducibilityStatusCore env declName matches .semireducible
-      && !isInstanceCore env declName
-    let unfoldInstance? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
-      getReducibilityStatusCore env declName matches .semireducible
-      && isInstanceCore env declName
-    let unfoldReducible? ← mkMessageBodyFor? (← get).diag.unfoldCounter threshold fun declName =>
-      getReducibilityStatusCore env declName matches .reducible
-    let heu? ← mkMessageBodyFor? (← get).diag.heuristicCounter threshold
-    let inst? ← mkMessageBodyFor? (← get).diag.instanceCounter threshold
-    if unfoldDefault?.isSome || unfoldInstance?.isSome || unfoldReducible?.isSome || heu?.isSome || inst?.isSome then
-      m := appendOptMessageData m "unfolded declarations:" unfoldDefault?
-      m := appendOptMessageData m "unfolded instances:" unfoldInstance?
-      m := appendOptMessageData m "unfolded reducible declarations:" unfoldReducible?
-      m := appendOptMessageData m "used instances:" inst?
-      m := appendOptMessageData m "`isDefEq` heuristic:" heu?
-      m := m ++ "\nuse `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+    let unfoldCounter := (← get).diag.unfoldCounter
+    let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
+    let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
+    let unfoldReducible ← mkDiagSummaryForUnfoldedReducible unfoldCounter
+    let heu ← mkDiagSummary (← get).diag.heuristicCounter
+    let inst ← mkDiagSummaryForUsedInstances
+    unless unfoldDefault.isEmpty && unfoldInstance.isEmpty && unfoldReducible.isEmpty && heu.isEmpty && inst.isEmpty do
+      let m := MessageData.nil
+      let m := appendSection m `reduction "unfolded declarations" unfoldDefault
+      let m := appendSection m `reduction "unfolded instances" unfoldInstance
+      let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
+      let m := appendSection m `type_class "used instances" inst
+      let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
+      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
       logInfo m
 
 end Lean.Meta

src/Lean/Meta/ExprDefEq.lean

@@ -120,9 +120,9 @@ private def isDefEqEta (a b : Expr) : MetaM LBool := do
     let bType ← inferType b
     let bType ← whnfD bType
     match bType with
-    | Expr.forallE n d _ c =>
+    | .forallE n d _ c =>
       let b' := mkLambda n c d (mkApp b (mkBVar 0))
-      toLBoolM <| checkpointDefEq <| Meta.isExprDefEqAux a b'
+      toLBoolM <| Meta.isExprDefEqAux a b'
     | _ => return .undef
   else
     return .undef
@@ -346,10 +346,12 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
       k
   loop 0
 
-/-- Auxiliary function for `isDefEqBinding` for handling binders `forall/fun`.
-   It accumulates the new free variables in `fvars`, and declare them at `lctx`.
-   We use the domain types of `e₁` to create the new free variables.
-   We store the domain types of `e₂` at `ds₂`. -/
+/--
+Auxiliary function for `isDefEqBinding` for handling binders `forall/fun`.
+It accumulates the new free variables in `fvars`, and declare them at `lctx`.
+We use the domain types of `e₁` to create the new free variables.
+We store the domain types of `e₂` at `ds₂`.
+-/
 private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr) (e₁ e₂ : Expr) (ds₂ : Array Expr) : MetaM Bool :=
   let process (n : Name) (d₁ d₂ b₁ b₂ : Expr) : MetaM Bool := do
     let d₁     := d₁.instantiateRev fvars
@@ -386,34 +388,34 @@ private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
         pure false
 
 /--
-  Auxiliary method for solving constraints of the form `?m xs := v`.
-  It creates a lambda using `mkLambdaFVars ys v`, where `ys` is a superset of `xs`.
-  `ys` is often equal to `xs`. It is a bigger when there are let-declaration dependencies in `xs`.
-  For example, suppose we have `xs` of the form `#[a, c]` where
-  ```
-  a : Nat
-  b : Nat := f a
-  c : b = a
-  ```
-  In this scenario, the type of `?m` is `(x1 : Nat) -> (x2 : f x1 = x1) -> C[x1, x2]`,
-  and type of `v` is `C[a, c]`. Note that, `?m a c` is type correct since `f a = a` is definitionally equal
-  to the type of `c : b = a`, and the type of `?m a c` is equal to the type of `v`.
-  Note that `fun xs => v` is the term `fun (x1 : Nat) (x2 : b = x1) => v` which has type
-  `(x1 : Nat) -> (x2 : b = x1) -> C[x1, x2]` which is not definitionally equal to the type of `?m`,
-  and may not even be type correct.
-  The issue here is that we are not capturing the `let`-declarations.
+Auxiliary method for solving constraints of the form `?m xs := v`.
+It creates a lambda using `mkLambdaFVars ys v`, where `ys` is a superset of `xs`.
+`ys` is often equal to `xs`. It is a bigger when there are let-declaration dependencies in `xs`.
+For example, suppose we have `xs` of the form `#[a, c]` where
+```
+a : Nat
+b : Nat := f a
+c : b = a
+```
+In this scenario, the type of `?m` is `(x1 : Nat) -> (x2 : f x1 = x1) -> C[x1, x2]`,
+and type of `v` is `C[a, c]`. Note that, `?m a c` is type correct since `f a = a` is definitionally equal
+to the type of `c : b = a`, and the type of `?m a c` is equal to the type of `v`.
+Note that `fun xs => v` is the term `fun (x1 : Nat) (x2 : b = x1) => v` which has type
+`(x1 : Nat) -> (x2 : b = x1) -> C[x1, x2]` which is not definitionally equal to the type of `?m`,
+and may not even be type correct.
+The issue here is that we are not capturing the `let`-declarations.
 
-  This method collects let-declarations `y` occurring between `xs[0]` and `xs.back` s.t.
-  some `x` in `xs` depends on `y`.
-  `ys` is the `xs` with these extra let-declarations included.
+This method collects let-declarations `y` occurring between `xs[0]` and `xs.back` s.t.
+some `x` in `xs` depends on `y`.
+`ys` is the `xs` with these extra let-declarations included.
 
-  In the example above, `ys` is `#[a, b, c]`, and `mkLambdaFVars ys v` produces
-  `fun a => let b := f a; fun (c : b = a) => v` which has a type definitionally equal to the type of `?m`.
+In the example above, `ys` is `#[a, b, c]`, and `mkLambdaFVars ys v` produces
+`fun a => let b := f a; fun (c : b = a) => v` which has a type definitionally equal to the type of `?m`.
 
-  Recall that the method `checkAssignment` ensures `v` does not contain offending `let`-declarations.
+Recall that the method `checkAssignment` ensures `v` does not contain offending `let`-declarations.
 
-  This method assumes that for any `xs[i]` and `xs[j]` where `i < j`, we have that `index of xs[i]` < `index of xs[j]`.
-  where the index is the position in the local context.
+This method assumes that for any `xs[i]` and `xs[j]` where `i < j`, we have that `index of xs[i]` < `index of xs[j]`.
+where the index is the position in the local context.
 -/
 private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : MetaM (Option Expr) := do
   if not (← hasLetDeclsInBetween) then
@@ -447,13 +449,13 @@ where
     let rec visit (e : Expr) : MonadCacheT Expr Unit (ReaderT Nat (StateRefT FVarIdHashSet MetaM)) Unit :=
       checkCache e fun _ => do
         match e with
-        | Expr.forallE _ d b _   => visit d; visit b
-        | Expr.lam _ d b _       => visit d; visit b
-        | Expr.letE _ t v b _    => visit t; visit v; visit b
-        | Expr.app f a           => visit f; visit a
-        | Expr.mdata _ b         => visit b
-        | Expr.proj _ _ b        => visit b
-        | Expr.fvar fvarId       =>
+        | .forallE _ d b _   => visit d; visit b
+        | .lam _ d b _       => visit d; visit b
+        | .letE _ t v b _    => visit t; visit v; visit b
+        | .app f a           => visit f; visit a
+        | .mdata _ b         => visit b
+        | .proj _ _ b        => visit b
+        | .fvar fvarId       =>
           let localDecl ← fvarId.getDecl
           if localDecl.isLet && localDecl.index > (← read) then
             modify fun s => s.insert localDecl.fvarId
@@ -846,18 +848,18 @@ mutual
       return e
     else checkCache e fun _ =>
       match e with
-      | Expr.mdata _ b       => return e.updateMData! (← check b)
-      | Expr.proj _ _ s      => return e.updateProj! (← check s)
-      | Expr.lam _ d b _     => return e.updateLambdaE! (← check d) (← check b)
-      | Expr.forallE _ d b _ => return e.updateForallE! (← check d) (← check b)
-      | Expr.letE _ t v b _  => return e.updateLet! (← check t) (← check v) (← check b)
-      | Expr.bvar ..         => return e
-      | Expr.sort ..         => return e
-      | Expr.const ..        => return e
-      | Expr.lit ..          => return e
-      | Expr.fvar ..         => checkFVar e
-      | Expr.mvar ..         => checkMVar e
-      | Expr.app ..          =>
+      | .mdata _ b       => return e.updateMData! (← check b)
+      | .proj _ _ s      => return e.updateProj! (← check s)
+      | .lam _ d b _     => return e.updateLambdaE! (← check d) (← check b)
+      | .forallE _ d b _ => return e.updateForallE! (← check d) (← check b)
+      | .letE _ t v b _  => return e.updateLet! (← check t) (← check v) (← check b)
+      | .bvar ..         => return e
+      | .sort ..         => return e
+      | .const ..        => return e
+      | .lit ..          => return e
+      | .fvar ..         => checkFVar e
+      | .mvar ..         => checkMVar e
+      | .app ..          =>
         try
           checkApp e
         catch ex => match ex with
@@ -902,24 +904,24 @@ partial def check
     if !e.hasExprMVar && !e.hasFVar then
       true
     else match e with
-    | Expr.mdata _ b       => visit b
-    | Expr.proj _ _ s      => visit s
-    | Expr.app f a         => visit f && visit a
-    | Expr.lam _ d b _     => visit d && visit b
-    | Expr.forallE _ d b _ => visit d && visit b
-    | Expr.letE _ t v b _  => visit t && visit v && visit b
-    | Expr.bvar ..         => true
-    | Expr.sort ..         => true
-    | Expr.const ..        => true
-    | Expr.lit ..          => true
-    | Expr.fvar fvarId ..  =>
+    | .mdata _ b       => visit b
+    | .proj _ _ s      => visit s
+    | .app f a         => visit f && visit a
+    | .lam _ d b _     => visit d && visit b
+    | .forallE _ d b _ => visit d && visit b
+    | .letE _ t v b _  => visit t && visit v && visit b
+    | .bvar ..         => true
+    | .sort ..         => true
+    | .const ..        => true
+    | .lit ..          => true
+    | .fvar fvarId ..  =>
       if mvarDecl.lctx.contains fvarId then true
       else match lctx.find? fvarId with
         | some (LocalDecl.ldecl ..) => false -- need expensive CheckAssignment.check
         | _ =>
           if fvars.any fun x => x.fvarId! == fvarId then true
           else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it
-    | Expr.mvar mvarId'    =>
+    | .mvar mvarId'    =>
       match mctx.getExprAssignmentCore? mvarId' with
       | some _ => false -- use CheckAssignment.check to instantiate
       | none   =>
@@ -1475,8 +1477,8 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
   return some (mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs)
 
 private def isAssignable : Expr → MetaM Bool
-  | Expr.mvar mvarId => do let b ← mvarId.isReadOnlyOrSyntheticOpaque; pure (!b)
-  | _                => pure false
+  | .mvar mvarId => do let b ← mvarId.isReadOnlyOrSyntheticOpaque; pure (!b)
+  | _            => pure false
 
 private def etaEq (t s : Expr) : Bool :=
   match t.etaExpanded? with
@@ -1551,7 +1553,7 @@ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM
 Removes unnecessary let-decls (both true `let`s and `let_fun`s).
 -/
 private partial def consumeLet : Expr → Expr
-  | e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b
+  | e@(.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b
   | e =>
     if let some (_, _, _, b) := e.letFun? then
       if b.hasLooseBVars then e else consumeLet b
@@ -1721,11 +1723,10 @@ private partial def isDefEqQuickMVarMVar (t s : Expr) : MetaM LBool := do
 end
 
 @[inline] def whenUndefDo (x : MetaM LBool) (k : MetaM Bool) : MetaM Bool := do
-  let status ← x
-  match status with
-  | LBool.true  => pure true
-  | LBool.false => pure false
-  | LBool.undef => k
+  match (← x) with
+  | .true  => return true
+  | .false => return false
+  | .undef => k
 
 @[specialize] private def unstuckMVar (e : Expr) (successK : Expr → MetaM Bool) (failK : MetaM Bool): MetaM Bool := do
   match (← getStuckMVar? e) with

src/Lean/Meta/LazyDiscrTree.lean

@@ -745,7 +745,6 @@ instance : Append (PreDiscrTree α) where
 end PreDiscrTree
 
 /-- Initial entry in lazy discrimination tree -/
-@[reducible]
 structure InitEntry (α : Type) where
   /-- Return root key for an entry. -/
   key : Key

src/Lean/Meta/Tactic/Simp.lean

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.Meta.Tactic.Simp.Attr
+import Lean.Meta.Tactic.Simp.Diagnostics
 
 namespace Lean
 

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

@@ -275,7 +275,7 @@ def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step :
       applySimprocConst (mkConst ``True) ``Nat.Simproc.le_add_le #[x, yb, yo, leProof]
     else
       let finExpr := mkLENat (toExpr (xn - yn)) yb
-      let geProof ← mkOfDecideEqTrue (mkGENat yo x)
+      let geProof ← mkOfDecideEqTrue (mkGENat x yo)
       applySimprocConst finExpr ``Nat.Simproc.le_add_ge #[x, yb, yo, geProof]
   | .offset xb xo xn, .offset yb yo yn => do
     if xn ≤ yn then

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

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Diagnostics
+import Lean.Meta.Tactic.Simp.Types
+
+namespace Lean.Meta.Simp
+
+def mkSimpDiagSummary (counters : PHashMap Origin Nat) (usedCounters? : Option (PHashMap Origin Nat) := none) : MetaM DiagSummary := do
+  let threshold := diagnostics.threshold.get (← getOptions)
+  let entries := collectAboveThreshold counters threshold (fun _ => true) (lt := (· < ·))
+  if entries.isEmpty then
+    return {}
+  else
+    let mut data := #[]
+    for (thmId, counter) in entries do
+      let key ← match thmId with
+        | .decl declName _ _ =>
+          if (← getEnv).contains declName then
+            pure m!"{MessageData.ofConst (← mkConstWithLevelParams declName)}"
+          else
+            pure m!"{declName} (builtin simproc)"
+        | .fvar fvarId => pure m!"{mkFVar fvarId}"
+        | _ => pure thmId.key
+      let usedMsg ← if let some usedCounters := usedCounters? then
+        if let some c := usedCounters.find? thmId then pure s!", succeeded: {c}" else pure s!" {crossEmoji}" -- not used
+      else
+        pure ""
+      data := data.push m!"{if data.isEmpty then "  " else "\n"}{key} ↦ {counter}{usedMsg}"
+    return { data, max := entries[0]!.2 }
+
+def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
+  if (← isDiagnosticsEnabled) then
+    let used ← mkSimpDiagSummary diag.usedThmCounter
+    let tried ← mkSimpDiagSummary diag.triedThmCounter diag.usedThmCounter
+    let congr ← mkDiagSummary diag.congrThmCounter
+    unless used.isEmpty && tried.isEmpty && congr.isEmpty do
+      let m := MessageData.nil
+      let m := appendSection m `simp "used theorems" used
+      let m := appendSection m `simp "tried theorems" tried
+      let m := appendSection m `simp "tried congruence theorems" congr
+      let m := m ++ "use `set_option diagnostics.threshold <num>` to control threshold for reporting counters"
+      logInfo m
+
+end Lean.Meta.Simp

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

@@ -8,6 +8,7 @@ import Lean.Meta.Transform
 import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Rewrite
+import Lean.Meta.Tactic.Simp.Diagnostics
 import Lean.Meta.Match.Value
 
 namespace Lean.Meta
@@ -243,28 +244,26 @@ def getSimpLetCase (n : Name) (t : Expr) (b : Expr) : MetaM SimpLetCase := do
 
 /--
 We use `withNewlemmas` whenever updating the local context.
-We use `withFreshCache` because the local context affects `simp` rewrites
-even when `contextual := false`.
-For example, the `discharger` may inspect the current local context. The default
-discharger does that when applying equational theorems, and the user may
-use `(discharger := assumption)` or `(discharger := omega)`.
-If the `wishFreshCache` introduces performance issues, we can design a better solution
-for the default discharger which is used most of the time.
 -/
-def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := withFreshCache do
+def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
   if (← getConfig).contextual then
-    let mut s ← getSimpTheorems
-    let mut updated := false
-    for x in xs do
-      if (← isProof x) then
-        s ← s.addTheorem (.fvar x.fvarId!) x
-        updated := true
-    if updated then
-      withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
-    else
-      f
-  else
+    withFreshCache do
+      let mut s ← getSimpTheorems
+      let mut updated := false
+      for x in xs do
+        if (← isProof x) then
+          s ← s.addTheorem (.fvar x.fvarId!) x
+          updated := true
+      if updated then
+        withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
+      else
+        f
+  else if (← getMethods).wellBehavedDischarge then
+    -- See comment at `Methods.wellBehavedDischarge` to understand why
+    -- we don't have to reset the cache
     f
+  else
+    withFreshCache do f
 
 def simpProj (e : Expr) : SimpM Result := do
   match (← reduceProj? e) with
@@ -519,6 +518,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
 
 /-- Try to rewrite `e` children using the given congruence theorem -/
 def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do
+  recordCongrTheorem c.theoremName
   trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
   let thm ← mkConstWithFreshMVarLevels c.theoremName
   let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)
@@ -652,63 +652,75 @@ where
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
     simpLoop e
 
-@[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
+@[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
 
-def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
-  let ctx := { ctx with config := (← ctx.config.updateArith) }
-  withSimpConfig ctx do withCatchingRuntimeEx do
+def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
+  let ctx := { ctx with config := (← ctx.config.updateArith), lctxInitIndices := (← getLCtx).numIndices }
+  withSimpContext ctx do
+    let (r, s) ← simpMain e methods.toMethodsRef ctx |>.run { stats with }
+    trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
+    return (r, { s with })
+where
+  simpMain (e : Expr) : SimpM Result := withCatchingRuntimeEx do
     try
-      withoutCatchingRuntimeEx do
-        let (r, s) ← simp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
-        trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
-        return (r, s.usedTheorems)
+      withoutCatchingRuntimeEx <| simp e
     catch ex =>
-      if ex.isRuntime then throwNestedTacticEx `simp ex else throw ex
+      reportDiag (← get).diag
+      if ex.isRuntime then
+        throwNestedTacticEx `simp ex
+      else
+        throw ex
 
-def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
-  withSimpConfig ctx do withCatchingRuntimeEx do
+def dsimpMain (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Expr × Stats) := do
+  withSimpContext ctx do
+    let (r, s) ← dsimpMain e methods.toMethodsRef ctx |>.run { stats with }
+    pure (r, { s with })
+where
+  dsimpMain (e : Expr) : SimpM Expr := withCatchingRuntimeEx do
     try
-      withoutCatchingRuntimeEx do
-        let (r, s) ← dsimp e methods.toMethodsRef ctx |>.run { usedTheorems := usedSimps }
-        pure (r, s.usedTheorems)
+      withoutCatchingRuntimeEx <| dsimp e
     catch ex =>
-      if ex.isRuntime then throwNestedTacticEx `dsimp ex else throw ex
+      reportDiag (← get).diag
+      if ex.isRuntime then
+        throwNestedTacticEx `simp ex
+      else
+        throw ex
 
 end Simp
-open Simp (UsedSimps SimprocsArray)
+open Simp (SimprocsArray Stats)
 
 def simp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (usedSimps : UsedSimps := {}) : MetaM (Simp.Result × UsedSimps) := do profileitM Exception "simp" (← getOptions) do
+    (stats : Stats := {}) : MetaM (Simp.Result × Stats) := do profileitM Exception "simp" (← getOptions) do
   match discharge? with
-  | none   => Simp.main e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs)
-  | some d => Simp.main e ctx usedSimps (methods := Simp.mkMethods simprocs d)
+  | none   => Simp.main e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs)
+  | some d => Simp.main e ctx stats (methods := Simp.mkMethods simprocs d (wellBehavedDischarge := false))
 
 def dsimp (e : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Expr × UsedSimps) := do profileitM Exception "dsimp" (← getOptions) do
-  Simp.dsimpMain e ctx usedSimps (methods := Simp.mkDefaultMethodsCore simprocs )
+    (stats : Stats := {}) : MetaM (Expr × Stats) := do profileitM Exception "dsimp" (← getOptions) do
+  Simp.dsimpMain e ctx stats (methods := Simp.mkDefaultMethodsCore simprocs )
 
 /-- See `simpTarget`. This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
   let target ← instantiateMVars (← mvarId.getType)
-  let (r, usedSimps) ← simp target ctx simprocs discharge? usedSimps
+  let (r, stats) ← simp target ctx simprocs discharge? stats
   if mayCloseGoal && r.expr.isTrue then
     match r.proof? with
     | some proof => mvarId.assign (← mkOfEqTrue proof)
     | none => mvarId.assign (mkConst ``True.intro)
-    return (none, usedSimps)
+    return (none, stats)
   else
-    return (← applySimpResultToTarget mvarId target r, usedSimps)
+    return (← applySimpResultToTarget mvarId target r, stats)
 
 /--
   Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
   where `mvarId'` is the simplified new goal. -/
 def simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) :=
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option MVarId × Stats) :=
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
-    simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal usedSimps
+    simpTargetCore mvarId ctx simprocs discharge? mayCloseGoal stats
 
 /--
   Apply the result `r` for `prop` (which is inhabited by `proof`). Return `none` if the goal was closed. Return `some (proof', prop')`
@@ -740,9 +752,9 @@ def applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result
 
   This method assumes `mvarId` is not assigned, and we are already using `mvarId`s local context. -/
 def simpStep (mvarId : MVarId) (proof : Expr) (prop : Expr) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (Expr × Expr) × UsedSimps) := do
-  let (r, usedSimps) ← simp prop ctx simprocs discharge? usedSimps
-  return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), usedSimps)
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (Expr × Expr) × Stats) := do
+  let (r, stats) ← simp prop ctx simprocs discharge? stats
+  return (← applySimpResultToProp mvarId proof prop r (mayCloseGoal := mayCloseGoal), stats)
 
 def applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId)) := do
   match r with
@@ -773,99 +785,99 @@ def applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Res
     applySimpResultToLocalDeclCore mvarId fvarId (← applySimpResultToFVarId mvarId fvarId r mayCloseGoal)
 
 def simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (mayCloseGoal := true) (usedSimps : UsedSimps := {}) : MetaM (Option (FVarId × MVarId) × UsedSimps) := do
+    (mayCloseGoal := true) (stats : Stats := {}) : MetaM (Option (FVarId × MVarId) × Stats) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let type ← instantiateMVars (← fvarId.getType)
-    let (r, usedSimps) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal usedSimps
-    return (← applySimpResultToLocalDeclCore mvarId fvarId r, usedSimps)
+    let (r, stats) ← simpStep mvarId (mkFVar fvarId) type ctx simprocs discharge? mayCloseGoal stats
+    return (← applySimpResultToLocalDeclCore mvarId fvarId r, stats)
 
 def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
+    (stats : Stats := {}) : MetaM (Option (Array FVarId × MVarId) × Stats) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarIdNew := mvarId
     let mut toAssert := #[]
     let mut replaced := #[]
-    let mut usedSimps := usedSimps
+    let mut stats := stats
     for fvarId in fvarIdsToSimp do
       let localDecl ← fvarId.getDecl
       let type ← instantiateMVars localDecl.type
       let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) }
-      let (r, usedSimps') ← simp type ctx simprocs discharge? usedSimps
-      usedSimps := usedSimps'
+      let (r, stats') ← simp type ctx simprocs discharge? stats
+      stats := stats'
       match r.proof? with
       | some _ => match (← applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with
-        | none => return (none, usedSimps)
+        | none => return (none, stats)
         | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
       | none =>
         if r.expr.isFalse then
           mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
-          return (none, usedSimps)
+          return (none, stats)
         -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
         -- Reason: it introduces a `mkExpectedTypeHint`
         mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId r.expr
         replaced := replaced.push fvarId
     if simplifyTarget then
-      match (← simpTarget mvarIdNew ctx simprocs discharge? (usedSimps := usedSimps)) with
-      | (none, usedSimps') => return (none, usedSimps')
-      | (some mvarIdNew', usedSimps') => mvarIdNew := mvarIdNew'; usedSimps := usedSimps'
+      match (← simpTarget mvarIdNew ctx simprocs discharge? (stats := stats)) with
+      | (none, stats') => return (none, stats')
+      | (some mvarIdNew', stats') => mvarIdNew := mvarIdNew'; stats := stats'
     let (fvarIdsNew, mvarIdNew') ← mvarIdNew.assertHypotheses toAssert
     mvarIdNew := mvarIdNew'
     let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
     mvarIdNew ← mvarIdNew.tryClearMany toClear
     if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
       throwError "simp made no progress"
-    return (some (fvarIdsNew, mvarIdNew), usedSimps)
+    return (some (fvarIdsNew, mvarIdNew), stats)
 
 def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none)
-    (usedSimps : UsedSimps := {}) : MetaM (TacticResultCNM × UsedSimps) := mvarId.withContext do
+    (stats : Stats := {}) : MetaM (TacticResultCNM × Stats) := mvarId.withContext do
   let mut ctx := ctx
   for h in (← getPropHyps) do
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
     let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
     ctx := { ctx with simpTheorems }
-  match (← simpTarget mvarId ctx simprocs discharge? (usedSimps := usedSimps)) with
-  | (none, usedSimps) => return (TacticResultCNM.closed, usedSimps)
-  | (some mvarId', usedSimps') =>
+  match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
+  | (none, stats) => return (TacticResultCNM.closed, stats)
+  | (some mvarId', stats') =>
     if (← mvarId.getType) == (← mvarId'.getType) then
-      return (TacticResultCNM.noChange, usedSimps)
+      return (TacticResultCNM.noChange, stats)
     else
-      return (TacticResultCNM.modified mvarId', usedSimps')
+      return (TacticResultCNM.modified mvarId', stats')
 
 def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
-    (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+    (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
    mvarId.withContext do
     mvarId.checkNotAssigned `simp
     let mut mvarIdNew := mvarId
-    let mut usedSimps : UsedSimps := usedSimps
+    let mut stats : Stats := stats
     for fvarId in fvarIdsToSimp do
       let type ← instantiateMVars (← fvarId.getType)
-      let (typeNew, usedSimps') ← dsimp type ctx simprocs
-      usedSimps := usedSimps'
+      let (typeNew, stats') ← dsimp type ctx simprocs
+      stats := stats'
       if typeNew.isFalse then
         mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
-        return (none, usedSimps)
+        return (none, stats)
       if typeNew != type then
         mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId typeNew
     if simplifyTarget then
       let target ← mvarIdNew.getType
-      let (targetNew, usedSimps') ← dsimp target ctx simprocs usedSimps
-      usedSimps := usedSimps'
+      let (targetNew, stats') ← dsimp target ctx simprocs stats
+      stats := stats'
       if targetNew.isTrue then
         mvarIdNew.assign (mkConst ``True.intro)
-        return (none, usedSimps)
+        return (none, stats)
       if let some (_, lhs, rhs) := targetNew.consumeMData.eq? then
         if (← withReducible <| isDefEq lhs rhs) then
           mvarIdNew.assign (← mkEqRefl lhs)
-          return (none, usedSimps)
+          return (none, stats)
       if target != targetNew then
         mvarIdNew ← mvarIdNew.replaceTargetDefEq targetNew
       pure () -- FIXME: bug in do notation if this is removed?
     if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
       throwError "dsimp made no progress"
-    return (some mvarIdNew, usedSimps)
+    return (some mvarIdNew, stats)
 
 end Lean.Meta

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

@@ -109,6 +109,7 @@ where
       return false
 
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
+  recordTriedSimpTheorem thm.origin
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
       unless (← synthesizeArgs thm.origin bis xs) do
@@ -406,6 +407,7 @@ def mkSEvalMethods : CoreM Methods := do
     dpre       := dpreDefault #[s]
     dpost      := dpostDefault #[s]
     discharge? := dischargeGround
+    wellBehavedDischarge := true
   }
 
 def mkSEvalContext : CoreM Context := do
@@ -493,10 +495,16 @@ where
     | .forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && go b
     | _ => e.isFalse
 
-def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
+private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
+  let lctxInitIndices := (← readThe Simp.Context).lctxInitIndices
+  let contextual := (← getConfig).contextual
   (← getLCtx).findDeclRevM? fun localDecl => do
     if localDecl.isImplementationDetail then
       return none
+    -- The following test is needed to ensure `dischargeUsingAssumption?` is a
+    -- well-behaved discharger. See comment at `Methods.wellBehavedDischarge`
+    else if !contextual && localDecl.index >= lctxInitIndices then
+      return none
     else if (← isDefEq e localDecl.type) then
       return some localDecl.toExpr
     else
@@ -545,16 +553,17 @@ def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
 
 abbrev Discharge := Expr → SimpM (Option Expr)
 
-def mkMethods (s : SimprocsArray) (discharge? : Discharge) : Methods := {
+def mkMethods (s : SimprocsArray) (discharge? : Discharge) (wellBehavedDischarge : Bool) : Methods := {
   pre        := preDefault s
   post       := postDefault s
   dpre       := dpreDefault s
   dpost      := dpostDefault s
-  discharge? := discharge?
+  discharge?
+  wellBehavedDischarge
 }
 
 def mkDefaultMethodsCore (simprocs : SimprocsArray) : Methods :=
-  mkMethods simprocs dischargeDefault?
+  mkMethods simprocs dischargeDefault? (wellBehavedDischarge := true)
 
 def mkDefaultMethods : CoreM Methods := do
   if simprocs.get (← getOptions) then

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

@@ -10,7 +10,7 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-open Simp (UsedSimps SimprocsArray)
+open Simp (Stats SimprocsArray)
 
 namespace SimpAll
 
@@ -24,12 +24,13 @@ structure Entry where
   deriving Inhabited
 
 structure State where
-  modified  : Bool := false
-  mvarId    : MVarId
-  entries   : Array Entry := #[]
-  ctx       : Simp.Context
-  simprocs  : SimprocsArray
-  usedSimps : UsedSimps := {}
+  modified     : Bool := false
+  mvarId       : MVarId
+  entries      : Array Entry := #[]
+  ctx          : Simp.Context
+  simprocs     : SimprocsArray
+  usedTheorems : Simp.UsedSimps := {}
+  diag         : Simp.Diagnostics := {}
 
 abbrev M := StateRefT State MetaM
 
@@ -62,8 +63,8 @@ private partial def loop : M Bool := do
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
     let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
-    let (r, usedSimps) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (usedSimps := (← get).usedSimps)
-    modify fun s => { s with usedSimps }
+    let (r, stats) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (stats := { (← get) with })
+    modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
     match r with
     | none => return true -- closed the goal
     | some (proofNew, typeNew) =>
@@ -102,8 +103,8 @@ private partial def loop : M Bool := do
         }
   -- simplify target
   let mvarId := (← get).mvarId
-  let (r, usedSimps) ← simpTarget mvarId (← get).ctx simprocs (usedSimps := (← get).usedSimps)
-  modify fun s => { s with usedSimps }
+  let (r, stats) ← simpTarget mvarId (← get).ctx simprocs (stats := { (← get) with })
+  modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
   match r with
   | none => return true
   | some mvarIdNew =>
@@ -143,12 +144,12 @@ def main : M (Option MVarId) := do
 
 end SimpAll
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
+def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray := #[]) (stats : Stats := {}) : MetaM (Option MVarId × Stats) := do
   mvarId.withContext do
-    let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps, simprocs }
+    let (r, s) ← SimpAll.main.run { stats with mvarId, ctx, simprocs }
     if let .some mvarIdNew := r then
       if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
         throwError "simp_all made no progress"
-    return (r, s.usedSimps)
+    return (r, { s with })
 
 end Lean.Meta

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

@@ -50,6 +50,9 @@ def Origin.key : Origin → Name
 
 instance : BEq Origin := ⟨(·.key == ·.key)⟩
 instance : Hashable Origin := ⟨(hash ·.key)⟩
+instance : LT Origin := ⟨(·.key.lt ·.key)⟩
+instance (a b : Origin) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (a.key.lt b.key = true))
 
 /-
 Note: we want to use iota reduction when indexing instances. Otherwise,

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

@@ -90,6 +90,12 @@ structure Context where
   -/
   parent?           : Option Expr := none
   dischargeDepth    : UInt32 := 0
+  /--
+  Number of indices in the local context when starting `simp`.
+  We use this information to decide which assumptions we can use without
+  invalidating the cache.
+  -/
+  lctxInitIndices   : Nat := 0
   deriving Inhabited
 
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
@@ -98,11 +104,25 @@ def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
 -- We should use `PHashMap` because we backtrack the contents of `UsedSimps`
 abbrev UsedSimps := PHashMap Origin Nat
 
+structure Diagnostics where
+  /-- Number of times each simp theorem has been used/applied. -/
+  usedThmCounter : PHashMap Origin Nat := {}
+  /-- Number of times each simp theorem has been tried. -/
+  triedThmCounter : PHashMap Origin Nat := {}
+  /-- Number of times each congr theorem has been tried. -/
+  congrThmCounter : PHashMap Name Nat := {}
+  deriving Inhabited
+
 structure State where
   cache        : Cache := {}
   congrCache   : CongrCache := {}
   usedTheorems : UsedSimps := {}
   numSteps     : Nat := 0
+  diag         : Diagnostics := {}
+
+structure Stats where
+  usedTheorems : UsedSimps := {}
+  diag : Diagnostics := {}
 
 private opaque MethodsRefPointed : NonemptyType.{0}
 
@@ -118,6 +138,10 @@ opaque simp (e : Expr) : SimpM Result
 @[extern "lean_dsimp"]
 opaque dsimp (e : Expr) : SimpM Expr
 
+@[inline] def modifyDiag (f : Diagnostics → Diagnostics) : SimpM Unit := do
+  if (← isDiagnosticsEnabled) then
+    modify fun { cache, congrCache, usedTheorems, numSteps, diag } => { cache, congrCache, usedTheorems, numSteps, diag := f diag }
+
 /--
 Result type for a simplification procedure. We have `pre` and `post` simplication procedures.
 -/
@@ -230,11 +254,18 @@ structure Simprocs where
   deriving Inhabited
 
 structure Methods where
-  pre        : Simproc                    := fun _ => return .continue
-  post       : Simproc                    := fun e => return .done { expr := e }
-  dpre       : DSimproc                   := fun _ => return .continue
-  dpost      : DSimproc                   := fun e => return .done e
+  pre        : Simproc  := fun _ => return .continue
+  post       : Simproc  := fun e => return .done { expr := e }
+  dpre       : DSimproc := fun _ => return .continue
+  dpost      : DSimproc := fun e => return .done e
   discharge? : Expr → SimpM (Option Expr) := fun _ => return none
+  /--
+  `wellBehavedDischarge` must **not** be set to `true` IF `discharge?`
+  access local declarations with index >= `Context.lctxInitIndices` when
+  `contextual := false`.
+  Reason: it would prevent us from aggressively caching `simp` results.
+  -/
+  wellBehavedDischarge : Bool := true
   deriving Inhabited
 
 unsafe def Methods.toMethodsRefImpl (m : Methods) : MethodsRef :=
@@ -288,10 +319,19 @@ Save current cache, reset it, execute `x`, and then restore original cache.
   modify fun s => { s with cache := {} }
   try x finally modify fun s => { s with cache := cacheSaved }
 
-@[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
-  withFreshCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
+@[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (wellBehavedDischarge : Bool) (x : SimpM α) : SimpM α :=
+  withFreshCache <|
+  withReader (fun r => { MethodsRef.toMethods r with discharge?, wellBehavedDischarge }.toMethodsRef) x
+
+def recordTriedSimpTheorem (thmId : Origin) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
+    let cNew := if let some c := triedThmCounter.find? thmId then c + 1 else 1
+    { usedThmCounter, triedThmCounter := triedThmCounter.insert thmId cNew, congrThmCounter }
 
 def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
+    let cNew := if let some c := usedThmCounter.find? thmId then c + 1 else 1
+    { usedThmCounter := usedThmCounter.insert thmId cNew, triedThmCounter, congrThmCounter }
   /-
   If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
   See issue #3547.
@@ -311,6 +351,11 @@ def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
     let n := s.usedTheorems.size
     { s with usedTheorems := s.usedTheorems.insert thmId n }
 
+def recordCongrTheorem (declName : Name) : SimpM Unit := do
+  modifyDiag fun { usedThmCounter, triedThmCounter, congrThmCounter } =>
+    let cNew := if let some c := congrThmCounter.find? declName then c + 1 else 1
+    { congrThmCounter := congrThmCounter.insert declName cNew, triedThmCounter, usedThmCounter }
+
 def Result.getProof (r : Result) : MetaM Expr := do
   match r.proof? with
   | some p => return p

src/Lean/Parser/Term.lean

@@ -807,6 +807,10 @@ It is especially useful for avoiding parentheses with repeated applications.
 Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.
 You can also view `h ▸ e` as a "type casting" operation
 where you change the type of `e` by using `h`.
+
+The macro tries both orientations of `h`. If the context provides an
+expected type, it rewrites the expeced type, else it rewrites the type of e`.
+
 See the Chapter "Quantifiers and Equality" in the manual
 "Theorem Proving in Lean" for additional information.
 -/

src/Lean/PrettyPrinter.lean

@@ -51,9 +51,9 @@ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (d
 
 @[export lean_pp_expr]
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
-  Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO {
-    options := opts, fileName := "<PrettyPrinter>", fileMap := default, diag := getDiag opts
-  } { env := env }
+  Prod.fst <$> ((withOptions (fun _ => opts) <| ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO
+    { fileName := "<PrettyPrinter>", fileMap := default }
+    { env := env }
 
 def ppTactic (stx : TSyntax `tactic) : CoreM Format := ppCategory `tactic stx
 

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -529,64 +529,57 @@ def withOverApp (arity : Nat) (x : Delab) : Delab := do
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where
   info        : MatcherInfo
-  matcherTy   : Expr
-  params      : Array Expr := #[]
+  /-- The `matcherTy` instantiated with universe levels and the matcher parameters, with a position at the type of
+  this application prefix. -/
+  matcherTy : SubExpr
+  /-- The motive, with the pi type version delaborated and the original expression version.
+  Once `AppMatchState` is complete, this is not `none`. -/
   motive      : Option (Term × Expr) := none
+  /-- Whether `pp.analysis.namedArg` was set for the motive argument. -/
   motiveNamed : Bool := false
+  /-- The delaborated discriminants, without `h :` annotations. -/
   discrs      : Array Term := #[]
+  /-- The collection of names used for the `h :` discriminant annotations, in order.
+  Uniquified names are constructed after the first phase. -/
+  hNames?     : Array (Option Name) := #[]
+  /-- Lambda subexpressions for each alternate. -/
+  alts        : Array SubExpr := #[]
+  /-- For each match alternative, the names to use for the pattern variables.
+  Each ends with `hNames?.filterMap id` exactly. -/
   varNames    : Array (Array Name) := #[]
+  /-- The delaborated right-hand sides for each match alternative. -/
   rhss        : Array Term := #[]
-  -- additional arguments applied to the result of the `match` expression
-  moreArgs    : Array Term := #[]
-/--
-  Extract arguments of motive applications from the matcher type.
-  For the example below: `#[#[`([])], #[`(a::as)]]` -/
-private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array Term)) :=
-  withReader (fun ctx => { ctx with inPattern := true, optionsPerPos := {} }) do
-    let ty ← instantiateForall st.matcherTy st.params
-    -- need to reduce `let`s that are lifted into the matcher type
-    forallTelescopeReducing ty fun params _ => do
-      -- skip motive and discriminators
-      let alts := Array.ofSubarray params[1 + st.discrs.size:]
-      alts.mapIdxM fun idx alt => do
-        let ty ← inferType alt
-        -- TODO: this is a hack; we are accessing the expression out-of-sync with the position
-        -- Currently, we reset `optionsPerPos` at the beginning of `delabPatterns` to avoid
-        -- incorrectly considering annotations.
-        withTheReader SubExpr ({ · with expr := ty }) $
-          usingNames st.varNames[idx]! do
-            withAppFnArgs (pure #[]) (fun pats => do pure $ pats.push (← delab))
-where
-  usingNames {α} (varNames : Array Name) (x : DelabM α) : DelabM α :=
-    usingNamesAux 0 varNames x
-  usingNamesAux {α} (i : Nat) (varNames : Array Name) (x : DelabM α) : DelabM α :=
-    if i < varNames.size then
-      withBindingBody varNames[i]! <| usingNamesAux (i+1) varNames x
-    else
-      x
 
-/-- Skip `numParams` binders, and execute `x varNames` where `varNames` contains the new binder names. -/
-private partial def skippingBinders {α} (numParams : Nat) (x : Array Name → DelabM α) : DelabM α :=
-  loop numParams #[]
+/--
+Skips `numParams` binders, and execute `x varNames` where `varNames` contains the new binder names.
+The `hNames` array is used for the last params.
+Helper for `delabAppMatch`.
+-/
+private partial def skippingBinders {α} (numParams : Nat) (hNames : Array Name) (x : Array Name → DelabM α) : DelabM α := do
+  loop 0 #[]
 where
-  loop : Nat → Array Name → DelabM α
-    | 0,   varNames => x varNames
-    | n+1, varNames => do
-      let rec visitLambda : DelabM α := do
-        let varName := (← getExpr).bindingName!.eraseMacroScopes
-        -- Pattern variables cannot shadow each other
-        if varNames.contains varName then
-          let varName := (← getLCtx).getUnusedName varName
-          withBindingBody varName do
-            loop n (varNames.push varName)
-        else
-          withBindingBodyUnusedName fun id => do
-            loop n (varNames.push id.getId)
+  loop (i : Nat) (varNames : Array Name) : DelabM α := do
+    let rec visitLambda : DelabM α := do
+      let varName := (← getExpr).bindingName!.eraseMacroScopes
+      if numParams - hNames.size ≤ i then
+        -- It is an "h annotation", so use the one we have already chosen.
+        let varName := hNames[i + hNames.size - numParams]!
+        withBindingBody varName do
+          loop (i + 1) (varNames.push varName)
+      else if varNames.contains varName then
+        -- Pattern variables must not shadow each other, so ensure a unique name
+        let varName := (← getLCtx).getUnusedName varName
+        withBindingBody varName do
+          loop (i + 1) (varNames.push varName)
+      else
+        withBindingBodyUnusedName fun id => do
+          loop (i + 1) (varNames.push id.getId)
+    if i < numParams then
       let e ← getExpr
       if e.isLambda then
         visitLambda
       else
-        -- eta expand `e`
+        -- Eta expand `e`
         let e ← forallTelescopeReducing (← inferType e) fun xs _ => do
           if xs.size == 1 && (← inferType xs[0]!).isConstOf ``Unit then
             -- `e` might be a thunk create by the dependent pattern matching compiler, and `xs[0]` may not even be a pattern variable.
@@ -597,75 +590,117 @@ where
           else
             mkLambdaFVars xs (mkAppN e xs)
         withTheReader SubExpr (fun ctx => { ctx with expr := e }) visitLambda
+    else x varNames
 
 /--
-  Delaborate applications of "matchers" such as
-  ```
-  List.map.match_1 : {α : Type _} →
-    (motive : List α → Sort _) →
-      (x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-  ```
+Delaborates applications of "matchers" such as
+```
+List.map.match_1 : {α : Type _} →
+  (motive : List α → Sort _) →
+    (x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
+```
 -/
 @[builtin_delab app]
-def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMatch do
-  -- incrementally fill `AppMatchState` from arguments
-  let st ← withAppFnArgs
-    (do
-      let (Expr.const c us) ← getExpr | failure
-      let (some info) ← getMatcherInfo? c | failure
-      let matcherTy ← instantiateTypeLevelParams (← getConstInfo c) us
-      return { matcherTy, info : AppMatchState })
-    (fun st => do
-      if st.params.size < st.info.numParams then
-        return { st with params := st.params.push (← getExpr) }
-      else if st.motive.isNone then
-        -- store motive argument separately
-        let lamMotive ← getExpr
-        let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
-        -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
-        -- Thus the binder types won't have any annotations
-        let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
-        let named ← getPPOption getPPAnalysisNamedArg
-        return { st with motive := (piStx, lamMotive), motiveNamed := named }
-      else if st.discrs.size < st.info.numDiscrs then
-        let idx := st.discrs.size
-        let discr ← delab
-        if let some hName := st.info.discrInfos[idx]!.hName? then
-          -- TODO: we should check whether the corresponding binder name, matches `hName`.
-          -- If it does not we should pretty print this `match` as a regular application.
-          return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName) : $discr)) }
+partial def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMatch do
+  -- Check that this is a matcher, and then set up overapplication.
+  let Expr.const c us := (← getExpr).getAppFn | failure
+  let some info ← getMatcherInfo? c | failure
+  withOverApp info.arity do
+    -- First pass visiting the match application. Incrementally fills `AppMatchState`,
+    -- collecting information needed to delaborate the patterns and RHSs.
+    -- No need to visit the parameters themselves.
+    let st : AppMatchState ← withBoundedAppFnArgs (1 + info.numDiscrs + info.numAlts)
+      (do
+        let params := (← getExpr).getAppArgs
+        let matcherTy : SubExpr :=
+          { expr := ← instantiateForall (← instantiateTypeLevelParams (← getConstInfo c) us) params
+            pos := (← getPos).pushType }
+        guard <| ← isDefEq matcherTy.expr (← inferType (← getExpr))
+        return { info, matcherTy })
+      (fun st => do
+        if st.motive.isNone then
+          -- A motive for match notation is a type, so need to delaborate the lambda motive as a pi type.
+          let lamMotive ← getExpr
+          let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body
+          -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive`
+          -- Thus the binder types won't have any annotations.
+          -- Though, by using the same position we can use the body annotations
+          let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab
+          let named ← getPPOption getPPAnalysisNamedArg
+          return { st with motive := (piStx, lamMotive), motiveNamed := named }
+        else if st.discrs.size < st.info.numDiscrs then
+          return { st with discrs := st.discrs.push (← delab) }
+        else if st.alts.size < st.info.numAlts then
+          return { st with alts := st.alts.push (← readThe SubExpr) }
         else
-          return { st with discrs := st.discrs.push (← `(matchDiscr| $discr:term)) }
-      else if st.rhss.size < st.info.altNumParams.size then
-        /- We save the variables names here to be able to implement safe_shadowing.
-           The pattern delaboration must use the names saved here. -/
-        let (varNames, rhs) ← skippingBinders st.info.altNumParams[st.rhss.size]! fun varNames => do
-          let rhs ← delab
-          return (varNames, rhs)
-        return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
-      else
-        return { st with moreArgs := st.moreArgs.push (← delab) })
+          panic! "impossible, number of arguments does not match arity")
 
-  if st.discrs.size < st.info.numDiscrs || st.rhss.size < st.info.altNumParams.size then
-    -- underapplied
-    failure
+    -- Second pass, create names for the h parameters, come up with pattern variable names,
+    -- and delaborate the RHSs.
+    -- We need to create dummy variables for the `h :` annotation variables first because they
+    -- come *last* in each alternative.
+    let st ← withDummyBinders (st.info.discrInfos.map (·.hName?)) (← getExpr) fun hNames? => do
+      let hNames := hNames?.filterMap id
+      let mut st := {st with hNames? := hNames?}
+      for i in [0:st.alts.size] do
+        st ← withTheReader SubExpr (fun _ => st.alts[i]!) do
+          -- We save the variables names here to be able to implement safe shadowing.
+          -- The pattern delaboration must use the names saved here.
+          skippingBinders st.info.altNumParams[i]! hNames fun varNames => do
+            let rhs ← delab
+            return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames }
+      return st
 
-  match st.discrs, st.rhss with
-  | #[discr], #[] =>
-    let stx ← `(nomatch $discr)
-    return Syntax.mkApp stx st.moreArgs
-  | _,        #[] => failure
-  | _,        _   =>
-    let pats ← delabPatterns st
-    let stx ← do
+    if st.rhss.isEmpty then
+      `(nomatch $(st.discrs),*)
+    else
+      -- Third pass, delaborate patterns.
+      -- Extracts arguments of motive applications from the matcher type.
+      -- For the example in the docstring, yields `#[#[([])], #[(a::as)]]`.
+      let pats ← withReader (fun ctx => { ctx with inPattern := true, subExpr := st.matcherTy }) do
+        -- Need to reduce since there can be `let`s that are lifted into the matcher type
+        forallTelescopeReducing (← getExpr) fun afterParams _ => do
+          -- Skip motive and discriminators
+          let alts := Array.ofSubarray afterParams[1 + st.discrs.size:]
+          -- Visit minor premises
+          alts.mapIdxM fun idx alt => do
+            let altTy ← inferType alt
+            withTheReader SubExpr (fun ctx =>
+                { ctx with expr := altTy, pos := ctx.pos.pushNthBindingDomain (1 + st.discrs.size + idx) }) do
+              usingNames st.varNames[idx]! <|
+                withAppFnArgs (pure #[]) fun pats => return pats.push (← delab)
+      -- Finally, assemble
+      let discrs ← (st.hNames?.zip st.discrs).mapM fun (hName?, discr) =>
+        match hName? with
+        | none => `(matchDiscr| $discr:term)
+        | some hName => `(matchDiscr| $(mkIdent hName) : $discr)
       let (piStx, lamMotive) := st.motive.get!
       let opts ← getOptions
       -- TODO: disable the match if other implicits are needed?
       if ← pure st.motiveNamed <||> shouldShowMotive lamMotive opts then
-        `(match (motive := $piStx) $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
+        `(match (motive := $piStx) $[$discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
       else
-        `(match $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
-    return Syntax.mkApp stx st.moreArgs
+        `(match $[$discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
+where
+  /-- Adds hNames to the local context to reserve their names and runs `m` in that context. -/
+  withDummyBinders {α : Type} (hNames? : Array (Option Name)) (body : Expr)
+      (m : Array (Option Name) → DelabM α) (acc : Array (Option Name) := #[]) : DelabM α := do
+    let i := acc.size
+    if i < hNames?.size then
+      if let some name := hNames?[i]! then
+        let n' ← getUnusedName name body
+        withLocalDecl n' .default (.sort levelZero) (kind := .implDetail) fun _ =>
+          withDummyBinders hNames? body m (acc.push n')
+      else
+        withDummyBinders hNames? body m (acc.push none)
+    else
+      m acc
+
+  usingNames {α} (varNames : Array Name) (x : DelabM α) (i : Nat := 0) : DelabM α :=
+    if i < varNames.size then
+      withBindingBody varNames[i]! <| usingNames varNames x (i+1)
+    else
+      x
 
 /--
 Delaborates applications of the form `letFun v (fun x => b)` as `let_fun x := v; b`.

src/Lean/ReducibilityAttrs.lean

@@ -16,6 +16,11 @@ inductive ReducibilityStatus where
   | reducible | semireducible | irreducible
   deriving Inhabited, Repr, BEq
 
+def ReducibilityStatus.toAttrString : ReducibilityStatus → String
+  | .reducible => "[reducible]"
+  | .irreducible => "[irreducible]"
+  | .semireducible => "[semireducible]"
+
 builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
   registerPersistentEnvExtension {
     name            := `reducibilityCore
@@ -48,7 +53,7 @@ def getReducibilityStatusCore (env : Environment) (declName : Name) : Reducibili
     | none => .semireducible
   | none => (reducibilityCoreExt.getState env).find? declName |>.getD .semireducible
 
-def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
+private def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment :=
   if attrKind matches .global then
     match env.getModuleIdxFor? declName with
     | some _ =>
@@ -65,15 +70,75 @@ def setReducibilityStatusCore (env : Environment) (declName : Name) (status : Re
 private def setReducibilityStatusImp (env : Environment) (declName : Name) (status : ReducibilityStatus) : Environment :=
   setReducibilityStatusCore env declName status .global .anonymous
 
+/-
+TODO: it would be great if we could distinguish between the following two situations
+
+1-
+```
+@[reducible] def foo := ...
+```
+
+2-
+```
+def foo := ...
+...
+attribute [reducible] foo
+```
+
+Reason: the second one is problematic if user has add simp theorems or TC instances that include `foo`.
+Recall that the discrimination trees unfold `[reducible]` declarations while indexing new entries.
+-/
+
+register_builtin_option allowUnsafeReducibility : Bool := {
+  defValue := false
+  descr    := "enables users to modify the reducibility settings for declarations even when such changes are deemed potentially hazardous. For example, `simp` and type class resolution maintain term indices where reducible declarations are expanded."
+}
+
+private def validate (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) : CoreM Unit := do
+  let suffix := "use `set_option allowUnsafeReducibility true` to override reducibility status validation"
+  unless allowUnsafeReducibility.get (← getOptions) do
+    match (← getConstInfo declName) with
+    | .defnInfo _ =>
+      let statusOld := getReducibilityStatusCore (← getEnv) declName
+      match attrKind with
+      | .scoped =>
+        throwError "failed to set reducibility status for `{declName}`, the `scoped` modifier is not recommended for this kind of attribute\n{suffix}"
+      | .global =>
+        if (← getEnv).getModuleIdxFor? declName matches some _ then
+          throwError "failed to set reducibility status, `{declName}` has not been defined in this file, consider using the `local` modifier\n{suffix}"
+        match status with
+        | .reducible =>
+          unless statusOld matches .semireducible do
+            throwError "failed to set `[reducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}"
+        | .irreducible =>
+          unless statusOld matches .semireducible do
+            throwError "failed to set `[irreducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}"
+        | .semireducible =>
+          throwError "failed to set `[semireducible]` for `{declName}`, declarations are `[semireducible]` by default\n{suffix}"
+      | .local =>
+        match status with
+        | .reducible =>
+          throwError "failed to set `[local reducible]` for `{declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution\n{suffix}"
+        | .irreducible =>
+          unless statusOld matches .semireducible do
+            throwError "failed to set `[local irreducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected\n{suffix}"
+        | .semireducible =>
+          unless statusOld matches .irreducible do
+            throwError "failed to set `[local semireducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected\n{suffix}"
+    | _ => throwError "failed to set reducibility status, `{declName}` is not a definition\n{suffix}"
+
+private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
+  Attribute.Builtin.ensureNoArgs stx
+  validate declName status attrKind
+  let ns ← getCurrNamespace
+  modifyEnv fun env => setReducibilityStatusCore env declName status attrKind ns
+
 builtin_initialize
   registerBuiltinAttribute {
     ref             := by exact decl_name%
     name            := `irreducible
     descr           := "irreducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .irreducible attrKind ns
+    add             := addAttr .irreducible
     applicationTime := .afterTypeChecking
  }
 
@@ -82,10 +147,7 @@ builtin_initialize
     ref             := by exact decl_name%
     name            := `reducible
     descr           := "reducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
+    add             := addAttr .reducible
     applicationTime := .afterTypeChecking
  }
 
@@ -94,10 +156,7 @@ builtin_initialize
     ref             := by exact decl_name%
     name            := `semireducible
     descr           := "semireducible declaration"
-    add             := fun declName stx attrKind => do
-      Attribute.Builtin.ensureNoArgs stx
-      let ns ← getCurrNamespace
-      modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns
+    add             := addAttr .semireducible
     applicationTime := .afterTypeChecking
  }
 

src/Lean/Replay.lean

@@ -50,7 +50,7 @@ def isTodo (name : Name) : M Bool := do
 
 /-- Use the current `Environment` to throw a `KernelException`. -/
 def throwKernelException (ex : KernelException) : M Unit := do
-    let ctx := { fileName := "", options := ({} : KVMap), fileMap := default, diag := false }
+    let ctx := { fileName := "", options := ({} : KVMap), fileMap := default }
     let state := { env := (← get).env }
     Prod.fst <$> (Lean.Core.CoreM.toIO · ctx state) do Lean.throwKernelException ex
 

src/Lean/SubExpr.lean

@@ -98,6 +98,7 @@ def pushLetBody       (p : Pos) := p.push 2
 def pushAppFn         (p : Pos) := p.push 0
 def pushAppArg        (p : Pos) := p.push 1
 def pushProj          (p : Pos) := p.push 0
+def pushType          (p : Pos) := p.push Pos.typeCoord
 
 def pushNaryFn (numArgs : Nat) (p : Pos) : Pos :=
   p.asNat * (maxChildren ^ numArgs)

src/Lean/ToExpr.lean

@@ -172,6 +172,12 @@ instance : ToExpr FVarId where
   toTypeExpr    := mkConst ``FVarId
   toExpr fvarId := mkApp (mkConst ``FVarId.mk) (toExpr fvarId.name)
 
+instance : ToExpr Syntax.Preresolved where
+  toTypeExpr := .const ``Syntax.Preresolved []
+  toExpr
+    | .namespace ns => mkApp (.const ``Syntax.Preresolved.namespace []) (toExpr ns)
+    | .decl a ls => mkApp2 (.const ``Syntax.Preresolved.decl []) (toExpr a) (toExpr ls)
+
 def Expr.toCtorIfLit : Expr → Expr
   | .lit (.natVal v) =>
     if v == 0 then mkConst ``Nat.zero

src/Lean/Util/Trace.lean

@@ -148,22 +148,27 @@ private def addTraceNode (oldTraces : PersistentArray TraceElem)
   modifyTraces fun _ =>
     oldTraces.push { ref, msg }
 
-def withStartStopSeconds [Monad m] [MonadLiftT BaseIO m] (act : m α) : m (α × Float × Float) := do
-  let start ← IO.monoNanosNow
-  let a ← act
-  let stop ← IO.monoNanosNow
-  return (a, start.toFloat / 1000000000, stop.toFloat / 1000000000)
-
 register_builtin_option trace.profiler : Bool := {
   defValue := false
   group    := "profiler"
-  descr    := "activate nested traces with execution time over threshold"
+  descr    :=
+    "activate nested traces with execution time above `trace.profiler.threshold` and annotate with \
+    time"
 }
 
 register_builtin_option trace.profiler.threshold : Nat := {
   defValue := 10
   group    := "profiler"
-  descr    := "threshold in milliseconds, traces below threshold will not be activated"
+  descr    :=
+    "threshold in milliseconds (or heartbeats if `trace.profiler.useHeartbeats` is true), \
+    traces below threshold will not be activated"
+}
+
+register_builtin_option trace.profiler.useHearbeats : Bool := {
+  defValue := false
+  group    := "profiler"
+  descr    :=
+    "if true, measure and report heartbeats instead of seconds"
 }
 
 register_builtin_option trace.profiler.output : String := {
@@ -177,20 +182,31 @@ register_builtin_option trace.profiler.output.pp : Bool := {
   defValue := false
   group    := "profiler"
   descr    :=
-    "if false, limit text in exported trace nodes to trace class name and `TraceData.tag`, if any"
+    "if false, limit text in exported trace nodes to trace class name and `TraceData.tag`, if any
+
+This is useful when we are interested in the time taken by specific subsystems instead of specific \
+invocations, which is the common case."
 }
 
-def trace.profiler.threshold.getSecs (o : Options) : Float :=
-  (trace.profiler.threshold.get o).toFloat / 1000
+@[inline] private def withStartStop [Monad m] [MonadLiftT BaseIO m] (opts : Options) (act : m α) :
+    m (α × Float × Float) := do
+  if trace.profiler.useHearbeats.get opts then
+    let start ← IO.getNumHeartbeats
+    let a ← act
+    let stop ← IO.getNumHeartbeats
+    return (a, start.toFloat, stop.toFloat)
+  else
+    let start ← IO.monoNanosNow
+    let a ← act
+    let stop ← IO.monoNanosNow
+    return (a, start.toFloat / 1000000000, stop.toFloat / 1000000000)
 
-@[inline]
-def shouldProfile : m Bool := do
-  let opts ← getOptions
-  return profiler.get opts || trace.profiler.get opts
-
-@[inline]
-def shouldEnableNestedTrace (cls : Name) (secs : Float) : m Bool := do
-  return (← isTracingEnabledFor cls) || secs < trace.profiler.threshold.getSecs (← getOptions)
+@[inline] def trace.profiler.threshold.unitAdjusted (o : Options) : Float :=
+  if trace.profiler.useHearbeats.get o then
+    (trace.profiler.threshold.get o).toFloat
+  else
+    -- milliseconds to seconds
+    (trace.profiler.threshold.get o).toFloat / 1000
 
 /--
 `MonadExcept` variant that is expected to catch all exceptions of the given type in case the
@@ -229,8 +245,9 @@ def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls :
   unless clsEnabled || trace.profiler.get opts do
     return (← k)
   let oldTraces ← getResetTraces
-  let (res, start, stop) ← withStartStopSeconds <| observing k
-  let aboveThresh := trace.profiler.get opts && stop - start > trace.profiler.threshold.getSecs opts
+  let (res, start, stop) ← withStartStop opts <| observing k
+  let aboveThresh := trace.profiler.get opts &&
+    stop - start > trace.profiler.threshold.unitAdjusted opts
   unless clsEnabled || aboveThresh do
     modifyTraces (oldTraces ++ ·)
     return (← MonadExcept.ofExcept res)
@@ -325,8 +342,9 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
   let ref ← getRef
   -- make sure to preserve context *before* running `k`
   let msg ← withRef ref do addMessageContext (← msg)
-  let (res, start, stop) ← withStartStopSeconds <| observing k
-  let aboveThresh := trace.profiler.get opts && stop - start > trace.profiler.threshold.getSecs opts
+  let (res, start, stop) ← withStartStop opts <| observing k
+  let aboveThresh := trace.profiler.get opts &&
+    stop - start > trace.profiler.threshold.unitAdjusted opts
   unless clsEnabled || aboveThresh do
     modifyTraces (oldTraces ++ ·)
     return (← MonadExcept.ofExcept res)

src/kernel/declaration.cpp

@@ -71,8 +71,10 @@ definition_val::definition_val(name const & n, names const & lparams, expr const
 
 definition_safety definition_val::get_safety() const { return static_cast<definition_safety>(lean_definition_val_get_safety(to_obj_arg())); }
 
-theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val):
-    object_ref(mk_cnstr(0, constant_val(n, lparams, type), val)) {
+extern "C" object * lean_mk_theorem_val(object * n, object * lparams, object * type, object * value, object * all);
+
+theorem_val::theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all):
+    object_ref(lean_mk_theorem_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), val.to_obj_arg(), all.to_obj_arg())) {
 }
 
 extern "C" object * lean_mk_opaque_val(object * n, object * lparams, object * type, object * value, uint8 is_unsafe, object * all);
@@ -206,7 +208,7 @@ declaration mk_definition(environment const & env, name const & n, names const &
 }
 
 declaration mk_theorem(name const & n, names const & lparams, expr const & type, expr const & val) {
-    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val)));
+    return declaration(mk_cnstr(static_cast<unsigned>(declaration_kind::Theorem), theorem_val(n, lparams, type, val, names(n))));
 }
 
 declaration mk_opaque(name const & n, names const & params, expr const & t, expr const & v, bool is_unsafe) {

src/kernel/declaration.h

@@ -112,12 +112,13 @@ public:
 typedef list_ref<definition_val> definition_vals;
 
 /*
-structure theorem_val extends constant_val :=
-(value : task expr)
+structure TheoremVal extends ConstantVal where
+  value : Expr
+  all : List Name := [name]
 */
 class theorem_val : public object_ref {
 public:
-    theorem_val(name const & n, names const & lparams, expr const & type, expr const & val);
+    theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all);
     theorem_val(theorem_val const & other):object_ref(other) {}
     theorem_val(theorem_val && other):object_ref(other) {}
     theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }

src/lake/Lake/Build/Package.lean

@@ -50,7 +50,7 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
 def Package.fetchRelease (self : Package) : SpawnM (BuildJob Unit) :=
-  withRegisterJob "Fetching {self.name} cloud release" <| Job.async do
+  withRegisterJob s!"Fetching {self.name} cloud release" <| Job.async do
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)

src/lake/Lake/Build/Run.lean

@@ -48,7 +48,8 @@ def Workspace.runFetchM
   let failLv : LogLevel := if ctx.failIfWarnings then .warning else .error
   let failed := log.any (·.level ≥ failLv)
   if !failed && io.isEmpty && !log.hasVisibleEntries verbosity then
-    if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
+    if showProgress then
+      if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
   else
     unless showProgress do
       out.putStr header
@@ -72,7 +73,8 @@ def Workspace.runFetchM
     let failed := log.any (·.level ≥ failLv)
     if failed then modify (·.push caption)
     if !(failed || log.hasVisibleEntries verbosity) then
-      if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
+      if showProgress then
+        if useANSI then out.putStr "\x1B[2K\r" else out.putStr "\n"
     else
       unless showProgress do
         out.putStr header

src/lake/Lake/CLI/Translate.lean

@@ -28,7 +28,7 @@ def Package.mkConfigString (pkg : Package) (lang : ConfigLang) : LogIO String :=
   | .lean => do
     let env ← importModulesUsingCache #[`Lake] {} 1024
     let pp := ppModule <| descopeTSyntax <| pkg.mkLeanConfig
-    match (← pp.toIO {fileName := "", fileMap := default, diag := false} {env} |>.toBaseIO) with
+    match (← pp.toIO {fileName := "", fileMap := default} {env} |>.toBaseIO) with
     | .ok (fmt, _) => pure <| (toString fmt).trim ++ "\n"
     | .error ex =>
       error s!"(internal) failed to pretty print Lean configuration: {ex.toString}"

src/lake/Lake/DSL/Require.lean

@@ -5,6 +5,7 @@ Authors: Mac Malone
 -/
 import Lean.Parser.Command
 import Lake.DSL.Extensions
+import Lake.DSL.DeclUtil
 
 namespace Lake.DSL
 open Lean Parser Command
@@ -18,24 +19,25 @@ syntax fromGit :=
 syntax depSpec :=
   ident " from " (fromGit <|> fromPath) (" with " term)?
 
-def expandDepSpec : TSyntax ``depSpec → MacroM Command
-| `(depSpec| $name:ident from git $url $[@ $rev?]? $[/ $path?]? $[with $opts?]?) => do
-  let rev ← match rev? with | some rev => `(some $rev) | none => `(none)
-  let path ← match path? with | some path => `(some $path) | none => `(none)
-  let opts := opts?.getD <| ← `({})
-  `(@[package_dep] def $name : Dependency := {
-    name := $(quote name.getId),
-    src := Source.git $url $rev $path,
-    opts := $opts
-  })
-| `(depSpec| $name:ident from $path:term $[with $opts?]?) => do
-  let opts := opts?.getD <| ← `({})
-  `(@[package_dep] def $name : Dependency := {
-    name :=  $(quote name.getId),
-    src := Source.path $path,
-    opts := $opts
-  })
-| _ => Macro.throwUnsupported
+def expandDepSpec (stx : TSyntax ``depSpec) (doc? : Option DocComment) : MacroM Command := do
+  match stx with
+  | `(depSpec| $name:ident from git $url $[@ $rev?]? $[/ $path?]? $[with $opts?]?) =>
+    let rev ← match rev? with | some rev => `(some $rev) | none => `(none)
+    let path ← match path? with | some path => `(some $path) | none => `(none)
+    let opts := opts?.getD <| ← `({})
+    `($[$doc?:docComment]? @[package_dep] def $name : Dependency := {
+      name := $(quote name.getId),
+      src := Source.git $url $rev $path,
+      opts := $opts
+    })
+  | `(depSpec| $name:ident from $path:term $[with $opts?]?) => do
+    let opts := opts?.getD <| ← `({})
+    `($[$doc?:docComment]? @[package_dep] def $name : Dependency := {
+      name :=  $(quote name.getId),
+      src := Source.path $path,
+      opts := $opts
+    })
+  | _ => Macro.throwUnsupported
 
 /--
 Adds a new package dependency to the workspace. Has two forms:
@@ -53,8 +55,9 @@ The elements of both the `from` and `with` clauses are proper terms so
 normal computation is supported within them (though parentheses made be
 required to disambiguate the syntax).
 -/
-scoped macro (name := requireDecl) "require " spec:depSpec : command =>
-  expandDepSpec spec
+scoped macro (name := requireDecl)
+doc?:(docComment)? "require " spec:depSpec : command =>
+  expandDepSpec spec doc?
 
 @[inherit_doc requireDecl] abbrev RequireDecl := TSyntax ``requireDecl
 

src/lake/Lake/Toml/Load.lean

@@ -22,7 +22,7 @@ def loadToml (ictx : InputContext) : EIO MessageLog Table := do
     throw <|  MessageLog.empty.add <| mkParserErrorMessage ictx s errorMsg
   else if ictx.input.atEnd s.pos then
     let act := elabToml ⟨s.stxStack.back⟩
-    match (← act.run {fileName := ictx.fileName, fileMap := ictx.fileMap, diag := false} {env} |>.toBaseIO) with
+    match (← act.run {fileName := ictx.fileName, fileMap := ictx.fileMap} {env} |>.toBaseIO) with
     | .ok (t, s) =>
       if s.messages.hasErrors then
         throw s.messages

src/lake/examples/deps/bar/lakefile.lean

@@ -3,6 +3,7 @@ open System Lake DSL
 
 package bar
 
+/-- Require statements can have doc comments. -/
 require foo from ".."/"foo"
 
 lean_lib Bar

src/lake/examples/ffi/app/lakefile.lean

@@ -6,8 +6,7 @@ package app
 require ffi from ".."/"lib"
 
 @[default_target]
-lean_exe app {
+lean_exe app where
   root := `Main
-}
 
 lean_lib Test

src/lake/examples/hello/lakefile.lean

@@ -6,6 +6,5 @@ package hello
 lean_lib Hello
 
 @[default_target]
-lean_exe hello {
+lean_exe hello where
   root := `Main
-}

src/lake/examples/hello/test.sh

@@ -8,6 +8,9 @@ $LAKE exe hello
 $LAKE exe hello Bob Bill
 .lake/build/bin/hello
 
+# Tests that quiet mode (-q) produces no output on no-op build
+$LAKE -q build hello 2>&1 | diff - /dev/null
+
 # Tests that build produces a manifest if there is none.
 # Related: https://github.com/leanprover/lean4/issues/2549
 test -f lake-manifest.json

src/lake/examples/targets/test.sh

@@ -20,7 +20,7 @@ fi
 ./clean.sh
 
 # Test error on nonexistent facet
-$LAKE build targets:noexistent && false || true
+$LAKE build targets:noexistent && exit 1 || true
 
 # Test custom targets and package, library, and module facets
 $LAKE build bark | awk '/bark/,/Bark!/' | wc -l | grep -q 2

src/lake/tests/badImport/test.sh

@@ -10,5 +10,5 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # https://github.com/leanprover/lean4/issues/2569
 # https://github.com/leanprover/lean4/issues/2415
 
-($LAKE build +X 2>&1 && exit 1 || true) | grep -F "X.lean"
-($LAKE setup-file ./X.lean Lib.B 2>&1 && exit 1 || true) | grep -F "Lib.B"
+($LAKE build +X 2>&1 && exit 1 || true) | grep --color -F "X.lean"
+($LAKE setup-file ./X.lean Lib.B 2>&1 && exit 1 || true) | grep --color -F "Lib.B"

src/lake/tests/clone/test.sh

@@ -30,7 +30,7 @@ HELLO_MAP="{\"hello\" : \"file://$(pwd)/hello\"}"
 cd test
 
 # test that `LAKE_PKG_URL_MAP` properly overwrites the config-specified Git URL
-LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | grep "file://"
+LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | grep --color "file://"
 # test that a second `lake update` is a no-op (with URLs)
 # see https://github.com/leanprover/lean4/commit/6176fdba9e5a888225a23e5d558a005e0d1eb2f6#r125905901
 LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | diff - /dev/null
@@ -45,15 +45,15 @@ $LAKE update 2>&1 | diff - /dev/null
 test -d .lake/packages/hello
 # test that Lake produces no warnings
 $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
-./.lake/build/bin/test | grep "Hello, world"
+./.lake/build/bin/test | grep --color "Hello, world"
 
 # Test that Lake produces a warning if local changes are made to a dependency
 # See https://github.com/leanprover/lake/issues/167
 
 sed_i "s/world/changes/" .lake/packages/hello/Hello/Basic.lean
-git -C .lake/packages/hello diff --exit-code && false || true
-$LAKE build 3>&1 1>&2 2>&3 | grep "has local changes"
-./.lake/build/bin/test | grep "Hello, changes"
+git -C .lake/packages/hello diff --exit-code && exit 1 || true
+$LAKE build 3>&1 1>&2 2>&3 | grep --color "has local changes"
+./.lake/build/bin/test | grep --color "Hello, changes"
 git -C .lake/packages/hello reset --hard
 $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
 

src/lake/tests/clone/test/lakefile.lean

@@ -7,6 +7,5 @@ package test
 require hello from git "../hello"
 
 @[default_target]
-lean_exe test {
+lean_exe test where
   root := `Main
-}

src/lake/tests/depTree/test.sh

@@ -38,7 +38,7 @@ cat >>lakefile.lean <<EOF
 require a from git "../a" @ "master"
 EOF
 $LAKE update -v
-grep "\"a\"" lake-manifest.json
+grep --color "\"a\"" lake-manifest.json
 git add .
 git config user.name test
 git config user.email test@example.com
@@ -59,7 +59,7 @@ cat >>lakefile.lean <<EOF
 require a from git "../a" @ "master"
 EOF
 $LAKE update -v
-grep "\"a\"" lake-manifest.json
+grep --color "\"a\"" lake-manifest.json
 git add .
 git config user.name test
 git config user.email test@example.com
@@ -75,7 +75,7 @@ require b from git "../b" @ "master"
 require c from git "../c" @ "master"
 EOF
 # make sure we pick up the version from b's manifest (a@1)
-$LAKE update -v 2>&1 | grep 'first commit in a'
+$LAKE update -v 2>&1 | grep --color 'first commit in a'
 git add .
 git config user.name test
 git config user.email test@example.com
@@ -90,10 +90,10 @@ pushd b
 # b: a@1/init -> a@2
 $LAKE update -v
 # test 84: `lake update` does update
-git diff | grep -m1 manifest
+git diff | grep --color manifest
 sed_i 's/master/init/g' lakefile.lean
 # test 85: warn when manifest and configuration differ
-$LAKE resolve-deps -v 2>&1 | grep 'manifest out of date'
+$LAKE resolve-deps -v 2>&1 | grep --color 'manifest out of date'
 # b: a@1
 git reset --hard
 popd
@@ -109,7 +109,7 @@ popd
 pushd d
 $LAKE update -v
 # test 70: we do not update transitive depednecies
-! grep 'third commit in a' .lake/packages/a/A.lean
+grep --color 'third commit in a' .lake/packages/a/A.lean && exit 1 || true
 git diff --exit-code
 popd
 
@@ -133,10 +133,10 @@ pushd d
 # d: b@1 -> b@2 => a@1 -> a@3
 $LAKE update b -v
 # test 119: pickup a@3 and not a@4
-grep 'third commit in a' .lake/packages/a/A.lean
+grep --color 'third commit in a' .lake/packages/a/A.lean
 # test the removal of `c` from the manifest
-grep "\"c\"" lake-manifest.json
+grep --color "\"c\"" lake-manifest.json
 sed_i '/require c/d' lakefile.lean
 $LAKE update c -v
-grep "\"c\"" lake-manifest.json && false || true
+grep --color "\"c\"" lake-manifest.json && exit 1 || true
 popd

src/lake/tests/env/test.sh

@@ -15,12 +15,12 @@ $LAKE env printenv LAKE
 $LAKE env printenv LAKE_HOME
 $LAKE env printenv LEAN_GITHASH
 $LAKE env printenv LEAN_SYSROOT
-$LAKE env printenv LEAN_AR | grep ar
+$LAKE env printenv LEAN_AR | grep --color ar
 $LAKE env printenv LEAN_PATH
-$LAKE -d ../../examples/hello env printenv LEAN_PATH | grep examples/hello
-$LAKE env printenv LEAN_SRC_PATH | grep lake
-$LAKE -d ../../examples/hello env printenv LEAN_SRC_PATH | grep examples/hello
-$LAKE -d ../../examples/hello env printenv PATH | grep examples/hello
+$LAKE -d ../../examples/hello env printenv LEAN_PATH | grep --color examples/hello
+$LAKE env printenv LEAN_SRC_PATH | grep --color lake
+$LAKE -d ../../examples/hello env printenv LEAN_SRC_PATH | grep --color examples/hello
+$LAKE -d ../../examples/hello env printenv PATH | grep --color examples/hello
 
 # Test that `env` preserves the input environment for certain variables
 test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = foo
@@ -30,8 +30,8 @@ test "`LEAN_CC=foo $LAKE env printenv LEAN_CC`" = foo
 
 # Test `LAKE_PKG_URL_MAP` setting and errors
 test "`LAKE_PKG_URL_MAP='{"a":"a"}' $LAKE env printenv LAKE_PKG_URL_MAP`" = '{"a":"a"}'
-(LAKE_PKG_URL_MAP=foo $LAKE env 2>&1 || true) | grep invalid
-(LAKE_PKG_URL_MAP=0 $LAKE env 2>&1 || true) | grep invalid
+(LAKE_PKG_URL_MAP=foo $LAKE env 2>&1 || true) | grep --color invalid
+(LAKE_PKG_URL_MAP=0 $LAKE env 2>&1 || true) | grep --color invalid
 
 # Test that the platform-specific shared library search path is set
 if [ "$OS" = Windows_NT ]; then
@@ -40,9 +40,9 @@ elif [ "`uname`" = Darwin ]; then
 # MacOS's System Integrity Protection does not permit
 # us to spawn a `printenv` process with `DYLD_LIBRARY_PATH` set
 # https://apple.stackexchange.com/questions/212945/unable-to-set-dyld-fallback-library-path-in-shell-on-osx-10-11-1
-$LAKE env | grep DYLD_LIBRARY_PATH | grep lib/lean
-$LAKE -d ../../examples/hello env | grep DYLD_LIBRARY_PATH | grep examples/hello
+$LAKE env | grep DYLD_LIBRARY_PATH | grep --color lib/lean
+$LAKE -d ../../examples/hello env | grep DYLD_LIBRARY_PATH | grep --color examples/hello
 else
-$LAKE env printenv LD_LIBRARY_PATH  | grep lib/lean
-$LAKE -d ../../examples/hello env printenv LD_LIBRARY_PATH | grep examples/hello
+$LAKE env printenv LD_LIBRARY_PATH  | grep --color lib/lean
+$LAKE -d ../../examples/hello env printenv LD_LIBRARY_PATH | grep --color examples/hello
 fi

src/lake/tests/init/test.sh

@@ -15,25 +15,25 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 # Test `new` and `init` with bad template/langauge (should error)
 
-($LAKE new foo bar 2>&1 && false || true) | grep "unknown package template"
-($LAKE new foo .baz 2>&1 && false || true) | grep "unknown configuration language"
-($LAKE init foo bar 2>&1 && false || true) | grep "unknown package template"
-($LAKE init foo std.baz 2>&1 && false || true) | grep "unknown configuration language"
+($LAKE new foo bar 2>&1 && exit 1 || true) | grep --color "unknown package template"
+($LAKE new foo .baz 2>&1 && exit 1 || true) | grep --color "unknown configuration language"
+($LAKE init foo bar 2>&1 && exit 1 || true) | grep --color "unknown package template"
+($LAKE init foo std.baz 2>&1 && exit 1 || true) | grep --color "unknown configuration language"
 
 # Test package name validation (should error)
 # https://github.com/leanprover/lean4/issues/2637
 
-($LAKE new  .    2>&1 && false || true) | grep "illegal package name"
+($LAKE new  .    2>&1 && exit 1 || true) | grep --color "illegal package name"
 for cmd in new init; do
-($LAKE $cmd ..   2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd .... 2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd '  ' 2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd a/bc 2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd a\\b 2>&1 && false || true) | grep "illegal package name"
-($LAKE $cmd init 2>&1 && false || true) | grep "reserved package name"
-($LAKE $cmd Lean 2>&1 && false || true) | grep "reserved package name"
-($LAKE $cmd Lake 2>&1 && false || true) | grep "reserved package name"
-($LAKE $cmd main 2>&1 && false || true) | grep "reserved package name"
+($LAKE $cmd ..   2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd .... 2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd '  ' 2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd a/bc 2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd a\\b 2>&1 && exit 1 || true) | grep --color "illegal package name"
+($LAKE $cmd init 2>&1 && exit 1 || true) | grep --color "reserved package name"
+($LAKE $cmd Lean 2>&1 && exit 1 || true) | grep --color "reserved package name"
+($LAKE $cmd Lake 2>&1 && exit 1 || true) | grep --color "reserved package name"
+($LAKE $cmd main 2>&1 && exit 1 || true) | grep --color "reserved package name"
 done
 
 # Test default (std) template
@@ -142,4 +142,4 @@ popd
 
 # Test bare `init` on existing package (should error)
 
-($LAKE -d hello_world init 2>&1 && false || true) | grep "package already initialized"
+($LAKE -d hello_world init 2>&1 && exit 1 || true) | grep --color "package already initialized"

src/lake/tests/llvm-bitcode-gen/test.sh

@@ -12,15 +12,15 @@ if [[ ! $(lean --features) =~ LLVM ]]; then
 fi
 
 $LAKE update
-$LAKE build -v | grep "Main.bc.o" # check that we build using the bitcode object file.
+$LAKE build -v | grep --color "Main.bc.o" # check that we build using the bitcode object file.
 
 # If we have the LLVM backend, check that the `lakefile.lean` is aware of this.
-lake script run llvm-bitcode-gen/hasLLVMBackend | grep "true"
+lake script run llvm-bitcode-gen/hasLLVMBackend | grep --color true
 
 # If we have the LLVM backend in the Lean toolchain, then we expect this to
 # print `true`, as this queries the same flag that Lake queries to check the presence
 # of the LLVM toolchian.
-./.lake/build/bin/llvm-bitcode-gen | grep 'true'
+./.lake/build/bin/llvm-bitcode-gen | grep --color true
 
 # If we have the LLVM backend, check that lake builds bitcode artefacts.
 test -f .lake/build/ir/LlvmBitcodeGen.bc

src/lake/tests/lock/test.sh

@@ -22,7 +22,7 @@ test1_pid=$!
 grep -q "Building" < <($TAIL --pid=$$ -f test1.log)
 test -f .lake/build/lake.lock
 kill $test1_pid
-! wait $test1_pid
+wait $test1_pid  && exit 1 || true
 
 # Test build waits when lock file present
 touch test2.log
@@ -37,7 +37,7 @@ wait $test2_pid
 test ! -f .lake/build/lake.lock
 
 # Test build error still deletes lock file
-! $LAKE build Error
+$LAKE build Error && exit 1 || true
 test ! -f .lake/build/lake.lock
 
 # Test that removing the lock during build does not cause it to fail
@@ -47,4 +47,4 @@ test3_pid=$!
 grep -q "Building" < <($TAIL --pid=$$ -f test3.log)
 rm .lake/build/lake.lock
 wait $test3_pid
-cat test3.log | grep "deleted before the lock"
+cat test3.log | grep --color "deleted before the lock"

src/lake/tests/manifest/lake-manifest-v6.json

@@ -10,4 +10,4 @@
     "name": "bar",
     "inputRev?": null,
     "inherited": false}}],
- "name": "test"}
+ "name": "«foo-bar»"}

src/lake/tests/manifest/lake-manifest-v7.json

@@ -16,5 +16,5 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"}],
- "name": "test",
+ "name": "«foo-bar»",
  "lakeDir": ".lake"}

src/lake/tests/manifest/lakefile.lean

@@ -1,7 +1,7 @@
 import Lake
 open Lake DSL
 
-package test
+package «foo-bar»
 
 require foo from "foo"
 require bar from git "bar"

src/lake/tests/manifest/test.sh

@@ -25,45 +25,43 @@ git commit -m "initial commit"
 GIT_REV=`git rev-parse HEAD`
 popd
 
+LATEST_VER=v7
 LOCKED_REV='0538596b94a0510f55dc820cabd3bde41ad93c3e'
 
+# Test an update produces the expected manifest of the latest version
+test_update() {
+  $LAKE update
+  sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
+  diff --strip-trailing-cr lake-manifest-$LATEST_VER.json lake-manifest.json
+}
+
 # ---
 # Test manifest manually upgrades from unsupported versions
 # ---
 
 # Test loading of a V4 manifest fails
 cp lake-manifest-v4.json lake-manifest.json
-($LAKE resolve-deps 2>&1 && exit 1 || true) | grep "incompatible manifest version '4'"
+($LAKE resolve-deps 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '4'"
 
 # Test package update fails as well
-($LAKE update bar 2>&1 && exit 1 || true) | grep "incompatible manifest version '4'"
+($LAKE update bar 2>&1 && exit 1 || true) | grep --color "incompatible manifest version '4'"
 
-# Test bare update produces the expected V7 manifest
-$LAKE update
-sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
-diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
+# Test bare update works
+test_update
 rm -rf .lake
 
 # ---
 # Test manifest automatically upgrades from supported versions
 # ---
 
-# Test successful loading of a V5 manifest
-cp lake-manifest-v5.json lake-manifest.json
-sed_i "s/253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f/$GIT_REV/g" lake-manifest.json
-$LAKE resolve-deps
+# Test successful load & update of a supported manifest version
+test_manifest() {
+  cp lake-manifest-$1.json lake-manifest.json
+  sed_i "s/$2/$GIT_REV/g" lake-manifest.json
+  $LAKE resolve-deps
+  test_update
+}
 
-# Test update produces the expected V7 manifest
-$LAKE update
-sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
-diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
-
-# Test successful loading of a V6 manifest
-cp lake-manifest-v6.json lake-manifest.json
-sed_i "s/dab525a78710d185f3d23622b143bdd837e44ab0/$GIT_REV/g" lake-manifest.json
-$LAKE resolve-deps
-
-# Test update produces the expected V7 manifest
-$LAKE update
-sed_i "s/$GIT_REV/$LOCKED_REV/g" lake-manifest.json
-diff --strip-trailing-cr lake-manifest-v7.json lake-manifest.json
+test_manifest v5 253735aaee71d8bb0f29ae5cfc3ce086a4b9e64f
+test_manifest v6 dab525a78710d185f3d23622b143bdd837e44ab0
+test_manifest v7 0538596b94a0510f55dc820cabd3bde41ad93c3e

src/lake/tests/meta/test.sh

@@ -10,18 +10,18 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # ---
 
 # Test `run_io`
-$LAKE resolve-deps -R 2>&1 | grep impure
-$LAKE resolve-deps 2>&1 | (grep impure && false || true)
+$LAKE resolve-deps -R 2>&1 | grep --color impure
+$LAKE resolve-deps 2>&1 | (grep --color impure && exit 1 || true)
 
 # Test `meta if` and command `do`
-$LAKE resolve-deps -R 2>&1 | (grep -E "foo|bar|baz|1|2" && false || true)
-$LAKE resolve-deps -R -Kbaz 2>&1 | grep baz
-$LAKE resolve-deps -R -Kenv=foo 2>&1 | grep foo
-$LAKE run print_env 2>&1 | grep foo
-$LAKE resolve-deps -R -Kenv=bar 2>&1 | grep bar
-$LAKE run print_env 2>&1 | grep bar
+$LAKE resolve-deps -R 2>&1 | (grep --color -E "foo|bar|baz|1|2" && exit 1 || true)
+$LAKE resolve-deps -R -Kbaz 2>&1 | grep --color baz
+$LAKE resolve-deps -R -Kenv=foo 2>&1 | grep --color foo
+$LAKE run print_env 2>&1 | grep --color foo
+$LAKE resolve-deps -R -Kenv=bar 2>&1 | grep --color bar
+$LAKE run print_env 2>&1 | grep --color bar
 
 # Test environment extension filtering
 # https://github.com/leanprover/lean4/issues/2632
 
-$LAKE run print_elab 2>&1 | grep elabbed-string
+$LAKE run print_elab 2>&1 | grep --color elabbed-string

src/lake/tests/order/test.sh

@@ -11,12 +11,12 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # https://github.com/leanprover/lean4/issues/2548
 
 $LAKE update
-$LAKE build +A -v | grep 222000
-$LAKE build +A.B -v | grep 333000
-$LAKE build +A.B.C -v | grep 333000
-$LAKE build +X -v | grep 555000
-$LAKE build +Y -v | grep 666000
-$LAKE exe Y | grep root
+$LAKE build +A -v | grep --color 222000
+$LAKE build +A.B -v | grep --color 333000
+$LAKE build +A.B.C -v | grep --color 333000
+$LAKE build +X -v | grep --color 555000
+$LAKE build +Y -v | grep --color 666000
+$LAKE exe Y | grep --color root
 
 # Tests that `lake update` does not reorder packages in the manifest
 # (if there have been no changes to the order in the configuration)

src/lake/tests/postUpdate/test.sh

@@ -11,6 +11,6 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 
 echo "root" > toolchain
 echo "dep" > dep/toolchain
-$LAKE update | grep -F "post-update hello w/ arguments: [get]"
+$LAKE update | grep --color -F "post-update hello w/ arguments: [get]"
 test "`cat toolchain`" = dep
 

src/lake/tests/precompileArgs/lakefile.lean

@@ -4,8 +4,6 @@ open Lake DSL
 package precompileArgs
 
 @[default_target]
-lean_lib Foo {
+lean_lib Foo where
   precompileModules := true
   moreLinkArgs := #["-lBaz"]
-}
-

src/lake/tests/precompileArgs/test.sh

@@ -6,4 +6,4 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 ./clean.sh
 
 # Test that `moreLinkArgs` are included when linking precompiled modules
-($LAKE build +Foo:dynlib 2>&1 || true) | grep -- "-lBaz"
+($LAKE build +Foo:dynlib 2>&1 || true) | grep --color -- "-lBaz"

src/lake/tests/rebuild/test.sh

@@ -15,9 +15,9 @@ mkdir -p Foo
 echo $'def a := "a"' > Foo/Test.lean
 echo $'import Foo.Test def hello := a' > Foo.lean
 ${LAKE} build
-./.lake/build/bin/foo | grep -m1 a
+./.lake/build/bin/foo | grep --color a
 echo $'def b := "b"' > Foo/Test.lean
 echo $'import Foo.Test def hello := b' > Foo.lean
 ${LAKE} build Foo
 ${LAKE} build
-./.lake/build/bin/foo | grep -m1 b
+./.lake/build/bin/foo | grep --color b

src/lake/tests/serve/test.sh

@@ -36,7 +36,7 @@ echo "tested 49"
 # Test that `lake setup-file` produces the error from `LAKE_INVALID_CONFIG`
 set -x
 # NOTE: For some reason, using `!` here does not work on macOS
-(LAKE_INVALID_CONFIG=$'foo\n' $LAKE setup-file ./Irrelevant.lean 2>&1 && exit 1 || true) | grep foo
+(LAKE_INVALID_CONFIG=$'foo\n' $LAKE setup-file ./Irrelevant.lean 2>&1 && exit 1 || true) | grep --color foo
 set +x
 
 # Test that `lake serve` produces the `Invalid Lake configuration message`.

src/lake/tests/test/test.sh

@@ -14,14 +14,14 @@ $LAKE -f exe.toml test | grep --color -F "exe: []"
 $LAKE -f exe.toml test -- hello | grep --color "hello"
 
 # Test runner validation
-($LAKE -f two.lean test 2>&1 && false || true) | grep --color "only one"
-($LAKE -f none.lean test 2>&1 && false || true) | grep --color "no test runner"
-($LAKE -f none.toml test 2>&1 && false || true) | grep --color "no test runner"
+($LAKE -f two.lean test 2>&1 && exit 1 || true) | grep --color "only one"
+($LAKE -f none.lean test 2>&1 && exit 1 || true) | grep --color "no test runner"
+($LAKE -f none.toml test 2>&1 && exit 1 || true) | grep --color "no test runner"
 
 # Test runner checker
 $LAKE -f exe.lean check-test
 $LAKE -f exe.toml check-test
 $LAKE -f script.lean check-test
-($LAKE -f two.lean check-test && false || true)
-($LAKE -f none.lean check-test && false || true)
-($LAKE -f none.toml check-test && false || true)
+($LAKE -f two.lean check-test && exit 1 || true)
+($LAKE -f none.lean check-test && exit 1 || true)
+($LAKE -f none.toml check-test && exit 1 || true)

src/lake/tests/toolchain/test.sh

@@ -11,17 +11,9 @@ if ! command -v elan > /dev/null; then
    exit 0
 fi
 
-unamestr=`uname`
-if [ "$unamestr" = Darwin ] || [ "$unamestr" = FreeBSD ]; then
-  sed_i() { sed -i '' "$@"; }
-else
-  sed_i() { sed -i "$@"; }
-fi
-
 ./clean.sh
-elan run leanprover/lean4:nightly-2022-06-30 lake new foo
+elan run --install leanprover/lean4:v4.0.0 lake new foo
 cd foo
-elan run leanprover/lean4:nightly-2022-06-30 lake build +Foo:olean | grep -m1 Foo.olean
+elan run leanprover/lean4:v4.0.0 lake build +Foo:olean -v | grep --color Foo.olean
 rm lean-toolchain
-sed_i 's/defaultTarget/default_target/g' lakefile.lean
-${LAKE:-../../../.lake/build/bin/lake} build -v | grep -m1 Foo.olean
+${LAKE:-../../../.lake/build/bin/lake} build -v | grep --color Foo.olean

src/library/constructions/projection.cpp

@@ -99,10 +99,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         expr proj_val  = mk_proj(n, i, c);
         proj_val = lctx.mk_lambda(proj_args, proj_val);
         declaration new_d;
-        // TODO: replace `if (false) {` with `if (is_prop) {`.
-        // Mathlib is crashing when prop fields are theorems.
-        // The crash is in the ir_interpreter. Kyle suspects this is an use-after-free bug in the interpreter.
-        if (false) { // if (is_prop) {
+        if (is_prop) {
             bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val);
             if (unsafe) {
                 // theorems cannot be unsafe

src/runtime/process.cpp

@@ -24,6 +24,7 @@ Author: Jared Roesch
 #include <fcntl.h>
 #include <sys/wait.h>
 #include <signal.h>
+#include <limits.h> // NOLINT
 #endif
 
 #include "runtime/object.h"
@@ -57,6 +58,24 @@ lean_object * wrap_win_handle(HANDLE h) {
     return lean_alloc_external(g_win_handle_external_class, static_cast<void *>(h));
 }
 
+extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
+    char path[MAX_PATH];
+    DWORD sz = GetCurrentDirectory(MAX_PATH, path);
+    if (sz != 0) {
+        return io_result_mk_ok(lean_mk_string_from_bytes(path, sz));
+    } else {
+        return io_result_mk_error((sstream() << GetLastError()).str());
+    }
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, obj_arg) {
+    if (SetCurrentDirectory(string_cstr(path))) {
+        return io_result_mk_ok(box(0));
+    } else {
+        return io_result_mk_error((sstream() << GetLastError()).str());
+    }
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
     return lean_io_result_mk_ok(box_uint32(GetCurrentProcessId()));
 }
@@ -252,6 +271,23 @@ void finalize_process() {}
 
 #else
 
+extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
+    char path[PATH_MAX];
+    if (getcwd(path, PATH_MAX)) {
+        return io_result_mk_ok(mk_string(path));
+    } else {
+        return io_result_mk_error(decode_io_error(errno, nullptr));
+    }
+}
+
+extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, obj_arg) {
+    if (!chdir(string_cstr(path))) {
+        return io_result_mk_ok(box(0));
+    } else {
+        return io_result_mk_error(decode_io_error(errno, path));
+    }
+}
+
 extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
     static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
     return lean_io_result_mk_ok(box_uint32(getpid()));

tests/lean/906.lean.expected.out

@@ -1,3 +1,5 @@
 906.lean:2:4-2:15: warning: declaration uses 'sorry'
 906.lean:14:2-14:28: error: tactic 'simp' failed, nested error:
-maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
+maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information

tests/lean/exceptionalTrace.lean.expected.out

@@ -1,4 +1,6 @@
-exceptionalTrace.lean:7:0-7:13: error: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
+exceptionalTrace.lean:7:0-7:13: error: maximum recursion depth has been reached
+use `set_option maxRecDepth <num>` to increase limit
+use `set_option diagnostics true` to get diagnostic information
 [Elab.step] expected type: <not-available>, term
     rt + 1
   [Elab.step] expected type: <not-available>, term

tests/lean/run/1123.lean

@@ -3,11 +3,9 @@ class OpAssoc (op : α → α → α) : Prop where
 
 abbrev op_assoc (op : α → α → α) [self : OpAssoc op] := self.op_assoc
 
-@[reducible]
 structure SemigroupSig (α) where
   op : α → α → α
 
-@[reducible]
 structure SemiringSig (α) where
   add : α → α → α
   mul : α → α → α

tests/lean/run/2575.lean

@@ -4,9 +4,8 @@ structure AtLeastThirtySeven where
 
 theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le
 
--- TODO: fix
 /--
-info: def AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
+info: theorem AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
 fun self => self.2
 -/
 #guard_msgs in

tests/lean/run/3943.lean

@@ -19,7 +19,20 @@ def overlap : Nat → Nat
   | n+1 => overlap n
 
 example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n  := by
-  simp only [overlap]
+  simp (config := { contextual := true }) only [overlap]
+  guard_target =ₛ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n
+  sorry
+
+example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n  := by
+  -- The following tactic should because the default discharger only uses assumptions available
+  -- when `simp` was invoked unless `contextual := true`
+  fail_if_success simp only [overlap]
+  guard_target =ₛ (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n
+  sorry
+
+example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n  := by
+  -- assumption is not a well-behaved discharger, and the following should still work as expected
+  simp (discharger := assumption) only [overlap]
   guard_target =ₛ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n
   sorry
 

tests/lean/run/autoparam.lean

@@ -4,3 +4,12 @@ x + x
 
 def g (x y z : Nat) (h : x = y) : Nat :=
 f x y
+
+def f2 (x y : Nat) (h : x = y := by exact rfl) : Nat :=
+x + x
+
+def f3 (x y : Nat) (h : x = y := by exact Eq.refl x) : Nat :=
+x + x
+
+#check fun x => f2 x x
+#check fun x => f3 x x

tests/lean/run/currentDir.lean

@@ -0,0 +1,18 @@
+def test : IO Unit := do
+  let cwd ← IO.Process.getCurrentDir
+  IO.println cwd
+  IO.Process.setCurrentDir ".."
+  let cwd' ← IO.Process.getCurrentDir
+  IO.println cwd'
+  let actual := cwd'.normalize
+  let expected := cwd.normalize.parent.getD
+    (cwd.components[0]!.push System.FilePath.pathSeparator)
+  unless expected == actual do
+    throw <| IO.userError s!"expected {expected}, got {actual}"
+
+-- Ensures this test is idempotent in an interactive session.
+def withoutModifyingCurrentDir (x : IO α) : IO α := do
+  let cwd ← IO.Process.getCurrentDir
+  try x finally IO.Process.setCurrentDir cwd
+
+#eval withoutModifyingCurrentDir test

tests/lean/run/delabMatch.lean

@@ -0,0 +1,126 @@
+import Lean
+/-!
+# Testing the `delabAppMatch` delaborator
+-/
+
+
+/-!
+Basic functionality
+-/
+/--
+info: def Nat.pred : Nat → Nat :=
+fun x =>
+  match x with
+  | 0 => 0
+  | a.succ => a
+-/
+#guard_msgs in
+#print Nat.pred
+/--
+info: def List.head?.{u_1} : {α : Type u_1} → List α → Option α :=
+fun {α} x =>
+  match x with
+  | [] => none
+  | a :: tail => some a
+-/
+#guard_msgs in
+#print List.head?
+
+
+/-!
+`h :` annotations
+-/
+/--
+info: fun x =>
+  let_fun this :=
+    match h : ↑x + 1 with
+    | 0 => Nat.noConfusion h
+    | n.succ => Exists.intro n (Nat.succ.inj h);
+  this : ∀ (x : Fin 1), ∃ n, ↑x = n
+-/
+#guard_msgs in
+#check fun (x : Fin 1) => show ∃ (n : Nat), x = n from
+  match h : x.1 + 1 with
+  | 0 => Nat.noConfusion h
+  | n + 1 => ⟨n, Nat.succ.inj h⟩
+
+
+/-!
+Shadowing with `h :` annotations
+-/
+/--
+info: fun h =>
+  let_fun this :=
+    match h_1 : ↑h + 1 with
+    | 0 => Nat.noConfusion h_1
+    | n.succ => Exists.intro n (Nat.succ.inj h_1);
+  this : ∀ (h : Fin 1), ∃ n, ↑h = n
+-/
+#guard_msgs in
+#check fun (h : Fin 1) => show ∃ (n : Nat), h = n from
+  match h : h.1 + 1 with
+  | 0 => Nat.noConfusion h
+  | n + 1 => ⟨n, Nat.succ.inj h⟩
+
+
+/-!
+Even more shadowing with `h :` annotations
+-/
+set_option linter.unusedVariables false in
+/--
+info: fun h =>
+  let_fun this :=
+    match h_1 : ↑h + 1 with
+    | 0 => Nat.noConfusion h_1
+    | h_2.succ => Exists.intro h_2 (Nat.succ.inj h_1);
+  this : ∀ (h : Fin 1), ∃ n, ↑h = n
+-/
+#guard_msgs in
+#check fun (h : Fin 1) => show ∃ (n : Nat), h = n from
+  match h : h.1 + 1 with
+  | 0 => Nat.noConfusion h
+  | h + 1 => ⟨_, Nat.succ.inj ‹_›⟩
+
+
+/-!
+Overapplication
+-/
+/--
+info: fun b =>
+  (match (motive := Bool → Bool → Bool) b with
+    | false => fun x => x
+    | true => fun x => !x)
+    b : Bool → Bool
+-/
+#guard_msgs in
+#check (fun b : Bool => (match b with | false => fun x => x | true => fun x => !x) b)
+
+
+namespace WithFoo
+
+def foo (b : Bool) : Bool := match b with | false => false | _ => b
+
+
+/-!
+Follows the names from the functions
+-/
+set_option linter.unusedVariables false in
+/--
+info: fun b =>
+  match b with
+  | false => false
+  | a => b : Bool → Bool
+-/
+#guard_msgs in
+#check fun b => foo.match_1 (fun _ => Bool) b (fun _ => false) fun a => b
+
+
+/-!
+Underapplied, no `match` notation
+-/
+set_option linter.unusedVariables false in
+/-- info: fun b => foo.match_1 (fun x => Bool) b fun x => false : Bool → (Bool → Bool) → Bool -/
+#guard_msgs in
+#check fun b => foo.match_1 (fun _ => Bool) b (fun _ => false)
+
+end WithFoo

tests/lean/run/diagRec.lean

@@ -7,15 +7,16 @@ termination_by n
 /--
 info: 89
 ---
-info: unfolded declarations:
-  Nat.rec ↦ 407
+info: [reduction] unfolded declarations (max: 407, num: 3):
+    Nat.rec ↦ 407
+  ⏎
   Or.rec ↦ 144
-  Acc.rec ↦ 108
-unfolded reducible declarations:
-  Nat.casesOn ↦ 352
+  ⏎
+  Acc.rec ↦ 108[reduction] unfolded reducible declarations (max: 352, num: 3):
+    Nat.casesOn ↦ 352
+  ⏎
   Or.casesOn ↦ 144
-  PProd.fst ↦ 126
-use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+   PProd.fst ↦ 126use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in
 set_option diagnostics true in

tests/lean/run/diagnostics.lean

@@ -0,0 +1,53 @@
+opaque q : Nat → Nat
+def f (x : Nat) : Nat :=
+  match x with
+  | 0 => 1
+  | x+1 => q (f x)
+
+theorem f_eq : f (x + 1) = q (f x) := rfl
+
+set_option trace.Meta.debug true
+
+/--
+info: [reduction] unfolded declarations (max: 15, num: 6):
+    Nat.rec ↦ 15
+  ⏎
+  Add.add ↦ 10
+  ⏎
+  HAdd.hAdd ↦ 10
+  ⏎
+  Nat.add ↦ 10
+  ⏎
+  f ↦ 5
+  ⏎
+  OfNat.ofNat ↦ 5[reduction] unfolded instances (max: 5, num: 1):
+    instOfNatNat ↦ 5[reduction] unfolded reducible declarations (max: 15, num: 1):
+    Nat.casesOn ↦ 15use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+example : f (x + 5) = q (q (q (q (q (f x))))) :=
+  set_option diagnostics.threshold 4 in
+  set_option diagnostics true in
+  rfl
+
+/--
+info: [reduction] unfolded declarations (max: 15, num: 6):
+    Nat.rec ↦ 15
+  ⏎
+  Add.add ↦ 10
+  ⏎
+  HAdd.hAdd ↦ 10
+  ⏎
+  Nat.add ↦ 10
+  ⏎
+  f ↦ 5
+  ⏎
+  OfNat.ofNat ↦ 5[reduction] unfolded instances (max: 5, num: 1):
+    instOfNatNat ↦ 5[reduction] unfolded reducible declarations (max: 15, num: 1):
+    Nat.casesOn ↦ 15use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
+-/
+#guard_msgs in
+example : f (x + 5) = q (q (q (q (q (f x))))) := by
+  set_option diagnostics.threshold 4 in
+  set_option diagnostics true in
+  rfl

tests/lean/run/isDefEqProjIssue.lean

@@ -51,7 +51,9 @@ where
     val.x
 
 /--
-error: (deterministic) timeout at 'whnf', maximum number of heartbeats (400) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
+error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
+use `set_option maxHeartbeats <num>` to set the limit
+use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs in
 set_option backward.isDefEq.lazyWhnfCore false in

tests/lean/run/issue4063.lean

@@ -0,0 +1,5 @@
+/-- error: no goals to be solved -/
+#guard_msgs in
+example : 3 = 3 := by
+  rfl
+  rfl

tests/lean/run/reducibilityAttrValidation.lean

@@ -0,0 +1,93 @@
+def f (x : Nat) := x + 1
+
+/--
+error: failed to set `[semireducible]` for `f`, declarations are `[semireducible]` by default
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [semireducible] f
+
+attribute [reducible] f
+
+/--
+error: failed to set `[reducible]`, `f` is not currently `[semireducible]`, but `[reducible]`
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [reducible] f -- should fail because of double reducible setting
+
+-- "Reset" `f`
+set_option allowUnsafeReducibility true in
+attribute [semireducible] f
+
+attribute [irreducible] f
+
+/--
+error: failed to set `[irreducible]`, `f` is not currently `[semireducible]`, but `[irreducible]`
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [irreducible] f
+
+attribute [local semireducible] f
+
+/--
+error: failed to set `[local semireducible]`, `f` is currently `[semireducible]`, `[irreducible]` expected
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [local semireducible] f
+
+attribute [local irreducible] f
+
+/--
+error: failed to set `[local irreducible]`, `f` is currently `[irreducible]`, `[semireducible]` expected
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [local irreducible] f
+
+/--
+error: failed to set `[local reducible]` for `f`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [local reducible] f
+
+/--
+error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [semireducible] Nat.add
+
+/--
+error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [reducible] Nat.add
+
+/--
+error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [irreducible] Nat.add
+
+/-- error: scoped attributes must be used inside namespaces -/
+#guard_msgs in
+attribute [scoped reducible] Nat.add
+
+namespace Foo
+/--
+error: failed to set reducibility status for `Nat.add`, the `scoped` modifier is not recommended for this kind of attribute
+use `set_option allowUnsafeReducibility true` to override reducibility status validation
+-/
+#guard_msgs in
+attribute [scoped reducible] Nat.add
+
+set_option allowUnsafeReducibility true in
+attribute [scoped reducible] Nat.add
+
+end Foo

tests/lean/run/rewrite.lean

@@ -40,6 +40,7 @@ example : f 1 = f 2 := by
 example : f 1 = f 2 := by
   rw [s 1 3, s 3 4] -- Closes the goal via `rfl`
 
+set_option allowUnsafeReducibility true
 -- For the remaining tests we prevent `rfl` from closing the goal.
 attribute [irreducible] f
 
@@ -109,5 +110,3 @@ example : f 2 = f 0 := by
   -- we can return the problem to the user.
   rw [@t' 2 ?_]
   constructor
-
-