Merge branch 'leanprover-community-master'

Author: Kripner

REPL/JSON.lean

@@ -16,6 +16,7 @@ namespace REPL
 
 structure CommandOptions where
   allTactics : Option Bool := none
+  rootGoals : Option Bool := none
   /--
   Should be "full", "tactics", "original", or "substantive".
   Anything else is ignored.
@@ -256,6 +257,7 @@ structure ProofStepResponse where
   traces : List String
   goalInfos: List GoalInfo := []
   mctxAfter : Option MetavarContext.Json
+  proofStatus : String
 deriving ToJson, FromJson
 
 instance : ToJson ProofStepResponse where
@@ -266,7 +268,8 @@ instance : ToJson ProofStepResponse where
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "traces" r.traces,
-    match r.mctxAfter with | some mctxAfter => [("mctxAfter", toJson mctxAfter)] | none => []
+    match r.mctxAfter with | some mctxAfter => [("mctxAfter", toJson mctxAfter)] | none => [],
+    [("proofStatus", r.proofStatus)]
   ]
 
 /-- Json wrapper for an error. -/

REPL/Lean/Environment.lean

@@ -25,7 +25,7 @@ and then replace the new constants.
 -/
 def unpickle (path : FilePath) : IO (Environment × CompactedRegion) := unsafe do
   let ((imports, map₂), region) ← _root_.unpickle (Array Import × PHashMap Name ConstantInfo) path
-  let env ← importModules imports {} 0
+  let env ← importModules imports {} 0 (loadExts := true)
   return (← env.replay (Std.HashMap.ofList map₂.toList), region)
 
 end Lean.Environment

REPL/Lean/InfoTree.lean

@@ -165,16 +165,45 @@ partial def findAllInfo (t : InfoTree) (ctx? : Option ContextInfo) (p : Info →
     info ++ rest
   | _ => []
 
+/-- Analogue of `findAllInfo` but specialized to tactics. It additionally returns root goals. -/
+partial def findAllInfoTactics (t : InfoTree) (ctx? : Option ContextInfo) (rootGoals : List MVarId := []) :
+  List (Info × Option ContextInfo × List MVarId) :=
+  match t with
+  | .context ctx t => t.findAllInfoTactics (ctx.mergeIntoOuter? ctx?) rootGoals
+  | .node info ts =>
+    let tInfo := match info with
+    | .ofTacticInfo i =>
+      if info.isOriginal && i.isSubstantive then
+        let rootGoals := if rootGoals.isEmpty then i.goalsBefore else rootGoals
+        [(info, ctx?, rootGoals)]
+      else
+        []
+    | _ => []
+    tInfo ++ ts.toList.flatMap (fun t => t.findAllInfoTactics ctx? rootGoals)
+  | _ => []
+
 /-- Return all `TacticInfo` nodes in an `InfoTree` with "original" syntax,
 each equipped with its relevant `ContextInfo`. -/
-def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo) :=
-  let infos := t.findAllInfo none fun i => match i with
-  | .ofTacticInfo i' => i.isOriginal && i'.isSubstantive
-  | _ => false
+def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVarId) :=
+  let infos := t.findAllInfoTactics none
   infos.filterMap fun p => match p with
-  | (.ofTacticInfo i, some ctx) => (i, ctx)
+  | (.ofTacticInfo i, some ctx, rootGoals) => (i, ctx, rootGoals)
   | _ => none
 
+/-- Returns the root goals for a given `InfoTree`. -/
+partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) :
+  List (TacticInfo × ContextInfo × List MVarId) :=
+  match t with
+  | .context ctx t => t.findRootGoals (ctx.mergeIntoOuter? ctx?)
+  | .node info ts =>
+    match info with
+    | .ofTacticInfo i =>
+      match ctx? with
+      | some ctx => [(i, ctx, i.goalsBefore)]
+      | _ => []
+    | _ => ts.toList.flatMap (fun t => t.findRootGoals ctx?)
+  | _ => []
+
 /-- Return all `TacticInfo` nodes in an `InfoTree`
 corresponding to explicit invocations of the `sorry` tactic,
 each equipped with its relevant `ContextInfo`. -/
@@ -217,17 +246,24 @@ def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Posit
   (t.findSorryTermNodes.map fun ⟨i, ctx⟩ =>
     (ctx, .term i.lctx i.expectedType?, stxRange ctx.fileMap i.stx))
 
-def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × Position × Position × Array Name) :=
+def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List MVarId × Position × Position × Array Name) :=
     -- HACK: creating a child ngen
-  t.findTacticNodes.map fun ⟨i, ctx⟩ =>
+  t.findTacticNodes.map fun ⟨i, ctx, rootGoals⟩ =>
     let range := stxRange ctx.fileMap i.stx
     ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 },
       i.stx,
