Pantograph.lean

@@ -133,8 +133,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         (match env.find? <| str_to_name copyFrom with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok cInfo.type)
-      | _, _ =>
+      | .none, .none =>
-        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
+        return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
+      | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
     match expr? with
     | .error error => return .error error
     | .ok expr =>
@@ -146,16 +147,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     match state.goalStates.get? args.stateId with
     | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    | .some goalState => do
+    | .some goalState =>
-      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
+      match ← GoalState.execute goalState args.goalId args.tactic with
-        | .some tactic, .none => do
+      | .success nextGoalState =>
-          pure ( Except.ok (← GoalState.execute goalState args.goalId tactic))
-        | .none, .some expr => do
-          pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr))
-        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
-      match nextGoalState? with
-      | .error error => return .error error
-      | .ok (.success nextGoalState) =>
         let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
         set { state with goalStates }
         let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
@@ -163,11 +157,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           nextStateId? := .some nextStateId,
           goals? := .some goals,
         }
-      | .ok (.parseError message) =>
+      | .parseError message =>
         return .ok { parseError? := .some message }
-      | .ok (.indexError goalId) =>
+      | .indexError goalId =>
         return .error $ errorIndex s!"Invalid goal id index {goalId}"
-      | .ok (.failure messages) =>
+      | .failure messages =>
         return .ok { tacticErrors? := .some messages }
   goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
     let state ← get

Pantograph/Goal.lean

@@ -47,15 +47,13 @@ protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α
 
 protected def GoalState.mctx (state: GoalState): MetavarContext :=
   state.savedState.term.meta.meta.mctx
-protected def GoalState.env (state: GoalState): Environment :=
-  state.savedState.term.meta.core.env
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
 
 /-- Inner function for executing tactic on goal state -/
 def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
-    M (Except (Array String) Elab.Tactic.SavedState):= do
+    M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do
-  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
+  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do
     state.restore
     Elab.Tactic.setGoals [goal]
     try
@@ -65,7 +63,9 @@ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax
         let errors ← (messages.map Message.data).mapM fun md => md.toString
         return .error errors
       else
-        return .ok (← MonadBacktrack.saveState)
+        let unsolved ← Elab.Tactic.getUnsolvedGoals
+        -- The order of evaluation is important here, since `getUnsolvedGoals` prunes the goals set
+        return .ok (← MonadBacktrack.saveState, unsolved)
     catch exception =>
       return .error #[← exception.toMessageData.toString]
   tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
@@ -97,7 +97,8 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
   match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
   | .error errors =>
     return .failure errors
-  | .ok nextSavedState =>
+  | .ok (nextSavedState, nextGoals) =>
+    assert! nextSavedState.tactic.goals.length == nextGoals.length
     -- Assert that the definition of metavariables are the same
     let nextMCtx := nextSavedState.term.meta.meta.mctx
     let prevMCtx := state.savedState.term.meta.meta.mctx
@@ -111,64 +112,12 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
         return acc.insert mvarId
       ) SSet.empty
     return .success {
-      state with
       savedState := nextSavedState
+      root := state.root,
       newMVars,
       parentGoalId := goalId,
     }
 
-protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  let expr ← match Parser.runParserCategory
-    (env := state.env)
-    (catName := `term)
-    (input := expr)
-    (fileName := "<stdin>") with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  let tacticM:  Elab.Tactic.TacticM TacticResult := do
-    state.savedState.restore
-    Elab.Tactic.setGoals [goal]
-    try
-      let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
-      -- Attempt to unify the expression
-      let goalType ← goal.getType
-      let exprType ← Meta.inferType expr
-      if !(← Meta.isDefEq goalType exprType) then
-        return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
-      goal.checkNotAssigned `GoalState.tryAssign
-      goal.assign expr
-      if (← getThe Core.State).messages.hasErrors then
-        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-        let errors ← (messages.map Message.data).mapM fun md => md.toString
-        return .failure errors
-      else
-        let prevMCtx := state.savedState.term.meta.meta.mctx
-        let nextMCtx ← getMCtx
-        -- Generate a list of mvarIds that exist in the parent state; Also test the
-        -- assertion that the types have not changed on any mvars.
-        let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
-          if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
-            assert! prevMVarDecl.type == mvarDecl.type
-            return acc
-          else
-            return mvarId :: acc
-          ) []
-        -- The new goals are the newMVars that lack an assignment
-        Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
-        let nextSavedState ← MonadBacktrack.saveState
-        return .success {
-          state with
-          savedState := nextSavedState,
-          newMVars := newMVars.toSSet,
-          parentGoalId := goalId,
-        }
-    catch exception =>
-      return .failure #[← exception.toMessageData.toString]
-  tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-
 /-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/
 protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState :=
   if target.root != graftee.root then

Pantograph/Protocol.lean

@@ -146,9 +146,7 @@ structure GoalTactic where
   -- Identifiers for tree, state, and goal
   stateId: Nat
   goalId: Nat := 0
-  -- One of the fields here must be filled
+  tactic: String
-  tactic?: Option String := .none
-  expr?: Option String := .none
   deriving Lean.FromJson
 structure GoalTacticResult where
   -- The next goal state id. Existence of this field shows success
@@ -174,8 +172,7 @@ structure GoalPrint where
   printContext: Bool := true
   printValue: Bool := true
   printNewMVars: Bool := false
