*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Fwd: Fw: The development of a large proof script.*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Thu, 05 Feb 2015 14:14:16 +0100*In-reply-to*: <2015020518060804507511@ios.ac.cn>*References*: <2015020518060804507511@ios.ac.cn>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

cheers chris -------- Forwarded Message -------- Subject: Fw: The development of a large proof script. Date: Thu, 5 Feb 2015 18:06:08 +0800 From: lyj238 at ios.ac.cn <lyj238 at ios.ac.cn> To: Christian Sternagel <c.sternagel at gmail.com> Daer christian: I looked up the manuals and 'build' commands. I'm confused on the session concepts. I briefly describe my problems. I need a basic theory file "cache.thy" "localesDef.thy", then for each case study on a protocol 'a', I imports the basic theory, and generate a 'a.thy' with the help of an external tool. Now I want to run Isabelle to check 'a.thy'. Due to special application on the domain, the generated proof script can be checked without much interactions. As I think, I divide the larger file into small parts, which are loaded one by one. And each smaller file are built into a session (or image). Three thy files are attached, the cache.thy and two case studies. One is small, and the other is moderate. The largest cannot be sent via email I can upload it at some web site. But I think, you can teach me the method to me at first. I try to use the following command: [lyj at localhost cache]$ ~/Isabelle2014/bin/isabelle build -b cache.thy ### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++) ### Using bulky 64bit version of Poly/ML instead *** Undefined session(s): "cache.thy" 0:00:01 elapsed time, 0:00:01 cpu time but fails, can you give me some details to build the theory. regards! On Wed, 2015-02-04 at 14:27 +0100, David Cock wrote: > 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 >

**Attachment:
cache.thy**

**Attachment:
localesDef.thy**

**Attachment:
mutualEx.thy**

**Follow-Ups**:**Re: [isabelle] Fwd: Fw: The development of a large proof script.***From:*Christian Sternagel

- Previous by Date: [isabelle] Interpretation of Partial Functions from Z to Isabelle/HOL
- Next by Date: Re: [isabelle] Fwd: Fw: The development of a large proof script.
- Previous by Thread: [isabelle] Interpretation of Partial Functions from Z to Isabelle/HOL
- Next by Thread: Re: [isabelle] Fwd: Fw: 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