[isabelle-dev] NEWS: support for ML_exception_debugger
Makarius
makarius at sketis.net
Wed Mar 2 22:40:14 CET 2016
*** ML ***
* 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 refers to Isabelle/5dfcc9697f29.
Building Pure + HOL with -o ML_debugger requires 40min with 6 cores. It is
no necessary to compile all ML modules with debugger support, but it helps
to find the needle in the haystack.
Makarius
More information about the isabelle-dev
mailing list