[isabelle-dev] Time

Tobias Nipkow nipkow at in.tum.de
Wed Aug 30 09:21:46 CEST 2017


I have a timing issue with b8a6f9337229 (and quite possibly other revisons):
isabelle build takes 22 secs before it says "Running ...". Since creating
latex documents requires many, many iterations, this is extremely painful. My
setup is the following:

session A = HOL +
   sessions
     "HOL-Library"
   theories
     10 theories either local or in ~~/src/HOL

session B = A +
   theories
   ...
   document_files
   ...

None of my files are part of a Mercurial repository.

I start with building A:

isabelle build -v -d . A

It takes 6 secs until the build of A actually starts.

 From now on I will always build B.

I start with an almost empty B: 0 theories and no document_files section.
It takes 6 secs before it starts the run.

Now I add a document_files section with 4 small (less than 3k each) tex files.
It takes 8 secs before it starts the run.

Now I add 8 pdf files of 70k each.
It takes 15 secs before it starts the run.

Now I add 10 theories that only import files that are part of session A.
It takes 22 secs before it starts the run.

All of this is linear: the more files I add, the longer it takes. In
Isabelle2016-1 it took 2 secs.

I have intentionally not included anything from the AFP. However, importing
an AFP session does not seem to make matters worse (although adding -d '$AFP'
to isabelle jedit does add 20 secs startup time.)

What am I doing wrong? How can I speed things up?

Thanks
Tobia

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170830/4f083c6b/attachment.p7s>


More information about the isabelle-dev mailing list