diff --git a/RELEASES.md b/RELEASES.md index 32378cc2a6..118cf027c6 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -155,6 +155,18 @@ fact.def : * `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed. +* The `MessageData.ofPPFormat` constructor has been removed. + Its functionality has been split into two: + + - for lazy structured messages, please use `MessageData.lazy`; + - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`. + + An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109). + +* The `MessageData.ofFormat` constructor has been turned into a function. + If you need to inspect `MessageData`, + you can pattern-match on `MessageData.ofFormatWithInfos`. + v4.7.0 --------- diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index a418d20a31..76df17262d 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -332,7 +332,8 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats) We used a similar hack at `Exception.isMaxRecDepth` -/ def Exception.isMaxHeartbeat (ex : Exception) : Bool := match ex with - | Exception.error _ (MessageData.ofFormat (Std.Format.text msg)) => "(deterministic) timeout".isPrefixOf msg + | Exception.error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) => + "(deterministic) timeout".isPrefixOf msg | _ => false /-- Creates the expression `d → b` -/ diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean index e42f45b5d9..6582868034 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -130,7 +130,7 @@ been defined yet. -/ def Exception.isMaxRecDepth (ex : Exception) : Bool := match ex with - | error _ (MessageData.ofFormat (Std.Format.text msg)) => msg == maxRecDepthErrorMessage + | error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) => msg == maxRecDepthErrorMessage | _ => false /-- diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 099ca0fcfb..9e426fcfd8 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -39,13 +39,6 @@ structure NamingContext where currNamespace : Name openDecls : List OpenDecl -/-- Lazily formatted text to be used in `MessageData`. -/ -structure PPFormat where - /-- Pretty-prints text using surrounding context, if any. -/ - pp : Option PPContext → IO FormatWithInfos - /-- Searches for synthetic sorries in original input. Used to filter out certain messages. -/ - hasSyntheticSorry : MetavarContext → Bool := fun _ => false - structure TraceData where /-- Trace class, e.g. `Elab.step`. -/ cls : Name @@ -60,10 +53,9 @@ structure TraceData where /-- Structured message data. We use it for reporting errors, trace messages, etc. -/ inductive MessageData where - /-- Eagerly formatted text. We inspect this in various hacks, so it is not immediately subsumed by `ofPPFormat`. -/ - | ofFormat : Format → MessageData - /-- Lazily formatted text. -/ - | ofPPFormat : PPFormat → MessageData + /-- Eagerly formatted text with info annotations. + This constructor is inspected in various hacks. -/ + | ofFormatWithInfos : FormatWithInfos → MessageData | ofGoal : MVarId → MessageData /-- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/ | withContext : MessageDataContext → MessageData → MessageData @@ -78,12 +70,45 @@ inductive MessageData where Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/ | tagged : Name → MessageData → MessageData | trace (data : TraceData) (msg : MessageData) (children : Array MessageData) - deriving Inhabited + /-- A lazy message. + The provided thunk will not be run until it is about to be displayed. + This can save computation in cases where the message may never be seen, + e.g. when nested inside a collapsed trace. + + The `Dynamic` value is expected to be a `MessageData`, + which is a workaround for the positivity restriction. + + If the thunked message is produced for a term that contains a synthetic sorry, + `hasSyntheticSorry` should return `true`. + This is used to filter out certain messages. -/ + | ofLazy (f : Option PPContext → IO Dynamic) (hasSyntheticSorry : MetavarContext → Bool) + deriving Inhabited, TypeName namespace MessageData +/-- Eagerly formatted text. -/ +def ofFormat (fmt : Format) : MessageData := .ofFormatWithInfos ⟨fmt, .empty⟩ + +/-- +Lazy message data production, with access to the context as given by +a surrounding `MessageData.withContext` (which is expected to exist). +-/ +def lazy (f : PPContext → IO MessageData) + (hasSyntheticSorry : MetavarContext → Bool := fun _ => false) : MessageData := + .ofLazy (hasSyntheticSorry := hasSyntheticSorry) fun ctx? => do + let msg ← match ctx? with + | .none => pure (.ofFormat "(invalid MessageData.lazy, missing context)") + | .some ctx => f ctx + return Dynamic.mk msg + variable (p : Name → Bool) in -/-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag` is true. -/ +/-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag` +is true. + +This does not descend into lazily generated subtress (`.ofLazy`); message tags +of interest (like those added by `logLinter`) are expected to be near the root +of the `MessageData`, and not hidden inside `.ofLazy`. +-/ partial def hasTag : MessageData → Bool | withContext _ msg => hasTag msg | withNamingContext _ msg => hasTag msg @@ -106,26 +131,14 @@ def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext := def ofSyntax (stx : Syntax) : MessageData := -- discard leading/trailing whitespace let stx := stx.copyHeadTailInfoFrom .missing - .ofPPFormat { - pp := fun - | some ctx => ppTerm ctx ⟨stx⟩ -- HACK: might not be a term - | none => return stx.formatStx - } + .lazy fun ctx => ofFormat <$> ppTerm ctx ⟨stx⟩ -- HACK: might not be a term def ofExpr (e : Expr) : MessageData := - .ofPPFormat { - pp := fun - | some ctx => ppExprWithInfos ctx e - | none => return format (toString e) - hasSyntheticSorry := (instantiateMVarsCore · e |>.1.hasSyntheticSorry) - } + .lazy (fun ctx => ofFormatWithInfos <$> ppExprWithInfos ctx e) + (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry) def ofLevel (l : Level) : MessageData := - .ofPPFormat { - pp := fun - | some ctx => ppLevel ctx l - | none => return format l - } + .lazy fun ctx => ofFormat <$> ppLevel ctx l def ofName (n : Name) : MessageData := ofFormat (format n) @@ -133,7 +146,7 @@ partial def hasSyntheticSorry (msg : MessageData) : Bool := visit none msg where visit (mctx? : Option MetavarContext) : MessageData → Bool - | ofPPFormat f => f.hasSyntheticSorry (mctx?.getD {}) + | ofLazy _ f => f (mctx?.getD {}) | withContext ctx msg => visit ctx.mctx msg | withNamingContext _ msg => visit mctx? msg | nest _ msg => visit mctx? msg @@ -144,8 +157,7 @@ where | _ => false partial def formatAux : NamingContext → Option MessageDataContext → MessageData → IO Format - | _, _, ofFormat fmt => return fmt - | nCtx, ctx?, ofPPFormat f => (·.fmt) <$> f.pp (ctx?.map (mkPPContext nCtx)) + | _, _, ofFormatWithInfos fmt => return fmt.1 | _, none, ofGoal mvarId => return "goal " ++ format (mkMVar mvarId) | nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId | nCtx, _, withContext ctx d => formatAux nCtx ctx d @@ -161,6 +173,11 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD msg := f!"{msg} {(← formatAux nCtx ctx header).nest 2}" let children ← children.mapM (formatAux nCtx ctx) return .nest 2 (.joinSep (msg::children.toList) "\n") + | nCtx, ctx?, ofLazy pp _ => do + let dyn ← pp (ctx?.map (mkPPContext nCtx)) + let some msg := dyn.get? MessageData + | panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}" + formatAux nCtx ctx? msg protected def format (msgData : MessageData) : IO Format := formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index 8c1d3e7b37..fa00764e6f 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -8,6 +8,7 @@ import Lean.Util.FindMVar import Lean.Meta.SynthInstance import Lean.Meta.CollectMVars import Lean.Meta.Tactic.Util +import Lean.PrettyPrinter namespace Lean.Meta /-- Controls which new mvars are turned in to goals by the `apply` tactic. @@ -50,8 +51,15 @@ def getExpectedNumArgs (e : Expr) : MetaM Nat := do let (numArgs, _) ← getExpectedNumArgsAux e pure numArgs -private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α := - throwTacticEx `apply mvarId m!"failed to unify{indentExpr eType}\nwith{indentExpr targetType}" +private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α := do + let explanation := MessageData.lazy + (f := fun ppctxt => ppctxt.runMetaM do + let (eType, targetType) ← addPPExplicitToExposeDiff eType targetType + return m!"{indentExpr eType}\nwith{indentExpr targetType}") + (hasSyntheticSorry := fun mvarctxt => + (instantiateMVarsCore mvarctxt eType |>.1.hasSyntheticSorry) || + (instantiateMVarsCore mvarctxt targetType |>.1.hasSyntheticSorry)) + throwTacticEx `apply mvarId m!"failed to unify{explanation}" def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo) (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit := diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 7ea1f5d428..dec7922f5b 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/src/Lean/PrettyPrinter.lean @@ -110,16 +110,14 @@ namespace MessageData open Lean PrettyPrinter Delaborator /-- -Turns a `MetaM FormatWithInfos` into a `MessageData` using `.ofPPFormat` and running the monadic value in the given context. -Uses the `pp.tagAppFns` option to annotate constants with terminfo, which is necessary for seeing the type on mouse hover. +Turns a `MetaM FormatWithInfos` into a `MessageData.lazy` which will run the monadic value. +Uses the `pp.tagAppFns` option to annotate constants with terminfo, +which is necessary for seeing the type on mouse hover. -/ -def ofFormatWithInfos - (fmt : MetaM FormatWithInfos) - (noContext : Unit → Format := fun _ => "") : MessageData := - .ofPPFormat - { pp := fun - | some ctx => ctx.runMetaM <| withOptions (pp.tagAppFns.set · true) fmt - | none => return noContext () } +def ofFormatWithInfosM (fmt : MetaM FormatWithInfos) : MessageData := + .lazy fun ctx => ctx.runMetaM <| + withOptions (pp.tagAppFns.set · true) <| + .ofFormatWithInfos <$> fmt /-- Pretty print a const expression using `delabConst` and generate terminfo. This function avoids inserting `@` if the constant is for a function whose first @@ -127,13 +125,13 @@ argument is implicit, which is what the default `toMessageData` for `Expr` does. Panics if `e` is not a constant. -/ def ofConst (e : Expr) : MessageData := if e.isConst then - .ofFormatWithInfos (PrettyPrinter.ppExprWithInfos (delab := delabConst) e) fun _ => f!"{e}" + .ofFormatWithInfosM (PrettyPrinter.ppExprWithInfos (delab := delabConst) e) else panic! "not a constant" /-- Generates `MessageData` for a declaration `c` as `c.{} : `, with terminfo. -/ def signature (c : Name) : MessageData := - .ofFormatWithInfos (PrettyPrinter.ppSignature c) fun _ => f!"{c}" + .ofFormatWithInfosM (PrettyPrinter.ppSignature c) end MessageData diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean index c895e1f782..9991cd7ac1 100644 --- a/src/Lean/Util/PPExt.lean +++ b/src/Lean/Util/PPExt.lean @@ -40,6 +40,10 @@ structure PPContext where openDecls : List OpenDecl := [] abbrev PrettyPrinter.InfoPerPos := RBMap Nat Elab.Info compare +/-- A format tree with `Elab.Info` annotations. +Each `.tag n _` node is annotated with `infos[n]`. +This is used to attach semantic data such as expressions +to pretty-printer outputs. -/ structure FormatWithInfos where fmt : Format infos : PrettyPrinter.InfoPerPos diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index a5e8be1c91..c572774aaf 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -128,10 +128,8 @@ where } go (nCtx : NamingContext) : Option MessageDataContext → MessageData → MsgFmtM Format - | _, ofFormat fmt => withIgnoreTags fmt - | none, ofPPFormat fmt => (·.fmt) <$> fmt.pp none - | some ctx, ofPPFormat fmt => do - let ⟨fmt, infos⟩ ← fmt.pp (mkPPContext nCtx ctx) + | none, ofFormatWithInfos ⟨fmt, _⟩ => withIgnoreTags fmt + | some ctx, ofFormatWithInfos ⟨fmt, infos⟩ => do let t ← pushEmbed <| EmbedFmt.code (mkContextInfo nCtx ctx) infos return Format.tag t fmt | none, ofGoal mvarId => pure $ "goal " ++ format (mkMVar mvarId) @@ -162,6 +160,11 @@ where pure (.strict (← children.mapM (go nCtx ctx))) let e := .trace data.cls header data.collapsed nodes return .tag (← pushEmbed e) ".\n" + | ctx?, ofLazy f _ => do + let dyn ← f (ctx?.map (mkPPContext nCtx)) + let some msg := dyn.get? MessageData + | throw <| IO.userError "MessageData.ofLazy: expected MessageData in Dynamic" + go nCtx ctx? msg /-- Recursively moves child nodes after the first `blockSize` into a new "more" node. -/ chopUpChildren (cls : Name) (blockSize : Nat) (children : Subarray MessageData) : diff --git a/tests/lean/issue3232.lean b/tests/lean/issue3232.lean new file mode 100644 index 0000000000..5f2201b7b0 --- /dev/null +++ b/tests/lean/issue3232.lean @@ -0,0 +1,11 @@ +inductive foo {n : Nat} : Prop + +-- Check that the error message will print the types with implicit arguments shown +example (h : @foo 42) : @foo 23 := by + apply h + +example : (1 : Nat) = 1 := by + apply (rfl : (1 : Int) = 1) + +example : PUnit.{0} = PUnit.{0} := by + apply Eq.refl PUnit.{1} -- TODO: addPPExplicitToExposeDiff is not handling this yet diff --git a/tests/lean/issue3232.lean.expected.out b/tests/lean/issue3232.lean.expected.out new file mode 100644 index 0000000000..f2e4b023a1 --- /dev/null +++ b/tests/lean/issue3232.lean.expected.out @@ -0,0 +1,16 @@ +issue3232.lean:5:2-5:9: error: tactic 'apply' failed, failed to unify + @foo 42 +with + @foo 23 +h : foo +⊢ foo +issue3232.lean:8:2-8:29: error: tactic 'apply' failed, failed to unify + @OfNat.ofNat Int 1 instOfNat = 1 +with + @OfNat.ofNat Nat 1 (instOfNatNat 1) = 1 +⊢ 1 = 1 +issue3232.lean:11:2-11:25: error: tactic 'apply' failed, failed to unify + PUnit = PUnit +with + PUnit = PUnit +⊢ PUnit = PUnit