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

doc: Update README.md

This commit is contained in:
Leni Aniva 2024-03-28 11:37:07 -07:00
parent 62d20be841
commit 47fabf333b
1 changed files with 21 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
README.md
View File

@ -6,6 +6,8 @@ An interaction system for Lean 4.
## Installation ## Installation
For Nix based workflow, see below.
Install `elan` and `lake`. Execute Install `elan` and `lake`. Execute
``` sh ``` sh
make build/bin/pantograph make build/bin/pantograph
@ -20,7 +22,7 @@ LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
``` ```
The provided `flake.nix` has a develop environment with Lean already setup. The provided `flake.nix` has a develop environment with Lean already setup.
## Usage ## Executable Usage
``` sh ``` sh
pantograph MODULES|LEAN_OPTIONS pantograph MODULES|LEAN_OPTIONS
@ -63,7 +65,7 @@ stat
``` ```
where the application of `assumption` should lead to a failure. where the application of `assumption` should lead to a failure.
## Commands ### Commands
See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
- `reset`: Delete all cached expressions and proof trees - `reset`: Delete all cached expressions and proof trees
@ -82,7 +84,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
- `goal.print {"stateId": <id>}"`: Print a goal state - `goal.print {"stateId": <id>}"`: Print a goal state
- `stat`: Display resource usage - `stat`: Display resource usage
## Errors ### Errors
When an error pertaining to the execution of a command happens, the returning JSON structure is When an error pertaining to the execution of a command happens, the returning JSON structure is
@ -97,16 +99,31 @@ Common error forms:
input of another is broken. For example, attempting to query a symbol not input of another is broken. For example, attempting to query a symbol not
existing in the library or indexing into a non-existent proof state. existing in the library or indexing into a non-existent proof state.
## Troubleshooting ### Troubleshooting
If lean encounters stack overflow problems when printing catalog, execute this before running lean: If lean encounters stack overflow problems when printing catalog, execute this before running lean:
```sh ```sh
ulimit -s unlimited ulimit -s unlimited
``` ```
## Library Usage
`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
with `Pantograph`.
## Testing ## Testing
The tests are based on `LSpec`. To run tests, The tests are based on `LSpec`. To run tests,
``` sh ``` sh
make test make test
``` ```
## Nix based workflow
To run tests:
``` sh
nix build .#checks.${system}.test
```
For example, `${system}` could be `x86_64-linux`. Using `nix develop` drops the
current session into a development shell with fixed Lean version.