Re: [isabelle] 回复: Re: The development of a large proof script.
Yes I have received your response. And I would appreciate if *all*
corresponding discussion would go through the isabelle mailing list
(instead of private email to me or others). This way, answers will be
archived and can be referenced later if similar questions arise again.
Having said that -- at least for me -- reminders about pending threads
on the mailing list will not speed up my answering. When I have time to
read and think about a question *and* come up with an answer I deem
useful, I will respond. Not before ;)
On 02/09/2015 12:44 PM, lyj238 at ios.ac.cn wrote:
Have you reveived my response email on the further discussion to
isabelle mail list?
lyj238 at ios.ac.cn
*发件人：* Christian Sternagel <mailto:c.sternagel at gmail.com>
*发送时间：* 2015-02-04 21:33
*收件人：* cl-isabelle-users <mailto:cl-isabelle-users at lists.cam.ac.uk>
*主题：* Re: [isabelle] The development of a large proof script.
maybe you could give as some more details?
For example: What do you mean by "proof script"? Is what you are
about a standard Isabelle/Isar development, i.e., a bunch of *.thy
with "lemma" statements inside and corresponding "proof/qed" blocks?
And how did you create your "proof script" if not with
The largest Isabelle development I've personally worked on is
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
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.
On 02/04/2015 02:18 PM, lyj238 at ios.ac.cn wrote:
> Dear experts:
> Now I want to ask some details on the development of a large
> A proof script on a real protocol case study has 20 MB. It
> 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 basic lemmas can be proved in parallel. Parallel proof (or
> proofs) are supported by Isabelle 2014?
> Best regards!
> lyj238 at ios.ac.cn
This archive was generated by a fusion of
Pipermail (Mailman edition) and