[isabelle] Further Discussion---The development of a large proof script.



Dear Christian, David, Markus:
   Thanks for your answering. I have used it in my machine, it works.
 
After looking up the manuals and my requirements for development of case studies, I have some further questions:
 
1. The concepts of checked proof theories for later use (or how to store the checked thoeiries)
 
In my experience, the public theory files cache.thy and localesDef.thy should be checked only once, will be imported each time in each later case studies.
 
I think, the ideal status is that the checked ublic theory files cache.thy and localesDef.thy should be stored in internal format ( is image files?), and not be checked again  If we develop a proof script on a case of a protocol.
 
For instance, if I model and verify the case study: 'mutualEx' protocol, I simply write a 'mutual.thy', import the checked 'cache.thy' and 'localesDef.thy'. Ideally, at this time, the two basic files  Should be imported directly without checking again because they are checked and not modified,  Thus I try to write my ROOT file as follows:
 
session cache_Session = HOL + 
       theories 
          cache
          localesDef 
          
session mutualEx_Session= HOL + 
         theories 
            mutualEx
            
session german_Session= HOL  +  
         theories 
            german    
 
,where german is another case study on german protocol, 
 
After building cache_Session, I build german, I see cache.thy and localesDef.thy are loaded and checked again, it seemed that "build" neglect the fact that cache.thy and localesDef.thy have been checked.
 
I EXTREMLY want to make these clearly:
(a)after session cache_Session is finished, cache and localesDef theories will be stored in an internal format?
(b)In the subsequent development of case study, cache and localesDef can be impoted without checking again?
(c) I checked the directory after executing the 'build' command, I found nothing more than the thy files;
(d) I think that there should be a mechanism to support "a public theory once checked -then used for more times"
 
(d) is important to develop a large proof script, for instance, if 50% of the script is checked, and an error is found. If the checked 50% is ok, and no need to modify, then I  store the former 50%, and  develop the later 50%  by directly importing  the former 50% (without checking).
 
2.There is  too little information to indicate the status of building process.
 
The most terrible thing is that some "auto", "simp","metis" command is executed and the building process is stucked.
At this time, no information is given.
It is preferable to have a hint message that which line are executed.
 
Reagrds!
 
-----邮件原件-----
发件人: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] 代表 Christian Sternagel
发送时间: 2015年2月5日 21:41
收件人: isabelle-users at cl.cam.ac.uk
抄送: lyj238 at ios.ac.cn
主题: 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
>           >
> 
> 
> 



lyj238 at ios.ac.cn

Attachment: german.rar
Description: Binary data



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