From f111da7de79ab8006a0bcda8a916c5785cabc8e8 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 11 Dec 2024 15:09:14 -0800 Subject: [PATCH] doc: Add limitations --- doc/rationale.md | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/doc/rationale.md b/doc/rationale.md index 4209474..d73bb22 100644 --- a/doc/rationale.md +++ b/doc/rationale.md @@ -24,7 +24,7 @@ The name Pantograph is a pun. It means two things a locomotive. In comparison the (relatively) simple Pantograph software powers theorem proving projects. -## Caveats +## Caveats and Limitations Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the flexibility it offers. To support tree search means Pantograph has to act @@ -38,7 +38,20 @@ differently from Lean in some times, but never at the sacrifice of soundness. it is supposed to finish at the end of a `by` block. Pantograph will raise the error in this case, since it indicates the termination of a proof search branch. - `pick_goal` or `swap` will not work since they run contrary to tree search - paradigms. + paradigms. However, if there are tactics which perform non-trivial operations + to multiple goals at the same time, this constrain could potentially be + relaxed at a cost of great bookkeeping overhead to the user. + +Pantograph cannot perform things that are inherently constrained by Lean. These +include: + +- If a tactic loses track of metavariables, it will not be caught until the end + of the proof search. This is a bug in the tactic itself. +- Timeouts for executing tactics is not available. Maybe this will change in the + future. +- Interceptions of parsing errors generally cannot be turned into goals (e.g. + `def mystery : Nat := :=`) due to Lean's parsing system. + ## References -- 2.44.1