Re: [isabelle] Isabelle2019-RC2: Cannot get exception trace

On 27/05/2019 09:56, Alexander Krauss wrote:
> I am failing to get a meaningful exception trace out of the system. Here
> is a small example which is typical for real-life debugging situations.

Some years ago, David Matthews has improved the performance of exception
handling by removing most of the classic exception_trace facilities. It
is now done with the ML debugger instead. See this NEWS entry for
Isabelle2016-1 (December 2016):

* Option ML_exception_debugger controls detailed exception trace via the
Poly/ML debugger. Relevant ML modules need to be compiled beforehand
with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
debugger information requires consirable time and space: main
Isabelle/HOL with full debugger support may need ML_system_64.

This still holds for Isabelle2019, but you can probably ignore
ML_system_64 for all practical applications.

Here is your example with these hints applied:

declare [[ML_debugger]]
ML ‹

(* Raises exception Empty eventually. Recursive to avoid inlining. *)
fun f xs = case xs of _::xs' => f xs' | _ => hd xs;

(* Returns the empty list. Recursive to avoid inlining. *)
fun g xs = case xs of _::xs' => g xs' | _ => xs;

(* Would expect to see which if f or g raises the exception, but I only get

  exception Empty raised (line 47 of "./basis/List.sml")

which does not help. *)
Runtime.exn_debugger (fn () => (f [0,1], g [2,3]))

Exception trace - exception Empty raised (line 47 of "./basis/List.sml")
val f = fn: 'a list -> 'a
val g = fn: 'a list -> 'a list
exception Empty raised (line 47 of "./basis/List.sml")

If you want to get information from a complex hierarchy of modules, you
need to rebuild them with ML_debugger enabled or the 'ML_debug' command
just in the right spots. This can be sometimes awkward, and sometimes
have bad effects (loss of performance, deadlocks).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.