.gitignore

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

README.md

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

doc/repl.md

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