[isabelle-dev] include option for "sessions" in ROOT

[Lars Hupel]

I'm playing around with the new "sessions" feature for qualified imports.

I think a prominent use case is to depend on various AFP entries. When
I'm working on my local development, I'd like to do this:

session Preliminiaries = ...
  sessions HOL-Library
  theories
    HOL-Library.FSet ...
  sessions Coinductive
  theories
    Coinductive ...

However, this only works when I have included the AFP, e.g. via "-d '$AFP'".

Why can I not specify this inline in the ROOT file? Like so:

session Preliminiaries = ...
  sessions HOL-Library
  theories
    HOL-Library.FSet ...
  sessions Coinductive (from "$AFP")
  theories
    Coinductive ...

That way, I don't have to remember to add the AFP in the command line.

Cheers
Lars