chore: allow omega to use classicality, in case Decidable instances are too big

On
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Notation.20in.20namespace.20not.20showing.20in.20pp/near/437016468),
Peter Nelson reported that notations that could be pretty printed with
generalized field notation did not pretty print using the intended
notation.

This PR makes it so that app unexpanders are considered before
generalized field notation. The complexity before was that we wanted to
do parent projection collapse, and since we did the collapse before
pretty printing that argument, it meant it wasn't possible to do app
unexpanders when there was a field notation candidate. The new solution
is to collapse parent projections only when actually considering field
notation, which can be done because we can safely strip off projection
syntax in an expression-directed way.

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

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

@@ -666,7 +666,6 @@ open Lean Elab Tactic Parser.Tactic
 def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
   liftMetaFinishingTactic fun g => do
     let g ← g.falseOrByContra
-      (useClassical := false) -- because all the hypotheses we can make use of are decidable
     g.withContext do
       let hyps := (← getLocalHyps).toList
       trace[omega] "analyzing {hyps.length} hypotheses:\n{← hyps.mapM inferType}"

src/Lean/Meta/Diagnostics.lean

@@ -58,7 +58,7 @@ def mkDiagSummaryForUnfoldedReducible (counters : PHashMap Name Nat) : MetaM Dia
     getReducibilityStatusCore env declName matches .reducible
 
 def mkDiagSummaryForUsedInstances : MetaM DiagSummary := do
-  mkDiagSummary (← get).diag.heuristicCounter
+  mkDiagSummary (← get).diag.instanceCounter
 
 def appendSection (m : MessageData) (cls : Name) (header : String) (s : DiagSummary) : MessageData :=
   if s.isEmpty then

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

@@ -257,6 +257,22 @@ private partial def withoutParentProjections (explicit : Bool) (d : DelabM α) :
   else
     d
 
+-- TODO(kmill): make sure that we only strip projections so long as it doesn't change how it elaborates.
+-- This affects `withoutParentProjections` as well.
+
+/-- Strips parent projections from `s`. Assumes that the current SubExpr is the same as the one used when delaborating `s`. -/
+private partial def stripParentProjections (s : Term) : DelabM Term :=
+  match s with
+  | `($x.$f:ident) => do
+    if let some field ← try parentProj? false (← getExpr) catch _ => pure none then
+      if f.getId == field then
+        withAppArg <| stripParentProjections x
+      else
+        return s
+    else
+      return s
+  | _ => return s
+
 /--
 In explicit mode, decides whether or not the applied function needs `@`,
 where `numArgs` is the number of arguments actually supplied to `f`.
@@ -313,6 +329,27 @@ def delabAppExplicitCore (fieldNotation : Bool) (numArgs : Nat) (delabHead : (in
   else
     return Syntax.mkApp fnStx argStxs
 
+/-- Records how a particular argument to a function is delaborated, in non-explicit mode. -/
+inductive AppImplicitArg
+  /-- An argument to skip, like an implicit argument. -/
+  | skip
+  /-- A regular argument. -/
+  | regular (s : Term)
+  /-- It's a named argument. Named arguments inhibit applying unexpanders. -/
+  | named (s : TSyntax ``Parser.Term.namedArgument)
+  deriving Inhabited
+
+/-- Whether unexpanding is allowed with this argument. -/
+def AppImplicitArg.canUnexpand : AppImplicitArg → Bool
+  | .regular .. | .skip => true
+  | .named .. => false
+
+/-- If the argument has associated syntax, returns it. -/
+def AppImplicitArg.syntax? : AppImplicitArg → Option Syntax
+  | .skip => none
+  | .regular s => s
+  | .named s => s
+
 /--
 Delaborates a function application in the standard mode, where implicit arguments are generally not
 included, unless `pp.analysis.namedArg` is set at that argument.
@@ -330,76 +367,74 @@ def delabAppImplicitCore (unexpand : Bool) (numArgs : Nat) (delabHead : Delab) (
       appFieldNotationCandidate?
     else
       pure none
-  let (shouldUnexpand, fnStx, fieldIdx?, _, _, argStxs, argData) ←
+  let (fnStx, args) ←
     withBoundedAppFnArgs numArgs
-      (do return (unexpand, ← delabHead, none, 0, paramKinds.toList, Array.mkEmpty numArgs, (Array.mkEmpty numArgs).push (unexpand, 0)))
-      (fun (shouldUnexpand, fnStx, fieldIdx?, idx, paramKinds, argStxs, argData) => do
-        /-
-        - `argStxs` is the accumulated array of arguments that should be pretty printed
-        - `argData` is a list of `Bool × Nat` used to figure out:
-          1. whether an unexpander could be used for the prefix up to this argument and
-          2. how many arguments we need to include after this one when annotating the result of unexpansion.
-          Argument `argStxs[i]` corresponds to `argData[i+1]`, with `argData[0]` being for the head itself.
-        -/
-        if some idx = field?.map Prod.fst then
-          -- This is the object for field notation.
-          let fieldObj ← withoutParentProjections (explicit := false) delab
-          return (false, fnStx, some argStxs.size, idx + 1, paramKinds.tailD [], argStxs.push fieldObj, argData.push (false, 1))
-        let (argUnexpandable, stx?) ← mkArgStx (numArgs - idx - 1) paramKinds
-        let shouldUnexpand := shouldUnexpand && argUnexpandable
-        let (argStxs, argData) :=
-          match stx?, argData.back with
-          -- By default, a pretty-printed argument accounts for just itself.
-          | some stx, _ => (argStxs.push stx, argData.push (shouldUnexpand, 1))
-          -- A non-pretty-printed argument is accounted for by the previous pretty printed one.
-          | none, (_, argCount) => (argStxs, argData.pop.push (shouldUnexpand, argCount + 1))
-        return (shouldUnexpand, fnStx, fieldIdx?, idx + 1, paramKinds.tailD [], argStxs, argData))
-  if let some fieldIdx := fieldIdx? then
-    -- Delaborate using field notation
-    let field := field?.get!.2
-    let obj := argStxs[fieldIdx]!
-    let mut head : Term ← `($obj.$(mkIdent field))
-    if fieldIdx == 0 then
-      -- If it's the first argument (after some implicit arguments), we can tag `obj.field` with a prefix of the application
-      -- including the implicit arguments immediately before and after `obj`.
-      head ← withBoundedAppFn (numArgs - argData[0]!.2 - argData[1]!.2) <| annotateTermInfo <| head
-    return Syntax.mkApp head (argStxs.eraseIdx fieldIdx)
-  if ← pure (argData.any Prod.fst) <&&> getPPOption getPPNotation then
+      (do return ((← delabHead), Array.mkEmpty numArgs))
+      (fun (fnStx, args) => do
+        let idx := args.size
+        let arg ← mkArg (numArgs - idx - 1) paramKinds[idx]!
+        return (fnStx, args.push arg))
+
+  -- App unexpanders
+  if ← pure unexpand <&&> getPPOption getPPNotation then
     -- Try using an app unexpander for a prefix of the arguments.
