Email Gateway (Aug 19 2022 at 14:50): Email Gateway (Aug 19 2022 at 14:50):From: Makarius <makarius@sketis.net>
I think this is just a consequence of the normal operation of creating
PIDE document nodes from buffers, non-buffers, not-yet-buffers,
no-longer-buffers. The Isabelle/jEdit manual has this slightly cryptic
entry in the last chapter, which is related, but does not tell the whole
story:
\item \textbf{Problem:} No way to delete document nodes from the overall
collection of theories.
\textbf{Workaround:} Ignore unused files. Restart whole
Isabelle/jEdit session in worst-case situation.
These mechanisms date back several years, and I did not have time yet to
brush them up. Anything that touches theory import management usually
causes entanglement in the "4 modes of Isabelle", as explained earlier on
this thread.
Makarius
Email Gateway (Aug 19 2022 at 14:50):From: Makarius <makarius@sketis.net>
It is awkward indeed, and these things are a recurrent topic over many
years.
The thread about "Name clashes in theory names" from Feb-2014 is related
to the whole complex. Shortly afterwards I made again some investigations
how this could be sorted out, but got entangled in old things.
So once again, nothing yet for the coming release.
Makarius
Email Gateway (Aug 19 2022 at 15:04):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 15:14):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Makarius,
I sometimes notice that the theory panel on Isabelle/jEdit lists
theory-nodes that do not exist (and never did). Finally, I was able to
construct a minimal example (but it often happened to me when editing
the headers of real theory files). On my machine (x86_64-linux; Fedora
20) I can somewhat reliably reconstruct the issue as follows:
1) From the command line start Isabelle/jEdit with new file, e.g.,
isabelle jedit Test.thy
2) In the first line, enter a symbol that will cause an error, e.g., "+".
3) Now after the plus-sign enter the usual
theory Test
imports M
begin
end
where the imports consist of the non-existent theory M.
4) Go to the first line and delete it.
5) Open the theory panel, which no contains entries for "Test" and "M".
Note that I'm unable to reproduce the above, when the theory panel is
already open on startup of Isabelle/jEdit.
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).
cheers
chris
Email Gateway (Aug 19 2022 at 15:14):From: René Neumann <rene.neumann@in.tum.de>
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...)
Last updated: Apr 23 2024 at 04:18 UTC