sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat: add structured TraceResult to TraceData (#12698)

Browse Source 
This PR adds a `result? : Option TraceResult` field to `TraceData` and
populates it in `withTraceNode` and `withTraceNodeBefore`, so that
metaprograms walking trace trees can determine success/failure
structurally instead of string-matching on emoji.

`TraceResult` has three cases: `.success` (checkEmoji), `.failure`
(crossEmoji), and `.error` (bombEmoji, exception thrown). An
`ExceptToTraceResult` typeclass converts `Except` results to
`TraceResult` directly, with instances for `Bool` and `Option`.
`TraceResult.toEmoji` converts back to emoji for display. This replaces
the previous `ExceptToEmoji` typeclass — `TraceResult` is now the
primary representation rather than being derived from emoji strings.

`withTraceNodeBefore` (used by `isDefEq`) uses
`ExceptToTraceResult.toTraceResult` directly, correctly handling `Bool`
(`.ok false` = failure) and `Option` (`.ok none` = failure), with
`Except.error` mapping to `.error`.

For `withTraceNode`, `result?` defaults to `none`. Callers can pass
`mkResult?` to provide structured results; when set, the corresponding
emoji is auto-prepended to the message.

Motivated by mathlib's `#defeq_abuse` diagnostic tactic
(https://github.com/leanprover-community/mathlib4/pull/35750) which
currently string-matches on emoji to determine trace node outcomes. See
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Kim Morrison
2026-03-10 13:42:57 +11:00
committed by Kim Morrison
parent b1ce232903
commit 04d3ba35de
46 changed files with 331 additions and 278 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Lean/AddDecl.lean
View File

@@ -169,7 +169,7 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
where
doAdd := do
profileitM Exception "type checking" (← getOptions) do
withTraceNode `Kernel (return m!"{exceptEmoji ·} typechecking declarations {decl.getTopLevelNames}") do
withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
warnIfUsesSorry decl
try
let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?

4
src/Lean/Elab/PreDefinition/Eqns.lean
View File

@@ -56,7 +56,7 @@ def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withC
deltaLHS mvarId
private partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
withTraceNode `Elab.definition.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
withTraceNode `Elab.definition.eqns (fun _ => return m!"proving:{indentExpr type}") do
withNewMCtxDepth do
let main ← mkFreshExprSyntheticOpaqueMVar type
let (_, mvarId) ← main.mvarId!.intros
@@ -78,7 +78,7 @@ private partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := d
recursion and structural recursion can and should use this too.
-/
go (mvarId : MVarId) : MetaM Unit := do
withTraceNode `Elab.definition.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
withTraceNode `Elab.definition.eqns (fun _ => return m!"step:\n{MessageData.ofGoal mvarId}") do
if (← tryURefl mvarId) then
return ()
else if (← tryContradiction mvarId) then

2
src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
View File

@@ -118,7 +118,7 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
The dictionary is built using the `PProd` (`And` for inductive predicates).
We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`. -/
partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions) (fnIndex : Nat) (recArg : Expr) : MetaM Expr := do
withTraceNode `Elab.definition.structural (return m!"{exceptEmoji ·} searching IH for {recArg} in {←inferType below}") do
withTraceNode `Elab.definition.structural (fun _ => return m!"searching IH for {recArg} in {←inferType below}") do
withBelowDict below numIndParams positions fun Cs belowDict =>
toBelowAux Cs[fnIndex]! belowDict recArg below

6
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View File

@@ -73,7 +73,7 @@ Creates the proof of the unfolding theorem for `declName` with type `type`. It
is solved using `rfl` or `contradiction`.
-/
partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
withTraceNode `Elab.definition.structural.eqns (fun _ => return m!"proving:{indentExpr type}") do
prependError m!"failed to generate equational theorem for `{.ofConstName declName}`" do
withNewMCtxDepth do
let main ← mkFreshExprSyntheticOpaqueMVar type
@@ -83,7 +83,7 @@ partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
instantiateMVars main
where
goUnfold (mvarId : MVarId) : MetaM Unit := do
withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} goUnfold:\n{MessageData.ofGoal mvarId}") do
withTraceNode `Elab.definition.structural.eqns (fun _ => return m!"goUnfold:\n{MessageData.ofGoal mvarId}") do
let mvarId' ← mvarId.withContext do
-- This should now be headed by `.brecOn`
let goal ← mvarId.getType
@@ -110,7 +110,7 @@ where
go mvarId'
go (mvarId : MVarId) : MetaM Unit := do
withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
withTraceNode `Elab.definition.structural.eqns (fun _ => return m!"step:\n{MessageData.ofGoal mvarId}") do
if (← tryURefl mvarId) then
trace[Elab.definition.structural.eqns] "tryURefl succeeded"
return ()

2
src/Lean/Elab/PreDefinition/WF/Eqns.lean
View File

@@ -53,7 +53,7 @@ So we create a unfold equation generator that aliases an existing private `eq_de
wherever the current module expects it.
-/
def copyPrivateUnfoldTheorem : GetUnfoldEqnFn := fun declName => do
withTraceNode `ReservedNameAction (pure m!"{exceptOptionEmoji ·} copyPrivateUnfoldTheorem running for {declName}") do
withTraceNode `ReservedNameAction (fun _ => pure m!"copyPrivateUnfoldTheorem running for {declName}") do
let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
if let some mod ← findModuleOf? declName then
let unfoldName' := mkPrivateNameCore mod (.str (privateToUserName declName) unfoldThmSuffix)

9
src/Lean/Elab/Tactic/NormCast.lean
View File

@@ -38,7 +38,7 @@ def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) :=
/-- Proves `a = b` by simplifying using move and squash lemmas. -/
def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} proving: {← mkEq a b}") do
withTraceNode `Tactic.norm_cast (fun _ => return m!"proving: {← mkEq a b}") do
proveEqUsing (← normCastExt.down.getTheorems) a b
/-- Constructs the expression `(e : ty)`. -/
@@ -97,9 +97,8 @@ def splittingProcedure (expr : Expr) : MetaM Simp.Result := do
let msg := m!"splitting {expr}"
let msg
| .error _ => return m!"{bombEmoji} {msg}"
| .ok r => return if r.expr == expr then m!"{crossEmoji} {msg}" else
m!"{checkEmoji} {msg} to {r.expr}"
| .error _ => return msg
| .ok r => return if r.expr == expr then msg else m!"{msg} to {r.expr}"
withTraceNode `Tactic.norm_cast msg do
try
@@ -140,7 +139,7 @@ Discharging function used during simplification in the "squash" step.
-- TODO: normCast takes a list of expressions to use as lemmas for the discharger
-- TODO: a tactic to print the results the discharger fails to prove
def prove (e : Expr) : SimpM (Option Expr) := do
withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} discharging: {e}") do
withTraceNode `Tactic.norm_cast (fun _ => return m!"discharging: {e}") do
return (← findLocalDeclWithType? e).map mkFVar
/--

20
src/Lean/Message.lean
View File

@@ -66,9 +66,29 @@ structure NamingContext where
currNamespace : Name
openDecls : List OpenDecl
/-- Structured result status of a trace node action, produced by `withTraceNode` and
`withTraceNodeBefore` and included in the `TraceData` of trace messages. Either
`.success` (✅️), `.failure` (❌️), or `.error` (💥️).
This is used both to render emojis in trace messages and to allow more
robust inspection of trace logs via metaprogramming.
See also `Except.toTraceResult` for converting an `Except ε α` to a `TraceResult`. -/
inductive TraceResult where
/-- The traced action succeeded (✅️, `checkEmoji`). -/
| success
/-- The traced action failed (❌️, `crossEmoji`). -/
| failure
/-- An exception was thrown during the traced action (💥️, `bombEmoji`). -/
| error
deriving Inhabited, BEq, Repr
structure TraceData where
/-- Trace class, e.g. `Elab.step`. -/
cls : Name
/-- Structured success/failure result set by `withTraceNode`/`withTraceNodeBefore`.
`none` for trace nodes not created by these functions (e.g. `addTrace`, diagnostic nodes). -/
result? : Option TraceResult := none
/-- Start time in seconds; 0 if unknown to avoid `Option` allocation. -/
startTime : Float := 0
/-- Stop time in seconds; 0 if unknown to avoid `Option` allocation. -/

3
src/Lean/Meta/AppBuilder.lean
View File

@@ -341,8 +341,7 @@ private def mkFun (constName : Name) : MetaM (Expr × Expr) := do
private def withAppBuilderTrace [ToMessageData α] [ToMessageData β]
(f : α) (xs : β) (k : MetaM Expr) : MetaM Expr :=
let emoji | .ok .. => checkEmoji | .error .. => crossEmoji
withTraceNode `Meta.appBuilder (return m!"{emoji ·} f: {f}, xs: {xs}") do
withTraceNode `Meta.appBuilder (fun _ => return m!"f: {f}, xs: {xs}") do
try
let res ← k
trace[Meta.appBuilder.result] res

4
src/Lean/Meta/Check.lean
View File

@@ -329,8 +329,8 @@ where
Throw an exception if `e` is not type correct.
-/
def check (e : Expr) : MetaM Unit :=
withTraceNode `Meta.check (fun res =>
return m!"{if res.isOk then checkEmoji else crossEmoji} {e}") do
withTraceNode `Meta.check (fun _ =>
return m!"{e}") do
try
withTransparency TransparencyMode.all $ checkAux e
catch ex =>

2
src/Lean/Meta/Eqns.lean
View File

@@ -304,7 +304,7 @@ def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) :
builtin_initialize
registerReservedNameAction fun name => do
withTraceNode `ReservedNameAction (pure m!"{exceptBoolEmoji ·} Lean.Meta.Eqns reserved name action for {name}") do
withTraceNode `ReservedNameAction (fun _ => pure m!"Lean.Meta.Eqns reserved name action for {name}") do
if let some (declName, suffix) := declFromEqLikeName (← getEnv) name then
if name == mkEqLikeNameFor (← getEnv) declName suffix then
if isEqnReservedNameSuffix suffix then

4
src/Lean/Meta/IndPredBelow.lean
View File

@@ -319,7 +319,7 @@ the first `nrealParams` are parameters and the remaining are motives.
public partial def mkBelowMatcher (matcherApp : MatcherApp) (belowParams : Array Expr) (nrealParams : Nat)
(ctx : RecursionContext) (transformAlt : RecursionContext → Expr → MetaM Expr) :
MetaM (Option (Expr × MetaM Unit)) :=
withTraceNode `Meta.IndPredBelow.match (return m!"{exceptEmoji ·} {matcherApp.toExpr} and {belowParams}") do
withTraceNode `Meta.IndPredBelow.match (fun _ => return m!"{matcherApp.toExpr} and {belowParams}") do
let mut input ← getMkMatcherInputInContext matcherApp (unfoldNamed := false)
let mut discrs := matcherApp.discrs
let mut matchTypeAdd := #[] -- #[(discrIdx, ), ...]
@@ -448,7 +448,7 @@ where
StateRefT (Array NewDecl) MetaM (Pattern × Pattern) := do
match originalPattern with
| .ctor ctorName us params fields =>
withTraceNode `Meta.IndPredBelow.match (return m!"{exceptEmoji ·} pattern {← originalPattern.toExpr} to {belowIndName}") do
withTraceNode `Meta.IndPredBelow.match (fun _ => return m!"pattern {← originalPattern.toExpr} to {belowIndName}") do
let ctorInfo ← getConstInfoCtor ctorName
let shortCtorName := ctorName.replacePrefix ctorInfo.induct .anonymous
let belowCtor ← getConstInfoCtor (belowIndName ++ shortCtorName)

6
src/Lean/Meta/Injective.lean
View File

@@ -107,7 +107,7 @@ def mkInjectiveTheoremNameFor (ctorName : Name) : Name :=
private def mkInjectiveTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
let name := mkInjectiveTheoremNameFor ctorVal.name
withTraceNode `Meta.injective (msg := (return m!"{exceptEmoji ·} generating `{name}`")) do
withTraceNode `Meta.injective (msg := (fun _ => return m!"generating `{name}`")) do
let some type ← mkInjectiveTheoremType? ctorVal
| return ()
trace[Meta.injective] "type: {type}"
@@ -164,7 +164,7 @@ private def mkInjectiveEqTheoremValue (ctorVal : ConstructorVal) (targetType : E
private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
let name := mkInjectiveEqTheoremNameFor ctorVal.name
withTraceNode `Meta.injective (msg := (return m!"{exceptEmoji ·} generating `{name}`")) do
withTraceNode `Meta.injective (msg := (fun _ => return m!"generating `{name}`")) do
let some type ← mkInjectiveEqTheoremType? ctorVal
| return ()
trace[Meta.injective] "type: {type}"
@@ -186,7 +186,7 @@ register_builtin_option genInjectivity : Bool := {
def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
if (← getEnv).contains ``Eq.propIntro && genInjectivity.get (← getOptions) && !(← isInductivePredicate declName) then
withTraceNode `Meta.injective (return m!"{exceptEmoji ·} {declName}") do
withTraceNode `Meta.injective (fun _ => return m!"{declName}") do
let info ← getConstInfoInduct declName
unless info.isUnsafe do
-- We need to reset the local context here because `solveEqOfCtorEq` uses

8
src/Lean/Meta/LetToHave.lean
View File

@@ -396,8 +396,8 @@ private partial def visitProj (e : Expr) (structName : Name) (idx : Nat) (struct
return { expr := e.updateProj! struct, type? := lastFieldTy }
private partial def visit (e : Expr) : M Result := do
withTraceNode `Meta.letToHave.debug (fun res =>
return m!"{if res.isOk then checkEmoji else crossEmoji} visit (check := {(← read).check}){indentExpr e}") do
withTraceNode `Meta.letToHave.debug (fun _ =>
return m!"visit (check := {(← read).check}){indentExpr e}") do
match e with
| .bvar .. => throwError "unexpected bound variable {e}"
| .fvar .. => visitFVar e
@@ -415,8 +415,8 @@ end
private def main (e : Expr) : MetaM Expr := do
Prod.fst <$> withTraceNode `Meta.letToHave (fun
| .ok (_, msg) => pure m!"{checkEmoji} {msg}"
| .error ex => pure m!"{crossEmoji} {ex.toMessageData}") do
| .ok (_, msg) => pure msg
| .error ex => pure ex.toMessageData) do
if hasDepLet e then
withTrackingZetaDelta <|
withTransparency TransparencyMode.all <|

