From 13dd11e9955dc12bf40208b22898c2942c844cce Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 18:55:30 -0800 Subject: [PATCH 1/2] chore: Update Lean to v4.14 --- Pantograph/Frontend/Basic.lean | 2 +- Pantograph/Frontend/Elab.lean | 15 ++++++++------- Test/Integration.lean | 2 +- Test/Proofs.lean | 24 ++++++++++++------------ Test/Tactic/MotivatedApply.lean | 6 +++--- lean-toolchain | 2 +- 6 files changed, 26 insertions(+), 25 deletions(-) diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean index 1074a94..51f3433 100644 --- a/Pantograph/Frontend/Basic.lean +++ b/Pantograph/Frontend/Basic.lean @@ -60,7 +60,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do let s := (← get).commandState let before := s.env 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 s' := (← get).commandState let after := s'.env diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean index ceecfae..57179c4 100644 --- a/Pantograph/Frontend/Elab.lean +++ b/Pantograph/Frontend/Elab.lean @@ -70,9 +70,9 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) : | .context ctx tree => tree.filter p m |>.map (.context ctx) | .node info children => if p info then - [.node info (children.toList.map (filter p m)).join.toPArray'] + [.node info (children.toList.map (filter p m)).flatten.toPArray'] else - (children.toList.map (filter p m)).join + (children.toList.map (filter p m)).flatten | .hole mvar => if m mvar then [.hole mvar] else [] end Lean.Elab.InfoTree @@ -137,7 +137,8 @@ partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) match t with | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred | .node i children => - (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred) + (if pred i then [(i, context?, children)] else []) ++ + children.toList.flatMap (fun t => findAllInfo t context? pred) | _ => [] /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics, @@ -155,10 +156,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation := @[export pantograph_frontend_collect_tactics_from_compilation_step_m] def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do - let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ + let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ | info@(.ofTacticInfo _) => info.isOriginal | _ => false - let tactics := tacticInfoTrees.bind collectTactics + let tactics := tacticInfoTrees.flatMap collectTactics tactics.mapM λ invocation => do let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty @@ -191,7 +192,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext := -- NOTE: Plural deliberately not spelled "sorries" @[export pantograph_frontend_collect_sorrys_m] def collectSorrys (step: CompilationStep) : List InfoWithContext := - step.trees.bind collectSorrysInTree + step.trees.flatMap collectSorrysInTree @@ -211,7 +212,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do | .ofTacticInfo tacticInfo => do MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context? | _ => panic! "Invalid info" - let goals := List.join (← goalsM.run {} |>.run' {}) + let goals := List.flatten (← goalsM.run {} |>.run' {}) let root := match goals with | [] => panic! "No MVars generated" | [g] => g diff --git a/Test/Integration.lean b/Test/Integration.lean index 9fb86b7..60f011f 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -73,7 +73,7 @@ def test_tactic : Test := step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult), step "goal.print" [("stateId", .num 1)] - ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult), + ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult), step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult), ] diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 02c1bf6..dfe3722 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -564,10 +564,10 @@ def test_nat_zero_add: TestM Unit := do return () addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = #[ - buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), - buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat", - buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", - buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit") + buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"), + buildNamedGoal "_uniq.72" [("n", "Nat")] "Nat", + buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", + buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit") ]) let tactic := "exact n" @@ -650,13 +650,13 @@ def test_nat_zero_add_alt: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - let major := "_uniq.68" + let major := "_uniq.72" addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = #[ - buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), + buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal major [("n", "Nat")] "Nat", - buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", - buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit") + buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", + buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit") ]) let tactic := "intro x" @@ -673,7 +673,7 @@ def test_nat_zero_add_alt: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87") + let (eqL, eqR, eqT) := ("_uniq.92", "_uniq.93", "_uniq.91") addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT] let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict" let state2b ← match state3m2.resume [conduit] with @@ -684,16 +684,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 cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))" - let fvN := "_uniq.63" + let fvN := "_uniq.67" 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}))" addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) = #[ { - name := "_uniq.70", + name := "_uniq.74", userName? := .some "conduit", target := { - pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)", + pp? := .some "(?m.96 ?m.72 = ?m.98 ?m.72) = (n + 0 = n)", sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})", }, vars := #[{ diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 4fb05e3..8c8fdad 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do "Nat → Prop", "Nat", "∀ (t : Nat), Nat.below t → ?motive t", - "?motive ?m.67 = (n + 0 = n)", + "?motive ?m.71 = (n + 0 = n)", ]) addTest test @@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do let target ← Meta.mkFreshExprSyntheticOpaqueMVar body let tactic := Tactic.evalMotivatedApply recursor let newGoals ← runTacticOnMVar tactic target.mvarId! - let majorId := 67 + let majorId := 71 addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [ "Nat → Prop", @@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do addTest $ ← conduit.withContext do let t := toString (← Meta.ppExpr $ ← conduit.getType) - return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)") + return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.146 ?m.{majorId}) = (n + 0 = n)") def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ diff --git a/lean-toolchain b/lean-toolchain index 8998520..1e70935 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0 +leanprover/lean4:v4.14.0 From fb3d36584fe7f5155669ab3227fc5213b8f3c3e6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 5 Dec 2024 18:59:14 -0800 Subject: [PATCH 2/2] chore: Add formatter, update lean4-nix --- flake.lock | 7 ++- flake.nix | 157 ++++++++++++++++++++++++++++------------------------- 2 files changed, 87 insertions(+), 77 deletions(-) diff --git a/flake.lock b/flake.lock index f40dde9..9f54bbe 100644 --- a/flake.lock +++ b/flake.lock @@ -42,15 +42,16 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1731711316, - "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=", + "lastModified": 1733351931, + "narHash": "sha256-ngMjY/ci6490G2gofaS9CODtpnmFoYzfaI13U14TkFM=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "136fc6057c48de970579e960b62421e9c295b67d", + "rev": "157c85903f668fadeb79f330961b7bbe5ee596de", "type": "github" }, "original": { "owner": "lenianiva", + "ref": "157c85903f668fadeb79f330961b7bbe5ee596de", "repo": "lean4-nix", "type": "github" } diff --git a/flake.nix b/flake.nix index 91901d8..d8ce698 100644 --- a/flake.nix +++ b/flake.nix @@ -4,7 +4,7 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05"; flake-parts.url = "github:hercules-ci/flake-parts"; - lean4-nix.url = "github:lenianiva/lean4-nix"; + lean4-nix.url = "github:lenianiva/lean4-nix?ref=157c85903f668fadeb79f330961b7bbe5ee596de"; lspec = { url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab"; flake = false; @@ -18,80 +18,89 @@ lean4-nix, lspec, ... - } : flake-parts.lib.mkFlake { inherit inputs; } { - flake = { - }; - systems = [ - "x86_64-linux" - "x86_64-darwin" - ]; - perSystem = { system, pkgs, ... }: let - pkgs = import nixpkgs { - inherit system; - overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ]; + }: + flake-parts.lib.mkFlake {inherit inputs;} { + flake = { }; - lspecLib = pkgs.lean.buildLeanPackage { - name = "LSpec"; - roots = [ "Main" "LSpec" ]; - src = "${lspec}"; - }; - project = pkgs.lean.buildLeanPackage { - name = "Pantograph"; - roots = [ "Pantograph" ]; - src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { - src = ./.; - filter = path: type: - !(pkgs.lib.hasInfix "/Test/" path) && - !(pkgs.lib.hasSuffix ".md" path) && - !(pkgs.lib.hasSuffix "Repl.lean" path); - }); - }; - repl = pkgs.lean.buildLeanPackage { - name = "Repl"; - roots = [ "Main" "Repl" ]; - deps = [ project ]; - src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { - src = ./.; - filter = path: type: - !(pkgs.lib.hasInfix "/Test/" path) && - !(pkgs.lib.hasSuffix ".md" path); - }); - }; - 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 - # Environment`) and thats where `lakefile.lean` resides. - roots = [ "Test.Main" ]; - deps = [ lspecLib repl ]; - src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { - src = ./.; - filter = path: type: - !(pkgs.lib.hasInfix "Pantograph" path); - }); - }; - in rec { - packages = { - inherit (pkgs.lean) lean lean-all; - inherit (project) sharedLib iTree; - inherit (repl) executable; - default = repl.executable; - }; - 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 ]; + systems = [ + "aarch64-linux" + "aarch64-darwin" + "x86_64-linux" + "x86_64-darwin" + ]; + perSystem = { + system, + pkgs, + ... + }: let + pkgs = import nixpkgs { + inherit system; + overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)]; + }; + lspecLib = pkgs.lean.buildLeanPackage { + name = "LSpec"; + roots = ["Main" "LSpec"]; + src = "${lspec}"; + }; + project = pkgs.lean.buildLeanPackage { + name = "Pantograph"; + roots = ["Pantograph"]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + !(pkgs.lib.hasInfix "/Test/" path) + && !(pkgs.lib.hasSuffix ".md" path) + && !(pkgs.lib.hasSuffix "Repl.lean" path); + }); + }; + repl = pkgs.lean.buildLeanPackage { + name = "Repl"; + roots = ["Main" "Repl"]; + deps = [project]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + !(pkgs.lib.hasInfix "/Test/" path) + && !(pkgs.lib.hasSuffix ".md" path); + }); + }; + 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 + # Environment`) and thats where `lakefile.lean` resides. + roots = ["Test.Main"]; + deps = [lspecLib repl]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + !(pkgs.lib.hasInfix "Pantograph" path); + }); + }; + in rec { + packages = { + inherit (pkgs.lean) lean lean-all; + inherit (project) sharedLib iTree; + inherit (repl) executable; + default = repl.executable; + }; + 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]; + }; }; }; - }; }