Compare commits
No commits in common. "8fd3649f32c426805fb2f1a079480399950d7e3e" and "86f69dd08cc7cf3dcc8119daed2a9538d4afd042" have entirely different histories.
8fd3649f32
...
86f69dd08c
|
@ -1,6 +1,6 @@
|
|||
namespace Pantograph
|
||||
|
||||
@[export pantograph_version]
|
||||
def version := "0.3.2"
|
||||
def version := "0.3.1"
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -52,9 +52,9 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
|
|||
state. The user is responsible to ensure the sender/receiver instances share
|
||||
the same environment.
|
||||
* `frontend.process { ["fileName": <fileName>,] ["file": <str>], readHeader: <bool>, inheritEnv: <bool>, invocations:
|
||||
<string>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
|
||||
<bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
|
||||
Executes the Lean frontend on a file, collecting the tactic invocations
|
||||
(`"invocations": output-path`), the sorrys and type errors into goal states
|
||||
(`"invocations": true`), the sorrys and type errors into goal states
|
||||
(`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
|
||||
`sorrys`, this command additionally outputs the position of each captured
|
||||
`sorry`. Conditionally inherit the environment from executing the file.
|
||||
|
|
Loading…
Reference in New Issue