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

Dear lyj238,

In your case the ROOT file could contain: session Main_Session = HOL + theories mutualEx

isabelle build -d . -b Main_Session

isabelle build -v -d . -b Main_Session results in ################################################## ISABELLE_BUILD_OPTIONS="threads=4" ML_PLATFORM="x86_64-linux" ML_HOME="/usr/local/Isabelle2014/contrib/polyml-5.5.2-1/x86_64-linux" ML_SYSTEM="polyml-5.5.2-1" ML_OPTIONS="-H 500" Session Pure/Pure Session HOL/HOL (main) Session Unsorted/Main_Session Building Main_Session ... Main_Session: theory cache Main_Session: theory localesDef Main_Session: theory mutualEx

Finished Main_Session (0:00:20 elapsed time, 0:00:43 cpu time, factor 2.15) Finished at Thu Feb 5 14:38:53 CET 2015 0:00:26 elapsed time, 0:00:55 cpu time, factor 2.11 ################################################## cheers chris

On 02/05/2015 02:14 PM, Christian Sternagel wrote:

I'm forwarding this to the mailing list, since the question was originally asked there and others might have something useful to say before I have time to look at it in detail. 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 >

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

- Previous by Date: [isabelle] Fwd: Fw: The development of a large proof script.
- Next by Date: [isabelle] Fwd: Re: Decision procedures through computation & code_reflect
- Previous by Thread: [isabelle] Fwd: Fw: The development of a large proof script.
- Next by Thread: [isabelle] Fwd: Re: Decision procedures through computation & code_reflect
- 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