Re: [isabelle] A single way to reference AFP entries



On 20/05/16 15:40, Joachim Breitner wrote:

> What could and should changed, either in Isabelle or the AFP component
> setup, so that it _becomes_ possible to use the theories in both setups
> (within the AFP directory structure, as well as stand-alone theories
> using the registered AFP component)?

Certain reforms about locating theory sources via the formal session
structure have been in the pipeline for several years. I hope to get
that through before every release, and still do hope so for the one in
autumn 2016.

The general principle is that theories are no longer addressed via
file-system locations, but by logical names that stem from the
collective session definitions that are presently active. The main
mechanism to vary that session context is what you see as option -d in
"isabelle build" or "isabelle jedit", or the "dirs" in Isabelle/Scala
interfaces.

Lets see what comes out of that, when we are finally standing there.
Stay tuned and keep an eye on isabelle-dev ...


	Makarius






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