> Am 05.06.2018 um 23:01 schrieb Makarius <makar...@sketis.net>:
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further refinement.
> In other words, the question behind this: Can be get rid of most
> auxiliary images in AFP (e.g. "Foo_Lib", "Pre_Foo")?
I started to use -S HOL-ODE-Numerics and got rid of HOL-ODE-Refinement (which 
was such an auxiliary image) in AFP/cf739ca.
-S is very helpful because it reduces the start-up time for Isabelle/jEdit 
(with the AFP in ROOTS) from 100s to 30s (compared to -R).

I can also imagine that auxiliary images get outdated easily (importing too 
much or too little), and so it is good that -R/-S takes care of this potential 
maintenance efforts.


Attachment: smime.p7s
Description: S/MIME cryptographic signature

isabelle-dev mailing list

Reply via email to