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

[Makarius]

On 08/08/2020 17:52, Mario Carneiro wrote:
> 
> 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.

I find this all very interesting, but it does not belong the the
administrative isabelle-dev mailing list.


	Makarius