search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
132 stars 33 forks source link

Supporting `exit on error` in Javascript mode #1250

Closed Halbaroth closed 1 month ago

Halbaroth commented 1 month ago

We use the system call exit in Solving_loop in order to halt quickly Alt-Ergo in case of fatal error or recoverable error if we turn on the flag exit_on_error. Unfortunately, this system call is not available in the Javascript runtime.

This issue can be tempered to some extent by turn off the flag exit_on_error in JS mode as it is done in #1249 but exit is still called for fatal errors.

I am not sure what is the best solution here. We may raise an exception in the main function of Solving_loop instead of calling exit and catch it immediately in both Main_text an Main_text_js. In the former, we call exit and in the latter we print a message and restart the worker.

bclement-ocp commented 1 month ago

We may raise an exception in the main function of Solving_loop instead of calling exit and catch it immediately in both Main_text an Main_text_js. In the former, we call exit and in the latter we print a message and restart the worker.

I believe that's the standard way of doing this and what we should do.

Halbaroth commented 1 month ago

Ok, I will do it after removing the legacy frontend.