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

doc: Documentation cleanup and update #133

Merged
aniva merged 2 commits from chore/cleanup into dev 2024-12-05 17:23:25 -08:00
Conversation 0 Commits 2 Files Changed 3 +10 -11
3 changed files with 10 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.gitignore vendored
View File

@ -1,6 +1,4 @@
.* .*
!.gitignore !.gitignore
*.[io]lean
*.olean /result
/build
/lake-packages

2
README.md
View File

@ -75,7 +75,7 @@ the environment might be setup like this:
``` sh ``` sh
LIB="../lib" LIB="../lib"
LIB_MATHLIB="$LIB/mathlib4/lake-packages" LIB_MATHLIB="$LIB/mathlib4/.lake"
export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" export LEAN_PATH="$LIB/mathlib4/build/lib:$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 build/bin/pantograph $@

13
doc/repl.md
View File

@ -11,8 +11,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
* `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a * `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
given symbol; If value flag is set, the value is printed or hidden. By default given symbol; If value flag is set, the value is printed or hidden. By default
only the values of definitions are printed. only the values of definitions are printed.
* `env.save { path }`, `env.load { path }`: Save/Load the current environment * `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
to/from a file current environment to/from a file
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
@ -39,10 +39,11 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
- `{ "goals": <names> }`: Resume the given goals - `{ "goals": <names> }`: Resume the given goals
* `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list * `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list
* `goal.print {"stateId": <id>}"`: Print a goal state * `goal.print {"stateId": <id>}"`: Print a goal state
* `goal.save{ id, path }`, `goal.load { path }`: Save/Load a goal state to/from a * `goal.save { "id": <id>, "path": <fileName> }`, `goal.load { "path": <fileName> }`:
file. The environment is not carried with the state. The user is responsible Save/Load a goal state to/from a file. The environment is not carried with the
to ensure the sender/receiver instances share the same environment. state. The user is responsible to ensure the sender/receiver instances share
* `frontend.process { ["fileName": <fileName>",] ["file": <str>], invocations: the same environment.
* `frontend.process { ["fileName": <fileName>,] ["file": <str>], invocations:
<bool>, sorrys: <bool> }`: Executes the Lean frontend on a file, collecting <bool>, sorrys: <bool> }`: Executes the Lean frontend on a file, collecting
either the tactic invocations (`"invocations": true`) or the sorrys into goal either the tactic invocations (`"invocations": true`) or the sorrys into goal
states (`"sorrys": true`) states (`"sorrys": true`)