2
src/Lean/Meta/LevelDefEq.lean
View File

@@ -132,7 +132,7 @@ mutual
partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool
| Level.succ lhs, Level.succ rhs => isLevelDefEqAux lhs rhs
| lhs, rhs =>
withTraceNode `Meta.isLevelDefEq (return m!"{exceptBoolEmoji ·} {lhs} =?= {rhs}") do
withTraceNode `Meta.isLevelDefEq (fun _ => return m!"{lhs} =?= {rhs}") do
if lhs.getLevelOffset == rhs.getLevelOffset then
return lhs.getOffset == rhs.getOffset
else

4
src/Lean/Meta/Match/Match.lean
View File

@@ -431,7 +431,7 @@ private def isCtorIdxHasNotBit? (e : Expr) : Option FVarId := do
private partial def contradiction (mvarId : MVarId) : MetaM Bool := do
mvarId.withContext do
withTraceNode `Meta.Match.match (msg := (return m!"{exceptBoolEmoji ·} Match.contradiction")) do
withTraceNode `Meta.Match.match (msg := (fun _ => return m!"Match.contradiction")) do
trace[Meta.Match.match] m!"Match.contradiction:\n{mvarId}"
if (← mvarId.contradictionCore {}) then
trace[Meta.Match.match] "Contradiction found!"
@@ -937,7 +937,7 @@ private def processFirstVarDone (p : Problem) : Problem :=
private def tracedForM (xs : Array α) (process : α → StateRefT State MetaM Unit) : StateRefT State MetaM Unit :=
if xs.size > 1 then
for x in xs, i in [:xs.size] do
withTraceNode `Meta.Match.match (msg := (return m!"{exceptEmoji ·} subgoal {i+1}/{xs.size}")) do
withTraceNode `Meta.Match.match (msg := (fun _ => return m!"subgoal {i+1}/{xs.size}")) do
process x
else
for x in xs do

