From 60903bf31f995a1a88b74635888e936546f5dcc6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 00:06:35 -0700 Subject: [PATCH] feat: Bump toolchain version --- Pantograph/Library.lean | 2 +- Test/Common.lean | 15 ++++++++------- Test/Environment.lean | 3 ++- Test/Holes.lean | 16 ++++------------ Test/Integration.lean | 12 +++--------- Test/Proofs.lean | 20 ++++++-------------- Test/Serial.lean | 7 ++----- flake.lock | 28 +++++++++++++++++++++++----- flake.nix | 10 +++++++++- lean-toolchain | 2 +- 10 files changed, 59 insertions(+), 56 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 52a88b6..078ca0f 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -63,7 +63,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do currNamespace := Lean.Name.str .anonymous "Aniva" openDecls := [], -- No 'open' directives needed fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] }, + fileMap := { source := "", positions := #[0] }, options := options } diff --git a/Test/Common.lean b/Test/Common.lean index 2257c7c..7c5b6e5 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,5 +1,6 @@ -import Pantograph.Protocol import Pantograph.Goal +import Pantograph.Library +import Pantograph.Protocol import LSpec namespace Pantograph @@ -35,12 +36,7 @@ def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message fa open Lean def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq): IO LSpec.TestSeq := do - let coreContext: Core.Context := { - currNamespace := Name.str .anonymous "Aniva" - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] } - } + let coreContext: Core.Context ← createCoreContext #[] match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "") @@ -53,4 +49,9 @@ def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α errToSorry := false, }) +def defaultTermElabMContext: Lean.Elab.Term.Context := { + declName? := some "_pantograph".toName, + errToSorry := false + } + end Pantograph diff --git a/Test/Environment.lean b/Test/Environment.lean index 977ed7d..9e3bd70 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -76,7 +76,8 @@ def test_inspect (env: Environment): IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do let env: Environment ← importModules - (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) + (imports := #[`Init]) + --(imports := #["Prelude"].map (λ str => { module := str.toName, runtimeOnly := false })) (opts := {}) (trustLevel := 1) diff --git a/Test/Holes.lean b/Test/Holes.lean index afad4e8..af322e9 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -44,16 +44,8 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options - let coreContext: Lean.Core.Context := { - currNamespace := Name.append .anonymous "Aniva", - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] } - } - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let coreContext: Lean.Core.Context ← createCoreContext #[] + let metaM := termElabM.run' (ctx := defaultTermElabMContext) let coreM := metaM.run' match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => @@ -169,7 +161,7 @@ def test_partial_continuation: TestM Unit := do return () | .ok state => pure state addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) + #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"]) addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone -- Roundtrip @@ -183,7 +175,7 @@ def test_partial_continuation: TestM Unit := do return () | .ok state => pure state addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]) + #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"]) addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone -- Continuation should fail if the state does not exist: diff --git a/Test/Integration.lean b/Test/Integration.lean index 0a6c210..83b3c9d 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -21,13 +21,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d let context: Context := { imports := ["Init"] } - let coreContext: Lean.Core.Context := { - currNamespace := Lean.Name.str .anonymous "Aniva" - openDecls := [], - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] }, - options := Lean.Options.empty - } + let coreContext: Lean.Core.Context ← createCoreContext #[] let commands: MainM LSpec.TestSeq := steps.foldlM (λ suite step => do let result ← step @@ -39,7 +33,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d return LSpec.check s!"Uncaught IO exception: {ex.toString}" false def test_option_modify : IO LSpec.TestSeq := - let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n" + let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ" let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))" let module? := Option.some "Init.Data.Nat.Basic" let options: Protocol.Options := {} @@ -142,7 +136,7 @@ def test_env : IO LSpec.TestSeq := subroutine_step "env.inspect" [("name", .str name2)] (Lean.toJson ({ - value? := .some { pp? := .some "fun a => Int.ofNat a + 1" }, + value? := .some { pp? := .some "fun a => ↑a + 1" }, type := { pp? := .some "Nat → Int" }, }: Protocol.EnvInspectResult)) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 85ba66d..833c02e 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -62,16 +62,8 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options - let coreContext: Lean.Core.Context := { - currNamespace := Name.append .anonymous "Aniva", - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] } - } - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let coreContext: Lean.Core.Context ← createCoreContext #[] + let metaM := termElabM.run' (ctx := defaultTermElabMContext) let coreM := metaM.run' match ← (coreM.run' coreContext { env := env }).toBaseIO with | .error exception => @@ -235,7 +227,7 @@ def proof_or_comm: TestM Unit := do let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false) -- This is due to delayed assignment addTest $ LSpec.test "(2 parent)" (state2parent == - "((:mv _uniq.45) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") + "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state @@ -243,7 +235,7 @@ def proof_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false) - addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.83))") + addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with | .success state => pure state @@ -252,7 +244,7 @@ def proof_or_comm: TestM Unit := do return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false) - addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.49)") + addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)") addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state @@ -304,7 +296,7 @@ def proof_or_comm: TestM Unit := do def suite: IO LSpec.TestSeq := do let env: Lean.Environment ← Lean.importModules - (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}]) + (imports := #[{ module := "Init".toName, runtimeOnly := false}]) (opts := {}) (trustLevel := 1) let tests := [ diff --git a/Test/Serial.lean b/Test/Serial.lean index 70e86e8..490b538 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -20,7 +20,7 @@ def test_name_to_ast: LSpec.TestSeq := def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do let entries: List (Name × Protocol.BoundExpression) := [ ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }), - ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" }) + ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" }) ] let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let env ← MonadEnv.getEnv @@ -58,10 +58,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do let expr := (← syntax_to_expr s) |>.toOption |>.get! let test := LSpec.check source ((← serialize_expression_ast expr) = target) return LSpec.TestSeq.append suites test) LSpec.TestSeq.done - let metaM := termElabM.run' (ctx := { - declName? := some "_pantograph", - errToSorry := false - }) + let metaM := termElabM.run' (ctx := defaultTermElabMContext) runMetaMSeq env metaM -- Instance parsing diff --git a/flake.lock b/flake.lock index 6278d68..1878e87 100644 --- a/flake.lock +++ b/flake.lock @@ -38,19 +38,20 @@ "flake-utils": "flake-utils", "lean4-mode": "lean4-mode", "nix": "nix", - "nixpkgs": "nixpkgs_2" + "nixpkgs": "nixpkgs_2", + "nixpkgs-old": "nixpkgs-old" }, "locked": { - "lastModified": 1710520221, - "narHash": "sha256-8Fm4bj9sqqsUHFZweSdGMM5GdUX3jkGK/ggGq27CeQc=", + "lastModified": 1711508550, + "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=", "owner": "leanprover", "repo": "lean4", - "rev": "f70895ede54501adf0db77474f452a7fef40d0b3", + "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", "type": "github" }, "original": { "owner": "leanprover", - "ref": "f70895ede54501adf0db77474f452a7fef40d0b3", + "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", "repo": "lean4", "type": "github" } @@ -141,6 +142,23 @@ "type": "github" } }, + "nixpkgs-old": { + "flake": false, + "locked": { + "lastModified": 1581379743, + "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "nixos-19.03", + "repo": "nixpkgs", + "type": "github" + } + }, "nixpkgs-regression": { "locked": { "lastModified": 1643052045, diff --git a/flake.nix b/flake.nix index dd98225..ed89fb0 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean.url = "github:leanprover/lean4?ref=f70895ede54501adf0db77474f452a7fef40d0b3"; + lean.url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; }; outputs = inputs @ { @@ -27,12 +27,20 @@ roots = [ "Main" "Pantograph" ]; src = ./.; }; + test = leanPkgs.buildLeanPackage { + name = "Test"; + roots = [ "Main" ]; + src = ./Test; + }; in rec { packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; default = project.executable; }; + checks = { + test = test.executable; + }; devShells.default = project.devShell; }; }; diff --git a/lean-toolchain b/lean-toolchain index faa2254..c630636 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.7.0-rc2 +leanprover/lean4:nightly-2024-03-27