<div dir="ltr"><div><div><div><div><div><div>(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.)<br><br></div><div>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.<br><br>The line that fails is:<br><br>lemmas [extraction_expand] = meta_spec<br><br></div>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<br><br>ML "Extraction.add_expand_thm false @{thm meta_spec} @{theory}"<br><br></div>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?<br><br></div>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).<br><br>--<br><br></div>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. <br><br> 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.<br><br></div>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.<br><br></div>Mario<br></div>