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

doc: Add design limitations about memory

This commit is contained in:
Leni Aniva 2025-05-01 12:30:17 -04:00
parent 06071c1044
commit beef22b945
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
doc/rationale.md
View File

@ -50,8 +50,13 @@ include:
- Although a timeout feature exists in Pantograph, it relies on the coöperative - Although a timeout feature exists in Pantograph, it relies on the coöperative
multitasking from the tactic implementation. There is nothing preventing a multitasking from the tactic implementation. There is nothing preventing a
buggy tactic from stalling Lean if it does not check for cancellation often. buggy tactic from stalling Lean if it does not check for cancellation often.
- For the same reason as above, there is no graceful way to stop a tactic which
leaks infinite memory. Users who wish to have this behaviour should run
Pantograph in a controlled environment with limited allocations. e.g.
Linux control groups.
- 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. This question is also
not well-defined.
## References ## References