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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
