[isabelle] Isabelle2014-RC0: phantom theories



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




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