Pantograph/Delate.lean

@@ -164,7 +164,7 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
   self e := instantiateDelayedMVars e
 
 /--
-Convert an expression to an equiavlent form with
+Convert an expression to an equivalent form with
 1. No nested delayed assigned mvars
 2. No aux lemmas or matchers
 3. No assigned mvars

README.md

@@ -81,7 +81,7 @@ the environment might be setup like this:
 ``` sh
 LIB="../lib"
 LIB_MATHLIB="$LIB/mathlib4/.lake"
-export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
 
 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```

doc/rationale.md

@@ -47,12 +47,12 @@ 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.
+- Although a timeout feature exists in Pantograph, it relies on the coöperative
+  multitasking from the tactic implementation. There is nothing preventing a
+  buggy tactic from stalling Lean if it does not check for cancellation often.
 - Interceptions of parsing errors generally cannot be turned into goals (e.g.
   `def mystery : Nat := :=`) due to Lean's parsing system.
 
-
 ## References
 
 * [Pantograph Paper](https://arxiv.org/abs/2410.16429)