aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 2 Packages Projects Releases Wiki Activity

doc: Remove stale documentation #236

Merged
aniva merged 3 commits from doc/readme into dev 2025-07-11 20:17:54 -07:00
Conversation 0 Commits 3 Files Changed 2 +34 -18
2 changed files with 34 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
README.md
View File

@ -17,17 +17,21 @@ nix build .#{sharedLib,executable}
``` ```
to build either the shared library or executable. to build either the shared library or executable.
Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and For non-Nix users, install `lake` and `lean` fixed to the version of the
run `lean-toolchain` file, and run
``` sh ``` sh
lake build lake build
``` ```
This builds the executable in `.lake/build/bin/pantograph-repl`. This builds the executable in `.lake/build/bin/repl`.
### Executable Usage ### 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 ### Library Usage
@ -39,7 +43,7 @@ Inject any project path via the `pantograph_init_search` function.
## Development ## Development
A Lean development shell is provided in the Nix flake. A Lean development shell is provided in the Nix flake. Nix usage is optional.
### Testing ### Testing

38
doc/repl.md
View File

@ -4,37 +4,49 @@ This documentation is about interacting with the REPL.
## Examples ## 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 ``` sh
pantograph-repl MODULES|LEAN_OPTIONS repl MODULES|LEAN_OPTIONS
``` ```
The `pantograph-repl` executable must be run with a list of modules to import. The `repl` executable must be given with a list of modules to import. By default
It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. it will import nothing, not even `Init`. It can also accept lean options of the
form `--key=value` e.g. `--pp.raw=true`.
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
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
``` ```
command { ... } command { ... }
{ "cmd": command, "payload": ... } { "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) Example: (~5k symbols)
``` ```
$ pantograph Init $ repl Init
env.catalog env.catalog
env.inspect {"name": "Nat.le_add_left"} env.inspect {"name": "Nat.le_add_left"}
``` ```
Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
``` ```
$ pantograph Mathlib.Analysis.Seminorm $ repl Mathlib.Analysis.Seminorm
env.catalog 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.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"stateId": 0, "tactic": "intro n m"} goal.tactic {"stateId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "tactic": "assumption"} goal.tactic {"stateId": 1, "tactic": "assumption"}
@ -59,7 +71,7 @@ LIB="../lib"
LIB_MATHLIB="$LIB/mathlib4/.lake" 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" 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 The `$LEAN_PATH` executable of any project can be extracted by
``` sh ``` sh