Pantograph/Delate.lean

@@ -63,16 +63,15 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
       (List.range numFields)
     mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
 
-def isAuxLemma (n : Name) : Bool :=
+def _root_.Lean.Name.isAuxLemma (n : Name) : Bool :=
   match n with
-  -- `mkAuxLemma` generally allows for arbitrary prefixes but these are the ones produced by core.
+  | .str _ s => "_proof_".isPrefixOf s
-  | .str _ s => "_proof_".isPrefixOf s || "_simp_".isPrefixOf s
   | _ => false
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
 @[export pantograph_unfold_aux_lemmas_m]
-def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
+def unfoldAuxLemmas : Expr → CoreM Expr :=
-  Meta.deltaExpand e isAuxLemma
+  (Meta.deltaExpand · Lean.Name.isAuxLemma)
 /-- Unfold all matcher applications -/
 @[export pantograph_unfold_matchers_m]
 def unfoldMatchers (expr : Expr) : CoreM Expr :=

Pantograph/Environment.lean

@@ -14,7 +14,7 @@ namespace Pantograph.Environment
 @[export pantograph_is_name_internal]
 def isNameInternal (n: Name): Bool :=
   -- Returns true if the name is an implementation detail which should not be shown to the user.
-  isAuxLemma n ∨ n.hasMacroScopes
+  n.isAuxLemma ∨ n.hasMacroScopes
 
 /-- Catalog all the non-internal and safe names -/
 @[export pantograph_environment_catalog]

Pantograph/Frontend/InfoTree.lean

@@ -10,7 +10,7 @@ namespace Lean.Elab
 private def elaboratorToString : Name → String
   | .anonymous => ""
   | n => s!"⟨{n}⟩ "
-private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("  " ++ .)
+private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .)
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
 protected def Info.stx? : Info → Option Syntax
@@ -131,16 +131,16 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
   | .node info children =>
     if let some ctx := ctx? then
       let node : String ← match info with
-      | .ofTermInfo    info => pure s!"[term] {info.stx}"
+      | .ofTermInfo    info => pure s!"[term] {(← info.toString ctx)}"
-      | .ofCommandInfo info => pure s!"[command] {info.stx}"
+      | .ofCommandInfo info => pure s!"[command] {(← info.toString ctx)}"
-      | .ofTacticInfo  info => pure s!"[tactic] {info.stx}"
+      | .ofTacticInfo  info => pure s!"[tactic] {(← info.toString ctx)}"
       | .ofMacroExpansionInfo _ => pure "[macro_exp]"
-      | .ofOptionInfo info => pure s!"[option] {info.stx}"
+      | .ofOptionInfo _ => pure "[option]"
       | .ofFieldInfo _ => pure "[field]"
-      | .ofCompletionInfo info => pure s!"[completion] {info.stx}"
+      | .ofCompletionInfo _ => pure "[completion]"
       | .ofUserWidgetInfo _ => pure "[user_widget]"
       | .ofCustomInfo _ => pure "[custom]"
-      | .ofFVarAliasInfo _ => pure "[fvar_alias]"
+      | .ofFVarAliasInfo _ => pure "[fvar]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
       | .ofChoiceInfo _ => pure "[choice]"
       | .ofPartialTermInfo  _ => pure "[partial_term]"

Pantograph/Version.lean

@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.3.4"
+def version := "0.3.3"
 
 end Pantograph

Test/Delate.lean

@@ -48,6 +48,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
 def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × (List Name) × String) := [
     ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
+    ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
     ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
     ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
     ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.20) (:mv _uniq.21) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"),

Test/Integration.lean

@@ -96,7 +96,7 @@ def test_tactic : Test := do
   step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult)
   step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
-   ({ messages? := .some #["tactic 'apply' failed, could not unify the conclusion of `@Nat.le_of_succ_le`\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith the goal\n  ∀ (q : Prop), x ∨ q → q ∨ x\n\nNote: The full type of `@Nat.le_of_succ_le` is\n  ∀ {n m : Nat}, n.succ ≤ m → n ≤ m\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
+   ({ messages? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
     Protocol.GoalTacticResult)
   step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult)
@@ -104,7 +104,7 @@ example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
   simp
 def test_tactic_timeout : Test := do
   step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.370" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.355" }: Protocol.GoalStartResult)
   -- timeout of 10 milliseconds
   step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet)
    ({ }: Protocol.OptionsSetResult)
