*To*: "lyj238 at ios.ac.cn" <lyj238 at ios.ac.cn>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] 回复: Re: The development of a large proof script.*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Mon, 09 Feb 2015 12:53:25 +0100*In-reply-to*: <2015020919440033389115@ios.ac.cn>*References*: <201502042111505364572@ios.ac.cn>, <54D21F8F.1000304@gmail.com> <2015020919440033389115@ios.ac.cn>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Dear lyj238,

cheers chris On 02/09/2015 12:44 PM, lyj238 at ios.ac.cn wrote:

Dear christian: Have you reveived my response email on the further discussion to isabelle mail list? ------------------------------------------------------------------------ lyj238 at ios.ac.cn *发件人：* Christian Sternagel <mailto:c.sternagel at gmail.com> *发送时间：* 2015-02-04 21:33 *收件人：* cl-isabelle-users <mailto:cl-isabelle-users at lists.cam.ac.uk> *主题：* Re: [isabelle] The development of a large proof script. Dear lyj238, maybe you could give as some more details? For example: What do you mean by "proof script"? Is what you are talking about a standard Isabelle/Isar development, i.e., a bunch of *.thy files with "lemma" statements inside and corresponding "proof/qed" blocks? And how did you create your "proof script" if not with Isabelle/jEdit or Isabelle/ProofGeneral? The largest Isabelle development I've personally worked on is roughly in the 5 MB area. This can be handled by session management that is standard nowadays (see the Isabelle system manual). In general, have a look at the System manual (that comes with the Isabelle distribution) and especially at session management and the "build" tool. As for your question about parallelization. Isabelle's "build" uses implicit parallelization possible due to interdependencies of theories (and maybe lemmas?). So yes, parallelization is supported *and* you get it essentially for free. cheers chris On 02/04/2015 02:18 PM, 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. > > (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? > > > > > > Best regards! > > > lyj238 at ios.ac.cn >

**References**:**[isabelle] The development of a large proof script.***From:*lyj238 at ios.ac.cn

**Re: [isabelle] The development of a large proof script.***From:*Christian Sternagel

- Previous by Date: [isabelle] First Call for Papers, PxTP 2015
- Next by Date: [isabelle] libisabelle: Small Scala library to communicate with Isabelle
- Previous by Thread: Re: [isabelle] The development of a large proof script.
- Next by Thread: Re: [isabelle] The development of a large proof script.
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list