[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