[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.


More information about the isabelle-dev mailing list