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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.