[isabelle] Isabelle2019-RC2: Cannot get exception trace



Hi all,

This might just be a misunderstanding, but it is also something that
would probably go unnoticed by automated tests when broken, so I am
reporting this here as a possible regression.

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.

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_trace (fn () => (f [0,1], g [2,3]))
›

I also experimented with [[ML_exception_trace = true]], but without success.

Thanks for any help.

Alex
theory Tracing_Example
  imports Pure
begin


ML \<open>

(* 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 function raises the exception, but I only get

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

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

end


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