Email Gateway (Aug 19 2022 at 17:05): Email Gateway (Aug 19 2022 at 17:05):From: Christian Sternagel <c.sternagel@gmail.com>
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@ios.ac.cn <lyj238@ios.ac.cn>
To: Christian Sternagel <c.sternagel@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@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@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
>
cache.thy
localesDef.thy
mutualEx.thy
Email Gateway (Aug 19 2022 at 17:06):From: Christian Sternagel <c.sternagel@gmail.com>
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).
Email Gateway (Aug 19 2022 at 17:10):From: Makarius <makarius@sketis.net>
(I did not find time yet to look closely on this thread, which also has
invisible parts in my private mail folder. For continuation it is
important to keep exactly one public thread on this mailing list.)
Generally, Isabelle and its Prover IDE have been made to cope with the
increasingly large formalizations that have emerged in recent years:
everytime there was some success in using more CPU cores and exploiting
larger memory, applications continued to catch up and grow beyond that.
Just throwing tons of theory and proof text into a single Isabelle/jEdit
buffer is unlikely to work: the practical limit is a few hundred kilobyte
per node in the theory graph, but the graph can be quite large.
If proof sketches are machine generated, it should be easy to sub-divide
into separate theories and see how far you get, before really smart
approaches need to be devised.
Makarius
Email Gateway (Aug 19 2022 at 17:14):From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
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.
(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?
Best regards!
Email Gateway (Aug 19 2022 at 17:15):From: "lyj238@ios.ac.cn" <lyj238@ios.ac.cn>
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.
(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?
Best regards!
Email Gateway (Aug 19 2022 at 17:16):From: David Cock <david.cock@inf.ethz.ch>
On 04/02/15 14:18, lyj238@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
Email Gateway (Aug 19 2022 at 17:17):From: Christian Sternagel <c.sternagel@gmail.com>
Dear lyj238,
maybe you could give as some more details?
For example: What do you mean by "proof script"? Is what you are talking
about a standard Isabelle/Isar development, i.e., a bunch of *.thy files
with "lemma" statements inside and corresponding "proof/qed" blocks?
And how did you create your "proof script" if not with Isabelle/jEdit or
Isabelle/ProofGeneral?
The largest Isabelle development I've personally worked on is roughly in
the 5 MB area. This can be handled by session management that is
standard nowadays (see the Isabelle system manual).
In general, have a look at the System manual (that comes with the
Isabelle distribution) and especially at session management and the
"build" tool.
As for your question about parallelization. Isabelle's "build" uses
implicit parallelization possible due to interdependencies of theories
(and maybe lemmas?). So yes, parallelization is supported and you get
it essentially for free.
cheers
chris
Last updated: Apr 19 2024 at 08:19 UTC