aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 12 Pull Requests 2 Packages Projects Releases Wiki Activity

feat(serial): Robust environment extension pickling #216

Merged
aniva merged 6 commits from serial/env-extensions into dev 2025-06-24 13:41:06 -07:00
Conversation 0 Commits 6 Files Changed 2 +9 -3
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit dfa491a5c2 - Show all commits

12
Test/Serial.lean
View File

@ -74,8 +74,8 @@ def test_goal_state_simple : TestM Unit := do
def test_pickling_env_extensions : TestM Unit := do def test_pickling_env_extensions : TestM Unit := do
let coreSrc : Core.State := { env := ← getEnv } let coreSrc : Core.State := { env := ← getEnv }
let p := mkIdent `p let coreDst : Core.State := { env := ← getEnv }
let h := mkIdent `h IO.FS.withTempFile λ _ statePath => do
let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do
let .ok e ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable! let .ok e ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable!
let state ← GoalState.create e let state ← GoalState.create e
@ -88,7 +88,13 @@ def test_pickling_env_extensions : TestM Unit := do
pure (type, value) pure (type, value)
let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable! let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
let parentExpr := state1.parentExpr?.get! let parentExpr := state1.parentExpr?.get!
checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
goalStatePickle state statePath
let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
let (state1, _) ← goalStateUnpickle statePath (← getEnv)
let parentExpr := state1.parentExpr?.get!
checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
return () return ()
structure Test where structure Test where