Report errors in import statements.

REPL/Frontend.lean

@@ -19,8 +19,9 @@ def processCommandsWithInfoTrees
     (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
     (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
   let commandState := { commandState with infoState.enabled := true }
+  let oldMessages := commandState.messages.toList
   let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.toList, s.infoState.trees.toList)
+  pure (s, oldMessages ++ s.messages.toList, s.infoState.trees.toList)
 
 /--
 Process some text input, with or without an existing command state.

REPL/JSON.lean

@@ -6,6 +6,9 @@ Authors: Scott Morrison
 import Lean.Data.Json
 import Lean.Message
 import Lean.Elab.InfoTree.Main
+import Lean.Meta.Basic
+import Lean.Meta.CollectMVars
+import REPL.Lean.InfoTree.ToJson
 
 open Lean Elab InfoTree
 
@@ -19,6 +22,7 @@ structure CommandOptions where
   Anything else is ignored.
   -/
   infotree : Option String
+  proofTrees : Option Bool := none
 
 /-- Run Lean commands.
 If `env = none`, starts a new session (in which you can use `import`).
@@ -34,6 +38,11 @@ structure File extends CommandOptions where
   path : System.FilePath
 deriving FromJson
 
+structure PruneSnapshots where
+  cmdFromId : Option Nat
+  proofFromId : Option Nat
+deriving ToJson, FromJson
+
 /--
 Run a tactic in a proof state.
 -/
@@ -71,11 +80,29 @@ def Message.of (m : Lean.Message) : IO Message := do pure <|
     | .error => .error,
     data := (← m.data.toString).trim }
 
+structure HypothesisInfo where
+  username : String
+  type : String
+  value : Option String
+  -- unique identifier for the hypothesis, fvarId
+  id : String
+  isProof : String
+  deriving Inhabited, ToJson, FromJson
+
+structure GoalInfo where
+  username : String
+  type : String
+  hyps : List HypothesisInfo
+  -- unique identifier for the goal, mvarId
+  id : MVarId
+  deriving Inhabited, ToJson, FromJson
+
 /-- A Lean `sorry`. -/
 structure Sorry where
   pos : Pos
   endPos : Pos
   goal : String
+  goalInfo: Option GoalInfo
   /--
   The index of the proof state at the sorry.
   You can use the `ProofStep` instruction to run a tactic at this state.
@@ -86,16 +113,20 @@ deriving FromJson
 instance : ToJson Sorry where
   toJson r := Json.mkObj <| .flatten [
     [("goal", r.goal)],
+    match r.goalInfo with
+    | some goalInfo => [("goalInfo", toJson goalInfo)]
+    | none => [],
     [("proofState", toJson r.proofState)],
     if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [],
     if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [],
   ]
 
 /-- Construct the JSON representation of a Lean sorry. -/
-def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry :=
+def Sorry.of (goal : String) (goalInfo : Option GoalInfo) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
     goal,
+    goalInfo,
     proofState }
 
 structure Tactic where
@@ -116,6 +147,83 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState :
     proofState,
     usedConstants }
 
