From 292fb0be4b300c5a4ae851ca59b9942579f59a63 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 17 Jun 2025 11:54:38 -0700 Subject: [PATCH 1/2] chore: Update version to 0.3.2 --- Pantograph/Version.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean index 6853517..4d937cd 100644 --- a/Pantograph/Version.lean +++ b/Pantograph/Version.lean @@ -1,6 +1,6 @@ namespace Pantograph @[export pantograph_version] -def version := "0.3.1" +def version := "0.3.2" end Pantograph From 04cbc55f3a8b64d1609c6b2b70cd00fea9f8fb17 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 17 Jun 2025 11:56:31 -0700 Subject: [PATCH 2/2] doc: Update invocations usage --- doc/repl.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/repl.md b/doc/repl.md index 7217139..aa2d5fa 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -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": ,] ["file": ], readHeader: , inheritEnv: , invocations: - , sorrys: , typeErrorsAsGoals: , newConstants: }`: + , sorrys: , typeErrorsAsGoals: , newConstants: }`: Executes the Lean frontend on a file, collecting the tactic invocations - (`"invocations": true`), the sorrys and type errors into goal states + (`"invocations": output-path`), 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.