From f9c2416979973c8a9221402b0ee6d4d15f3919cb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 2 Jul 2026 18:30:53 +0000 Subject: [PATCH 1/2] Add OOM error kind. --- src/internal/error_data/imandrax_errors.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/internal/error_data/imandrax_errors.ml b/src/internal/error_data/imandrax_errors.ml index 3c1bcc18..ce5ef7b4 100644 --- a/src/internal/error_data/imandrax_errors.ml +++ b/src/internal/error_data/imandrax_errors.ml @@ -55,7 +55,7 @@ let all : t list = make "LowerFolError" "Error in lowering RIR to FOL"; make "ValidationError" "Error while validating a definition"; make "LspError" "Error in LSP server"; - make "Interrupted" "Computation was interrupted"; + make "Interrupted" "Computation was interrupted (usually for exceeding the time limit)"; make "RedisError" "Redis error"; make "CIRDeclNotFoundInStorage" "CIR storage error"; make "SerializationError" "Error during serialization"; @@ -77,6 +77,6 @@ let all : t list = make "Debounced" "Task has been cancelled due to debouncing"; make "FileNotFound" "A file could not be found"; make "InvalidSession" "The session ID provided is invalid"; - make "NoCounterExample" "Test did not find a counter-example" - ] + make "NoCounterExample" "Test did not find a counter-example"; + make "OutOfMemory" "The memory limit has been exceeded" ] [@ocamlformat "disable"] From cf4e7748bec85074c2418c0c91787f2f02ca35ab Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 15 Jul 2026 18:07:27 +0000 Subject: [PATCH 2/2] Add infrastructure error kind --- src/internal/error_data/imandrax_errors.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/internal/error_data/imandrax_errors.ml b/src/internal/error_data/imandrax_errors.ml index ce5ef7b4..030f1c90 100644 --- a/src/internal/error_data/imandrax_errors.ml +++ b/src/internal/error_data/imandrax_errors.ml @@ -78,5 +78,6 @@ let all : t list = make "FileNotFound" "A file could not be found"; make "InvalidSession" "The session ID provided is invalid"; make "NoCounterExample" "Test did not find a counter-example"; - make "OutOfMemory" "The memory limit has been exceeded" ] + make "OutOfMemory" "The memory limit has been exceeded"; + make "Infrastructure" "A part of the infrastructure failed" ] [@ocamlformat "disable"]