Re: [isabelle-dev] Bad theory import "Main"

[Tobias Nipkow]

The Isabelle regression test system shows similar behaviour:



Tobias

On 22/04/2017 13:13, Makarius wrote:

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")

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