[isabelle-dev] Debugging help: Hacking the kernel for proof export

[Makarius]

On 08/08/2020 18:27, Kevin Kappelmann wrote:
> On 08.08.20 17:52, Mario Carneiro wrote:> ....
>> Also, is there any way for me to do "printf debugging" in isabelle/ML?
>> The focus on pure functional programming makes debugging especially
>> difficult, but I'm sure I'm just missing the idioms for doing so
>> (understandably, I can't find any examples of debugging in the source).
> 
> The ML-cookbook has a section (2.2) about debugging that might help you:
> https://nms.kcl.ac.uk/christian.urban/Cookbook/
> Some  combinators (like "tap") might also speed up your development (see
> section 2.3).

Standard disclaimer: the cookbook is somewhat outdated and non-standard.
People who have learned special "tricks" over there might have to unlearn them
later: there is a 50/50 chance that they are conceptually wrong, or just old.


Answer to the original question: see the "implementation" manual section "0.2.4
Printing ML values" (with examples).

(These questions belong to the isabelle-users mailing list, where more people
can benefit from the answers as well.)


	Makarius