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

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.



-------- 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
        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
        proof script can be checked without much interactions.
        As I think, I divide the larger file into small parts, which are
        one by one. And each smaller file are built into  a session (or
        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
        ### Cannot execute Poly/ML in 32bit mode (missing shared
        libraries for
        ### 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.
        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
         > 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
Description: Binary data

Attachment: localesDef.thy
Description: Binary data

Attachment: mutualEx.thy
Description: Binary data

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