Re: [isabelle] Isabelle2014-RC0: phantom theories



On Tue, 8 Jul 2014, René Neumann wrote:

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...)

These problems with the flat theory name space and odd rules to locate theory sources files are very old and well-known, but quite annoying nonetheless, especially since many other aspects of the system have improved.

Substantial reforms and simplications (removal of adhoc features) are in the pipeline for many years. This spring I have revisited that once again, but did not finish for the release -- due to the Isar TTY loop and Proof General standing in the way.

It is something to be sorted out eventually, together with the canonical question about "remaining uses of Proof General".


At VSL/Coq-6 there was an interesting talk about "Coqoon: towards a modern IDE for Coq" http://www.easychair.org/smart-program/VSL2014/Coq-program.html -- he replaced the old-fashioned make-based coqc build process by a canonical solution within Eclipse, and encountered similar problems with multiple ways to locate files within implicit load paths, asking for just one unique way to address theories within "packages".

The quirks and workarounds sounded very familiar to me.


	Makarius


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