-    if let some stx ← (some <$> tryAppUnexpanders fnStx argStxs argData) <|> pure none then
+    if let some stx ← (some <$> tryAppUnexpanders fnStx args) <|> pure none then
       return stx
-  let stx := Syntax.mkApp fnStx argStxs
-  if ← pure shouldUnexpand <&&> getPPOption getPPStructureInstances then
+
+  let stx := Syntax.mkApp fnStx (args.filterMap (·.syntax?))
+
+  -- Structure instance notation
+  if ← pure (unexpand && args.all (·.canUnexpand)) <&&> getPPOption getPPStructureInstances then
     -- Try using the structure instance unexpander.
-    -- It only makes sense applying this to the entire application, since structure instances cannot themselves be applied.
     if let some stx ← (some <$> unexpandStructureInstance stx) <|> pure none then
       return stx
+
+  -- Field notation
+  if let some (fieldIdx, field) := field? then
+    if fieldIdx < args.size then
+      let obj? : Option Term ← do
+        let arg := args[fieldIdx]!
+        if let .regular s := arg then
+          withNaryArg fieldIdx <| some <$> stripParentProjections s
+        else
+          pure none
+      if let some obj := obj? then
+        let isFirst := args[0:fieldIdx].all (· matches .skip)
+        -- Clear the `obj` argument from `args`.
+        let args' := args.set! fieldIdx .skip
+        let mut head : Term ← `($obj.$(mkIdent field))
+        if isFirst then
+          -- If the object is the first argument (after some implicit arguments),
+          -- we can annotate `obj.field` with the prefix of the application
+          -- that includes all the implicit arguments immediately before and after `obj`.
+          let objArity := args'.findIdx? (fun a => !(a matches .skip)) |>.getD args'.size
+          head ← withBoundedAppFn (numArgs - objArity) <| annotateTermInfo <| head
+        return Syntax.mkApp head (args'.filterMap (·.syntax?))
+
+  -- Normal application
   return stx
 where
-  mkNamedArg (name : Name) (argStx : Syntax) : DelabM (Bool × Option Syntax) :=
-    return (false, ← `(Parser.Term.namedArgument| ($(mkIdent name) := $argStx)))
+  mkNamedArg (name : Name) : DelabM AppImplicitArg :=
+    return .named <| ← `(Parser.Term.namedArgument| ($(mkIdent name) := $(← delab)))
   /--
-  If the argument should be pretty printed then it returns the syntax for that argument.
-  The boolean is `false` if an unexpander should not be used for the application due to this argument.
-  The argumnet `remainingArgs` is the number of arguments in the application after this one.
+  Delaborates the current argument.
+  The argument `remainingArgs` is the number of arguments in the application after this one.
   -/
-  mkArgStx (remainingArgs : Nat) (paramKinds : List ParamKind) : DelabM (Bool × Option Syntax) := do
-    if ← getPPOption getPPAnalysisSkip then return (true, none)
-    else if ← getPPOption getPPAnalysisHole then return (true, ← `(_))
+  mkArg (remainingArgs : Nat) (param : ParamKind) : DelabM AppImplicitArg := do
+    let arg ← getExpr
+    if ← getPPOption getPPAnalysisSkip then return .skip
+    else if ← getPPOption getPPAnalysisHole then return .regular (← `(_))
+    else if ← getPPOption getPPAnalysisNamedArg then
+      mkNamedArg param.name
+    else if param.defVal.isSome && remainingArgs == 0 && param.defVal.get! == arg then
+      -- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument
+      return .skip
+    else if param.bInfo.isExplicit then
+      return .regular (← delab)
+    else if ← pure (param.name == `motive) <&&> shouldShowMotive arg (← getOptions) then
+      mkNamedArg param.name
     else
