search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

Consider use of Makarius' YXML library #71

Open mn200 opened 12 years ago

mn200 commented 12 years ago

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 commented 12 years ago

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 commented 12 years ago

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 notifications@github.com 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 commented 12 years ago

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

mn200 commented 1 year ago

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