Compare commits

..

No commits in common. "misc/version" and "dev" have entirely different histories.

8 changed files with 91 additions and 109 deletions

View File

@ -67,7 +67,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
let s := (← get).commandState let s := (← get).commandState
let before := s.env let before := s.env
let done ← Elab.Frontend.processCommand let done ← Elab.Frontend.processCommand
let stx := (← get).commands.back! let stx := (← get).commands.back
let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
let s' := (← get).commandState let s' := (← get).commandState
let after := s'.env let after := s'.env

View File

@ -80,10 +80,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
@[export pantograph_frontend_collect_tactics_from_compilation_step_m] @[export pantograph_frontend_collect_tactics_from_compilation_step_m]
def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
| info@(.ofTacticInfo _) => info.isOriginal | info@(.ofTacticInfo _) => info.isOriginal
| _ => false | _ => false
let tactics := tacticInfoTrees.flatMap collectTactics let tactics := tacticInfoTrees.bind collectTactics
tactics.mapM λ invocation => do tactics.mapM λ invocation => do
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
@ -131,7 +131,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
-- NOTE: Plural deliberately not spelled "sorries" -- NOTE: Plural deliberately not spelled "sorries"
@[export pantograph_frontend_collect_sorrys_m] @[export pantograph_frontend_collect_sorrys_m]
def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
return (← step.trees.mapM collectSorrysInTree).flatten return (← step.trees.mapM collectSorrysInTree).join
structure AnnotatedGoalState where structure AnnotatedGoalState where
state : GoalState state : GoalState
@ -155,7 +155,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState
let range := stxByteRange tacticInfo.stx let range := stxByteRange tacticInfo.stx
return mvarIds.map (·, range) return mvarIds.map (·, range)
| _ => panic! "Invalid info" | _ => panic! "Invalid info"
let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {}) let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
let goals := annotatedGoals.map Prod.fst let goals := annotatedGoals.map Prod.fst
let srcBoundaries := annotatedGoals.map Prod.snd let srcBoundaries := annotatedGoals.map Prod.snd
let root := match goals with let root := match goals with

View File

@ -87,9 +87,9 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ =>
| .context ctx tree => tree.filter p m |>.map (.context ctx) | .context ctx tree => tree.filter p m |>.map (.context ctx)
| .node info children => | .node info children =>
if p info then if p info then
[.node info (children.toList.map (filter p m)).flatten.toPArray'] [.node info (children.toList.map (filter p m)).join.toPArray']
else else
(children.toList.map (filter p m)).flatten (children.toList.map (filter p m)).join
| .hole mvar => if m mvar then [.hole mvar] else [] | .hole mvar => if m mvar then [.hole mvar] else []
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/ /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@ -103,7 +103,7 @@ partial def InfoTree.findAllInfo
| .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
| .node i children => | .node i children =>
let head := if pred i then [(i, context?, children)] else [] let head := if pred i then [(i, context?, children)] else []
let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.flatMap (fun t => findAllInfo t context? haltOnMatch pred) let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
head ++ tail head ++ tail
| _ => [] | _ => []
@ -119,7 +119,7 @@ partial def InfoTree.findAllInfoM [Monad m]
let (flagCollect, flagRecurse) ← pred i context? let (flagCollect, flagRecurse) ← pred i context?
let head := if flagCollect then [(i, context?, children)] else [] let head := if flagCollect then [(i, context?, children)] else []
let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred) let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred)
return head ++ (← tail).flatten return head ++ (← tail).join
| _ => return [] | _ => return []
@[export pantograph_infotree_to_string_m] @[export pantograph_infotree_to_string_m]

View File

