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



Dear lyj238,

what constitutes a single session has to be put into a "driver"/"project"/"session" file (I'm not sure whether there is any official name for this file, except for ROOT) called ROOT (see "System Manual", Section 2.1).

In your case the ROOT file could contain:

    session Main_Session = HOL +
      theories
         mutualEx

which defines a session called "Main_Session" on top of HOL (for bigger developments, as suggested by David, you can have several of these sessions built on top of each other). The session consists of the theory "mutualEx" (and implicitly all the theories on which "mutualEx" depends and that are not yet part of the "HOL" session).

Now, in order to build this newly defined session you have to tell "isabelle build" where your ROOT file is *and* which session to build (since there could be several sessions in a single ROOT file). This is done via

    isabelle build -d . -b Main_Session

adding "-v" will give you some more details about your environment which might be interesting here, in order to analyze the error you obtain. E.g,. on my machine

    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
Timing Main_Session (4 threads, 6.904s elapsed time, 20.347s cpu time, 0.749s GC time, factor 2.95)
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

Side remark: Conventionally you would start theory-names (as well as session-names) with a capital letter and use underscores to delimit words (not CamelCaseAsIsConvetionForSomeProgrammingLanguages).

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
          >







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