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

On 22/08/17 12:15, Lars Hupel wrote:
> 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").

This actually needs to be updated for Isabelle2017:

  * Users of AFP need to formally provide its session name space to
Isabelle tools, e.g. via "isabelle build -d 'path/to/afp/thys'" or
"isabelle jedit -d 'path/to/afp/thys'" or by adding a line with
"path/to/afp/thys" to $ISABELLE_HOME_USER/ROOTS to make this persistent.

  * Imports of theories from other sessions should always use the formal
session-qualified name, e.g. "HOL-Library.AList" or
"Coinductive.Coinductive_List". This requires to specify the other
sessions as parent or as imported 'sessions' in ROOT.

  * The command-line tool "isabelle imports -U -d ... My_Session" helps
to standardize imports in .thy and ROOT files in this respect.

> 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' ...

It is *possible* to use option -d, and there are other ways.

Maybe we should advertize $ISABELLE_HOME_USER/ROOTS to users more
prominently. At some point the Prover IDE might provide an editor for
that: at the moment it just means to open that text file directly using
the above symbolic name (maybe I should add a menu item for that).

> 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.

The component has de-facto no relevance to AFP users. It merely contains
various administrative settings and tools that have accumulated over
time, without a specific plan behind it.

I am using the component myself only to get a symbolic handle $AFP for
various command-line invocations like "isabelle build -d '$AFP' -a" to
build Isabelle + AFP as a whole.

> 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.

Performance is one problem, and polluting the logical session name space
another (i.e. the important option "-a" becomes hardly usable).

Since the component is not required to refer to path/to/afp/thys, it can
be ignored for this purpose (and maybe not even advertized to users


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