[isabelle-dev] smt2

[Gerwin Klein]

On 15.03.2014, at 2:39 am, Makarius <makarius at sketis.net> wrote:

> On Fri, 14 Mar 2014, Andreas Lochbihler wrote:
>
>> IIRC, the AFP policy is (was?) that all entries that import at least one theory from HOL-Library are based on HOL-Library.
>
> I can't speak for the AFP editors, but that might be just some old-fashioned custom.  In general it does not even work out, since the session images structure is just a tree, without the possibility of merge nodes.

Yes, this is not a strict rule, just used as a rule of thumb to avoid rebuilding theories that are used very frequently: If the only session dependency is HOL, and there is a HOL-Library theory used, the entry should be built on HOL-Library. But other than that, it’s up to whatever makes sense in the particular case.


> I have recently started to rethink the way theory imports from other sessions are specified, which would remove any coincidence on how the image tree was formed, oddities like "../Foo/Bar" vs just Bar, and oddities about fluctuating options [document = false].  As usual such reforms are encumbered by having to think thrice: for batch build, PIDE, Proof General.  Getting rid of the latter would speed the process.
>
> I'd like to see a situation where one can just fire up the Prover IDE and edit any of the AFP theories without thinking about accidental session images.

Yes, that would be nice. The paths in the entries should definitely not rely on being from an image, but usable either way. This is hard to enforce and imports that implicitly refer to other sessions creep in easily, because it usually does not fail, so we don’t notice right away.

We tried introducing the $AFP/ prefix (analogously to ~~/), but that only works when the afp component is registered, so it’s not a very stable way of doing things and not the default currently.

Cheers,
Gerwin



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.