From 60903bf31f995a1a88b74635888e936546f5dcc6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 00:06:35 -0700 Subject: [PATCH 1/3] 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 -- 2.44.1 From 22fdb7bea91021478fa0e98057f585fc0c25ddb7 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 11:33:15 -0700 Subject: [PATCH 2/3] build: Nix build targets and checks --- flake.lock | 40 ++++++++++++++++++++++------------------ flake.nix | 36 ++++++++++++++++++++++++++++++++---- 2 files changed, 54 insertions(+), 22 deletions(-) diff --git a/flake.lock b/flake.lock index 1878e87..f7f3012 100644 --- a/flake.lock +++ b/flake.lock @@ -38,7 +38,9 @@ "flake-utils": "flake-utils", "lean4-mode": "lean4-mode", "nix": "nix", - "nixpkgs": "nixpkgs_2", + "nixpkgs": [ + "nixpkgs" + ], "nixpkgs-old": "nixpkgs-old" }, "locked": { @@ -88,6 +90,23 @@ "type": "github" } }, + "lspec": { + "flake": false, + "locked": { + "lastModified": 1701971219, + "narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=", + "owner": "lurk-lab", + "repo": "LSpec", + "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "type": "github" + }, + "original": { + "owner": "lurk-lab", + "ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "repo": "LSpec", + "type": "github" + } + }, "nix": { "inputs": { "lowdown-src": "lowdown-src", @@ -176,22 +195,6 @@ } }, "nixpkgs_2": { - "locked": { - "lastModified": 1686089707, - "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=", - "owner": "NixOS", - "repo": "nixpkgs", - "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397", - "type": "github" - }, - "original": { - "owner": "NixOS", - "ref": "nixpkgs-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, - "nixpkgs_3": { "locked": { "lastModified": 1697456312, "narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=", @@ -211,7 +214,8 @@ "inputs": { "flake-parts": "flake-parts", "lean": "lean", - "nixpkgs": "nixpkgs_3" + "lspec": "lspec", + "nixpkgs": "nixpkgs_2" } } }, diff --git a/flake.nix b/flake.nix index ed89fb0..539d391 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,14 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean.url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; + lean = { + url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; + inputs.nixpkgs.follows = "nixpkgs"; + }; + lspec = { + url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; + flake = false; + }; }; outputs = inputs @ { @@ -12,6 +19,7 @@ nixpkgs, flake-parts, lean, + lspec, ... } : flake-parts.lib.mkFlake { inherit inputs; } { flake = { @@ -22,24 +30,44 @@ ]; perSystem = { system, pkgs, ... }: let leanPkgs = lean.packages.${system}; + lspecLib = leanPkgs.buildLeanPackage { + name = "LSpec"; + roots = [ "Main" "LSpec" ]; + src = "${lspec}"; + }; project = leanPkgs.buildLeanPackage { name = "Pantograph"; + #roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ]; roots = [ "Main" "Pantograph" ]; src = ./.; }; test = leanPkgs.buildLeanPackage { name = "Test"; - roots = [ "Main" ]; - src = ./Test; + # NOTE: The src directory must be ./. since that is where the import + # root begins (e.g. `import Test.Environment` and not `import + # Environment`) and thats where `lakefile.lean` resides. + roots = [ "Test.Main" ]; + deps = [ lspecLib project ]; + src = pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + !(pkgs.lib.hasInfix "Pantograph" path); + }; }; in rec { packages = { inherit (leanPkgs) lean lean-all; inherit (project) sharedLib executable; + test = test.executable; default = project.executable; }; checks = { - test = test.executable; + test = pkgs.runCommand "test" { + buildInputs = [ test.executable leanPkgs.lean-all ]; + } '' + #export LEAN_SRC_PATH="${./.}" + ${test.executable}/bin/test > $out + ''; }; devShells.default = project.devShell; }; -- 2.44.1 From 91e55245fae149b2e455dff84c3de976e2326f82 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 28 Mar 2024 11:37:07 -0700 Subject: [PATCH 3/3] doc: Update README.md --- README.md | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 1ca4d7b..c845b89 100644 --- a/README.md +++ b/README.md @@ -6,6 +6,8 @@ An interaction system for Lean 4. ## Installation +For Nix based workflow, see below. + Install `elan` and `lake`. Execute ``` sh make build/bin/pantograph @@ -20,7 +22,7 @@ LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ ``` The provided `flake.nix` has a develop environment with Lean already setup. -## Usage +## Executable Usage ``` sh pantograph MODULES|LEAN_OPTIONS @@ -63,7 +65,7 @@ stat ``` where the application of `assumption` should lead to a failure. -## Commands +### Commands See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. - `reset`: Delete all cached expressions and proof trees @@ -82,7 +84,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `goal.print {"stateId": }"`: Print a goal state - `stat`: Display resource usage -## Errors +### Errors When an error pertaining to the execution of a command happens, the returning JSON structure is @@ -97,16 +99,31 @@ Common error forms: input of another is broken. For example, attempting to query a symbol not existing in the library or indexing into a non-existent proof state. -## Troubleshooting +### Troubleshooting If lean encounters stack overflow problems when printing catalog, execute this before running lean: ```sh ulimit -s unlimited ``` +## Library Usage + +`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call +with `Pantograph`. + ## Testing The tests are based on `LSpec`. To run tests, ``` sh make test ``` + +## Nix based workflow + +To run tests: +``` sh +nix build .#checks.${system}.test +``` + +For example, `${system}` could be `x86_64-linux`. Using `nix develop` drops the +current session into a development shell with fixed Lean version. -- 2.44.1