[isabelle-dev] Bad theory import "Main"
j.c.blanchette at vu.nl
Sat Apr 22 13:26:00 CEST 2017
> Odd. I cannot reproduce this on Linux or macOS Sierra.
It didn't happen to me yesterday night either, even though I was using the same changeset. It just started this morning when I restarted Isabelle/jEdit, for no apparent reason.
I'm using El Capitan on this laptop. I've been using this system with Isabelle for over two years now. I also have a Sierra laptop at work, which I can test on Monday.
> What is your $ISABELLE_HOME actually?
$ isabelle getenv ISABELLE_HOME
> Is there anything special with the underlying file-system?
Not that I am aware of.
> Here is an example for the Console/Scala toplevel within Isabelle/jEdit:
> scala> PIDE.resources.session_base.known.files.toList.find(p =>
> p._2.exists(_.theory == "Main"))
> res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] =
> What is your result?
<console>:12: error: not found: value PIDE
PIDE.resources.session_base.known.files.toList.find(p => p._2.exists(_.theory == "Main"))
Maybe the Scala build state is not clean? (I couldn't find how to clean it in the system manual.)
More information about the isabelle-dev