diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index 6245877..ceecfae 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -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 diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 08c67ef..fcd5ebe 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -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 diff --git a/Test/Integration.lean b/Test/Integration.lean index 413ed1c..9fb86b7 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -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"], }, ] }], diff --git a/flake.lock b/flake.lock index dc83369..f40dde9 100644 --- a/flake.lock +++ b/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" } diff --git a/flake.nix b/flake.nix index d4c903f..91901d8 100644 --- a/flake.nix +++ b/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 ]; }; }; };