From 12b7190a309d2754b58a5fdfe40533b5792eaf1c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Mar 2026 13:03:59 +0100 Subject: [PATCH 1/3] fix: prototype safe goal rendering for flake investigation --- RunAt/Plugin.lean | 108 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 107 insertions(+), 1 deletion(-) diff --git a/RunAt/Plugin.lean b/RunAt/Plugin.lean index f06750f8..6c66d093 100644 --- a/RunAt/Plugin.lean +++ b/RunAt/Plugin.lean @@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias import Lean.Server.FileWorker.RequestHandling import Lean.Server.Requests +import Lean.Meta.PPGoal import Lean.Widget.InteractiveGoal import Lean.Compiler.IR import RunAt.ProofSnapshot @@ -89,6 +90,111 @@ private def goalOfInteractive (goal : Lean.Widget.InteractiveGoal) : Goal := hyps := goal.hyps.map goalHypOfInteractive } +private def safePpExprTagged (e : Expr) : + MetaM Lean.Widget.CodeWithInfos := do + if pp.raw.get (← getOptions) then + let e ← if getPPInstantiateMVars (← getOptions) then instantiateMVars e else pure e + return .text (toString e) + let ppCtx : PPContext := { + env := (← getEnv) + mctx := (← getMCtx) + lctx := (← getLCtx) + opts := (← getOptions) + currNamespace := (← getCurrNamespace) + openDecls := (← getOpenDecls) + } + let ⟨fmt, infos⟩ ← liftM <| Lean.ppExprWithInfos ppCtx e + let tt := Lean.Widget.TaggedText.prettyTagged fmt + let ctx : Elab.ContextInfo := { + env := (← getEnv) + mctx := (← getMCtx) + options := (← getOptions) + currNamespace := (← getCurrNamespace) + openDecls := (← getOpenDecls) + fileMap := default + ngen := (← getNGen) + } + Lean.Widget.tagCodeInfos ctx infos tt + +private def addInteractiveHypothesisBundleSafe (hyps : Array Lean.Widget.InteractiveHypothesisBundle) + (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) (tactic := false ) : + MetaM (Array Lean.Widget.InteractiveHypothesisBundle) := do + if ids.size == 0 then + throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle." + let fvarIds := ids.map Prod.snd + let names := ids.map Prod.fst + return hyps.push { + names + fvarIds + type := (← safePpExprTagged type) + val? := (← value?.mapM ppLetValueExprTagged) + isInstance? := if (← Meta.isClass? type).isSome then true else none + isType? := if (← instantiateMVars type).isSort then true else none + } +where + ppLetValueExprTagged (value : Expr) : MetaM Lean.Widget.CodeWithInfos := do + let _ := tactic + safePpExprTagged value + +private def goalToInteractiveSafe (mvarId : MVarId) : MetaM Lean.Widget.InteractiveGoal := do + let ppAuxDecls := (← getOptions).getBool `pp.auxDecls false + let ppImplDetailHyps := (← getOptions).getBool `pp.implementationDetailHyps false + Lean.Widget.withGoalCtx mvarId fun lctx mvarDecl => do + let tactic := mvarDecl.kind.isSyntheticOpaque + let pushPending + (ids : Array (String × FVarId)) + (type? : Option Expr) + (hyps : Array Lean.Widget.InteractiveHypothesisBundle) : + MetaM (Array Lean.Widget.InteractiveHypothesisBundle) := + if ids.isEmpty then + pure hyps + else + match type? with + | none => pure hyps + | some type => addInteractiveHypothesisBundleSafe hyps ids type + let mut varNames : Array (String × FVarId) := #[] + let mut prevType? : Option Expr := none + let mut hyps : Array Lean.Widget.InteractiveHypothesisBundle := #[] + for localDecl in lctx do + if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then + continue + else + match localDecl with + | LocalDecl.cdecl _index fvarId varName type .. + | LocalDecl.ldecl _index fvarId varName type (nondep := true) .. => + let varName := toString varName + let type ← instantiateMVars type + if prevType? == none || prevType? == some type then + varNames := varNames.push (varName, fvarId) + else + hyps ← pushPending varNames prevType? hyps + varNames := #[(varName, fvarId)] + prevType? := some type + | LocalDecl.ldecl _index fvarId varName type val (nondep := false) .. => do + let varName := toString varName + hyps ← pushPending varNames prevType? hyps + let type ← instantiateMVars type + let val ← instantiateMVars val + hyps ← addInteractiveHypothesisBundleSafe hyps #[(varName, fvarId)] type val tactic + varNames := #[] + prevType? := none + hyps ← pushPending varNames prevType? hyps + let goalTp ← instantiateMVars mvarDecl.type + let goalFmt ← safePpExprTagged goalTp + let userName? := match mvarDecl.userName with + | Name.anonymous => none + | name => some <| toString name.eraseMacroScopes + let goalPrefix := + if isLHSGoal? mvarDecl.type |>.isSome then "| " else "⊢ " + return { + hyps + type := goalFmt + ctx := ← WithRpcRef.mk {← Elab.CommandContextInfo.save with } + userName? + goalPrefix + mvarId + } + private structure ExecutionArtifacts where messages : Array RunAt.Message traces : Array String @@ -506,7 +612,7 @@ private def runCommandText (snap : Snapshots.Snapshot) (text : String) : Request private def proofStateOfSnapshot (snapshot : ProofSnapshot) : RequestM ProofState := do let (interactiveGoals, _) ← snapshot.runMetaM do - snapshot.tacticState.goals.mapM Lean.Widget.goalToInteractive + snapshot.tacticState.goals.mapM goalToInteractiveSafe return { goals := interactiveGoals.toArray.map goalOfInteractive } From 73bfabe151cc6e7de5482e2d8e325054cc9ad4a9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Mar 2026 15:52:46 +0100 Subject: [PATCH 2/3] fix: render proof states without widget goals --- RunAt/Plugin.lean | 149 ++++++++++++++++++---------------------------- 1 file changed, 58 insertions(+), 91 deletions(-) diff --git a/RunAt/Plugin.lean b/RunAt/Plugin.lean index 6c66d093..7611914e 100644 --- a/RunAt/Plugin.lean +++ b/RunAt/Plugin.lean @@ -7,7 +7,6 @@ Author: Emilio J. Gallego Arias import Lean.Server.FileWorker.RequestHandling import Lean.Server.Requests import Lean.Meta.PPGoal -import Lean.Widget.InteractiveGoal import Lean.Compiler.IR import RunAt.ProofSnapshot import RunAt.Protocol @@ -75,124 +74,92 @@ private def tracesToStrings (traces : List TraceElem) : IO (Array String) := do traces.toArray.mapM fun trace => do return (← trace.msg.toString) -private def goalHypOfInteractive (hyp : Lean.Widget.InteractiveHypothesisBundle) : GoalHyp := - { - names := hyp.names - type := hyp.type.stripTags - value? := hyp.val?.map (·.stripTags) - } +private def ppExprString (e : Expr) : MetaM String := do + let e ← if getPPInstantiateMVars (← getOptions) then instantiateMVars e else pure e + return (← Meta.ppExpr e).pretty -private def goalOfInteractive (goal : Lean.Widget.InteractiveGoal) : Goal := - { - userName? := goal.userName? - goalPrefix := goal.goalPrefix - target := goal.type.stripTags - hyps := goal.hyps.map goalHypOfInteractive - } - -private def safePpExprTagged (e : Expr) : - MetaM Lean.Widget.CodeWithInfos := do - if pp.raw.get (← getOptions) then - let e ← if getPPInstantiateMVars (← getOptions) then instantiateMVars e else pure e - return .text (toString e) - let ppCtx : PPContext := { - env := (← getEnv) - mctx := (← getMCtx) - lctx := (← getLCtx) - opts := (← getOptions) - currNamespace := (← getCurrNamespace) - openDecls := (← getOpenDecls) - } - let ⟨fmt, infos⟩ ← liftM <| Lean.ppExprWithInfos ppCtx e - let tt := Lean.Widget.TaggedText.prettyTagged fmt - let ctx : Elab.ContextInfo := { - env := (← getEnv) - mctx := (← getMCtx) - options := (← getOptions) - currNamespace := (← getCurrNamespace) - openDecls := (← getOpenDecls) - fileMap := default - ngen := (← getNGen) - } - Lean.Widget.tagCodeInfos ctx infos tt - -private def addInteractiveHypothesisBundleSafe (hyps : Array Lean.Widget.InteractiveHypothesisBundle) - (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) (tactic := false ) : - MetaM (Array Lean.Widget.InteractiveHypothesisBundle) := do - if ids.size == 0 then - throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle." - let fvarIds := ids.map Prod.snd - let names := ids.map Prod.fst - return hyps.push { - names - fvarIds - type := (← safePpExprTagged type) - val? := (← value?.mapM ppLetValueExprTagged) - isInstance? := if (← Meta.isClass? type).isSome then true else none - isType? := if (← instantiateMVars type).isSort then true else none - } -where - ppLetValueExprTagged (value : Expr) : MetaM Lean.Widget.CodeWithInfos := do - let _ := tactic - safePpExprTagged value +private def ppLetValueString? (tactic : Bool) (value : Expr) : MetaM (Option String) := do + if ← Lean.Meta.ppGoal.shouldShowLetValue tactic value then + some <$> ppExprString value + else + pure none + +private def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → MetaM α) : MetaM α := do + let mctx ← getMCtx + let some mvarDecl := mctx.findDecl? goal + | throwError "unknown goal {goal.name}" + let lctx := mvarDecl.lctx |>.sanitizeNames.run' { options := (← getOptions) } + Meta.withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl) + +private def addGoalHypBundle + (hyps : Array GoalHyp) + (names : Array String) + (type : Expr) + (value? : Option Expr := none) + (tactic : Bool := false) : MetaM (Array GoalHyp) := do + if names.isEmpty then + pure hyps + else + let renderedValue? ← + match value? with + | some value => ppLetValueString? tactic value + | none => pure none + return hyps.push { + names + type := ← ppExprString type + value? := renderedValue? + } -private def goalToInteractiveSafe (mvarId : MVarId) : MetaM Lean.Widget.InteractiveGoal := do +private def goalOfMVarId (mvarId : MVarId) : MetaM Goal := do let ppAuxDecls := (← getOptions).getBool `pp.auxDecls false let ppImplDetailHyps := (← getOptions).getBool `pp.implementationDetailHyps false - Lean.Widget.withGoalCtx mvarId fun lctx mvarDecl => do + withGoalCtx mvarId fun lctx mvarDecl => do let tactic := mvarDecl.kind.isSyntheticOpaque let pushPending - (ids : Array (String × FVarId)) + (names : Array String) (type? : Option Expr) - (hyps : Array Lean.Widget.InteractiveHypothesisBundle) : - MetaM (Array Lean.Widget.InteractiveHypothesisBundle) := - if ids.isEmpty then + (hyps : Array GoalHyp) : MetaM (Array GoalHyp) := + if names.isEmpty then pure hyps else match type? with | none => pure hyps - | some type => addInteractiveHypothesisBundleSafe hyps ids type - let mut varNames : Array (String × FVarId) := #[] + | some type => addGoalHypBundle hyps names type (tactic := tactic) + let mut pendingNames : Array String := #[] let mut prevType? : Option Expr := none - let mut hyps : Array Lean.Widget.InteractiveHypothesisBundle := #[] + let mut hyps : Array GoalHyp := #[] for localDecl in lctx do if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then continue else match localDecl with - | LocalDecl.cdecl _index fvarId varName type .. - | LocalDecl.ldecl _index fvarId varName type (nondep := true) .. => + | LocalDecl.cdecl _index _fvarId varName type .. + | LocalDecl.ldecl _index _fvarId varName type (nondep := true) .. => let varName := toString varName let type ← instantiateMVars type if prevType? == none || prevType? == some type then - varNames := varNames.push (varName, fvarId) + pendingNames := pendingNames.push varName else - hyps ← pushPending varNames prevType? hyps - varNames := #[(varName, fvarId)] + hyps ← pushPending pendingNames prevType? hyps + pendingNames := #[varName] prevType? := some type - | LocalDecl.ldecl _index fvarId varName type val (nondep := false) .. => do + | LocalDecl.ldecl _index _fvarId varName type val (nondep := false) .. => do let varName := toString varName - hyps ← pushPending varNames prevType? hyps + hyps ← pushPending pendingNames prevType? hyps let type ← instantiateMVars type let val ← instantiateMVars val - hyps ← addInteractiveHypothesisBundleSafe hyps #[(varName, fvarId)] type val tactic - varNames := #[] + hyps ← addGoalHypBundle hyps #[varName] type (value? := some val) (tactic := tactic) + pendingNames := #[] prevType? := none - hyps ← pushPending varNames prevType? hyps - let goalTp ← instantiateMVars mvarDecl.type - let goalFmt ← safePpExprTagged goalTp + hyps ← pushPending pendingNames prevType? hyps let userName? := match mvarDecl.userName with | Name.anonymous => none | name => some <| toString name.eraseMacroScopes - let goalPrefix := - if isLHSGoal? mvarDecl.type |>.isSome then "| " else "⊢ " return { - hyps - type := goalFmt - ctx := ← WithRpcRef.mk {← Elab.CommandContextInfo.save with } userName? - goalPrefix - mvarId + goalPrefix := Lean.Meta.getGoalPrefix mvarDecl + target := ← ppExprString (← instantiateMVars mvarDecl.type) + hyps } private structure ExecutionArtifacts where @@ -239,7 +206,7 @@ private def mkExecutionResult private def proofStateOfGoals (goals : List MVarId) (ctxInfo : ContextInfo) : RequestM ProofState := do let goals ← goals.mapM fun goal => - return goalOfInteractive (← ctxInfo.runMetaM {} <| Lean.Widget.goalToInteractive goal) + ctxInfo.runMetaM {} <| goalOfMVarId goal return { goals := goals.toArray } private def mkBasisCtxInfo (result : GoalsAtResult) (useAfter : Bool := result.useAfter) : ContextInfo := @@ -612,9 +579,9 @@ private def runCommandText (snap : Snapshots.Snapshot) (text : String) : Request private def proofStateOfSnapshot (snapshot : ProofSnapshot) : RequestM ProofState := do let (interactiveGoals, _) ← snapshot.runMetaM do - snapshot.tacticState.goals.mapM goalToInteractiveSafe + snapshot.tacticState.goals.mapM goalOfMVarId return { - goals := interactiveGoals.toArray.map goalOfInteractive + goals := interactiveGoals.toArray } private def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (text : String) : From b62dedce1330f346503d3ba221f09147febc5c0d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Mar 2026 16:10:24 +0100 Subject: [PATCH 3/3] refactor: simplify plugin proof state rendering --- RunAt/Plugin.lean | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/RunAt/Plugin.lean b/RunAt/Plugin.lean index 7611914e..a6fc8dc8 100644 --- a/RunAt/Plugin.lean +++ b/RunAt/Plugin.lean @@ -204,11 +204,13 @@ private def mkExecutionResult proofState? } -private def proofStateOfGoals (goals : List MVarId) (ctxInfo : ContextInfo) : RequestM ProofState := do - let goals ← goals.mapM fun goal => - ctxInfo.runMetaM {} <| goalOfMVarId goal +private def proofStateOfGoalList (goals : List MVarId) : MetaM ProofState := do + let goals ← goals.mapM goalOfMVarId return { goals := goals.toArray } +private def proofStateOfGoals (goals : List MVarId) (ctxInfo : ContextInfo) : RequestM ProofState := do + ctxInfo.runMetaM {} <| proofStateOfGoalList goals + private def mkBasisCtxInfo (result : GoalsAtResult) (useAfter : Bool := result.useAfter) : ContextInfo := if useAfter then { result.ctxInfo with mctx := result.tacticInfo.mctxAfter } @@ -291,10 +293,9 @@ private def singleLineText (text : String) : String := String.intercalate " " parts private def formatErrorDiagnostic (diagnostic : Lean.Widget.InteractiveDiagnostic) : String := - let diagnostic := Lean.Widget.InteractiveDiagnostic.toDiagnostic diagnostic let line := diagnostic.range.start.line + 1 let character := diagnostic.range.start.character + 1 - s!"{line}:{character}: {singleLineText diagnostic.message}" + s!"{line}:{character}: {singleLineText diagnostic.message.stripTags}" private def summarizeErrorItems (items : Array String) (maxItems : Nat := 3) : String := let limit := Nat.min maxItems items.size @@ -578,11 +579,8 @@ private def runCommandText (snap : Snapshots.Snapshot) (text : String) : Request return (result, nextHandle?) private def proofStateOfSnapshot (snapshot : ProofSnapshot) : RequestM ProofState := do - let (interactiveGoals, _) ← snapshot.runMetaM do - snapshot.tacticState.goals.mapM goalOfMVarId - return { - goals := interactiveGoals.toArray - } + let (proofState, _) ← snapshot.runMetaM <| proofStateOfGoalList snapshot.tacticState.goals + return proofState private def runTacticText (snapshot : ProofSnapshot) (initialProofState : ProofState) (text : String) : RequestM (Result × Option StoredHandleState) := do