diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 09b7987..8dd09dd 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -136,8 +136,9 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] Meta.mapMetaM <| state.withContext' state.root private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit := + let { nextMacroScope, ngen, .. } := state modifyGetThe Core.State (fun st => ((), - { st with nextMacroScope := state.nextMacroScope, ngen := state.ngen })) + { st with nextMacroScope, ngen })) -- Restore the name generator and macro scopes of the core state protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := restoreCoreMExtra state.coreState @@ -335,6 +336,9 @@ protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM core := { core with ngen, + env := ← core.env.replayConsts src.env src'.env (skipExisting := true), + -- Reset the message log when declaration uses `sorry` + messages := {} } meta := { meta with @@ -476,7 +480,10 @@ private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × Array /-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/ def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do - assert! (← Core.getMessageLog).toList.isEmpty + let messageLog ← Core.getMessageLog + unless messageLog.toList.isEmpty do + IO.eprintln s!"{← messageLog.toList.mapM (·.toString)}" + assert! messageLog.toList.isEmpty try let state ← elabM diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 5b49018..ff82752 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -1,19 +1,19 @@ -import Lean.Environment -import Lean.Replay -import Init.System.IOError -import Std.Data.HashMap import Pantograph.Goal +import Lean.Environment +import Lean.Replay +import Std.Data.HashMap + +open Lean + /-! -Input/Output functions +Input/Output functions borrowed from REPL # Pickling and unpickling objects By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk. -/ -open Lean - namespace Pantograph /-- @@ -46,6 +46,21 @@ unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type} region.free pure r +abbrev ConstArray := Array (Name × ConstantInfo) +abbrev DistilledEnvironment := Array Import × ConstArray + +/-- Boil an environment down to minimal components -/ +def distillEnvironment (env : Environment) (background? : Option Environment := .none) + : DistilledEnvironment := + let filter : Name → Bool := match background? with + | .some env => (¬ env.contains ·) + | .none => λ _ => true + let constants : ConstArray := env.constants.map₂.foldl (init := #[]) λ acc name info => + if filter name then + acc.push (name, info) + else + acc + (env.header.imports, constants) /-- Pickle an `Environment` to disk. @@ -56,15 +71,23 @@ and when unpickling, we build a fresh `Environment` from the imports, and then add the new constants. -/ @[export pantograph_env_pickle_m] -def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit := - Pantograph.pickle path (env.header.imports, env.constants.map₂) +def environmentPickle (env : Environment) (path : System.FilePath) (background? : Option Environment := .none) + : IO Unit := + pickle path $ distillEnvironment env background? + +deriving instance BEq for Import def resurrectEnvironment - (imports : Array Import) - (map₂ : PHashMap Name ConstantInfo) + (distilled : DistilledEnvironment) + (background? : Option Environment := .none) : IO Environment := do - let env ← importModules imports {} 0 (loadExts := true) - env.replay (Std.HashMap.ofList map₂.toList) + let (imports, constArray) := distilled + let env ← match background? with + | .none => importModules imports {} 0 (loadExts := true) + | .some env => + assert! env.imports == imports + pure env + env.replay (Std.HashMap.ofList constArray.toList) /-- Unpickle an `Environment` from disk. @@ -72,9 +95,10 @@ We construct a fresh `Environment` with the relevant imports, and then replace the new constants. -/ @[export pantograph_env_unpickle_m] -def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do - let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path - return (← resurrectEnvironment imports map₂, region) +def environmentUnpickle (path : System.FilePath) (background? : Option Environment := .none) + : IO (Environment × CompactedRegion) := unsafe do + let (distilled, region) ← unpickle (Array Import × ConstArray) path + return (← resurrectEnvironment distilled background?, region) open Lean.Core in @@ -88,7 +112,8 @@ structure CompactCoreState where -- infoState : Elab.InfoState := {} @[export pantograph_goal_state_pickle_m] -def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit := +def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background? : Option Environment := .none) + : IO Unit := let { savedState := { term := { @@ -106,8 +131,8 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit : parentMVars, fragments, } := goalState - Pantograph.pickle path ( - env.constants.map₂, + pickle path ( + distillEnvironment env background?, ({ nextMacroScope, ngen } : CompactCoreState), meta, @@ -120,10 +145,10 @@ def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit : ) @[export pantograph_goal_state_unpickle_m] -def goalStateUnpickle (path : System.FilePath) (env : Environment) +def goalStateUnpickle (path : System.FilePath) (background? : Option Environment := .none) : IO (GoalState × CompactedRegion) := unsafe do let (( - map₂, + distilledEnv, compactCore, meta, @@ -134,7 +159,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment) parentMVars, fragments, ), region) ← Pantograph.unpickle ( - PHashMap Name ConstantInfo × + DistilledEnvironment × CompactCoreState × Meta.State × @@ -145,7 +170,7 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment) List MVarId × FragmentMap ) path - let env ← env.replay (Std.HashMap.ofList map₂.toList) + let env ← resurrectEnvironment distilledEnv background? let goalState := { savedState := { term := { diff --git a/Repl.lean b/Repl.lean index 54d1bb6..3811f96 100644 --- a/Repl.lean +++ b/Repl.lean @@ -412,10 +412,10 @@ def execute (command: Protocol.Command): MainM Json := do let state ← getMainState let .some goalState := state.goalStates[args.id]? | Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.id}" - goalStatePickle goalState args.path + goalStatePickle goalState args.path (background? := .some $ ← getEnv) return {} goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do - let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv) + let (goalState, _) ← goalStateUnpickle args.path (background? := .some $ ← getEnv) let id ← newGoalState goalState return { id } diff --git a/Test/Common.lean b/Test/Common.lean index 34ce07b..22926aa 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -187,9 +187,11 @@ namespace Tactic /-- Create an aux lemma and assigns it to `mvarId`, which is circuitous, but exercises the aux lemma generator. -/ -def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do +def assignWithAuxLemma (type : Expr) (value? : Option Expr := .none) : Elab.Tactic.TacticM Unit := do let type ← instantiateMVars type - let value ← instantiateMVars value + let value ← match value? with + | .some value => instantiateMVars value + | .none => Meta.mkSorry type (synthetic := false) if type.hasExprMVar then throwError "Type has expression mvar" if value.hasExprMVar then @@ -200,6 +202,7 @@ def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do unless ← Meta.isDefEq type (← goal.getType) do throwError "Type provided is incorrect" goal.assign (.const name []) + Elab.Tactic.pruneSolvedGoals end Tactic diff --git a/Test/Metavar.lean b/Test/Metavar.lean index e8a3282..19d6ecd 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -281,6 +281,32 @@ def test_branch_unification : TestM Unit := do let .some root := stateT.rootExpr? | fail "Root expression must exist" checkEq "(root)" (toString $ ← Meta.ppExpr root) "fun p q h => ⟨h, Or.inl h⟩" +def test_replay_environment : TestM Unit := do + let .ok rootTarget ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable! + let state ← GoalState.create rootTarget + let .success state _ ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | fail "apply And.intro failed to run" + let goal := state.goals[0]! + let type ← goal.withContext do + let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable! + pure type + let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "left" + + state.restoreMetaM + let goal := state.goals[1]! + let type ← goal.withContext do + let .ok type ← elabTerm (← `(term|(3: Nat) ≤ 5)) (.some $ .sort 0) | unreachable! + pure type + let .success state2 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "right" + checkEq "(state1 goals)" state1.goals.length 0 + checkEq "(state2 goals)" state2.goals.length 0 + let stateT ← state2.replay state state1 + checkEq "(stateT goals)" stateT.goals.length 0 + let .some root := stateT.rootExpr? | fail "Root expression must exist" + checkTrue "root has aux lemma" $ root.getUsedConstants.any (·.isAuxLemma) + checkEq "(root)" (toString $ ← Meta.ppExpr root) "⟨_proof_1, _proof_2⟩" + let root ← unfoldAuxLemmas root + checkEq "(root unfold)" (toString $ ← Meta.ppExpr root) "⟨sorry, sorry⟩" + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("Instantiate", test_instantiate_mvar), @@ -289,6 +315,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Proposition Generation", test_proposition_generation), ("Partial Continuation", test_partial_continuation), ("Branch Unification", test_branch_unification), + ("Replay Environment", test_replay_environment), ] tests.map (fun (name, test) => (name, proofRunner env test)) diff --git a/Test/Serial.lean b/Test/Serial.lean index 0cf6e2a..cca7dbd 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -82,18 +82,17 @@ def test_pickling_env_extensions : TestM Unit := do let .success state _ ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | unreachable! let goal := state.goals[0]! - let (type, value) ← goal.withContext do + let type ← goal.withContext do let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable! - let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable! - pure (type, value) - let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable! + pure type + let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable! let parentExpr := state1.parentExpr! - checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma + checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma) goalStatePickle state1 statePath let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do let (state1, _) ← goalStateUnpickle statePath (← getEnv) let parentExpr := state1.parentExpr! - checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma + checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma) return ()