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
|
||||
}
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
28
flake.lock
28
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,
|
||||
|
|
10
flake.nix
10
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;
|
||||
};
|
||||
};
|
||||
|
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:4.7.0-rc2
|
||||
leanprover/lean4:nightly-2024-03-27
|
||||
|
|
Loading…
Reference in New Issue