[isabelle-dev] Printing terms for debugging (Re: implicit beta normalization in the pretty-printer)

[Makarius]

On Wed, 18 Jan 2012, Alexander Krauss wrote:

> On 01/18/2012 03:34 PM, Ondřej Kunčar wrote:
>> It's a bit annoying if you want to do
>> debugging on the ML level and you have to inspect every term by
>> inspecting its ML representation (which is really tedious for larger
>> terms).
>
> This is a common problem, and everybody has come up with private hacks. 
> Mine goes roughly like this:

Meta-Answer:  This is a perfectly normal isabelle-users question.

ML has always been part of the regular Isabelle user space.  In ancient 
times every proof script was in ML.  When I introduced the Isabelle/Isar 
toplevel, its very first command was 'ML' to re-integrate the runtime 
compilation-execution that is so important for many Isabelle applications. 
(Paradoxically, serious Isabelle/ML integration really started with the 
Isar toplevel.)

The isabelle-dev mailing list is mainly for things relevant to the process 
around the repository and administrative issues (isatest, mira etc.). 
For postings related to repository versions one always needs to quote a 
proper changeset id so that things can be followed days/weeks/months later 
(we have more than 46245 "current" Isabelle versions now, as of 
Isabelle/9f39ae84b593, and in a distributed setting there is not global 
tip version anyway.)


In contrast, things posted on isabelle-users can usually refer implicitly 
to "the latest" official release.  In the worst case one merely has to try 
1-3 latests official releases.  So users don't have to be tought how to 
quote versions.


 	Makarius