From 1ce2c89e8fd2f80b49fcac9e045667b7233391ef Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:51 +0000 Subject: Added backtrace primitives. Using OCaml 3.11+ builtin facilities to record stack frames during exception raising, we can now recover at runtime the backtrace of an uncaught toplevel exception and display it to the user, without the infamous OCaml debugger. The backtrace is displayed when using the [-debug] flag. This requires a bit of discipline, as each time we reraise an exception we need to keep track of those frames we discarded between the previous raise and the current [try-with] branch. Currently, only [Anomaly] is handled, but this can be ported to any exception as long as we add the backtrace info into the exception, and we provide the corresponding handler to [Backtracke.register_backtrace_handler]. Hopefully this should not be to costly, as we only do little work when reraising, and only with the [-debug] flag set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16166 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/check.mllib | 1 + 1 file changed, 1 insertion(+) (limited to 'checker/check.mllib') diff --git a/checker/check.mllib b/checker/check.mllib index 1bc23734a..2d56e163b 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,4 +1,5 @@ Coq_config +Backtrace Int Pp_control Flags -- cgit v1.2.3