Re: [isabelle] The development of a large proof script.




On 04/02/15 14:18, lyj238 at ios.ac.cn wrote:
Dear experts:
    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 have used the tty model to run a smaller script with 2MBs in batch in previous Isabelle 2012. But
it is very inconvenient, and the tty model is not supported
    by Isabelle 2014.

You can still run noninteractive proofs, you just need to set up the appropriate build files. This is covered in the Isabelle system manual. Also, if you can factor your proof into several logic images, with each building on the last, then you can work interactively on any of them, by loading the next-lowest as your ambient logic.

(1) How to run the larger proof in Isabelle 2014?

(2)Essentially, my proof script contain a main lemma and thousands of basic
lemmas which is used in the proof of the main lemma.  The proof of thousands
of  basic lemmas can be proved in parallel. Parallel proof (or distributing
proofs) are supported by Isabelle 2014?

Yes, very much so.

David




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