[isabelle-dev] Bad theory import "Main"

[Blanchette, J.C.]

> 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
ISABELLE_HOME=/Users/blanchette/isabelle

> 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])] =
> Some((/home/makarius/isabelle/repos/src/HOL/Main.thy,List(Main)))
> 
> 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.)

Jasmin