Thomas Sewell

Yuck. It's perhaps worth considering that graph-refine might want to support some kind of relocations between the read-only data as addressed in `kernel.elf.rodata` and as it appears in memory. That...

Another option is to use lazy strings rather than terms, types, etc, since the most common case is for them to be printed to strings. I wrote that up in...

For discussion, I've thought through how to implement this, and I'd be happy to have a go. The interface of SharingTables would probably have to change a bit. I would...

Yes, I meant to address the first failing, as @mn200 has described it, that the sharing is done per-theory. Yes, the advantage of per-theory sharing is the clean interface, whereas...

With regard to the second issue, it looks like SharingTables already knows how to share compound terms, but for some reason this isn't used, and .dat files only contain TMV...

OK, I've implemented a version of this ( see https://github.com/talsewell/HOL/tree/theory-share-terms ). I've done some easy tests on effectiveness. Everything seems to be working. The *Theory.dat files inside HOL4 generally grow...

I might just blog where I'm up to here. I compared core-theory build time, and I saw a bunch of variation, with some theories up or down by 10-20% time,...

OK, back to my desk this week. I have a version that might be ready to merge, but the last time I tried it the result was a problem with...

No, unfortunately. As @konrad-slind pointed out, it's a little tricky to write a version that's obviously an improvement, since it costs CPU time on each theory encoding, but saves disk/CPU/memory...

Hmm, so someone's interested in the explorer output. I think you have freedom to operate here. I don't think anyone's actively using the explorer output. I did a little bit...