Re: [isabelle] Isabelle2017-RC0: jEdit plugin insists all files for all sessions are present

On 22/08/17 09:01, Matthew.Brecknell at wrote:
> We have many theories and other source files which are generated at various times during our lengthy build process. It seems that before I can use `isabelle jedit -d` to load even our very first session, I must first generate all files mentioned in all sessions accessible from the ROOTS file, and all their theories.

This sounds like a conflict of a legacy build process based on "make"
versus Isabelle session structure with "isabelle build" and now
increasingly inside Isabelle/jEdit.

At some point you should try to overcome this tension, and do it all
within static theory sources (by loading other files into a theory from

> Can this requirement be relaxed again, so that I only need the files for the session I want to load?

See the following NEWS entry:

* Command-line invocation "isabelle jedit -R -l SESSION" uses the parent
image of the SESSION, with qualified theory imports restricted to that
portion of the session graph. Moreover, the ROOT entry of the SESSION is
opened in the editor.

Note that after Isabelle2017-RC0 (e.g. in current snapshots from the session-qualified
imports are even more rigorous. It might cause additional problems for
your setup.


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