build: Toolchain bump and Nix flake fix #49
|
@ -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 := "<Pantograph>",
|
||||
fileMap := { source := "", positions := #[0], lines := #[1] },
|
||||
fileMap := { source := "", positions := #[0] },
|
||||
options := options
|
||||
}
|
||||
|
||||
|
|
25
README.md
25
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": <id>}"`: 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.
|
||||
|
|
|
@ -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 := "<Pantograph/Test>",
|
||||
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
|
||||
|
|
|
@ -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)
|
||||
|
||||
|
|
|
@ -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 := "<Pantograph>",
|
||||
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:
|
||||
|
|
|
@ -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 := "<Test>",
|
||||
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))
|
||||
|
|
|
@ -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 := "<Pantograph>",
|
||||
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 := [
|
||||
|
|
|
@ -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
|
||||
|
|
66
flake.lock
66
flake.lock
|
@ -38,19 +38,22 @@
|
|||
"flake-utils": "flake-utils",
|
||||
"lean4-mode": "lean4-mode",
|
||||
"nix": "nix",
|
||||
"nixpkgs": "nixpkgs_2"
|
||||
"nixpkgs": [
|
||||
"nixpkgs"
|
||||
],
|
||||
"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"
|
||||
}
|
||||
|
@ -87,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",
|
||||
|
@ -141,6 +161,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,
|
||||
|
@ -158,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=",
|
||||
|
@ -193,7 +214,8 @@
|
|||
"inputs": {
|
||||
"flake-parts": "flake-parts",
|
||||
"lean": "lean",
|
||||
"nixpkgs": "nixpkgs_3"
|
||||
"lspec": "lspec",
|
||||
"nixpkgs": "nixpkgs_2"
|
||||
}
|
||||
}
|
||||
},
|
||||
|
|
38
flake.nix
38
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=f70895ede54501adf0db77474f452a7fef40d0b3";
|
||||
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,17 +30,45 @@
|
|||
];
|
||||
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";
|
||||
# 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 = pkgs.runCommand "test" {
|
||||
buildInputs = [ test.executable leanPkgs.lean-all ];
|
||||
} ''
|
||||
#export LEAN_SRC_PATH="${./.}"
|
||||
${test.executable}/bin/test > $out
|
||||
'';
|
||||
};
|
||||
devShells.default = project.devShell;
|
||||
};
|
||||
};
|
||||
|
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:4.7.0-rc2
|
||||
leanprover/lean4:nightly-2024-03-27
|
||||
|
|
Loading…
Reference in New Issue