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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and