2
src/Lean/Meta/Match/Rewrite.lean
View File

@@ -96,7 +96,7 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
return { expr := e }
let eqnThm := eqns[altIdx]!
try
withTraceNode `Meta.Match.debug (pure m!"{exceptEmoji ·} rewriting with {.ofConstName eqnThm} in{indentExpr e}") do
withTraceNode `Meta.Match.debug (fun _ => pure m!"rewriting with {.ofConstName eqnThm} in{indentExpr e}") do
let eqProof := mkAppN (mkConst eqnThm e.getAppFn.constLevels!) e.getAppArgs
let (hyps, _, eqType) ← forallMetaTelescope (← inferType eqProof)
trace[Meta.Match.debug] "eqProof has type{indentExpr eqType}"

4
src/Lean/Meta/SplitSparseCasesOn.lean
View File

@@ -28,7 +28,7 @@ public def reduceSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
lhs.withApp fun f xs => do
let .const matchDeclName _ := f | throwError "Not a const application"
let some sparseCasesOnInfo ← getSparseCasesOnInfo matchDeclName | throwError "Not a sparse casesOn application"
withTraceNode `Meta.Match.matchEqs (msg := (return m!"{exceptEmoji ·} splitSparseCasesOn")) do
withTraceNode `Meta.Match.matchEqs (msg := (fun _ => return m!"splitSparseCasesOn")) do
if xs.size < sparseCasesOnInfo.arity then
throwError "Not enough arguments for sparse casesOn application"
let majorIdx := sparseCasesOnInfo.majorPos
@@ -52,7 +52,7 @@ public def splitSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
lhs.withApp fun f xs => do
let .const matchDeclName _ := f | throwError "Not a const application"
let some sparseCasesOnInfo ← getSparseCasesOnInfo matchDeclName | throwError "Not a sparse casesOn application"
withTraceNode `Meta.Match.matchEqs (msg := (return m!"{exceptEmoji ·} splitSparseCasesOn")) do
withTraceNode `Meta.Match.matchEqs (msg := (fun _ => return m!"splitSparseCasesOn")) do
try
trace[Meta.Match.matchEqs] "splitSparseCasesOn running on\n{mvarId}"
if xs.size < sparseCasesOnInfo.arity then

12
src/Lean/Meta/SynthInstance.lean
View File

