Consider use of Makarius' YXML library

[mn200]

See http://permalink.gmane.org/gmane.comp.mathematics.hol/1502 and https://bitbucket.org/makarius/yxml/src/

We already have a compressed (hash-consed) format for our types, terms and theorems in DiskThms and TheoryPP.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[xrchz]

It would also be worth testing whether saving theories as OpenTheory packages and replaying the proofs on load would be intolerably slow. (Proofs, not proof search.) One advantage would be enabling better compositionality/reuse of stuff under src.

[myreen]

I doubt proof replay on load would be tolerable. Anyway, how large would these proofs be? My impression is that real proof developments produce enormous OpenTheory proofs.

On 7 August 2012 08:35, Ramana Kumar [email protected] wrote:

It would also be worth testing whether saving theories as OpenTheory packages and replaying the proofs on load would be intolerably slow. (Proofs, not proof search.) One advantage would be enabling better compositionality/reuse of stuff under src.

— Reply to this email directly or view it on GitHubhttps://github.com/mn200/HOL/issues/71#issuecomment-7545888.

[mn200]

It's an experiment worth doing. But it certainly belongs to another issue.

[mn200]

The gmane link is no good; this one at mail-archive.com is probably/possibly what I linked to earlier.