On 04/06/18 14:27, Makarius wrote: > *** 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 required theories > from other sessions, relative to an ancestor session given by option > -A (default: 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) > > 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 > > > This refers to Isabelle/bcdc47c9d4af, it is a clarification and > simplification from earlier options. That changeset also contains the > updated documentation.
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")? Typically they just slow down the build process -- due to reduced parallelism and extra file-system operations to compact/store/load the intermediate image. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev