Merge pull request 'feat(goal): Detect unsafe and sorry' (#201) from goal/detect-unsafe-sorry into dev

Reviewed-on: #201

Pantograph/Goal.lean

@@ -140,8 +140,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
   -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
   let unassigned := goals.filter λ goal =>
     let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
-    let isDuplicate := state.goals.contains goal
-    (¬ isDuplicate) && (¬ isSolved)
+    ¬ isSolved
   return {
     state with
     savedState := {
@@ -167,13 +166,13 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
     .none
   let expr ← goalState.mctx.eAssignment.find? goalState.root
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  if expr.hasExprMVar then
-    -- Must not assert that the goal state is empty here. We could be in a branch goal.
-    --assert! ¬goalState.goals.isEmpty
-    .none
-  else
-    assert! goalState.goals.isEmpty
   return expr
+@[export pantograph_goal_state_is_solved]
+protected def GoalState.isSolved (goalState : GoalState) : Bool :=
+  let solvedRoot := match goalState.rootExpr? with
+    | .some e => ¬ e.hasExprMVar
+    | .none => true
+  goalState.goals.isEmpty && solvedRoot
 @[export pantograph_goal_state_parent_expr]
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
   let parent ← goalState.parentMVar?

Pantograph/Library.lean

@@ -123,8 +123,9 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
   : CoreM Protocol.GoalPrintResult := runMetaM do
   state.restoreMetaM
 
+  let rootExpr? := state.rootExpr?
   let root? ← if rootExpr then
-      state.rootExpr?.mapM λ expr => state.withRootContext do
+      rootExpr?.mapM λ expr => state.withRootContext do
         serializeExpression options (← instantiateAll expr)
     else
       pure .none
@@ -143,11 +144,15 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
     state.withContext mvarId do
       let .some expr ← getExprMVarAssignment? mvarId | return {}
       serializeExpression options (← instantiateAll expr)
+  let env ← getEnv
   return {
     root?,
     parent?,
     goals,
     extraMVars,
+    rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
+    rootHasUnsafe := rootExpr?.map (env.hasUnsafe ·) |>.getD false,
+    rootHasMVar := rootExpr?.map (·.hasExprMVar) |>.getD false,
   }
 
 @[export pantograph_goal_have_m]

Pantograph/Protocol.lean

@@ -276,6 +276,9 @@ structure GoalTacticResult where
 
   -- Existence of this field shows the tactic parsing has failed
   parseError? : Option String       := .none
+
+  hasSorry : Bool := false
+  hasUnsafe : Bool := false
   deriving Lean.ToJson
 structure GoalContinue where
   -- State from which the continuation acquires the context
@@ -319,6 +322,10 @@ structure GoalPrintResult where
   parent?: Option Expression := .none
   goals: Array Goal := #[]
   extraMVars: Array Expression := #[]
+
+  rootHasSorry : Bool := false
+  rootHasUnsafe : Bool := false
+  rootHasMVar : Bool := true
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL

Repl.lean

@@ -338,11 +338,14 @@ def execute (command: Protocol.Command): MainM Json := do
           pure result
         | false, _ => pure nextGoalState
       let nextStateId ← newGoalState nextGoalState
+      let parentExpr := nextGoalState.parentExpr?.get!
       let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
       return {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
         messages? := .some messages,
+        hasSorry := parentExpr.hasSorry,
+        hasUnsafe := (← getEnv).hasUnsafe parentExpr,
       }
     | .ok (.parseError message) =>
       return { messages? := .none, parseError? := .some message }

Test/Integration.lean

@@ -84,12 +84,17 @@ def test_tactic : Test :=
     step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
     step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
-     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
+     ({
+       root? := .some { pp? := "fun x => ?m.11"},
+       parent? := .some { pp? := .some "fun x => ?m.11" },
+     }: Protocol.GoalPrintResult),
     step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
     step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
      ({ messages? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
-      Protocol.GoalTacticResult)
+      Protocol.GoalTacticResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult),
   ]
 example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
   simp

Test/Metavar.lean

@@ -85,14 +85,14 @@ def test_m_couple: TestM Unit := do
       return ()
   addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
-  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  checkTrue "(1 root)" $ ¬ state1.isSolved
   -- Set m to 3
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
     | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  checkTrue "(1b root)" $ ¬ state2.isSolved
   let state1b ← match state2.continue state1 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
@@ -100,7 +100,7 @@ def test_m_couple: TestM Unit := do
     | .ok state => pure state
   addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ 3", .some "3 ≤ 5"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  checkTrue "(2 root)" $ ¬ state1b.isSolved
 
 def test_m_couple_simp: TestM Unit := do
   let state? ← startProof "(2: Nat) ≤ 5"
@@ -126,7 +126,7 @@ def test_m_couple_simp: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  checkTrue "(1b root)" $ ¬ state2.isSolved
   let state1b ← match state2.continue state1 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
@@ -134,7 +134,7 @@ def test_m_couple_simp: TestM Unit := do
     | .ok state => pure state
   addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ 2", .some "2 ≤ 5"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  checkTrue "(2 root)" $ ¬ state1b.isSolved
   let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
     | .success state _ => pure state
     | other => do
@@ -184,7 +184,7 @@ def test_proposition_generation: TestM Unit := do
       ])
   if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
     addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
