Re: [isabelle] Isabelle2014-RC0: phantom theories

Am 08.07.2014 10:52, schrieb Christian Sternagel:
> While I'm at it, another thing (but I guess this is well-known): In
> IsaFoR we have a session HOL-AFP which builds a heap-image containing
> all AFP entries we rely on. After building this image it is possible to
> open (with Isabelle/jEdit) a file as follows
>   isabelle jedit -d . -l HOL-AFP Some_File.thy
> that contains an import like
>   "$AFP/some_path_that_no_longer_exists/Misc"
> and there is no error-message (note that theory Misc exists, but at a
> different location). When I try
>   isabelle jedit -d . Some_File.thy
> instead and let Isabelle/jEdit figure out the dependencies itself
> without any intermediate heap-images, then I obtain the error that the
> above file does not exist. This asymmetry between using and not using a
> heamp-image seems a bit awkward (although it is not clear to me whether
> it can be avoided in general).

This also happens quite a lot for our CAVA project and is not related to
jEdit, but (as an educated guess) due to the flat namespace of theories:
Isabelle first checks whether a theory with the name (NB: not path!) to
be imported already exists in the current image, and, if so, omits
looking at it.

I'd be in favor of changing this behavior to at least also check for the
existance of the path. Because it happens (for us at least) quite often,
that a theory is always loaded with a specific image and therefore an
erroneous import never gets detected.

(FWIW: This also produces funny results, if you happen to have a theory
"A" in the image, and try to load another, though different, theory also
named "A". It then again omits loading it instead of saying something
about a clash of theory names, producing funny results later on when you
are trying to find out why certain facts seem to be not available...)

- René

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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