From 798ff6f1bda2b904afaa484350083700f01c5c4a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 19:46:29 -0700 Subject: [PATCH 1/4] doc: Add documentation for tomograph --- README.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 963ef97..f0f436e 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,10 @@ This builds the executable in `.lake/build/bin/pantograph-repl`. ### Executable Usage -See [Executable Usage](./doc/repl.md) +The default build target is a Read-Eval-Print-Loop (REPL). See [REPL Documentation](./doc/repl.md) + +Another executable is the `tomograph`, which processes a Lean file and displays +syntax or elaboration level data. ### Library Usage -- 2.44.1 From c287d14f86388f727339fb9b63832af3e53cec08 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 20:00:05 -0700 Subject: [PATCH 2/4] feat(frontend): Improve `InfoTree` printing --- Pantograph/Frontend/InfoTree.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean index cbf2b71..dddaf21 100644 --- a/Pantograph/Frontend/InfoTree.lean +++ b/Pantograph/Frontend/InfoTree.lean @@ -10,7 +10,6 @@ namespace Lean.Elab private def elaboratorToString : Name → String | .anonymous => "" | n => s!"⟨{n}⟩ " -private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map (" " ++ .) /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/ protected def Info.stx? : Info → Option Syntax @@ -125,7 +124,9 @@ partial def InfoTree.findAllInfoM [Monad m] | _ => return [] @[export pantograph_infotree_to_string_m] -partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do +partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) (indent : Nat := 0) + : IO String := do + let space := String.join $ List.replicate indent " " match t with | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?) | .node info children => @@ -145,13 +146,15 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := . | .ofChoiceInfo _ => pure "[choice]" | .ofPartialTermInfo _ => pure "[partial_term]" | .ofDelabTermInfo _ => pure "[delab_term]" - let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx) - return s!"{node}\n{children}" + let children ← children.toList.mapM λ t' => do + t'.toString ctx (indent := indent + 1) + let children := String.join children + return s!"{space}{node}\n{children}" else throw <| IO.userError "No `ContextInfo` available." | .hole mvarId => if let some ctx := ctx? then let payload := (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty - return s!"[hole] {payload}" + return s!"{space}[hole] {payload}" else throw <| IO.userError "No `ContextInfo` available." end Lean.Elab -- 2.44.1 From 3ff45927a2b3d0de643c97b9d6c2a6e4393feddb Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 20:15:14 -0700 Subject: [PATCH 3/4] doc: Remove stale repl documentation --- doc/repl.md | 33 ++++++++++++++++++++++----------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/doc/repl.md b/doc/repl.md index 7ee9750..62dbaf4 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -4,37 +4,48 @@ This documentation is about interacting with the REPL. ## Examples +After building the `repl`, it will be available in `.lake/build/bin/repl`. +Execute it by either directly referring to its name, or `lake exe repl`. + ``` sh -pantograph-repl MODULES|LEAN_OPTIONS +repl MODULES|LEAN_OPTIONS ``` -The `pantograph-repl` executable must be run with a list of modules to import. -It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. +The `repl` executable must be given with a list of modules to import. By default +it will import nothing, not even `Init`. It can also accept lean options of the +form `--key=value` e.g. `--pp.raw=true`. The REPL loop accepts commands as single-line JSON inputs and outputs either an `Error:` (indicating malformed command) or a JSON return value indicating the -result of a command execution. The command can be passed in one of two formats +result of a command execution. It accepts commands in one of two formats + ``` command { ... } { "cmd": command, "payload": ... } ``` -The list of available commands can be found in `Pantograph/Protocol.lean` and below. An -empty command aborts the REPL. + +The list of available commands can be found below. An empty command aborts the +REPL. Example: (~5k symbols) ``` -$ pantograph Init +$ repl Init env.catalog env.inspect {"name": "Nat.le_add_left"} ``` + Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) + ``` -$ pantograph Mathlib.Analysis.Seminorm +$ repl Mathlib.Analysis.Seminorm env.catalog ``` -Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof + +Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) +to prime the proof + ``` -$ pantograph Init +$ repl Init goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} goal.tactic {"stateId": 0, "tactic": "intro n m"} goal.tactic {"stateId": 1, "tactic": "assumption"} @@ -59,7 +70,7 @@ LIB="../lib" LIB_MATHLIB="$LIB/mathlib4/.lake" export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" -LEAN_PATH=$LEAN_PATH build/bin/pantograph $@ +LEAN_PATH=$LEAN_PATH repl $@ ``` The `$LEAN_PATH` executable of any project can be extracted by ``` sh -- 2.44.1 From 8111c442e5f7cd288b83e6f535f469f4d6c37910 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 11 Jul 2025 20:17:27 -0700 Subject: [PATCH 4/4] doc: Wording --- doc/repl.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/doc/repl.md b/doc/repl.md index 62dbaf4..9c1f3ba 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -15,9 +15,10 @@ The `repl` executable must be given with a list of modules to import. By default it will import nothing, not even `Init`. It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. -The REPL loop accepts commands as single-line JSON inputs and outputs either an -`Error:` (indicating malformed command) or a JSON return value indicating the -result of a command execution. It accepts commands in one of two formats +After it emits the `ready.` signal, `repl` accepts commands as single-line JSON +inputs and outputs either an `Error:` (indicating malformed command) or a JSON +return value indicating the result of a command execution. The command must be +given in one of two formats ``` command { ... } -- 2.44.1