Email Gateway (Aug 22 2022 at 20:09): Email Gateway (Aug 22 2022 at 20:09):From: Joshua Chen <josh@joshchen.io>
Is there any way to alleviate this for the moment? Or will I just have
to accept long startup times whenever I need to work with the AFP?
Cheers,
Josh
Email Gateway (Aug 22 2022 at 20:10):From: Makarius <makarius@sketis.net>
It depends what you mean by "work with the AFP".
If you are mainly focused on a particular session, the following NEWS
entry for Isabelle2018 may help:
* Isabelle/jEdit Prover IDE *
The command-line tool "isabelle jedit" provides more flexible options
for session management:
option -R builds an auxiliary logic image with all theories from
other sessions that are not already present in its parent
option -S is like -R, with a focus on the selected session and its
descendants (this reduces startup time for big projects like AFP)
option -A specifies an alternative ancestor session for options -R
and -S
option -i includes additional sessions into the name-space of
theories
Examples:
isabelle jedit -R HOL-Number_Theory
isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL
If you are working with all of AFP somehow, e.g. extensive testing, it
helps to use a really fast Linux or macOS machine with really fast SSD.
Windows is much slower in this respect.
Makarius
Email Gateway (Aug 22 2022 at 20:10):From: "Achim D. Brucker" <brucker@spamfence.net>
Hi,
as a work-around, you can only include the AFP entries (transitively, i.e.,
including their dependencies) that you actually need. Just include the
folders of the entries into your main ROOTS file.
While this is less convenient, it speeds up the starting time significantly.
My current projects require, in total, around ten AFP entries and including
all of them in my $ISABELLE_HOME_USER/ROOTS file does not slow down the
start of Isabelle significantly, while allowing me to work "as if I would have
included the whole AFP".
Cheers,
Achim
Email Gateway (Aug 22 2022 at 20:17):From: Joshua Chen <josh@joshchen.io>
Dear Isabelle list,
I find that the time and CPU usage during Isabelle startup increases
greatly if I have the AFP entry in my ROOTS file, factor ~3, is this
normal? This happens both on Isabelle2018 and 2019.
Best,
Josh
Email Gateway (Aug 22 2022 at 20:17):From: Makarius <makarius@sketis.net>
Yes. AFP is very big, and this is an indication that the approach to
explore all dependencies of sessions/theories on startup of the Prover
IDE will not scale much further.
Makarius
Last updated: Apr 20 2024 at 08:16 UTC