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

doc: Update rationale about timeout

This commit is contained in:
Leni Aniva 2025-04-13 22:55:41 -07:00
parent c547d9c8dc
commit 77b517f4c6
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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)