@@ -351,8 +351,8 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext
let localInsts ← getLocalInstances
forallTelescopeReducing mvarType fun xs mvarTypeBody => do
let { subgoals, instVal, instTypeBody } ← getSubgoals lctx localInsts xs inst
withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
withTraceNode `Meta.synthInstance.tryResolve (fun _ => do withMCtx (← getMCtx) do
return m!"{← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
if (← isDefEq mvarTypeBody instTypeBody) then
/-
We set `etaReduce := true`.
@@ -425,7 +425,7 @@ def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
else
withTraceNode `Meta.synthInstance.answer
(fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") do
(fun _ => return m!"{← instantiateMVars (← inferType cNode.mvar)}") do
let answer ← mkAnswer cNode
-- Remark: `answer` does not contain assignable or assigned metavariables.
let key := cNode.key
@@ -573,8 +573,8 @@ def generate : SynthM Unit := do
modify fun s => { s with generatorStack := s.generatorStack.pop }
return
discard do withMCtx mctx do
withTraceNode `Meta.synthInstance
(return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
withTraceNode `Meta.synthInstance.apply
(fun _ => return m!"apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
modifyTop fun gNode => { gNode with currInstanceIdx := idx }
if let some (mctx, subgoals) ← tryResolve mvar inst then
consume { key, mvar, subgoals, mctx, size := 0 }
@@ -875,7 +875,7 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
let opts ← getOptions
let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
withTraceNode `Meta.synthInstance
(return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
(fun _ => return m!"{← instantiateMVars type}") do
withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
withInTypeClassResolution do

8
src/Lean/Meta/Tactic/Backtrack.lean
View File

@@ -110,25 +110,25 @@ private def run (goals : List MVarId) (n : Nat) (curr acc : List MVarId) : MetaM
cfg.proc goals curr
catch e =>
withTraceNode trace
(return m!"{exceptEmoji ·} BacktrackConfig.proc failed: {e.toMessageData}") do
(fun _ => return m!"BacktrackConfig.proc failed: {e.toMessageData}") do
throw e
match procResult? with
| some curr' => run goals n curr' acc
| none =>
match curr with
-- If there are no active goals, return the accumulated goals.
| [] => withTraceNode trace (return m!"{exceptEmoji ·} success!") do
| [] => withTraceNode trace (fun _ => return m!"success!") do
return acc.reverse
| g :: gs =>
-- Discard any goals which have already been assigned.
if ← g.isAssigned then
withTraceNode trace (return m!"{exceptEmoji ·} discarding already assigned goal {g}") do
withTraceNode trace (fun _ => return m!"discarding already assigned goal {g}") do
run goals (n+1) gs acc
else
withTraceNode trace
-- Note: the `addMessageContextFull` ensures we show the goal using the mvar context before
-- the `do` block below runs, potentially unifying mvars in the goal.
(return m!"{exceptEmoji ·} working on: {← addMessageContextFull g}")
(fun _ => return m!"working on: {← addMessageContextFull g}")
do
-- Check if we should suspend the search here:
if (← cfg.suspend g) then

6
src/Lean/Meta/Tactic/FunInd.lean
View File

@@ -287,7 +287,7 @@ fails.
partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M Expr := withoutExporting do
unless e.containsFVar oldIH do
return e
withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} foldAndCollect ({mkFVar oldIH} → {mkFVar newIH})::{indentExpr e}") do
withTraceNode `Meta.FunInd (fun _ => pure m!"foldAndCollect ({mkFVar oldIH} → {mkFVar newIH})::{indentExpr e}") do
let e' ← id do
if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
@@ -496,7 +496,7 @@ def M2.branch {α} (act : M2 α) : M2 α :=
/-- Base case of `buildInductionBody`: Construct a case for the final induction hypothesis. -/
def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (toErase toClear : Array FVarId)
(goal : Expr) (e : Expr) : M2 Expr := do
withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} buildInductionCase:{indentExpr e}") do
withTraceNode `Meta.FunInd (fun _ => pure m!"buildInductionCase:{indentExpr e}") do
let _e' ← foldAndCollect oldIH newIH isRecCall e
let IHs : Array Expr ← M.ask
let IHs ← deduplicateIHs IHs
@@ -611,7 +611,7 @@ as `MVars` as it goes.
partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
(oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M2 Expr := do
withTraceNode `Meta.FunInd
(pure m!"{exceptEmoji ·} buildInductionBody: {oldIH.name} → {newIH.name}\ngoal: {goal}:{indentExpr e}") do
(fun _ => pure m!"buildInductionBody: {oldIH.name} → {newIH.name}\ngoal: {goal}:{indentExpr e}") do
-- if-then-else cause case split:
match_expr e with

11
src/Lean/Meta/Tactic/LibrarySearch.lean
View File

@@ -223,11 +223,6 @@ def mkHeartbeatCheck (leavePercent : Nat) : MetaM (MetaM Bool) := do
else do
return (← getRemainingHeartbeats) < hbThreshold
private def librarySearchEmoji : Except ε (Option α) → String
| .error _ => bombEmoji
| .ok (some _) => crossEmoji
| .ok none => checkEmoji
/--
Interleave x y interleaves the elements of x and y until one is empty and then returns
final elements in other list.
@@ -291,8 +286,6 @@ def librarySearchSymm (searchFn : CandidateFinder) (goal : MVarId) : MetaM (Arra
else
pure $ l1.map (coreGoalCtx, ·)
private def emoji (e : Except ε α) := if e.toBool then checkEmoji else crossEmoji
/-- Create lemma from name and mod. -/
def mkLibrarySearchLemma (lem : Name) (mod : DeclMod) : MetaM Expr := do
let lem ← mkConstWithFreshMVarLevels lem
@@ -319,7 +312,7 @@ private def librarySearchLemma (cfg : ApplyConfig) (act : List MVarId → MetaM
let ((goal, mctx), (name, mod)) := cand
let ppMod (mod : DeclMod) : MessageData :=
match mod with | .none => "" | .mp => " with mp" | .mpr => " with mpr"
withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name}{ppMod mod} ") do
withTraceNode `Tactic.librarySearch (fun _ => return m!"trying {name}{ppMod mod} ") do
setMCtx mctx
let lem ← mkLibrarySearchLemma name mod
let newGoals ← goal.apply lem cfg
@@ -371,7 +364,7 @@ private def librarySearch' (goal : MVarId)
(includeStar : Bool := true)
(collectAll : Bool := false) :
MetaM (Option (Array (List MVarId × MetavarContext))) := do
withTraceNode `Tactic.librarySearch (return m!"{librarySearchEmoji ·} {← goal.getType}") do
withTraceNode `Tactic.librarySearch (fun _ => return m!"{← goal.getType}") do
profileitM Exception "librarySearch" (← getOptions) do
let cfg : ApplyConfig := { allowSynthFailures := true }
let shouldAbort ← mkHeartbeatCheck leavePercentHeartbeats

2
src/Lean/Meta/Tactic/Simp/Main.lean
View File

@@ -434,7 +434,7 @@ but if `Config.letToHave` is enabled then we attempt to transform it into a `hav
If that does not change it, then it is only `dsimp`ed.
-/
def simpLet (e : Expr) : SimpM Result := do
withTraceNode `Debug.Meta.Tactic.simp (return m!"{exceptEmoji ·} let{indentExpr e}") do
withTraceNode `Debug.Meta.Tactic.simp (fun _ => return m!"let{indentExpr e}") do
assert! e.isLet
/-
Recall: `simpLet` is called after `reduceStep` is applied, so `simpLet` is not responsible for zeta reduction.

2
src/Lean/Meta/Tactic/SolveByElim.lean
View File

@@ -54,7 +54,7 @@ def applyTactics (cfg : ApplyConfig := {}) (transparency : TransparencyMode := .
(lemmas : List Expr) (g : MVarId) : MetaM (Lean.Meta.Iterator (List Lean.MVarId)) := do
pure <|
(← Meta.Iterator.ofList lemmas).filterMapM (fun e => observing? do
withTraceNode `Meta.Tactic.solveByElim (return m!"{exceptEmoji ·} trying to apply: {e}") do
withTraceNode `Meta.Tactic.solveByElim (fun _ => return m!"trying to apply: {e}") do
let goals ← withTransparency transparency (g.apply e cfg)
-- When we call `apply` interactively, `Lean.Elab.Tactic.evalApplyLikeTactic`
-- deals with closing new typeclass goals by calling

2
src/Lean/Meta/UnificationHint.lean
View File

@@ -114,7 +114,7 @@ where
tryCandidate candidate : MetaM Bool :=
withTraceNode `Meta.isDefEq.hint
(return m!"{exceptBoolEmoji ·} hint {candidate} at {t} =?= {s}") do
(fun _ => return m!"hint {candidate} at {t} =?= {s}") do
checkpointDefEq do
let cinfo ← getConstInfo candidate
let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar

2
src/Lean/ReservedNameAction.lean
View File

@@ -36,7 +36,7 @@ Note that the handler can throw an exception.
-/
def executeReservedNameAction (name : Name) : CoreM Unit := do
discard <|
withTraceNode `ReservedNameAction (pure m!"{exceptBoolEmoji ·} executeReservedNameAction for {name}") do
withTraceNode `ReservedNameAction (fun _ => pure m!"executeReservedNameAction for {name}") do
(← reservedNameActionsRef.get).anyM (· name)
/--

101
src/Lean/Util/Trace.lean
View File

@@ -255,6 +255,43 @@ instance [always : MonadAlwaysExcept ε m] [STWorld ω m] [BEq α] [Hashable α]
MonadAlwaysExcept ε (MonadCacheT α β m) where
except := let _ := always.except; inferInstance
def bombEmoji := "💥️"
def checkEmoji := "✅️"
def crossEmoji := "❌️"
/-- Convert a `TraceResult` to its emoji representation. -/
def TraceResult.toEmoji : TraceResult → String
| .success => checkEmoji
| .failure => crossEmoji
| .error => bombEmoji
/-- Convert an `Except` result to a `TraceResult`.
`Except.error` always maps to `.error`.
For `Bool`, `.ok false` maps to `.failure`. For `Option`, `.ok none` maps to `.failure`. -/
class ExceptToTraceResult (ε α : Type) where
toTraceResult : Except ε α → TraceResult
instance : ExceptToTraceResult ε Bool where
toTraceResult
| .error _ => .error
| .ok true => .success
| .ok false => .failure
instance : ExceptToTraceResult ε (Option α) where
toTraceResult
| .error _ => .error
| .ok (some _) => .success
| .ok none => .failure
instance (priority := low) : ExceptToTraceResult ε α where
toTraceResult
| .error _ => .error
| .ok _ => .success
/-- Convert an `Except` to a `TraceResult` using the `ExceptToTraceResult` instance. -/
def _root_.Except.toTraceResult [ExceptToTraceResult ε α] (e : Except ε α) : TraceResult :=
ExceptToTraceResult.toTraceResult e
/-- Run the provided action `k`, and log its execution within a trace node.
The message is produced after the action completes, and has access to its return value.
@@ -262,16 +299,20 @@ If it is more convenient to produce the message as part of the computation,
then `Lean.withTraceNode'` can be used instead.
If profiling is enabled, this will also log the runtime of `k`.
A typical invocation might be:
The class `ExceptToTraceResult` is used to convert the result produced by `k` into a `TraceResult`
(success/failure/error), which is stored in `TraceData.result?` and also used to select the
emoji prefix (✅️/❌️/💥️). A typical invocation might be:
```lean4
withTraceNode `isPosTrace (msg := (return m!"{ExceptToEmoji.toEmoji ·} checking positivity")) do
withTraceNode `isPosTrace
(msg := fun _ => return m!"checking positivity") do
return 0 < x
```
The `cls`, `collapsed`, and `tag` arguments are forwarded to the constructor of `TraceData`.
-/
@[inline]
def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Name)
def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m]
[ExceptToTraceResult ε α] (cls : Name)
(msg : Except ε α → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
let opts ← getOptions
if !opts.hasTrace then
@@ -293,7 +334,9 @@ where
return (← MonadExcept.ofExcept res)
let ref ← getRef
let mut m ← try msg res catch _ => pure m!"<exception thrown while producing trace node message>"
let mut data := { cls, collapsed, tag }
let result := res.toTraceResult
m := m!"{result.toEmoji} {m}"
let mut data : TraceData := { cls, collapsed, tag, result? := some result }
if trace.profiler.get opts then
data := { data with startTime := start, stopTime := stop }
addTraceNode oldTraces data ref m
@@ -339,56 +382,19 @@ private meta def expandTraceMacro (id : Syntax) (s : Syntax) : MacroM (TSyntax `
macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
expandTraceMacro id s.raw
def bombEmoji := "💥️"
def checkEmoji := "✅️"
def crossEmoji := "❌️"
/-- Visualize an `Except _ Bool` using a checkmark or cross.
`bombEmoji` is used for `Except.error`. -/
def exceptBoolEmoji : Except ε Bool → String
| .error _ => bombEmoji
| .ok true => checkEmoji
| .ok false => crossEmoji
/-- Visualize an `Except _ (Option _)` using a checkmark or cross.
`bombEmoji` is used for `Except.error`. -/
def exceptOptionEmoji : Except ε (Option α) → String
| .error _ => bombEmoji
| .ok (some _) => checkEmoji
| .ok none => crossEmoji
/-- Visualize an `Except` using a checkmark or a cross.
Unlike `exceptBoolEmoji` this shows `.error` with `crossEmoji`. -/
def exceptEmoji : Except ε α → String
| .error _ => crossEmoji
| .ok _ => checkEmoji
class ExceptToEmoji (ε α : Type) where
/-- Visualize an `Except.ok x` using a checkmark or cross.
By convention, `bombEmoji` is used for `Except.error`. -/
toEmoji : Except ε α → String
instance : ExceptToEmoji ε Bool where
toEmoji := exceptBoolEmoji
instance : ExceptToEmoji ε (Option α) where
toEmoji := exceptOptionEmoji
/--
Similar to `withTraceNode`, but msg is constructed **before** executing `k`.
This is important when debugging methods such as `isDefEq`, and we want to generate the message
before `k` updates the metavariable assignment. The class `ExceptToEmoji` is used to convert
the result produced by `k` into an emoji (e.g., `💥️`, `✅️`, `❌️`).
before `k` updates the metavariable assignment. The class `ExceptToTraceResult` is used to convert
the result produced by `k` into a `TraceResult` (success/failure/error), which is stored in
`TraceData.result?` and also used to select the emoji prefix (✅️/❌️/💥️).
TODO: find better name for this function.
-/
@[inline]
def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
[always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [ExceptToEmoji ε α] (cls : Name)
[always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [ExceptToTraceResult ε α] (cls : Name)
(msg : Unit → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
let opts ← getOptions
if !opts.hasTrace then
@@ -411,8 +417,9 @@ where
unless clsEnabled || aboveThresh do
modifyTraces (oldTraces ++ ·)
return (← MonadExcept.ofExcept res)
let mut msg := m!"{ExceptToEmoji.toEmoji res} {msg}"
let mut data := { cls, collapsed, tag }
let result := res.toTraceResult
let mut msg := m!"{result.toEmoji} {msg}"
let mut data : TraceData := { cls, collapsed, tag, result? := some result }
if trace.profiler.get opts then
data := { data with startTime := start, stopTime := stop }
addTraceNode oldTraces data ref msg

2
tests/bench/workspaceSymbolsNewRanges.lean
View File

@@ -801,7 +801,7 @@ def consts := ["_private.«external:file:///Users/paul/code/lean4/tests/bench/wo
"List.dropLastTR",
"Lean.ScopedEnvExtension.Descr.name._autoParam",
"USize.toISize_and",
"Lean.instExceptToEmojiOption",
"Lean.instExceptToTraceResultOption",
"_private.Init.Data.Nat.Lemmas.0.Nat.min_assoc.match_1_1",
"Lean.PersistentArray.root",
"List.set_drop",

2
tests/elab/setOptionTermTactic.lean.out.expected
View File

@@ -1,5 +1,5 @@
[Meta.synthInstance] 💥️ OfNat ?m 1
[Meta.synthInstance] new goal OfNat ?m 1
[Meta.synthInstance] ✅️ new goal OfNat ?m 1
[Meta.synthInstance.instances] #[@Lean.Grind.Semiring.ofNat, @One.toOfNat1, @Int16.instOfNat, @UInt64.instOfNat, @Rat.instOfNat, @Int8.instOfNat, @instOfNatFloat, @BitVec.instOfNat, Dyadic.instOfNat, @Int64.instOfNat, @instOfNat, @Id.instOfNat, @UInt16.instOfNat, instOfNatNat, @UInt32.instOfNat, @UInt8.instOfNat, @Fin.instOfNat, @ISize.instOfNat, @instOfNatFloat32, @Int32.instOfNat, @USize.instOfNat, @Lean.Grind.CommRing.OfCommSemiring.instOfNatQ]
[Meta.synthInstance.apply] 💥️ apply @Lean.Grind.CommRing.OfCommSemiring.instOfNatQ to OfNat ?m 1
[Meta.synthInstance.tryResolve] 💥️ OfNat ?m 1 ≟ OfNat (Lean.Grind.Ring.OfSemiring.Q ?m) ?m

2
tests/lean/366.lean.expected.out
View File

@@ -1,6 +1,6 @@
366.lean:1:0-2:72: warning: Definition `foo` of class type must be marked with `@[reducible]` or `@[implicit_reducible]`
[Meta.synthInstance] ✅️ Inhabited Nat
[Meta.synthInstance] new goal Inhabited Nat
[Meta.synthInstance] ✅️ new goal Inhabited Nat
[Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
[Meta.synthInstance] ✅️ apply instInhabitedNat to Inhabited Nat
[Meta.synthInstance.tryResolve] ✅️ Inhabited Nat ≟ Inhabited Nat

42
tests/lean/815b.lean.expected.out
View File

@@ -6,13 +6,13 @@
815b.lean:10:9-10:13: warning: declaration uses `sorry`
815b.lean:11:9-11:13: warning: declaration uses `sorry`
[Meta.synthInstance] ✅️ IsSmooth fun g a => f (g a) d
[Meta.synthInstance] new goal IsSmooth fun g a => f (g a) d
[Meta.synthInstance] ✅️ new goal IsSmooth fun g a => f (g a) d
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance] ❌️ apply inst✝ to IsSmooth fun g a => f (g a) d
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g a => f (g a) d ≟ IsSmooth f
[Meta.synthInstance] ✅️ apply @swap to IsSmooth fun g a => f (g a) d
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance] ✅️ new goal ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth f
@@ -23,19 +23,19 @@
IsSmooth f
Transformer
fun redf a => redf
[Meta.synthInstance] new goal IsSmooth f
[Meta.synthInstance] ✅️ new goal IsSmooth f
[Meta.synthInstance.instances] #[inst✝]
[Meta.synthInstance] ✅️ apply inst✝ to IsSmooth f
[Meta.synthInstance.tryResolve] ✅️ IsSmooth f ≟ IsSmooth f
[Meta.synthInstance.answer] ✅️ IsSmooth f
[Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] ✅️ propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
has unused arguments, reduced type
IsSmooth f
Transformer
fun redf a => redf
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth f to subgoal ∀ (a : α), IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 2
[Meta.synthInstance.unusedArgs] ∀ (a : α) (b : β), IsSmooth (f b)
@@ -43,7 +43,7 @@
∀ (b : β), IsSmooth (f b)
Transformer
fun redf a => redf
[Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b)
[Meta.synthInstance] ✅️ new goal ∀ (b : β), IsSmooth (f b)
[Meta.synthInstance.instances] #[inst✝]
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (b : β), IsSmooth (f b)
[Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth f
@@ -51,13 +51,13 @@
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
[Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance] ✅️ new goal ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) ≟ IsSmooth f
[Meta.synthInstance] ✅️ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1
[Meta.synthInstance] new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance] ✅️ new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
@@ -68,7 +68,7 @@
IsSmooth f
Transformer
fun redf a a_1 => redf
[Meta.synthInstance.resume] propagating ∀ (a : α) (a : δ),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α) (a : δ),
IsSmooth f to subgoal ∀ (a : α) (a : δ), IsSmooth f of ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ) (b : β), IsSmooth (f b)
@@ -99,10 +99,10 @@
IsSmooth f
Transformer
fun redf a => redf
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth f to subgoal ∀ (a : α), IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance] ✅️ new goal ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth f
@@ -117,7 +117,7 @@
IsSmooth fun g => g
Transformer
fun redf a => redf
[Meta.synthInstance] new goal IsSmooth fun g => g
[Meta.synthInstance] ✅️ new goal IsSmooth fun g => g
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
[Meta.synthInstance] ❌️ apply inst✝ to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth f
@@ -134,7 +134,7 @@
[Meta.synthInstance] ✅️ apply @identity to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun a => a
[Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
[Meta.synthInstance.resume] propagating IsSmooth fun a =>
[Meta.synthInstance.resume] ✅️ propagating IsSmooth fun a =>
a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
@@ -142,15 +142,15 @@
IsSmooth fun g => g
Transformer
fun redf a => redf
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a => a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 2
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of IsSmooth fun g => g
[Meta.synthInstance.resume] size: 3
[Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
[Meta.synthInstance.resume] propagating IsSmooth fun b a =>
[Meta.synthInstance.resume] ✅️ propagating IsSmooth fun b a =>
b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 4
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
@@ -158,24 +158,24 @@
IsSmooth fun g => g
Transformer
fun redf a => redf
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun b a => b a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 8
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a => a to subgoal ∀ (a : α), IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 5
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] size: 4
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a_1 =>
f (a_1 a) to subgoal ∀ (a : α), IsSmooth fun g => f (g a) of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 5
[Meta.synthInstance.answer] ✅️ ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] propagating ∀ (a : α),
[Meta.synthInstance.resume] ✅️ propagating ∀ (a : α),
IsSmooth fun a_1 =>
f (a_1 a) d to subgoal ∀ (a : α), IsSmooth fun g => f (g a) d of IsSmooth fun g a => f (g a) d
[Meta.synthInstance.resume] size: 6

4
tests/lean/973b.lean.expected.out
View File

@@ -1,6 +1,6 @@
973b.lean:5:8-5:10: warning: declaration uses `sorry`
[Meta.Tactic.simp.discharge] ex discharge ❌️
[Meta.Tactic.simp.discharge] ✅️ ex discharge ❌️
?p x
[Meta.Tactic.simp.discharge] ex discharge ❌️
[Meta.Tactic.simp.discharge] ✅️ ex discharge ❌️
?p (f x)
973b.lean:9:8-9:11: warning: declaration uses `sorry`

6
tests/lean/exceptionalTrace.lean.expected.out
View File

@@ -1,9 +1,9 @@
exceptionalTrace.lean:7:0-7:13: error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
[Elab.step] expected type: <not-available>, term
[Elab.step] 💥️ expected type: <not-available>, term
rt + 1
[Elab.step] expected type: <not-available>, term
[Elab.step] 💥️ expected type: <not-available>, term
binop% HAdd.hAdd✝ rt 1
[Elab.step] expected type: <not-available>, term
[Elab.step] 💥️ expected type: <not-available>, term
rt

33
tests/lean/interactive/highlightMatches.lean.expected.out
View File

@@ -14,7 +14,11 @@
"msg":
{"tag":
[{"trace":
{"msg": {"tag": [{"expr": {"text": "root"}}, {"text": ""}]},
{"msg":
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag": [{"expr": {"text": "root"}}, {"text": ""}]}]},
"indent": 0,
"collapsed": true,
"cls": "Meta.debug",
@@ -22,7 +26,11 @@
{"text": ""}]}}
{"tag":
[{"trace":
{"msg": {"tag": [{"expr": {"text": "root"}}, {"text": ""}]},
{"msg":
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag": [{"expr": {"text": "root"}}, {"text": ""}]}]},
"indent": 0,
"collapsed": false,
"cls": "Meta.debug",
@@ -31,9 +39,12 @@
[{"tag":
[{"trace":
{"msg":
{"tag":
[{"expr": {"tag": ["highlighted", {"text": "child1"}]}},
{"text": ""}]},
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag":
[{"expr": {"tag": ["highlighted", {"text": "child1"}]}},
{"text": ""}]}]},
"indent": 2,
"collapsed": false,
"cls": "Meta.debug",
@@ -84,7 +95,11 @@
{"text": ""}]},
{"tag":
[{"trace":
{"msg": {"tag": [{"expr": {"text": "child2"}}, {"text": ""}]},
{"msg":
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag": [{"expr": {"text": "child2"}}, {"text": ""}]}]},
"indent": 2,
"collapsed": true,
"cls": "Meta.debug",
@@ -92,7 +107,11 @@
{"text": ""}]},
{"tag":
[{"trace":
{"msg": {"tag": [{"expr": {"text": "child3"}}, {"text": ""}]},
{"msg":
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag": [{"expr": {"text": "child3"}}, {"text": ""}]}]},
"indent": 2,
"collapsed": true,
"cls": "Meta.debug",

24
tests/lean/interactive/interactiveTraces.lean.expected.out
View File

@@ -17,7 +17,11 @@
"message":
{"tag":
[{"trace":
{"msg": {"tag": [{"expr": {"text": "root"}}, {"text": ""}]},
{"msg":
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag": [{"expr": {"text": "root"}}, {"text": ""}]}]},
"indent": 0,
"collapsed": false,
"cls": "Meta.debug",
@@ -25,7 +29,11 @@
{"strict":
[{"tag":
[{"trace":
{"msg": {"tag": [{"expr": {"text": "child1"}}, {"text": ""}]},
{"msg":
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag": [{"expr": {"text": "child1"}}, {"text": ""}]}]},
"indent": 2,
"collapsed": false,
"cls": "Meta.debug",
@@ -58,7 +66,11 @@
{"text": ""}]},
{"tag":
[{"trace":
{"msg": {"tag": [{"expr": {"text": "child2"}}, {"text": ""}]},
{"msg":
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag": [{"expr": {"text": "child2"}}, {"text": ""}]}]},
"indent": 2,
"collapsed": false,
"cls": "Meta.debug",
@@ -83,7 +95,11 @@
{"text": ""}]},
{"tag":
[{"trace":
{"msg": {"tag": [{"expr": {"text": "child3"}}, {"text": ""}]},
{"msg":
{"append":
[{"tag": [{"expr": {"text": "✅️"}}, {"text": ""}]},
{"tag": [{"expr": {"text": " "}}, {"text": ""}]},
{"tag": [{"expr": {"text": "child3"}}, {"text": ""}]}]},
"indent": 2,
"collapsed": false,
"cls": "Meta.debug",

4
tests/lean/partialSyntaxTraces.lean.expected.out
View File

@@ -1,6 +1,6 @@
partialSyntaxTraces.lean:6:0: error: unexpected end of input; expected ':=', 'where' or '|'
[Elab.command] [Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.]
[Elab.command] 💥️ [Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.]
(Command.declaration
(Command.declModifiers [] [] [] [] [] [] [])
(Command.definition "def" (Command.declId `f []) (Command.optDeclSig [] []) (Command.whereStructInst <missing>)))
[Elab.command]
[Elab.command] ✅️

6
tests/lean/run/1234.lean
View File

@@ -17,7 +17,7 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
k ≤ v - 1
==>
True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
[Meta.Tactic.simp.discharge] ✅️ succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000:
0 < v
@@ -57,7 +57,7 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
k ≤ v - 1
==>
True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
[Meta.Tactic.simp.discharge] ✅️ succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000:
0 < v
@@ -95,7 +95,7 @@ trace: [Meta.Tactic.simp.rewrite] h₁:1000:
k ≤ v - 1
==>
True
[Meta.Tactic.simp.discharge] succ_pred_eq_of_pos discharge ✅️
[Meta.Tactic.simp.discharge] ✅️ succ_pred_eq_of_pos discharge ✅️
0 < v
[Meta.Tactic.simp.rewrite] h₂:1000:
0 < v

2
tests/lean/run/1380.lean
View File

@@ -17,7 +17,7 @@ trace: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
?a = ?a
with
v₂ = v₁
[Meta.Tactic.simp.discharge] Nat.ne_of_gt discharge ✅️
[Meta.Tactic.simp.discharge] ✅️ Nat.ne_of_gt discharge ✅️
v₁ < v₂
[Meta.Tactic.simp.rewrite] hv:1000:
v₁ < v₂

2
tests/lean/run/3257.lean
View File

@@ -14,7 +14,7 @@ example : U := by
simp [foo, T.mk]
/--
trace: [Meta.Tactic.simp.discharge] bar discharge ✅️
trace: [Meta.Tactic.simp.discharge] ✅️ bar discharge ✅️
autoParam T bar._auto_1
[Meta.Tactic.simp.rewrite] T.mk:1000:
T

2
tests/lean/run/grind_field_panic.lean
View File

@@ -62,7 +62,7 @@ initialize registerTraceClass `Elab.fast_instance
private partial def makeFastInstance (provided : Expr) (trace : Array Name := #[]) :
MetaM Expr := withReducible do
let ty ← inferType provided
withTraceNode `Elab.fast_instance (fun e => return m!"{exceptEmoji e} type: {ty}") do
withTraceNode `Elab.fast_instance (fun _ => return m!"type: {ty}") do
let some className ← isClass? ty | failure
trace[Elab.fast_instance] "class is {className}"
if ← withDefault <| Meta.isProp ty then failure

40
tests/lean/run/infoFromFailure.lean
View File

@@ -15,49 +15,49 @@ set_option trace.Meta.synthInstance true
info: B.foo "hello" : String × String
---
trace: [Meta.synthInstance] ❌️ Add String
[Meta.synthInstance] new goal Add String
[Meta.synthInstance] ✅️ new goal Add String
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
[Meta.synthInstance] new goal Lean.Grind.Semiring String
[Meta.synthInstance] ✅️ new goal Lean.Grind.Semiring String
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring]
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String
[Meta.synthInstance] new goal Lean.Grind.CommSemiring String
[Meta.synthInstance] ✅️ new goal Lean.Grind.CommSemiring String
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring]
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring String ≟ Lean.Grind.CommSemiring String
[Meta.synthInstance] new goal Lean.Grind.CommRing String
[Meta.synthInstance] ✅️ new goal Lean.Grind.CommRing String
[Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing String ≟ Lean.Grind.CommRing String
[Meta.synthInstance] no instances for Lean.Grind.Field String
[Meta.synthInstance] ✅️ no instances for Lean.Grind.Field String
[Meta.synthInstance.instances] #[]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String
[Meta.synthInstance] new goal Lean.Grind.Ring String
[Meta.synthInstance] ✅️ new goal Lean.Grind.Ring String
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String
[Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add String
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
[Meta.synthInstance] new goal Lean.Grind.AddCommMonoid String
[Meta.synthInstance] ✅️ new goal Lean.Grind.AddCommMonoid String
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
[Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
[Meta.synthInstance] new goal Lean.Grind.NatModule String
[Meta.synthInstance] ✅️ new goal Lean.Grind.NatModule String
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
[Meta.synthInstance] new goal Lean.Grind.IntModule String
[Meta.synthInstance] ✅️ new goal Lean.Grind.IntModule String
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
[Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
[Meta.synthInstance] new goal Lean.Grind.AddCommGroup String
[Meta.synthInstance] ✅️ new goal Lean.Grind.AddCommGroup String
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup String
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
@@ -72,49 +72,49 @@ trace: [Meta.synthInstance] ❌️ Add String
/--
trace: [Meta.synthInstance] ❌️ Add Bool
[Meta.synthInstance] new goal Add Bool
[Meta.synthInstance] ✅️ new goal Add Bool
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
[Meta.synthInstance] new goal Lean.Grind.Semiring Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.Semiring Bool
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring]
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool
[Meta.synthInstance] new goal Lean.Grind.CommSemiring Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.CommSemiring Bool
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring]
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring Bool ≟ Lean.Grind.CommSemiring Bool
[Meta.synthInstance] new goal Lean.Grind.CommRing Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.CommRing Bool
[Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing Bool ≟ Lean.Grind.CommRing Bool
[Meta.synthInstance] no instances for Lean.Grind.Field Bool
[Meta.synthInstance] ✅️ no instances for Lean.Grind.Field Bool
[Meta.synthInstance.instances] #[]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool
[Meta.synthInstance] new goal Lean.Grind.Ring Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.Ring Bool
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool
[Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add Bool
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
[Meta.synthInstance] new goal Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
[Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance] new goal Lean.Grind.NatModule Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.NatModule Bool
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
[Meta.synthInstance] new goal Lean.Grind.IntModule Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.IntModule Bool
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
[Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
[Meta.synthInstance] new goal Lean.Grind.AddCommGroup Bool
[Meta.synthInstance] ✅️ new goal Lean.Grind.AddCommGroup Bool
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup Bool
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool

8
tests/lean/run/trace.lean
View File

@@ -54,13 +54,13 @@ withReader
(tryCatch (tryFinally x printTraces) (fun _ => IO.println "ERROR"))
/--
info: [module] message
info: [module] 💥️ message
[module] hello
world
[bughunt] at test2
ERROR
---
trace: [module] message
trace: [module] 💥️ message
[module] hello
world
[bughunt] at test2
@@ -69,7 +69,7 @@ trace: [module] message
#eval run (tst3 true)
/--
info: [module] message
info: [module] ✅️ message
[module] hello
world
[bughunt] at test2
@@ -79,7 +79,7 @@ info: [module] message
world
[bughunt] at end of tst3
---
trace: [module] message
trace: [module] ✅️ message
[module] hello
world
[bughunt] at test2

6
tests/lean/run/trace_synth.lean
View File

@@ -22,11 +22,11 @@ error: failed to synthesize instance of type class
Foo "two"
---
trace: [Meta.synthInstance] ❌️ Foo "two"
[Meta.synthInstance] new goal Foo "two"
[Meta.synthInstance] ✅️ new goal Foo "two"
[Meta.synthInstance.instances] #[@instFoo_1]
[Meta.synthInstance] ✅️ apply @instFoo_1 to Foo "two"
[Meta.synthInstance.tryResolve] ✅️ Foo "two" ≟ Foo "two"
[Meta.synthInstance] no instances for Foo "three"
[Meta.synthInstance] ✅️ no instances for Foo "three"
[Meta.synthInstance.instances] #[]
[Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ Foo "two"
@@ -41,7 +41,7 @@ error: failed to synthesize instance of type class
Foo "three"
---
trace: [Meta.synthInstance] ❌️ Foo "three"
[Meta.synthInstance] no instances for Foo "three"
[Meta.synthInstance] ✅️ no instances for Foo "three"
[Meta.synthInstance.instances] #[]
[Meta.synthInstance] result <not-available>
[Meta.synthInstance] ❌️ Foo "three"

12
tests/lean/sanitizeMacroScopes.lean.expected.out
View File

@@ -1,17 +1,17 @@
fun x x_1 => x : (x : ?m) → ?m x → ?m
[Elab.step] expected type: <not-available>, term
[Elab.step] ✅️ expected type: <not-available>, term
fun x => m x
[Elab.step] expected type: Sort ?u, term
[Elab.step] ✅️ expected type: Sort ?u, term
_
[Elab.step.result] ?m
[Elab.step] expected type: <not-available>, term
[Elab.step] ✅️ expected type: <not-available>, term
m x
[Elab.step] expected type: <not-available>, term
[Elab.step] ✅️ expected type: <not-available>, term
fun x✝ => x
[Elab.step] expected type: Sort ?u, term
[Elab.step] ✅️ expected type: Sort ?u, term
_
[Elab.step.result] ?m
[Elab.step] expected type: <not-available>, term
[Elab.step] ✅️ expected type: <not-available>, term
x
[Elab.step.result] x
[Elab.step.result] fun x_1 => x

152
tests/lean/snapshotTree.lean.expected.out
View File

@@ -1,78 +1,78 @@
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] Lean.Elab.Command.elabMutualDef⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨15, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ⟨15, 2⟩-⟨15, 9⟩
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨16, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ⟨16, 2⟩-⟨16, 11⟩
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] Lean.cdot⟨17, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] Lean.Parser.Tactic.«tacticNext_=>_»⟨17, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] Lean.Parser.Tactic.induction<range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo⟨18, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo<no range>
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨19, 4⟩-⟨21, 13⟩
[Elab.snapshotTree] ⟨20, 6⟩-⟨20, 15⟩
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨21, 6⟩-⟨21, 13⟩
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] Lean.Parser.Tactic.sleep⟨22, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] ⟨23, 6⟩-⟨23, 15⟩
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] Lean.Parser.Tactic.tacticTrivial⟨24, 6⟩-⟨24, 13⟩
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩
[Elab.snapshotTree] _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] Lean.Parser.Tactic.apply<range inherited>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] <range inherited>
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabFunValues⟨14, 0⟩-⟨14, 0⟩
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] <no range>
[Elab.snapshotTree] _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask<no range>
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] ✅️ Lean.Language.instInhabitedDynamicSnapshot⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨13, 0⟩-⟨13, 39⟩
[Elab.snapshotTree] ✅️ Lean.Elab.Command.runLintersAsync<range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] ✅️ Lean.Elab.Command.elabMutualDef⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.sleep⟨15, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ ⟨15, 2⟩-⟨15, 9⟩
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.sleep⟨16, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ ⟨16, 2⟩-⟨16, 11⟩
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ Lean.cdot⟨17, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.«tacticNext_=>_»⟨17, 2⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨17, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.induction<range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo⟨18, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.evalAlts.goWithInfo<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.sleep⟨19, 4⟩-⟨21, 13⟩
[Elab.snapshotTree] ✅️ ⟨20, 6⟩-⟨20, 15⟩
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.tacticTrivial⟨21, 6⟩-⟨21, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨21, 6⟩-⟨21, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.apply<range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.sleep⟨22, 4⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ ⟨23, 6⟩-⟨23, 15⟩
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.tacticTrivial⟨24, 6⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval⟨24, 6⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.Basic.0.Lean.Elab.Tactic.evalTactic.expandEval<no range>
[Elab.snapshotTree] ✅️ Lean.Parser.Tactic.apply<range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.Tactic.BuiltinTactic.0.Lean.Elab.Tactic.evalSepTactics.goEven<no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabFunValues⟨14, 0⟩-⟨14, 0⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨14, 0⟩-⟨24, 13⟩
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ <no range>
[Elab.snapshotTree] ✅️ _private.Lean.Elab.MutualDef.0.Lean.Elab.Term.logGoalsAccomplishedSnapshotTask<no range>
• Goals accomplished!
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] Lean.Language.instInhabitedDynamicSnapshot⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] Lean.Elab.Command.runLintersAsync<range inherited>
[Elab.snapshotTree] ✅️ Lean.Elab.Command.runLintersAsync<range inherited>
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd<no range>
[Elab.snapshotTree] ✅️ Lean.Language.instInhabitedDynamicSnapshot⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] ✅️ _private.Lean.Language.Lean.0.Lean.Language.Lean.process.parseCmd⟨25, 0⟩-⟨25, 0⟩
[Elab.snapshotTree] ✅️ Lean.Elab.Command.runLintersAsync<range inherited>

6
tests/lean/syntaxPrec.lean.expected.out
View File

@@ -1,10 +1,10 @@
syntaxPrec.lean:1:17-1:21: error: unexpected token '<|>'; expected ':'
[Elab.command] @[term_parser 1000]
[Elab.command] ✅️ @[term_parser 1000]
public meta def «termFoo*_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `«termFoo*_» 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
(ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) ","
(ParserDescr.symbol✝ ", ") Bool.false✝)))
[Elab.command] syntax "foo" ("*" <|> term,+) : term
[Elab.command]
[Elab.command] ✅️ syntax "foo" ("*" <|> term,+) : term
[Elab.command] ✅️