-      let arg ← getExpr
-      let param :: _ := paramKinds | unreachable!
-      if ← getPPOption getPPAnalysisNamedArg then
-        mkNamedArg param.name (← delab)
-      else if param.defVal.isSome && remainingArgs == 0 && param.defVal.get! == arg then
-        -- Assumption: `useAppExplicit` has already detected whether it is ok to omit this argument
-        return (true, none)
-      else if param.bInfo.isExplicit then
-        return (true, ← delab)
-      else if ← pure (param.name == `motive) <&&> shouldShowMotive arg (← getOptions) then
-        mkNamedArg param.name (← delab)
-      else
-        return (true, none)
+      return .skip
   /--
   Runs the given unexpanders, returning the resulting syntax if any are applicable, and otherwise fails.
   -/
@@ -414,23 +449,26 @@ where
   try applying an app unexpander using some prefix of the arguments, longest prefix first.
   This function makes sure that the unexpanded syntax is annotated and given TermInfo so that it is hoverable in the InfoView.
   -/
-  tryAppUnexpanders (fnStx : Term) (argStxs : Array Syntax) (argData : Array (Bool × Nat)) : Delab := do
+  tryAppUnexpanders (fnStx : Term) (args : Array AppImplicitArg) : Delab := do
     let .const c _ := (← getExpr).getAppFn.consumeMData | unreachable!
     let fs := appUnexpanderAttribute.getValues (← getEnv) c
     if fs.isEmpty then failure
-    let rec go (prefixArgs : Nat) : DelabM Term := do
-      let (unexpand, argCount) := argData[prefixArgs]!
-      match prefixArgs with
+    let rec go (i : Nat) (implicitArgs : Nat) (argStxs : Array Syntax) : DelabM Term := do
+      match i with
       | 0 =>
-        guard unexpand
         let stx ← tryUnexpand fs fnStx
-        return Syntax.mkApp (← annotateTermInfo stx) argStxs
-      | prefixArgs' + 1 =>
-        (do guard unexpand
-            let stx ← tryUnexpand fs <| Syntax.mkApp fnStx (argStxs.extract 0 prefixArgs)
-            return Syntax.mkApp (← annotateTermInfo stx) (argStxs.extract prefixArgs argStxs.size))
-        <|> withBoundedAppFn argCount (go prefixArgs')
-    go argStxs.size
+        return Syntax.mkApp (← annotateTermInfo stx) (args.filterMap (·.syntax?))
+      | i' + 1 =>
+        if args[i']!.syntax?.isSome then
+          (do let stx ← tryUnexpand fs <| Syntax.mkApp fnStx argStxs
+              let argStxs' := args.extract i args.size |>.filterMap (·.syntax?)
+              return Syntax.mkApp (← annotateTermInfo stx) argStxs')
+          <|> withBoundedAppFn (implicitArgs + 1) (go i' 0 argStxs.pop)
+        else
+          go i' (implicitArgs + 1) argStxs
+    let maxUnexpand := args.findIdx? (!·.canUnexpand) |>.getD args.size
+    withBoundedAppFn (args.size - maxUnexpand) <|
+      go maxUnexpand 0 (args.extract 0 maxUnexpand |>.filterMap (·.syntax?))
 
 /--
 Returns true if an application should use explicit mode when delaborating.

src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -102,14 +102,24 @@ def fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldN
   return none
 
 /--
-Returns `true` if `e` is an application that is a projection to a parent structure.
-If `explicit` is `true`, then further requires that the structure have no parameters.
+Returns the field name of the projection if `e` is an application that is a projection to a parent structure.
+If `explicit` is `true`, then requires that the structure have no parameters.
 -/
-def isParentProj (explicit : Bool) (e : Expr) : MetaM Bool := do
-  unless e.isApp do return false
+def parentProj? (explicit : Bool) (e : Expr) : MetaM (Option Name) := do
+  unless e.isApp do return none
   try
     let .const c .. := e.getAppFn | failure
-    let (_, numParams, isParentProj) ← projInfo c
-    return isParentProj && (!explicit || numParams == 0) && e.getAppNumArgs == numParams + 1
+    let (field, numParams, isParentProj) ← projInfo c
+    if isParentProj && (!explicit || numParams == 0) && e.getAppNumArgs == numParams + 1 then
+      return some field
+    else
+      return none
   catch _ =>
-    return false
+    return none
+
+/--
+Returns `true` if `e` is an application that is a projection to a parent structure.
+If `explicit` is `true`, then requires that the structure have no parameters.
+-/
+def isParentProj (explicit : Bool) (e : Expr) : MetaM Bool := do
+  return (← parentProj? explicit e).isSome

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

@@ -116,6 +116,17 @@ Check overapplication.
 /-- info: f.toFun 0 : Int -/
 #guard_msgs in #check f.toFun 0
 
+/-!
+Check that field notation doesn't disrupt unexpansion.
+-/
+notation:max "☺ " f:max => Fn.toFun f
+
+/-- info: ☺ f : Nat → Int -/
+#guard_msgs in #check f.toFun
+
+/-- info: ☺ f 0 : Int -/
+#guard_msgs in #check f.toFun 0
+
 /-!
 Basic generalized field notation
 -/
@@ -148,3 +159,28 @@ Special case: do not use generalized field notation for numeric literals.
 #guard_msgs in #check Nat.succ 2
 /-- info: Float.abs 2.2 : Float -/
 #guard_msgs in #check Float.abs 2.2
+
+/-!
+Verifying that unexpanders defined by `infix` interact properly with generalized field notation
+-/
+structure MySet (α : Type) where
+  p : α → Prop
+
+namespace MySet
+
+def MySubset {α : Type} (s t : MySet α) : Prop := ∀ x, s.p x → t.p x
+
+infix:50 " ⊆⊆ " => MySubset
+
+end MySet
+
+/-- info: ∀ {α : Type} (s t : MySet α), s ⊆⊆ t : Prop -/
+#guard_msgs in #check ∀ {α : Type} (s t : MySet α), s ⊆⊆ t
+
+set_option pp.notation false in
+/-- info: ∀ {α : Type} (s t : MySet α), s.MySubset t : Prop -/
+#guard_msgs in #check ∀ {α : Type} (s t : MySet α), s ⊆⊆ t
+
+set_option pp.notation false in set_option pp.fieldNotation.generalized false in
+/-- info: ∀ {α : Type} (s t : MySet α), MySet.MySubset s t : Prop -/
+#guard_msgs in #check ∀ {α : Type} (s t : MySet α), s ⊆⊆ t

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

@@ -377,8 +377,12 @@ example (i j : Nat) (p : i ≥ j) : True := by
 -- From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Nat.2Emul_sub_mod/near/428107094
 example (a b : Nat) (h : a % b + 1 = 0) : False := by omega
 
-/-! ### Fin -/
+-- From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/omega.20regression.20in.204.2E8.2E0-rc1/near/437150155
+example (x : Nat) : x < 2 →
+    (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧ (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3) := by
+  omega
 
+/-! ### Fin -/
 
 -- Test `<`
 example (n : Nat) (i j : Fin n) (h : i < j) : (i : Nat) < n - 1 := by omega

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

tests/lean/run/scopedLocalReducibility.lean

@@ -1,5 +1,5 @@
 @[irreducible] def f (x : Nat) := x + 1
-
+set_option allowUnsafeReducibility true
 /--
 error: type mismatch
   rfl

tests/lean/run/sealCommand.lean

@@ -0,0 +1,34 @@
+def f (x : Nat) := x + 1
+
+example : f x = x + 1 := rfl
+
+/--
+error: type mismatch
+  rfl
+has type
+  f x = f x : Prop
+but is expected to have type
+  f x = x + 1 : Prop
+-/
+#guard_msgs in
+seal f in
+example : f x = x + 1 := rfl
+
+example : f x = x + 1 := rfl
+
+seal f
+
+/--
+error: type mismatch
+  rfl
+has type
+  f x = f x : Prop
+but is expected to have type
+  f x = x + 1 : Prop
+-/
+#guard_msgs in
+example : f x = x + 1 := rfl
+
+unseal f
+
+example : f x = x + 1 := rfl

tests/lean/run/simproc1.lean

@@ -32,3 +32,5 @@ example : x + foo 2 = 12 + x := by
   -- We can use `-` to disable `simproc`s
   fail_if_success simp [-reduce_foo]
   simp_arith
+
+example (x : Nat) (h : x < 86) : ¬100 ≤ x + 14 := by simp; exact h

tests/lean/substFails.lean

@@ -2,13 +2,15 @@ def foo := 3
 def bar := 4
 
 def ex1  (heq : foo = bar) (P : Nat → Prop) (h : P foo)         := heq ▸ h
+#check ex1
 def ex2  (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P 4   := heq ▸ h -- error
 def ex3  (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h
 def ex4  (heq : foo = bar) (P : Nat → Prop) (h : P 3)           := heq ▸ h -- error
 def ex5  (heq : foo = bar) (P : Nat → Prop) (h : P 3)   : P 4   := heq ▸ h -- error
 def ex6  (heq : foo = bar) (P : Nat → Prop) (h : P 3)   : P bar := heq ▸ h
 
-def ex7  (heq : bar = foo) (P : Nat → Prop) (h : P foo)         := heq ▸ h -- error
+def ex7  (heq : bar = foo) (P : Nat → Prop) (h : P foo)         := heq ▸ h
+#check ex7
 def ex8  (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P 4   := heq ▸ h -- error
 def ex9  (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h
 def ex10 (heq : bar = foo) (P : Nat → Prop) (h : P 3)           := heq ▸ h -- error

tests/lean/substFails.lean.expected.out

@@ -1,43 +1,39 @@
-substFails.lean:5:67-5:74: error: invalid `▸` notation, expected result type of cast is 
+ex1 (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P bar
+substFails.lean:6:67-6:74: error: invalid `▸` notation, expected result type of cast is 
   P 4
 however, the equality 
   heq
 of type 
   foo = bar
 does not contain the expected result type on either the left or the right hand side
-substFails.lean:7:67-7:74: error: invalid `▸` notation, the equality
+substFails.lean:8:67-8:74: error: invalid `▸` notation, the equality
   heq
 has type 
   foo = bar
-but its left hand side is not mentioned in the type
+but neither side of the equality is mentioned in the type
   P 3
-substFails.lean:8:67-8:74: error: invalid `▸` notation, expected result type of cast is 
+substFails.lean:9:67-9:74: error: invalid `▸` notation, expected result type of cast is 
   P 4
 however, the equality 
   heq
 of type 
   foo = bar
 does not contain the expected result type on either the left or the right hand side
-substFails.lean:11:67-11:74: error: invalid `▸` notation, the equality
-  heq
-has type 
-  bar = foo
-but its left hand side is not mentioned in the type
-  P foo
-substFails.lean:12:67-12:74: error: invalid `▸` notation, expected result type of cast is 
+ex7 (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P bar
+substFails.lean:14:67-14:74: error: invalid `▸` notation, expected result type of cast is 
   P 4
 however, the equality 
   heq
 of type 
   bar = foo
 does not contain the expected result type on either the left or the right hand side
-substFails.lean:14:67-14:74: error: invalid `▸` notation, the equality
+substFails.lean:16:67-16:74: error: invalid `▸` notation, the equality
   heq
 has type 
   bar = foo
-but its left hand side is not mentioned in the type
+but neither side of the equality is mentioned in the type
   P 3
-substFails.lean:15:67-15:74: error: invalid `▸` notation, expected result type of cast is 
+substFails.lean:17:67-17:74: error: invalid `▸` notation, expected result type of cast is 
   P 4
 however, the equality 
   heq

tests/pkg/builtin_attr/UserAttr/Tst.lean

@@ -3,7 +3,7 @@ import UserAttr.BlaAttr
 @[bar] def f (x : Nat) := x + 2
 @[bar] def g (x : Nat) := x + 1
 
-attribute [irreducible] myFun
+attribute [local irreducible] myFun
 
 /--
 error: type mismatch