+      rootGoals,
       i.goalsBefore,
       range.fst,
       range.snd,
       i.getUsedConstantsAsSet.toArray )
 
+def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) :=
+  t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 },
+      rootGoals,
+      range.fst )
 
 end Lean.Elab.InfoTree
 
@@ -282,7 +318,7 @@ namespace Lean.Elab.InfoTree
 Finds all tactic invocations in an `InfoTree`,
 ignoring structuring tactics (e.g. `by`, `;`, multiline tactics, parenthesized tactics).
 -/
-def substantiveTactics (t : InfoTree) : List (TacticInfo × ContextInfo) :=
+def substantiveTactics (t : InfoTree) : List (TacticInfo × ContextInfo × List MVarId) :=
   t.findTacticNodes.filter fun i => i.1.isSubstantive
 
 end Lean.Elab.InfoTree

REPL/Main.lean

@@ -95,25 +95,26 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   modify fun s => { s with proofStates := s.proofStates.push proofState }
   return id
 
-def sorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) :=
+def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Option (List MVarId))
+: M m (List Sorry) :=
   trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with
     | .term _ none => false
     | _ => true ) |>.mapM
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-           let s ← ProofSnapshot.create ctx none env? [g]
+           let s ← ProofSnapshot.create ctx none env? [g] rootGoals?
            pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term lctx (some t) => do
-           let s ← ProofSnapshot.create ctx lctx env? [] [t]
+           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
            pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term _ none => unreachable!
         let proofStateId ← proofState.mapM recordProofSnapshot
         let goalInfo : Option GoalInfo ← match proofState with
         | some proofState => do
            match proofState.tacticState.goals[0]? with
            | some goalId => do
-             -- TODO: this does not work when it's just `sorry` instead of `by sorry`
+             -- TODO: this does not work when it's just `sorry` instead of `by sorry` - allow printGoalInfo to return none
              let info ← printGoalInfo ctx goalId
              pure (some info)
            | none => pure none
@@ -128,8 +129,8 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
 
 def tactics (trees : List InfoTree) : M m (List Tactic) :=
   trees.flatMap InfoTree.tactics |>.mapM
-    fun ⟨ctx, stx, goals, pos, endPos, ns⟩ => do
-      let proofState := some (← ProofSnapshot.create ctx none none goals)
+    fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
+      let proofState := some (← ProofSnapshot.create ctx none none goals rootGoals)
       let goals := s!"{(← ctx.ppGoals goals)}".trim
       let tactic := Format.pretty (← ppTactic ctx stx)
       let proofStateId ← proofState.mapM recordProofSnapshot
@@ -142,6 +143,59 @@ def proofTrees (infoTrees : List InfoTree) : M m (List (List ProofStepInfo)) :=
     | .some proofTree => return proofTree.steps
     | .none => return []
 
+def collectRootGoalsAsSorries (trees : List InfoTree) : M m (List Sorry) := do
+  trees.flatMap InfoTree.rootGoals |>.mapM
+    fun ⟨ctx, goals, pos⟩ => do
+      let proofState := some (← ProofSnapshot.create ctx none none goals goals)
+      let goals := s!"{(← ctx.ppGoals goals)}".trim
+      let proofStateId ← proofState.mapM recordProofSnapshot
+      return Sorry.of goals none pos pos proofStateId
+
+/--
+Evaluates the current status of a proof, returning a string description.
+Main states include:
+- "Completed": Proof is complete and type checks successfully
+- "Incomplete": When goals remain, or proof contains sorry/metavariables
+- "Error": When kernel type checking errors occur
+
+Inspired by LeanDojo REPL's status tracking.
+-/
+def getProofStatus (proofState : ProofSnapshot) : M m String := do
+  match proofState.tacticState.goals with
+    | [] =>
+      let res := proofState.runMetaM do
+        match proofState.rootGoals with
+        | [goalId] =>
+          match proofState.metaState.mctx.getExprAssignmentCore? goalId with
+          | none => return "Error: Goal not assigned"
+          | some pf => do
+            let pf ← instantiateMVars pf
+            let pft ← Meta.inferType pf >>= instantiateMVars
+            if pf.hasSorry then
+              return "Incomplete: contains sorry"
+            if pf.hasExprMVar then
+              return "Incomplete: contains metavariable(s)"
+
+            let decl := Declaration.defnDecl ({
+              name := Name.anonymous,
+              type := pft,
+              value := pf,
+              levelParams := (collectLevelParams {} pft).params.toList,
+              hints := ReducibilityHints.opaque,
+              safety := DefinitionSafety.safe
+            })
+
+            try
+              let _ ← addDecl decl
+            catch ex =>
+              return s!"Error: kernel type check failed: {← ex.toMessageData.toString}"
+            return "Completed"
+
+        | _ => return "Not verified: more than one initial goal"
+      return (← res).fst
+
+    | _ => return "Incomplete: open goals remain"
+
 /-- Record a `ProofSnapshot` and generate a JSON response for it. -/
 def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnapshot := none) :
     M m ProofStepResponse := do