24
tests/lean/traceTacticSteps.lean.expected.out
View File

@@ -1,31 +1,31 @@
[Elab.step] expected type: Prop, term
[Elab.step] ✅️ expected type: Prop, term
True
[Elab.step.result] True
[Elab.step] expected type: True, term
[Elab.step] ✅️ expected type: True, term
by
skip
trivial
[Elab.step.result] ?m
[Elab.step]
[Elab.step] ✅️
skip
trivial
[Elab.step]
[Elab.step] ✅️
skip
trivial
[Elab.step] skip
[Elab.step] trivial
[Elab.step] (apply And.intro✝) <;> trivial
[Elab.step] focus
[Elab.step] ✅️ skip
[Elab.step] ✅️ trivial
[Elab.step] 💥️ (apply And.intro✝) <;> trivial
[Elab.step] 💥️ focus
apply And.intro✝
with_annotate_state"<;>" skip
all_goals trivial
[Elab.step]
[Elab.step] 💥️
apply And.intro✝
with_annotate_state"<;>" skip
all_goals trivial
[Elab.step]
[Elab.step] 💥️
apply And.intro✝
with_annotate_state"<;>" skip
all_goals trivial
[Elab.step] apply And.intro✝
[Elab.step] apply True.intro✝
[Elab.step] 💥️ apply And.intro✝
[Elab.step] ✅️ apply True.intro✝