in Coq we would like to modernize our exception handling a bit. Coq’s codebase predates many modern OCaml constructions and thus we have some overlap with existing functionality. In particular, we have:
the Backtrace module, which is used to implement a custom backtrace handling mechanism, and in particular to support re-raise without losing backtrace data. Ideally we would remove this module entirely but there has been reluctance w.r.t. what is the proper way to allow “safe” re-raise.
Exninfo module, which is used to attach other kinds of data to exceptions. I get the feeling that this approach is not in general safe except for debug, non-critical data, but I’m not expert here.
What do you folks think the way forward should be here? Is it possible to have similar functionality with “native” OCaml libs?
Some relevant Coq issues: