[isabelle-dev] Bad theory import "Main"

[Tobias Nipkow]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170423/107dcfd3/attachment.bin>