+private def mayBeProof (expr : Expr) : MetaM String := do
+  let type : Expr ← Lean.Meta.inferType expr
+  if ← Meta.isProof expr then
+    return "proof"
+  if type.isSort then
+    return "universe"
+  else
+    return "data"
+
+def printGoalInfo (printCtx : ContextInfo) (id : MVarId) : IO GoalInfo := do
+  let some decl := printCtx.mctx.findDecl? id
+    | panic! "printGoalInfo: goal not found in the mctx"
+  -- to get tombstones in name ✝ for unreachable hypothesis
+  let lctx := decl.lctx |>.sanitizeNames.run' {options := {}}
+  let ppContext := printCtx.toPPContext lctx
+
+  let hyps ← lctx.foldrM (init := []) (fun hypDecl acc => do
+    if hypDecl.isAuxDecl || hypDecl.isImplementationDetail then
+      return acc
+
+    let type ← liftM (ppExprWithInfos ppContext hypDecl.type)
+    let value ← liftM (hypDecl.value?.mapM (ppExprWithInfos ppContext))
+    let isProof : String ← printCtx.runMetaM decl.lctx (mayBeProof hypDecl.toExpr)
+    return ({
+      username := hypDecl.userName.toString,
+      type := type.fmt.pretty,
+      value := value.map (·.fmt.pretty),
+      id := hypDecl.fvarId.name.toString,
+      isProof := isProof,
+    } : HypothesisInfo) :: acc)
+  return ⟨ decl.userName.toString, (← ppExprWithInfos ppContext decl.type).fmt.pretty, hyps, id⟩
+
+
+instance : BEq GoalInfo where
+  beq g1 g2 := g1.id == g2.id
+
+instance : Hashable GoalInfo where
+  hash g := hash g.id
+structure MetavarDecl.Json where
+  mvarId : String
+  userName : String
+  type : String
+  mvarsInType : List MVarId
+  value : Option String
+deriving ToJson, FromJson
+
+structure MetavarContext.Json where
+  decls : Array MetavarDecl.Json
+deriving ToJson, FromJson
+
+def MetavarContext.toJson (mctx : MetavarContext) (ctx : ContextInfo) : IO MetavarContext.Json := do
+  let mut decls := #[]
+  for (mvarId, decl) in mctx.decls do
+    let (_, typeMVars) ← ctx.runMetaM decl.lctx ((Meta.collectMVars decl.type).run {})
+    decls := decls.push {
+      mvarId := toString mvarId.name
+      userName := toString decl.userName
+      type := (← ctx.ppExpr {} decl.type).pretty
+      mvarsInType := typeMVars.result.toList
+      -- value := (mctx.getExprAssignmentCore? mvarId).map toString
+      value := "N/A"
+    }
+  return { decls }
+
+structure ProofStepInfo where
+  tacticString : String
+  infoTree : Option Json
+  goalBefore : GoalInfo
+  goalsAfter : List GoalInfo
+  mctxBefore : Option MetavarContext.Json
+  mctxAfter : Option MetavarContext.Json
+  tacticDependsOn : List String
+  spawnedGoals : List GoalInfo
+  start : Option Lean.Position
+  finish : Option Lean.Position
+  deriving Inhabited, ToJson, FromJson
+
 /--
 A response to a Lean command.
 `env` can be used in later calls, to build on the stored environment.
@@ -126,6 +234,7 @@ structure CommandResponse where
   sorries : List Sorry := []
   tactics : List Tactic := []
   infotree : Option Json := none
+  proofTreeEdges : Option (List (List ProofStepInfo)) := none
 deriving FromJson
 
 def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Json)
@@ -138,7 +247,10 @@ instance : ToJson CommandResponse where
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "tactics" r.tactics,
-    match r.infotree with | some j => [("infotree", j)] | none => []
+    match r.infotree with | some j => [("infotree", j)] | none => [],
+    match r.proofTreeEdges with
+    | some edges => Json.nonemptyList "proofTreeEdges" edges
+    | none => [],
   ]
 
 /--
@@ -151,17 +263,23 @@ structure ProofStepResponse where
   messages : List Message := []
   sorries : List Sorry := []
   traces : List String
+  goalInfos: List GoalInfo := []
+  mctxAfter : Option MetavarContext.Json
   proofStatus : String
+  stepVerification : String
 deriving ToJson, FromJson
 
 instance : ToJson ProofStepResponse where
   toJson r := Json.mkObj <| .flatten [
     [("proofState", r.proofState)],
     [("goals", toJson r.goals)],
+    [("goalInfos", toJson r.goalInfos)],
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "traces" r.traces,
-    [("proofStatus", r.proofStatus)]
+    match r.mctxAfter with | some mctxAfter => [("mctxAfter", toJson mctxAfter)] | none => [],
+    [("proofStatus", r.proofStatus)],
+    [("stepVerification", r.stepVerification)]
   ]
 
 /-- Json wrapper for an error. -/

REPL/Lean/InfoTree/ToJson.lean

@@ -24,7 +24,7 @@ deriving ToJson
 
 structure Syntax.Json where
   pp : Option String
-  -- raw : String
+  raw : String
   range : Range
 deriving ToJson
 
@@ -42,7 +42,7 @@ def _root_.Lean.Syntax.toJson (stx : Syntax) (ctx : ContextInfo) (lctx : LocalCo
     pp := match (← ctx.ppSyntax lctx stx).pretty with
       | "failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)" => none
       | pp => some pp
-    -- raw := toString stx
+    raw := toString stx
     range := stx.toRange ctx }
 
 structure TacticInfo.Json where
@@ -58,7 +58,7 @@ def TacticInfo.toJson (i : TacticInfo) (ctx : ContextInfo) : IO TacticInfo.Json
     name := i.name?
     stx :=
     { pp := Format.pretty (← i.pp ctx),
-      -- raw := toString i.info.stx,
+      raw := toString i.stx,
       range := i.stx.toRange ctx },
     goalsBefore := (← i.goalState ctx).map Format.pretty,
     goalsAfter := (← i.goalStateAfter ctx).map Format.pretty }