aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 2 Packages Projects Releases Wiki Activity

Merge pull request 'doc: Update rationale' (#189) from doc/rationale into dev 

Reviewed-on: #189
This commit is contained in:
Leni Aniva 2025-04-18 01:08:23 -07:00
parent c547d9c8dc 60f79f5f02
commit fa5d423005
3 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Pantograph/Delate.lean
View File

@ -164,7 +164,7 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
self e := instantiateDelayedMVars e 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 1. No nested delayed assigned mvars
2. No aux lemmas or matchers 2. No aux lemmas or matchers
3. No assigned mvars 3. No assigned mvars

2
README.md
View File

@ -81,7 +81,7 @@ the environment might be setup like this:
``` sh ``` sh
LIB="../lib" LIB="../lib"
LIB_MATHLIB="$LIB/mathlib4/.lake" 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 $@ LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
``` ```

6
doc/rationale.md
View File

@ -47,12 +47,12 @@ include:
- If a tactic loses track of metavariables, it will not be caught until the end - 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. 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 - Although a timeout feature exists in Pantograph, it relies on the coöperative
future. 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. - Interceptions of parsing errors generally cannot be turned into goals (e.g.
`def mystery : Nat := :=`) due to Lean's parsing system. `def mystery : Nat := :=`) due to Lean's parsing system.
## References ## References
* [Pantograph Paper](https://arxiv.org/abs/2410.16429) * [Pantograph Paper](https://arxiv.org/abs/2410.16429)