From 77b517f4c6ec1ec953d18839d5feac93cc3849f8 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 13 Apr 2025 22:55:41 -0700 Subject: [PATCH 1/3] doc: Update rationale about timeout --- doc/rationale.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/rationale.md b/doc/rationale.md index d73bb22..217b4c8 100644 --- a/doc/rationale.md +++ b/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) From 4abe2fa72f9947ccfabfb8a7b2b389bae32e4c61 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 14 Apr 2025 16:27:29 -0700 Subject: [PATCH 2/3] fix: LEAN_PATH example --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 02de68c..24722eb 100644 --- a/README.md +++ b/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 $@ ``` From 60f79f5f02f2debf0e121f20d8c409e148d74db6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 14 Apr 2025 23:26:14 -0700 Subject: [PATCH 3/3] doc: Fix typo --- Pantograph/Delate.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index a745854..a021b72 100644 --- a/Pantograph/Delate.lean +++ b/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