Re: [isabelle-dev] Bad theory import "Main"
The Isabelle regression test system shows similar behaviour: 23:23:27 *** No such file: "/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/Main.thy" 23:23:27 *** The error(s) above occurred for theory "Main" (line 8 of "/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/ROOT") 23:23:27 *** The error(s) above occurred in session "HOL" (line 3 of "/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/ROOT") Tobias On 22/04/2017 13:13, Makarius wrote: On 22/04/17 11:48, Jasmin Blanchette wrote: I get the error Bad theory import "Main" Steps to reproduce the problem: cd src/HOL/Library isabelle jedit Cancellation.thy Odd. I cannot reproduce this on Linux or macOS Sierra. What is your $ISABELLE_HOME actually? Is there anything special with the underlying file-system? 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? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bad theory import "Main"
On 22/04/17 19:34, Blanchette, J.C. wrote: > >> On 22.04.2017, at 19:17, Makarius wrote: >> >>> scala> PIDE.resources.session_base.known.files.toList.find(p => >>> p._2.exists(_.theory == "Main")) >>> :12: error: not found: value PIDE >>> PIDE.resources.session_base.known.files.toList.find(p => >>> p._2.exists(_.theory == "Main")) >>> ^ >> >> You need to do this in the Console plugin of Isabelle/jEdit, switched >> into Scala mode. > > I see. It prints > > res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] = None There is probably something wrong with the general session layout. The critical changeset shows an old fallback to Pure: http://isabelle.in.tum.de/repos/isabelle/rev/ae09b9f5980b#l4.10 You should see the error like this in the Console/Scala plugin: val dirs = JEdit_Sessions.session_dirs() val session_base = Sessions.session_base(PIDE.options.value, "HOL", dirs = dirs, all_known = true) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bad theory import "Main"
> On 22.04.2017, at 19:17, Makarius wrote: > >> scala> PIDE.resources.session_base.known.files.toList.find(p => >> p._2.exists(_.theory == "Main")) >> :12: error: not found: value PIDE >> PIDE.resources.session_base.known.files.toList.find(p => >> p._2.exists(_.theory == "Main")) >> ^ > > You need to do this in the Console plugin of Isabelle/jEdit, switched > into Scala mode. I see. It prints res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] = None Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bad theory import "Main"
On 22/04/17 18:10, Blanchette, J.C. wrote: > > It doesn't help: > > $ isabelle jedit -bf > ### Building Isabelle/Scala ... > ### Building Isabelle/jEdit ... > > $ isabelle scala > Welcome to Scala 2.11.8 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_121). > Type in expressions for evaluation. Or try :help. > > scala> PIDE.resources.session_base.known.files.toList.find(p => > p._2.exists(_.theory == "Main")) > :12: error: not found: value PIDE >PIDE.resources.session_base.known.files.toList.find(p => > p._2.exists(_.theory == "Main")) >^ You need to do this in the Console plugin of Isabelle/jEdit, switched into Scala mode. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bad theory import "Main"
> On 22.04.2017, at 17:24, Makarius wrote: > > On 22/04/17 13:26, Blanchette, J.C. wrote: >> >> :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.) > > A forced build of everything works like this: > > isabelle jedit -bf It doesn't help: $ isabelle jedit -bf ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... $ isabelle scala Welcome to Scala 2.11.8 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_121). Type in expressions for evaluation. Or try :help. scala> PIDE.resources.session_base.known.files.toList.find(p => p._2.exists(_.theory == "Main")) :12: error: not found: value PIDE PIDE.resources.session_base.known.files.toList.find(p => p._2.exists(_.theory == "Main")) ^ Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bad theory import "Main"
On 22/04/17 13:26, Blanchette, J.C. wrote: > > :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.) A forced build of everything works like this: isabelle jedit -bf Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bad theory import "Main"
> 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? :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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bad theory import "Main"
On 22/04/17 11:48, Jasmin Blanchette wrote: > I get the error > > Bad theory import "Main" > > Steps to reproduce the problem: > > cd src/HOL/Library > isabelle jedit Cancellation.thy Odd. I cannot reproduce this on Linux or macOS Sierra. What is your $ISABELLE_HOME actually? Is there anything special with the underlying file-system? 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? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Bad theory import "Main"
Hi again, I wrote: > Something strange is happening with the repository (as per > Isabelle/701bb74c5f97). I nailed it down to change ae09b9f5980b. Before that change, Main is loaded normally. With this change, I get the error Bad theory import "Main" Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
