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 +1 -1
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 6323c02f47 - Show all commits

2
Test/Serial.lean
View File

@ -89,7 +89,7 @@ def test_pickling_env_extensions : TestM Unit := do
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 "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
goalStatePickle state statePath goalStatePickle state1 statePath
let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
let (state1, _) ← goalStateUnpickle statePath (← getEnv) let (state1, _) ← goalStateUnpickle statePath (← getEnv)
let parentExpr := state1.parentExpr?.get! let parentExpr := state1.parentExpr?.get!