feat: State and environment pickling #120
|
|
@ -122,6 +122,13 @@ protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
|
|||
protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
|
||||
t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
|
||||
|
||||
protected def usedConstants (t: TacticInvocation) : NameSet :=
|
||||
let info := t.info
|
||||
info.goalsBefore
|
||||
|>.filterMap info.mctxAfter.getExprAssignmentCore?
|
||||
|>.map Expr.getUsedConstantsAsSet
|
||||
|>.foldl .union .empty
|
||||
|
||||
end TacticInvocation
|
||||
|
||||
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
|
||||
|
|
@ -158,7 +165,13 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
|
|||
let tactic ← invocation.ctx.runMetaM {} do
|
||||
let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
|
||||
return t.pretty
|
||||
return { goalBefore, goalAfter, tactic }
|
||||
let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
|
||||
return {
|
||||
goalBefore,
|
||||
goalAfter,
|
||||
tactic,
|
||||
usedConstants,
|
||||
}
|
||||
|
||||
structure InfoWithContext where
|
||||
info: Elab.Info
|
||||
|
|
|
|||
|
|
@ -304,6 +304,9 @@ structure InvokedTactic where
|
|||
goalBefore: String
|
||||
goalAfter: String
|
||||
tactic: String
|
||||
|
||||
-- List of used constants
|
||||
usedConstants: Array String
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure CompilationUnit where
|
||||
|
|
|
|||
|
|
@ -167,8 +167,8 @@ example : ∀ (p: Prop), p → p := by
|
|||
|
||||
def test_frontend_process : Test :=
|
||||
[
|
||||
let file := "example : ∀ (p: Prop), p → p := by\n intro p h\n exact h"
|
||||
let goal1 := "p : Prop\nh : p\n⊢ p"
|
||||
let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n intro p q h\n exact Or.inl h"
|
||||
let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
|
||||
step "frontend.process"
|
||||
[
|
||||
("file", .str file),
|
||||
|
|
@ -180,14 +180,16 @@ def test_frontend_process : Test :=
|
|||
boundary := (0, file.utf8ByteSize),
|
||||
invocations? := .some [
|
||||
{
|
||||
goalBefore := "⊢ ∀ (p : Prop), p → p",
|
||||
goalBefore := "⊢ ∀ (p q : Prop), p → p ∨ q",
|
||||
goalAfter := goal1,
|
||||
tactic := "intro p h",
|
||||
tactic := "intro p q h",
|
||||
usedConstants := #[],
|
||||
},
|
||||
{
|
||||
goalBefore := goal1 ,
|
||||
goalAfter := "",
|
||||
tactic := "exact h",
|
||||
tactic := "exact Or.inl h",
|
||||
usedConstants := #["Or.inl"],
|
||||
},
|
||||
]
|
||||
}],
|
||||
|
|
|
|||
137
flake.lock
137
flake.lock
|
|
@ -5,11 +5,11 @@
|
|||
"nixpkgs-lib": "nixpkgs-lib"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1709336216,
|
||||
"narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
|
||||
"lastModified": 1730504689,
|
||||
"narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=",
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
|
||||
"rev": "506278e768c2a08bec68eb62932193e341f55c90",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
|
@ -18,40 +18,40 @@
|
|||
"type": "github"
|
||||
}
|
||||
},
|
||||
"flake-utils": {
|
||||
"locked": {
|
||||
"lastModified": 1656928814,
|
||||
"narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lean": {
|
||||
"flake-parts_2": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils",
|
||||
"nixpkgs": "nixpkgs",
|
||||
"nixpkgs-cadical": "nixpkgs-cadical",
|
||||
"nixpkgs-old": "nixpkgs-old"
|
||||
"nixpkgs-lib": "nixpkgs-lib_2"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1727749878,
|
||||
"narHash": "sha256-O2Egyh2D0TfQWzQKfHUeAh7qAjMfeLVwXwGUw5QqcvE=",
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4",
|
||||
"rev": "dc2533473114eb8656439ff2b9335209784aa640",
|
||||
"lastModified": 1727826117,
|
||||
"narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "leanprover",
|
||||
"ref": "v4.12.0",
|
||||
"repo": "lean4",
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lean4-nix": {
|
||||
"inputs": {
|
||||
"flake-parts": "flake-parts_2",
|
||||
"nixpkgs": "nixpkgs"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1731711316,
|
||||
"narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
|
||||
"owner": "lenianiva",
|
||||
"repo": "lean4-nix",
|
||||
"rev": "136fc6057c48de970579e960b62421e9c295b67d",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "lenianiva",
|
||||
"repo": "lean4-nix",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
|
|
@ -74,83 +74,56 @@
|
|||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1686089707,
|
||||
"narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
|
||||
"owner": "NixOS",
|
||||
"lastModified": 1728500571,
|
||||
"narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
|
||||
"rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"ref": "nixpkgs-unstable",
|
||||
"owner": "nixos",
|
||||
"ref": "nixos-24.05",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-cadical": {
|
||||
"locked": {
|
||||
"lastModified": 1722221733,
|
||||
"narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-lib": {
|
||||
"locked": {
|
||||
"dir": "lib",
|
||||
"lastModified": 1709237383,
|
||||
"narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
|
||||
"type": "github"
|
||||
"lastModified": 1730504152,
|
||||
"narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=",
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
|
||||
},
|
||||
"original": {
|
||||
"dir": "lib",
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-unstable",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
|
||||
}
|
||||
},
|
||||
"nixpkgs-old": {
|
||||
"flake": false,
|
||||
"nixpkgs-lib_2": {
|
||||
"locked": {
|
||||
"lastModified": 1581379743,
|
||||
"narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
|
||||
"type": "github"
|
||||
"lastModified": 1727825735,
|
||||
"narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-19.03",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
|
||||
}
|
||||
},
|
||||
"nixpkgs_2": {
|
||||
"locked": {
|
||||
"lastModified": 1711703276,
|
||||
"narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
|
||||
"lastModified": 1731386116,
|
||||
"narHash": "sha256-lKA770aUmjPHdTaJWnP3yQ9OI1TigenUqVC3wweqZuI=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
|
||||
"rev": "689fed12a013f56d4c4d3f612489634267d86529",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"ref": "nixos-unstable",
|
||||
"ref": "nixos-24.05",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
|
|
@ -158,7 +131,7 @@
|
|||
"root": {
|
||||
"inputs": {
|
||||
"flake-parts": "flake-parts",
|
||||
"lean": "lean",
|
||||
"lean4-nix": "lean4-nix",
|
||||
"lspec": "lspec",
|
||||
"nixpkgs": "nixpkgs_2"
|
||||
}
|
||||
|
|
|
|||
33
flake.nix
33
flake.nix
|
|
@ -2,12 +2,9 @@
|
|||
description = "Pantograph";
|
||||
|
||||
inputs = {
|
||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
|
||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
|
||||
flake-parts.url = "github:hercules-ci/flake-parts";
|
||||
lean = {
|
||||
# Do not follow input's nixpkgs since it could cause build failures
|
||||
url = "github:leanprover/lean4?ref=v4.12.0";
|
||||
};
|
||||
lean4-nix.url = "github:lenianiva/lean4-nix";
|
||||
lspec = {
|
||||
url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
|
||||
flake = false;
|
||||
|
|
@ -18,7 +15,7 @@
|
|||
self,
|
||||
nixpkgs,
|
||||
flake-parts,
|
||||
lean,
|
||||
lean4-nix,
|
||||
lspec,
|
||||
...
|
||||
} : flake-parts.lib.mkFlake { inherit inputs; } {
|
||||
|
|
@ -29,13 +26,16 @@
|
|||
"x86_64-darwin"
|
||||
];
|
||||
perSystem = { system, pkgs, ... }: let
|
||||
leanPkgs = lean.packages.${system}.deprecated;
|
||||
lspecLib = leanPkgs.buildLeanPackage {
|
||||
pkgs = import nixpkgs {
|
||||
inherit system;
|
||||
overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
|
||||
};
|
||||
lspecLib = pkgs.lean.buildLeanPackage {
|
||||
name = "LSpec";
|
||||
roots = [ "Main" "LSpec" ];
|
||||
src = "${lspec}";
|
||||
};
|
||||
project = leanPkgs.buildLeanPackage {
|
||||
project = pkgs.lean.buildLeanPackage {
|
||||
name = "Pantograph";
|
||||
roots = [ "Pantograph" ];
|
||||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||
|
|
@ -46,7 +46,7 @@
|
|||
!(pkgs.lib.hasSuffix "Repl.lean" path);
|
||||
});
|
||||
};
|
||||
repl = leanPkgs.buildLeanPackage {
|
||||
repl = pkgs.lean.buildLeanPackage {
|
||||
name = "Repl";
|
||||
roots = [ "Main" "Repl" ];
|
||||
deps = [ project ];
|
||||
|
|
@ -57,7 +57,7 @@
|
|||
!(pkgs.lib.hasSuffix ".md" path);
|
||||
});
|
||||
};
|
||||
test = leanPkgs.buildLeanPackage {
|
||||
test = pkgs.lean.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
|
||||
|
|
@ -72,24 +72,25 @@
|
|||
};
|
||||
in rec {
|
||||
packages = {
|
||||
inherit (leanPkgs) lean lean-all;
|
||||
inherit (project) sharedLib;
|
||||
inherit (pkgs.lean) lean lean-all;
|
||||
inherit (project) sharedLib iTree;
|
||||
inherit (repl) executable;
|
||||
default = repl.executable;
|
||||
};
|
||||
legacyPackages = {
|
||||
inherit project leanPkgs;
|
||||
inherit project;
|
||||
leanPkgs = pkgs.lean;
|
||||
};
|
||||
checks = {
|
||||
test = pkgs.runCommand "test" {
|
||||
buildInputs = [ test.executable leanPkgs.lean-all ];
|
||||
buildInputs = [ test.executable pkgs.lean.lean-all ];
|
||||
} ''
|
||||
#export LEAN_SRC_PATH="${./.}"
|
||||
${test.executable}/bin/test > $out
|
||||
'';
|
||||
};
|
||||
devShells.default = pkgs.mkShell {
|
||||
buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
|
||||
buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
|
||||
};
|
||||
};
|
||||
};
|
||||
|
|
|
|||
Loading…
Reference in New Issue