@@ -157,7 +211,7 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
   | none => pure trees
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees none
+  let sorries ← sorries trees none (some proofState.rootGoals)
   let proofStateId ← recordProofSnapshot proofState
   let (ctx, _) ← proofState.runMetaM do return { ← CommandContextInfo.save with }
   let goalInfos ← proofState.tacticState.goals.mapM (fun mvarId => do
@@ -172,7 +226,7 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
     traces
     goalInfos
     mctxAfter := mctxAfterJson
-  }
+    proofStatus := (← getProofStatus proofState) }
 
 /-- Pickle a `CommandSnapshot`, generating a JSON response. -/
 def pickleCommandSnapshot (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do
@@ -234,7 +288,10 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let messages ← messages.mapM fun m => Message.of m
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees (initialCmdState?.map (·.env))
+  let sorries ← sorries trees (initialCmdState?.map (·.env)) none
+  let sorries ← match s.rootGoals with
+  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees))
+  | _ => pure sorries
   let tactics ← match s.allTactics with
   | some true => tactics trees
   | _ => pure []

REPL/Snapshots.lean

@@ -83,7 +83,7 @@ def unpickle (path : FilePath) : IO (CommandSnapshot × CompactedRegion) := unsa
   let ((imports, map₂, cmdState, cmdContext), region) ←
     _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCommandSnapshot ×
       Command.Context) path
-  let env ← (← importModules imports {} 0).replay (Std.HashMap.ofList map₂.toList)
+  let env ← (← importModules imports {} 0 (loadExts := true)).replay (Std.HashMap.ofList map₂.toList)
   let p' : CommandSnapshot :=
   { cmdState := { cmdState with env }
     cmdContext }
@@ -108,6 +108,7 @@ structure ProofSnapshot where
   termContext   : Term.Context
   tacticState   : Tactic.State
   tacticContext : Tactic.Context
+  rootGoals     : List MVarId
 
 namespace ProofSnapshot
 
@@ -191,7 +192,8 @@ For convenience, we also allow a list of `Expr`s, and these are appended to the
 as fresh metavariables with the given types.
 -/
 def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
-    (goals : List MVarId) (types : List Expr := []) : IO ProofSnapshot := do
+    (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
+    : IO ProofSnapshot := do
   ctx.runMetaM (lctx?.getD {}) do
     let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
     let s ← getThe Core.State
@@ -206,7 +208,10 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi
       termState := {}
       termContext := {}
       tacticState := { goals }
-      tacticContext := { elaborator := .anonymous } }
+      tacticContext := { elaborator := .anonymous }
+      rootGoals := match rootGoals? with
+        | none => goals
+        | some gs => gs }
 
 open Lean.Core in
 /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/
@@ -270,22 +275,23 @@ def pickle (p : ProofSnapshot) (path : FilePath) : IO Unit := do
      p'.termState,
      ({ p'.termContext with } : CompactableTermContext),
      p'.tacticState,
-     p'.tacticContext)
+     p'.tacticContext,
+     p'.rootGoals)
 
 /--
 Unpickle a `ProofSnapshot`.
 -/
 def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) :
     IO (ProofSnapshot × CompactedRegion) := unsafe do
   let ((imports, map₂, coreState, coreContext, metaState, metaContext, termState, termContext,
-    tacticState, tacticContext), region) ←
+    tacticState, tacticContext, rootGoals), region) ←
     _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCoreState ×
       Core.Context × Meta.State × CompactableMetaContext × Term.State × CompactableTermContext ×
-      Tactic.State × Tactic.Context) path
+      Tactic.State × Tactic.Context × List MVarId) path
   let env ← match cmd? with
   | none =>
     enableInitializersExecution
-    (← importModules imports {} 0).replay (Std.HashMap.ofList map₂.toList)
+    (← importModules imports {} 0 (loadExts := true)).replay (Std.HashMap.ofList map₂.toList)
   | some cmd =>
     cmd.cmdState.env.replay (Std.HashMap.ofList map₂.toList)
   let p' : ProofSnapshot :=
@@ -296,7 +302,8 @@ def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) :
     termState
     termContext := { termContext with }
     tacticState
-    tacticContext }
+    tacticContext
+    rootGoals }
   let (_, p'') ← p'.runCoreM do
     for o in ← getOpenDecls do
       if let .simple ns _ := o then

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.18.0
+leanprover/lean4:v4.19.0-rc2