Re: [isabelle] The development of a large proof script.
On Wed, 4 Feb 2015, lyj238 at ios.ac.cn wrote:
Now I want to ask some details on the development of a large proof script.
A proof script on a real protocol case study has 20 MB. It is really
beyond the ability of Isabelle's JEDIT interface.
(I did not find time yet to look closely on this thread, which also has
invisible parts in my private mail folder. For continuation it is
important to keep exactly one *public* thread on this mailing list.)
Generally, Isabelle and its Prover IDE have been made to cope with the
increasingly large formalizations that have emerged in recent years:
everytime there was some success in using more CPU cores and exploiting
larger memory, applications continued to catch up and grow beyond that.
Just throwing tons of theory and proof text into a single Isabelle/jEdit
buffer is unlikely to work: the practical limit is a few hundred kilobyte
per node in the theory graph, but the graph can be quite large.
If proof sketches are machine generated, it should be easy to sub-divide
into separate theories and see how far you get, before really smart
approaches need to be devised.
This archive was generated by a fusion of
Pipermail (Mailman edition) and