Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 19:44):

From: Alexander Krauss <krauss@in.tum.de>
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
Tracing_Example.thy

Email Gateway (Aug 22 2022 at 19:45):

From: Makarius <makarius@sketis.net>
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]))
›

Output:
Exception trace - exception Empty raised (line 47 of "./basis/List.sml")
f⌂
f⌂
f⌂
it-(1)⌂
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).

Makarius

Email Gateway (Aug 22 2022 at 19:45):

From: Alexander Krauss <krauss@in.tum.de>
Am 29.05.2019 um 19:48 schrieb Makarius:

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.

[...]

Here is your example with these hints applied:

[...]
Thanks that helps.

Does this mean that the old tracing flags/functions are obsolete by now?

Alex

Email Gateway (Aug 22 2022 at 19:59):

From: Makarius <makarius@sketis.net>
Maybe. I will think about removing them after the Isabelle2019 release.

Makarius

Last updated: Apr 19 2024 at 16:20 UTC