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

[Manuel Eberl]

On 08/08/2020 17:52, Mario Carneiro wrote:
> So I've managed to successfully modify the kernel to support better
> proof traces, with ~0 performance impact, but while processing HOL I hit
> an error in Extraction.thy that am having trouble debugging.

Oof, I can't help you with your actual question, but my advice would be
to just ignore Extraction for now (i.e. just remove it from HOL). It's
not really used much and I don't think anyone except Stefan Berghofer
understands the code in detail. For an experiment such as the one that
you are doing, I think it is safe to ignore whatever problems arise from
Extraction for now.

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

There are a few functions ("writeln", "Pretty.writeln", "print_tac" for
tactics) but the easiest one in most circumstances is the @{print}
antiquotation which takes just about anything (integers, lists, types,
terms, theorems) and just prints it. For instance:

let
  val _ = @{print} my_term
in
  <actual code>
end

I sometimes turn terms into cterms before printing them like this
because then they are printed more nicely.


Very interesting thing that you're trying here, and I must commend you
for your bravery to delve this deep into the internals of Isabelle all
by yourself!

I recall you saying earlier this year that you might try to do this, but
I didn't expect you to actually go through with it. You must /really/
want some of our precious Isabelle/HOL theorems very badly. ;)

Manuel