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