> 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. Fabian
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
