doc: Update README.md

This commit is contained in:
Leni Aniva 2024-03-28 11:37:07 -07:00
parent 22fdb7bea9
commit 91e55245fa
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 21 additions and 4 deletions

View File

@ -6,6 +6,8 @@ An interaction system for Lean 4.
## Installation
For Nix based workflow, see below.
Install `elan` and `lake`. Execute
``` sh
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.
## Usage
## Executable Usage
``` sh
pantograph MODULES|LEAN_OPTIONS
@ -63,7 +65,7 @@ stat
```
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.
- `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
- `stat`: Display resource usage
## Errors
### Errors
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
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:
```sh
ulimit -s unlimited
```
## Library Usage
`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
with `Pantograph`.
## Testing
The tests are based on `LSpec`. To run tests,
``` sh
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.