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?
Backtrace: as a starting point I’d look at the implementation of Fun.protect in the standard library which is designed to avoid losing the backtrace if the finally clause uses exceptions internally.
Exninfo: I’m curious about what use-case motivates having some stateful information about the last exceptions raised. How is it used outside of the Backtrace module?
What would be your opinion about the exception handling in the style of Base.Error module? I have found that in general replacing all exceptions with Base.Or_error.t style returns works exceptionally well, and that using a generic exception like
exception Error of Base.Error.t
when I have to use exceptions, and raising them like
raise (Error (Error.create "invalid index" i [%sexp_of: int]))
works very well, and is very consistent. I presume that the data relevant to debugging, like e.g. backtrace information you’ve mentioned earlier, would be coming in the Error.t type. Of course, the Coq developers might define their own equivalent of Error.t, since the dependency even on Base from JaneStreet may very legitimately be undesirable for this project.
I look forward to digging into all the packages/tools that people mention; it should be a real eye-opening experience! Recently I found that the “rresult” has some nice exception-trapping and re-raising functionality, and I’ve been switching to it. What’s particularly nice is that it has a nice monadic wrapper, so while
(1) on the one hand I almost NEVER use monads, and kinda sneer at them [so I just trap with the monadic construct, print a message, and re-raise]
(2) on the other hand, WHEN I want to trap exceptions and pile 'em up until I’m ready to deal with 'em (e.g., typecheck list of expressions, and only at the end deal with any errors that were found), rresult is conveniently precisely what I want.
But I’m a complete foreigner to using libraries for this, so I’m sure there’s something better, and I look forward to learning what it is!
