8 changed files with 109 additions and 91 deletions
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@ -67,7 +67,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
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@ -80,10 +80,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
@ -131,7 +131,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
 -- NOTE: Plural deliberately not spelled "sorries"
@[export pantograph_frontend_collect_sorrys_m]
 def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
-  return (← step.trees.mapM collectSorrysInTree).join
+  return (← step.trees.mapM collectSorrysInTree).flatten

 structure AnnotatedGoalState where
  state : GoalState
@ -155,7 +155,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState
      let range := stxByteRange tacticInfo.stx
      return mvarIds.map (·, range)
    | _ => panic! "Invalid info"
-  let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
+  let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
  let goals := annotatedGoals.map Prod.fst
  let srcBoundaries := annotatedGoals.map Prod.snd
  let root := match goals with
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@ -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)
  | .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 []

 /-- 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
  | .node i children  =>
    let head := if pred i then [(i, context?, children)] else []
-    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
+    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.flatMap (fun t => findAllInfo t context? haltOnMatch pred)
    head ++ tail
  | _ => []

@ -119,7 +119,7 @@ partial def InfoTree.findAllInfoM [Monad m]
    let (flagCollect, flagRecurse) ← pred i context?
    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)
-    return head ++ (← tail).join
+    return head ++ (← tail).flatten
  | _ => return []

@[export pantograph_infotree_to_string_m]
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -561,10 +561,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"
@ -647,13 +647,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"
@ -670,7 +670,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
@ -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 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 := #[{
--- 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) :=
  [
--- 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"
      }
--- 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;
@ -32,68 +32,85 @@
        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;
-      };
-      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];
+        };
      };
    };
-  };
 }
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.14.0