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

[Kevin Kappelmann]

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

> Currently I'm in the first stage, which involves modifying primarily
> thm.ML and proofterm.ML to support "proof traces" instead of "proof
> terms".

Do you mind giving more details about what you mean by "proof traces" in
this context?

Best wishes,

Kevin