-  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  checkTrue "(1 root)" $ ¬ state1.isSolved
 
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
     | .success state _ => pure state
@@ -193,7 +193,7 @@ def test_proposition_generation: TestM Unit := do
       return ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "?m.30 x"])
-  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
+  checkTrue "(2 root)" $ ¬ state2.isSolved
 
   let assign := "Eq.refl x"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
@@ -204,7 +204,7 @@ def test_proposition_generation: TestM Unit := do
   addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[])
 
-  addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
+  checkTrue "(3 root)" state3.isSolved
   return ()
 
 def test_partial_continuation: TestM Unit := do
@@ -238,23 +238,23 @@ def test_partial_continuation: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue 1)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
 
   -- Roundtrip
   --let coupled_goals := coupled_goals.map (λ g =>
   --  { name := str_to_name $ serializeName g.name (sanitize := false)})
-  let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
-  let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
+  let coupled_goals := coupled_goals.map (·.name.toString)
+  let coupled_goals := coupled_goals.map ({ name := ·.toName })
   let state1b ← match state2.resume (goals := coupled_goals) with
     | .error msg => do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
 
   -- Continuation should fail if the state does not exist:
   match state0.resume coupled_goals with

Test/Proofs.lean

@@ -192,14 +192,14 @@ def test_arith: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check tactic (state1.goals.length = 1)
-  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  checkTrue "(1 root)" state1.rootExpr?.get!.hasExprMVar
   let state2 ← match ← state1.tacticOn (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
+  checkTrue "(2 root)" state2.rootExpr?.get!.hasExprMVar
   let tactic := "assumption"
   let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
     | .success state _ => pure state
@@ -207,7 +207,7 @@ def test_arith: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.test tactic state3.goals.isEmpty
-  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
+  checkTrue "(3 root)" $ ¬ state3.rootExpr?.get!.hasExprMVar
   return ()
 
 -- Two ways to write the same theorem
@@ -257,8 +257,8 @@ def test_or_comm: TestM Unit := do
         { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
       ]
     }])
-  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
-  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
+  checkTrue "(1 parent)" state1.parentExpr?.isSome
+  checkTrue "(1 root)" $ ¬ state1.isSolved
 
   let state1parent ← state1.withParentContext do
     serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
@@ -276,8 +276,8 @@ def test_or_comm: TestM Unit := do
   let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
     #[caseL, caseR])
-  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
-  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
+  checkTrue "(2 parent exists)" state2.parentExpr?.isSome
+  checkTrue "(2 root)" $ ¬ state2.isSolved
 
   let state2parent ← state2.withParentContext do
     serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
@@ -308,7 +308,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
   let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
   addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
-  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
+  checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
   let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
     | .success state _ => pure state
     | other => do
@@ -321,7 +321,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
-  addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
+  checkTrue "(4_2 root)" $ ¬ state4_2.isSolved
   -- Ensure the proof can continue from `state4_2`.
   let state2b ← match state4_2.continue state2 with
     | .error msg => do
@@ -341,7 +341,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
+  checkTrue "(4_1 root)" $ ¬ state4_1.rootExpr?.get!.hasExprMVar
 
   return ()
   where