@ -561,10 +561,10 @@ def test_nat_zero_add: TestM Unit := do
return () return ()
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[ #[
buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal "_uniq.72" [("n", "Nat")] "Nat", buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit") buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
]) ])
let tactic := "exact n" let tactic := "exact n"
@ -647,13 +647,13 @@ def test_nat_zero_add_alt: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
let major := "_uniq.72" let major := "_uniq.68"
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[ #[
buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal major [("n", "Nat")] "Nat", buildNamedGoal major [("n", "Nat")] "Nat",
buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit") buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
]) ])
let tactic := "intro x" let tactic := "intro x"
@ -670,7 +670,7 @@ def test_nat_zero_add_alt: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
let (eqL, eqR, eqT) := ("_uniq.92", "_uniq.93", "_uniq.91") let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT] addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict" let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
let state2b ← match state3m2.resume [conduit] with let state2b ← match state3m2.resume [conduit] with
@ -681,16 +681,16 @@ def test_nat_zero_add_alt: TestM Unit := do
let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))" let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))" let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
let fvN := "_uniq.67" let fvN := "_uniq.63"
let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))" let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))" let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) = addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
#[ #[
{ {
name := "_uniq.74", name := "_uniq.70",
userName? := .some "conduit", userName? := .some "conduit",
target := { target := {
pp? := .some "(?m.96 ?m.72 = ?m.98 ?m.72) = (n + 0 = n)", pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})", sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
}, },
vars := #[{ vars := #[{

View File

