From beef22b9450857e7573278d3ae98620ed42a63bf Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 1 May 2025 12:30:17 -0400 Subject: [PATCH] doc: Add design limitations about memory --- doc/rationale.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/doc/rationale.md b/doc/rationale.md index 217b4c8..3f99d1d 100644 --- a/doc/rationale.md +++ b/doc/rationale.md @@ -50,8 +50,13 @@ include: - 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. +- 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. - `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