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



Dear Matthew, Makarius,
I'd like to add another (tangential) observation to this thread.

Previously, when editing some theories in the AFP, it was sufficient to
just open Isabelle/jEdit â no special command line flags required
(assuming HOL as a base image). To ensure this, AFP policy states that
imports from other entries should be relative (i.e.
"../Other_Entry/Thy") instead of absolute (i.e. "$AFP/Other_Entry/Thy").

While I appreciate the sentiment behind qualified imports (no more
incoherent imports!), this workflow doesn't work anymore. It is
necessary to start Isabelle/jEdit from the command line as follows:

  isabelle jedit -d 'path/to/afp/thys' ...

Even if the AFP is registered as a component, this is still necessary.
While components are automatically registered as session roots, the AFP
base directory is not a session root.

I'd like to make a suggestion to mitigate this situation: make the AFP
base directory a session root, by adding a "ROOTS" file pointing to
"thys" [0]. This might come with a performance penalty because on every
tool invocation, Isabelle/Scala has to traverse the sessions graph.
Makarius might be able to estimate that penalty.

Maybe there is also another way to include session roots.

Cheers
Lars


[0] This is basically the approach I took in
<https://github.com/larsrh/afp>.




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