[isabelle-dev] NEWS: isabelle jedit options

[Makarius]

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