@@ -168,15 +168,15 @@ def test_conv_calc : Test := do
   step "options.set" ({automaticMode? := .some false}: Protocol.OptionsSet)
    ({}: Protocol.OptionsSetResult)
   step "goal.start" ({ expr := "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b"} : Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.171" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.163" }: Protocol.GoalStartResult)
   let vars := #[
-    { name := "_uniq.172", userName := "a", type? := .some { pp? := .some "Nat" }},
+    { name := "_uniq.164", userName := "a", type? := .some { pp? := .some "Nat" }},
-    { name := "_uniq.175", userName := "b", type? := .some { pp? := .some "Nat" }},
+    { name := "_uniq.167", userName := "b", type? := .some { pp? := .some "Nat" }},
-    { name := "_uniq.178", userName := "h", type? := .some { pp? := .some "b = 2" }},
+    { name := "_uniq.170", userName := "h", type? := .some { pp? := .some "b = 2" }},
   ]
   let goal : Protocol.Goal := {
     vars,
-    name := "_uniq.179",
+    name := "_uniq.171",
     target := { pp? := "1 + a + 1 = a + b" },
   }
   step "goal.tactic" ({ stateId := 0, tactic? := .some "intro a b h" }: Protocol.GoalTactic)
@@ -185,13 +185,13 @@ def test_conv_calc : Test := do
    ({ nextStateId? := .some 2, goals? := #[{ goal with fragment := .calc }], }: Protocol.GoalTacticResult)
   let goalCalc : Protocol.Goal := {
     vars,
-    name := "_uniq.381",
+    name := "_uniq.363",
     userName? := .some "calc",
     target := { pp? := "1 + a + 1 = a + 1 + 1" },
   }
   let goalMain : Protocol.Goal := {
     vars,
-    name := "_uniq.400",
+    name := "_uniq.382",
     fragment := .calc,
     target := { pp? := "a + 1 + 1 = a + b" },
   }
@@ -201,7 +201,7 @@ def test_conv_calc : Test := do
     goalCalc with
     fragment := .conv,
     userName? := .none,
-    name := "_uniq.468",
+    name := "_uniq.450",
   }
   step "goal.tactic" ({ stateId := 3, mode? := .some "conv" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 4, goals? := #[goalConv], }: Protocol.GoalTacticResult)
@@ -319,9 +319,9 @@ def test_frontend_process_sorry : Test := do
 def test_import_open : Test := do
   let header := "import Init\nopen Nat\nuniverse u"
   let goal1: Protocol.Goal := {
-    name := "_uniq.81",
+    name := "_uniq.77",
     target := { pp? := .some "n + 1 = n.succ" },
-    vars := #[{ name := "_uniq.80", userName := "n", type? := .some { pp? := .some "Nat" }}],
+    vars := #[{ name := "_uniq.76", userName := "n", type? := .some { pp? := .some "Nat" }}],
   }
   step "frontend.process"
     ({
@@ -336,7 +336,7 @@ def test_import_open : Test := do
      ],
    }: Protocol.FrontendProcessResult)
   step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.79" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.75" }: Protocol.GoalStartResult)
   step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
   step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)

Test/Metavar.lean

@@ -159,7 +159,7 @@ def test_m_couple_simp: TestM Unit := do
       addTest $ assertUnreachable "(5 root)"
       return ()
   let rootStr: String := toString (← Lean.Meta.ppExpr root)
-  --checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
+  checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
   let unfoldedRoot ←  unfoldAuxLemmas root
   checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot))
     "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
@@ -259,7 +259,7 @@ def test_partial_continuation: TestM Unit := do
 
   -- Continuation should fail if the state does not exist:
   match state0.resume coupled_goals with
-  | .error error => checkEq "(continuation failure message)" error "Goals [_uniq.45, _uniq.46, _uniq.43, _uniq.52] are not in scope"
+  | .error error => checkEq "(continuation failure message)" error "Goals [_uniq.44, _uniq.45, _uniq.42, _uniq.51] are not in scope"
   | .ok _ => fail "(continuation should fail)"
   -- Continuation should fail if some goals have not been solved
   match state2.continue state1 with
@@ -303,7 +303,7 @@ def test_replay_environment : TestM Unit := do
   let stateT ← state2.replay state state1
   checkEq "(stateT goals)" stateT.goals.length 0
   let .some root := stateT.rootExpr? | fail "Root expression must exist"
-  checkTrue "root has aux lemma" $ root.getUsedConstants.any isAuxLemma
+  checkTrue "root has aux lemma" $ root.getUsedConstants.any (·.isAuxLemma)
   checkEq "(root)" (toString $ ← Meta.ppExpr root) "⟨_proof_1, _proof_2⟩"
   let root ← unfoldAuxLemmas root
   checkEq "(root unfold)" (toString $ ← Meta.ppExpr root) "⟨sorry, sorry⟩"

Test/Serial.lean

@@ -87,12 +87,12 @@ def test_pickling_env_extensions : TestM Unit := do
       instantiateMVars type
     let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable!
     let parentExpr := state1.parentExpr!
-    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any isAuxLemma
+    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)
     goalStatePickle state1 statePath
   let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
     let (state1, _) ← goalStateUnpickle statePath (← getEnv)
     let parentExpr := state1.parentExpr!
-    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any isAuxLemma
+    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any (·.isAuxLemma)
 
   return ()
 

Tomograph.lean

@@ -1,41 +0,0 @@
-/- A tool for analysing Lean source code. -/
-import Pantograph.Frontend
-import Pantograph.Library
-
-open Lean
-
-namespace Pantograph
-
-def fail (s : String) : IO UInt32 := do
-  IO.eprintln s
-  return 2
-
-def dissect (args : List String) : IO UInt32 := do
-  let fileName :: _args := args | fail s!"Must supply a file name"
-  let file ← IO.FS.readFile fileName
-  let (context, state) ← do Frontend.createContextStateFromFile file fileName (env? := .none) {}
-  let frontendM: Elab.Frontend.FrontendM _ :=
-    Frontend.mapCompilationSteps λ step => do
-      IO.println s!"🐈 {step.stx.getKind.toString}"
-      for (tree, i) in step.trees.zipIdx do
-        IO.println s!"🌲[{i}] {← tree.toString}"
-      for (msg, i) in step.msgs.zipIdx do
-        IO.println s!"🔈[{i}] {← msg.toString}"
-  let (_, _) ← frontendM.run context |>.run state
-  return 0
-
-end Pantograph
-
-open Pantograph
-
-def help : IO UInt32 := do
-  IO.println "Usage: tomograph dissect FILE_NAME"
-  return 1
-
-def main (args : List String) : IO UInt32 := do
-  let command :: args := args | help
-  unsafe do
-    Pantograph.initSearch ""
-  match command with
-  | "dissect" => dissect args
-  | _ => fail s!"Unknown command {command}"

flake.lock

@@ -39,7 +39,9 @@
     "lean4-nix": {
       "inputs": {
         "flake-parts": "flake-parts_2",
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": [
+          "nixpkgs"
+        ]
       },
       "locked": {
         "lastModified": 1750369222,
@@ -57,16 +59,16 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1743095683,
+        "lastModified": 1750151854,
-        "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=",
+        "narHash": "sha256-3za+1J9FifMetO7E/kwgyW+dp+8pPBNlWKfcBovnn6M=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6",
+        "rev": "ad5c70bcc5cc5178205161b7a7d61a6e80f6d244",
         "type": "github"
       },
       "original": {
         "owner": "nixos",
-        "ref": "nixos-unstable",
+        "ref": "nixos-24.11",
         "repo": "nixpkgs",
         "type": "github"
       }
@@ -98,27 +100,11 @@
         "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       }
     },
-    "nixpkgs_2": {
-      "locked": {
-        "lastModified": 1751048012,
-        "narHash": "sha256-MYbotu4UjWpTsq01wglhN5xDRfZYLFtNk7SBY0BcjkU=",
-        "owner": "nixos",
-        "repo": "nixpkgs",
-        "rev": "a684c58d46ebbede49f280b653b9e56100aa3877",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nixos",
-        "ref": "nixos-24.11",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
     "root": {
       "inputs": {
         "flake-parts": "flake-parts",
         "lean4-nix": "lean4-nix",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs"
       }
     }
   },

flake.nix

@@ -4,7 +4,10 @@
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix";
+    lean4-nix = {
+      url = "github:lenianiva/lean4-nix";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
   };
 
   outputs = inputs @ {

lakefile.lean

@@ -10,7 +10,6 @@ lean_lib Pantograph {
 
 lean_lib Repl {
 }
-
 @[default_target]
 lean_exe repl {
   root := `Main
@@ -18,13 +17,6 @@ lean_exe repl {
   supportInterpreter := true
 }
 
-@[default_target]
-lean_exe tomograph {
-  root := `Tomograph
-  -- Solves the native symbol not found problem
-  supportInterpreter := true
-}
-
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d"
 lean_lib Test {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.21.0
+leanprover/lean4:v4.20.1