[isabelle-dev] NEWS: support for ML_exception_debugger

[Florian Haftmann]

The matter turned out quite simple: a literal type constructor name has
to be adjusted:

> diff -r eef7af6af2ce thys/Native_Word/Uint32.thy
> --- a/thys/Native_Word/Uint32.thy	Thu Mar 03 08:24:04 2016 +0100
> +++ b/thys/Native_Word/Uint32.thy	Thu Mar 03 13:13:04 2016 +0100
> @@ -300,7 +300,7 @@
>    defines "TR \<equiv> typerep.Typerep" and "bit0 \<equiv> STR ''Numeral_Type.bit0''" 
>    shows
>    "term_of_class.term_of x = 
> -   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
> +   Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []]))
>         (term_of_class.term_of (Rep_uint32' x))"
>  by(simp add: term_of_anything)

Maybe it is high time for me to provide input syntax CONSTANT ''…'' and
TYPE_CONSTRUCTOR ''…'' for safe references to named entities in HOL.

Hope this helps,
	Florian


Am 02.03.2016 um 22:40 schrieb Makarius:
> *** 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160303/16cc1980/attachment.sig>