aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 16 Pull Requests 3 Packages Projects Releases Wiki Activity

chore: Update Lean to v4.20.1 #209

Merged
aniva merged 6 commits from chore/toolchain into dev 2025-06-18 16:39:19 -07:00
Conversation 1 Commits 6 Files Changed 9 +2 -10
1 changed files with 2 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit b7f0ae435a - Show all commits

12
Test/Serial.lean
View File

@ -7,9 +7,6 @@ open Lean
namespace Pantograph.Test.Serial namespace Pantograph.Test.Serial
def tempPath : IO System.FilePath := do
Prod.snd <$> IO.FS.createTempFile
structure MultiState where structure MultiState where
coreContext : Core.Context coreContext : Core.Context
env: Environment env: Environment
@ -35,7 +32,7 @@ def test_environment_pickling : TestM Unit := do
let coreDst : Core.State := { env := ← getEnv } let coreDst : Core.State := { env := ← getEnv }
let name := `mystery let name := `mystery
let envPicklePath ← tempPath IO.FS.withTempFile λ _ envPicklePath => do
let ((), _) ← runCoreM coreSrc do let ((), _) ← runCoreM coreSrc do
let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default
@ -56,13 +53,10 @@ def test_environment_pickling : TestM Unit := do
let anotherName := `mystery2 let anotherName := `mystery2
checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone
IO.FS.removeFile envPicklePath
def test_goal_state_pickling_simple : TestM Unit := do def test_goal_state_pickling_simple : TestM Unit := do
let coreSrc : Core.State := { env := ← getEnv } let coreSrc : Core.State := { env := ← getEnv }
let coreDst : Core.State := { env := ← getEnv } let coreDst : Core.State := { env := ← getEnv }
let statePath ← tempPath IO.FS.withTempFile λ _ statePath => do
let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
let stateGenerate : MetaM GoalState := runTermElabMInMeta do let stateGenerate : MetaM GoalState := runTermElabMInMeta do
GoalState.create type GoalState.create type
@ -78,8 +72,6 @@ def test_goal_state_pickling_simple : TestM Unit := do
let types ← metaM.run' let types ← metaM.run'
checkTrue "Goals" $ types[0]!.equal type checkTrue "Goals" $ types[0]!.equal type
IO.FS.removeFile statePath
structure Test where structure Test where
name : String name : String
routine: TestM Unit routine: TestM Unit