@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
"Nat → Prop", "Nat → Prop",
"Nat", "Nat",
"∀ (t : Nat), Nat.below t → ?motive t", "∀ (t : Nat), Nat.below t → ?motive t",
"?motive ?m.71 = (n + 0 = n)", "?motive ?m.67 = (n + 0 = n)",
]) ])
addTest test addTest test
@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let tactic := Tactic.evalMotivatedApply recursor let tactic := Tactic.evalMotivatedApply recursor
let newGoals ← runTacticOnMVar tactic target.mvarId! let newGoals ← runTacticOnMVar tactic target.mvarId!
let majorId := 71 let majorId := 67
addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
[ [
"Nat → Prop", "Nat → Prop",
@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
addTest $ ← conduit.withContext do addTest $ ← conduit.withContext do
let t := toString (← Meta.ppExpr $ ← conduit.getType) let t := toString (← Meta.ppExpr $ ← conduit.getType)
return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.146 ?m.{majorId}) = (n + 0 = n)") return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
def suite (env: Environment): List (String × IO LSpec.TestSeq) := def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[ [

View File

@ -42,16 +42,15 @@
"nixpkgs": "nixpkgs" "nixpkgs": "nixpkgs"
}, },
"locked": { "locked": {
"lastModified": 1733351931, "lastModified": 1731711316,
"narHash": "sha256-ngMjY/ci6490G2gofaS9CODtpnmFoYzfaI13U14TkFM=", "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
"owner": "lenianiva", "owner": "lenianiva",
"repo": "lean4-nix", "repo": "lean4-nix",
"rev": "157c85903f668fadeb79f330961b7bbe5ee596de", "rev": "136fc6057c48de970579e960b62421e9c295b67d",
"type": "github" "type": "github"
}, },
"original": { "original": {
"owner": "lenianiva", "owner": "lenianiva",
"ref": "157c85903f668fadeb79f330961b7bbe5ee596de",
"repo": "lean4-nix", "repo": "lean4-nix",
"type": "github" "type": "github"
} }

143
flake.nix
View File

@ -4,7 +4,7 @@
inputs = { inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05"; nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
flake-parts.url = "github:hercules-ci/flake-parts"; flake-parts.url = "github:hercules-ci/flake-parts";
lean4-nix.url = "github:lenianiva/lean4-nix?ref=157c85903f668fadeb79f330961b7bbe5ee596de"; lean4-nix.url = "github:lenianiva/lean4-nix";
lspec = { lspec = {
url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab"; url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
flake = false; flake = false;
@ -32,85 +32,68 @@
inherit system; inherit system;
overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ]; overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
}; };
systems = [ lspecLib = pkgs.lean.buildLeanPackage {
"aarch64-linux" name = "LSpec";
"aarch64-darwin" roots = [ "Main" "LSpec" ];
"x86_64-linux" src = "${lspec}";
"x86_64-darwin" };
]; project = pkgs.lean.buildLeanPackage {
perSystem = { name = "Pantograph";
system, roots = [ "Pantograph" ];
pkgs, src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
... src = ./.;
}: let filter = path: type:
pkgs = import nixpkgs { !(pkgs.lib.hasInfix "/Test/" path) &&
inherit system; !(pkgs.lib.hasSuffix ".md" path) &&
overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)]; !(pkgs.lib.hasSuffix "Repl.lean" path);
}; });
lspecLib = pkgs.lean.buildLeanPackage { };
name = "LSpec"; repl = pkgs.lean.buildLeanPackage {
roots = ["Main" "LSpec"]; name = "Repl";
src = "${lspec}"; roots = [ "Main" "Repl" ];
}; deps = [ project ];
project = pkgs.lean.buildLeanPackage { src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
name = "Pantograph"; src = ./.;
roots = ["Pantograph"]; filter = path: type:
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { !(pkgs.lib.hasInfix "/Test/" path) &&
src = ./.; !(pkgs.lib.hasSuffix ".md" path);
filter = path: type: });
!(pkgs.lib.hasInfix "/Test/" path) };
&& !(pkgs.lib.hasSuffix ".md" path) test = pkgs.lean.buildLeanPackage {
&& !(pkgs.lib.hasSuffix "Repl.lean" path); name = "Test";
}); # NOTE: The src directory must be ./. since that is where the import
}; # root begins (e.g. `import Test.Environment` and not `import
repl = pkgs.lean.buildLeanPackage { # Environment`) and thats where `lakefile.lean` resides.
name = "Repl"; roots = [ "Test.Main" ];
roots = ["Main" "Repl"]; deps = [ lspecLib repl ];
deps = [project]; src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { src = ./.;
src = ./.; filter = path: type:
filter = path: type: !(pkgs.lib.hasInfix "Pantograph" path);
!(pkgs.lib.hasInfix "/Test/" path) });
&& !(pkgs.lib.hasSuffix ".md" path); };
}); in rec {
}; packages = {
test = pkgs.lean.buildLeanPackage { inherit (pkgs.lean) lean lean-all;
name = "Test"; inherit (project) sharedLib iTree;
# NOTE: The src directory must be ./. since that is where the import inherit (repl) executable;
# root begins (e.g. `import Test.Environment` and not `import default = repl.executable;
# Environment`) and thats where `lakefile.lean` resides. };
roots = ["Test.Main"]; legacyPackages = {
deps = [lspecLib repl]; inherit project;
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { leanPkgs = pkgs.lean;
src = ./.; };
filter = path: type: checks = {
!(pkgs.lib.hasInfix "Pantograph" path); test = pkgs.runCommand "test" {
}); buildInputs = [ test.executable pkgs.lean.lean-all ];
}; } ''
in rec { #export LEAN_SRC_PATH="${./.}"
packages = { ${test.executable}/bin/test > $out
inherit (pkgs.lean) lean lean-all; '';
inherit (project) sharedLib iTree; };
inherit (repl) executable; devShells.default = pkgs.mkShell {
default = repl.executable; buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
};
formatter = pkgs.alejandra;
legacyPackages = {
inherit project;
leanPkgs = pkgs.lean;
};
checks = {
test =
pkgs.runCommand "test" {
buildInputs = [test.executable pkgs.lean.lean-all];
} ''
#export LEAN_SRC_PATH="${./.}"
${test.executable}/bin/test > $out
'';
};
devShells.default = pkgs.mkShell {
buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
};
}; };
}; };
};
} }

View File

@ -1 +1 @@
leanprover/lean4:v4.14.0 leanprover/lean4:v4.12.0