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

[Mario Carneiro]

(I'm posting this to isabelle-dev since it's a very internal technical
question that probably won't be of interest to end users.)

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.

The line that fails is:

lemmas [extraction_expand] = meta_spec

which gives an error "add_expand_thm: unnamed theorem". I believe this
means that add_expand_thm is being passed the wrong theorem, or a variant
on the theorem, that hasn't been explicitly tagged with the name. However,
as near as I can tell, this lemmas directive does the same thing as

ML "Extraction.add_expand_thm false @{thm meta_spec} @{theory}"

and this has no errors. How can I more precisely unfold the meaning of the
lemmas command here to get ML code that has exactly the same behavior, so
that I can inline functions until I've isolated the source of the
problematic theorem?

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

--

In order to avoid spamming too many threads, I will keep future kernel
hacking questions in this thread. For context: I'm currently working on
large scale proof export from isabelle. Currently I'm in the first stage,
which involves modifying primarily thm.ML and proofterm.ML to support
"proof traces" instead of "proof terms". Proof traces are extremely cheap
to create, and they involve essentially no new memory allocation (which
also helps to keep them cheap), but they hold on to old data which means
that the garbage collector can't clean up as much, and memory usage may
increase as a result.

The next stage is to perform "proof compaction", which serializes the
proofs into more compact data structures, and optionally writes them out to
disk and deletes them. This is slightly more expensive, but still only
involves a single pass deduplication step, and so I am betting that the
runtime of this pass will also be lost in the noise. I believe that a
combination of these two steps might be efficient enough to be enabled by
default, but I still need to perform more tests once it gets working.

The serialized proof traces are still somewhat far from being proofs in
pure lambda calculus, but they are a good starting point for
postprocessing, and I think it is more important that they are minimal and
computationally efficient to create given the context.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200808/83de2b8c/attachment.html>