Re: [isabelle] Slow startup if AFP in ROOTS



On 29/07/2019 15:09, Joshua Chen wrote:
> 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?

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.