-  -- Print all mvars
+  printNonVisible: Bool := false
-  printAll: Bool := false
 
 
 end Pantograph.Protocol

Pantograph/Serial.lean

@@ -262,6 +262,9 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt
     let parentGoal := parentState.goals.get! state.parentGoalId
     parentState.mctx.findDecl? parentGoal)
   goals.mapM fun goal => do
+    if options.noRepeat then
+      let key := if parentDecl?.isSome then "is some" else "is none"
+      IO.println s!"goal: {goal.name}, {key}"
     match state.mctx.findDecl? goal with
     | .some mvarDecl =>
       let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
@@ -293,7 +296,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrin
     else if mvarId == goalState.root then
       printMVar (pref := ">") mvarId decl
     -- Print the remainig ones that users don't see in Lean
-    else if options.printAll then
+    else if options.printNonVisible then
       let pref := if goalState.newMVars.contains mvarId then "~" else " "
       printMVar pref mvarId decl
     else

Test/Integration.lean

@@ -82,31 +82,12 @@ def test_malformed_command : IO LSpec.TestSeq :=
        error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
       Protocol.InteractionError))
   ]
-def test_tactic : IO LSpec.TestSeq :=
-  let goal: Protocol.Goal := {
-    target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
-    vars := #[{ name := "_uniq 9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
-  }
-  subroutine_runner [
-    subroutine_step "goal.start"
-      [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
-     (Lean.toJson ({stateId := 0}:
-      Protocol.GoalStartResult)),
-    subroutine_step "goal.tactic"
-      [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
-     (Lean.toJson ({
-       nextStateId? := .some 1,
-       goals? := #[goal],
-     }:
-      Protocol.GoalTacticResult))
-  ]
 
 def suite: IO LSpec.TestSeq := do
 
   return LSpec.group "Integration" $
     (LSpec.group "Option modify" (← test_option_modify)) ++
-    (LSpec.group "Malformed command" (← test_malformed_command)) ++
+    (LSpec.group "Malformed command" (← test_malformed_command))
-    (LSpec.group "Tactic" (← test_tactic))
 
 
 end Pantograph.Test.Integration

Test/Proofs.lean

@@ -66,9 +66,8 @@ def startProof (start: Start): TestM (Option GoalState) := do
 
 def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
 
-def buildGoal (nameType: List (String × String)) (target: String) (caseName?: Option String := .none): Protocol.Goal :=
+def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goal :=
   {
-    caseName?,
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
       userName := x.fst,
@@ -188,21 +187,21 @@ def proof_arith: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "intros" (state1.goals.length = 1)
-  addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone
+  addTest $ LSpec.test "1 root" state1.rootExpr.isNone
   let state2 ← match ← state1.execute (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
-  addTest $ LSpec.check "(2 root)" state2.rootExpr.isNone
+  addTest $ LSpec.check "2 root" state2.rootExpr.isNone
   let state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.test "assumption" state3.goals.isEmpty
-  addTest $ LSpec.check "(3 root)" state3.rootExpr.isSome
+  addTest $ LSpec.check "3 root" state3.rootExpr.isSome
   return ()
 
 -- Two ways to write the same theorem
@@ -254,7 +253,7 @@ def proof_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
+  addTest $ LSpec.check "· assumption" state4_1.goals.isEmpty
   addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isNone
   let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
     | .success state => pure state
@@ -267,7 +266,7 @@ def proof_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
+  addTest $ LSpec.check "· assumption" state4_2.goals.isEmpty
   addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr.isNone
   -- Ensure the proof can continue from `state4_2`.
   let state2b ← match state2.continue state4_2 with
@@ -287,8 +286,8 @@ def proof_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
+  addTest $ LSpec.check "· assumption" state4_1.goals.isEmpty
-  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr.isSome
+  addTest $ LSpec.check "4_1 root" state4_1.rootExpr.isSome
 
   return ()
   where
@@ -337,45 +336,7 @@ def proof_m_couple: TestM Unit := do
   addTest $ LSpec.test "(2 root)" state1b.rootExpr.isNone
   return ()
 
-def proof_proposition_generation: TestM Unit := do
+/-- Tests the most basic form of proofs whose goals do not relate to each other -/
-  let state? ← startProof (.expr "Σ' p:Prop, p")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      buildGoal [] "?fst" (caseName? := .some "snd"),
-      buildGoal [] "Prop" (caseName? := .some "fst")
-      ])
-  addTest $ LSpec.test "(1 root)" state1.rootExpr.isNone
-
-  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
-  addTest $ LSpec.test "(2 root)" state2.rootExpr.isNone
-
-  let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[])
-  addTest $ LSpec.test "(3 root)" state3.rootExpr.isSome
-  return ()
-
 def suite: IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
     (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
@@ -387,8 +348,8 @@ def suite: IO LSpec.TestSeq := do
     ("Nat.add_comm delta", proof_delta_variable),
     ("arithmetic", proof_arith),
     ("Or.comm", proof_or_comm),
-    ("2 < 5", proof_m_couple),
+    ("2 < 5", proof_m_couple)
-    ("Proposition Generation", proof_proposition_generation)
+    --("delta variable", proof_delta_variable)
   ]
   let tests ← tests.foldlM (fun acc tests => do
     let (name, tests) := tests