Qiyuan Xu (Jul 01 2021 at 03:03): Qiyuan Xu (Jul 01 2021 at 03:03):I'm struggling with why the exception trace doesn't work, by the ML function Runtime.exn_trace.
In this minimal example,
fun f i = if i = 0 then raise Fail "" else f (i-1)
val x = Runtime.exn_trace (fn _ => f 10)
The output dialogue doesn't print any stack trace as expected, but only a simple error in a line.
Should I set some other configurations to enable the stack trace?
Lukas Stevens (Jul 01 2021 at 08:26):I remember that I had a similar issue in the past where the exception trace wasn't working. I never managed to resolve the issue though. The exception trace needs to be enabled in the Isabelle plugin options but it is enabled by default.
Lukas Stevens (Jul 01 2021 at 08:34):You may have more luck if you ask about this on the mailing list.
Qiyuan Xu (Jul 01 2021 at 13:48):Oh, thank you. I made it works by enabling options in the setting panel Ctrl+F12/Plugin Options/Isabelle/the section for ML system/ML Debugger and ML Exception Trace. A reboot of the Isabelle is also required to make the setting works. I don't know why they're disabled in my case, but it doesn't matter anymore.
Lukas Stevens (Jul 01 2021 at 13:52):Lukas Stevens said:
I remember that I had a similar issue in the past where the exception trace wasn't working. I never managed to resolve the issue though. The exception trace needs to be enabled in the Isabelle plugin options but it is enabled by default.
The part with it being enabled by default might be wrong.
Last updated: Dec 21 2024 at 16:20 UTC