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

[Makarius]

On 24/04/17 15:21, Lars Hupel wrote:
> 
>> I actually offered an open dialog about it last December, and you
>> rejected that.
> 
> Because the offer consisted merely of rehashing things we already talked
> about in person. To be completely frank, I'm tired of repeating myself
> and others endlessly.

I actually wanted to resolve all the open questions that remained in the
Jenkins project. Open problems that are still open need to be
"rehashed", even this is tiresome.


> For the record, the lxcisa0 host is the result of a compromise that both
> Jenkins and what you asked for (a publicly-accessible beefy machine)
> should be accommodated for. I wouldn't call that rejection.

So far, I did not even know that the ssh access was now "official". I
thought it was just privately for me, to do some basic hardware tests.

It shows that in "blame game" mode it is hard to communicate in a plain
and simple way.


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"

[Blanchette, J.C.]

Hi Makarius,

> The problem is in the HOL-Lib session from isafor. It is somewhere in
> your ROOTS (or -d specifications).

Ah!

> Are you working with IsaFoR on purpose, or is this just an accident?

That's it. I had IsaFoR as a component -- half on purpose, half by accident.

Thanks for helping me debug it.

> In current Isabelle/6acb28e5ba41 it is also possible to use something
> like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space
> to the requirements of MY_SESSION.

Good to know.

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"

[Lars Hupel]

> This is still "blame game".

If you say so.

> I actually offered an open dialog about it last December, and you
> rejected that.

Because the offer consisted merely of rehashing things we already talked
about in person. To be completely frank, I'm tired of repeating myself
and others endlessly.

For the record, the lxcisa0 host is the result of a compromise that both
Jenkins and what you asked for (a publicly-accessible beefy machine)
should be accommodated for. I wouldn't call that rejection.
___
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"

[Makarius]

On 24/04/17 14:36, Makarius wrote:
> On 23/04/17 18:10, Blanchette, J.C. wrote:
>>
>> *** No such file: 
>> "/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy"
>> *** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17 
>> of "/Users/blanchette/hgs/isafor/thys/ROOT")
> 
> The transition from unqualified theories to qualified theories is not
> smooth -- there can be intermediate situations, where certain sessions
> cannot import certain theories anymore.
> 
> The emerging tool "isabelle imports" tools helps to sort out the
> situation, but it requires some care to use it and I am still exploring
> the overall situation.

The situation is actually more basic: src/HOL/Library/Fraction_Field.thy
etc. were moved to a separate session in fc41a5650fb1 and thus you have
a broken IsaFoR still lying around by accident.

What I said about "isabelle imports" is not yet relevant (presently at
10f4a17e5928), because I did not move that far ahead yet -- although I
was pondering when to do it.

(Right now I have the impression that there is an aversion to any kind
of change on the ever changing isabelle-dev repository. We are between
the releases and now is the usual time for bigger reforms. Or are we
already in a state where big things can no longer happen?)


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"

[Tobias Nipkow]

On 24/04/2017 14:24, Makarius wrote:

In the past 1.5 years, I've spent a lot of time trying to explain how
the Isabelle administration works. If we don't manage to overcome the
"blame game", things will decline further.


If you think I was trying to blame you for having forgotten to commit a file, 
that is a misunderstanding. I wasn't sure what had happened and merely brought 
to your attention the jenkins report. I didn't include any remark about the 
importance of not breaking the distribution.


Jenkins is giving me better coverage than before, which is what we wanted. If 
something does not work anymore and has to be worked around, it can hardly be 
the effect of an additional test system.


Tobias



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"

[Makarius]

On 24/04/17 14:46, Lars Hupel wrote:
> Then, out of the blue, you stopped caring,
> unsubscribed for strange reasons from the CI list and started calling
> Jenkins a "monster" and a "waste of resources".
> 
> It is because of that that I'm having a hard time believing that you're
> willing to engage in constructive dialog about regression testing anymore.
> 
> You claim that you "did not get any answers". In reality, you got all
> the answers and ignored them.

This is still "blame game".

I actually offered an open dialog about it last December, and you
rejected that.


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"

[Makarius]

On 23/04/17 18:10, Blanchette, J.C. wrote:
> 
> Yes, it does both I guess. The "half-decent error message" looks like this:
> 
> /Users/blanchette/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
> Cannot start: 
> *** No such file: 
> "/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy"
> *** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17 
> of "/Users/blanchette/hgs/isafor/thys/ROOT")
> *** No such file: 
> "/Users/blanchette/isabelle/src/HOL/Library/Fundamental_Theorem_Algebra.thy"
> *** The error(s) above occurred for theory 
> "HOL-Lib.Fundamental_Theorem_Algebra" (line 18 of 
> "/Users/blanchette/hgs/isafor/thys/ROOT")
> *** No such file: 
> "/Users/blanchette/isabelle/src/HOL/Library/Polynomial_Factorial.thy"
> *** The error(s) above occurred for theory "HOL-Lib.Polynomial_Factorial" 
> (line 29 of "/Users/blanchette/hgs/isafor/thys/ROOT")
> *** The error(s) above occurred in session "HOL-Lib" (line 1 of 
> "/Users/blanchette/hgs/isafor/thys/ROOT")
> 
> But then I can't use Isabelle/jEdit.

The problem is in the HOL-Lib session from isafor. It is somewhere in
your ROOTS (or -d specifications).

Are you working with IsaFoR on purpose, or is this just an accident?


The transition from unqualified theories to qualified theories is not
smooth -- there can be intermediate situations, where certain sessions
cannot import certain theories anymore.

The emerging tool "isabelle imports" tools helps to sort out the
situation, but it requires some care to use it and I am still exploring
the overall situation.

In current Isabelle/6acb28e5ba41 it is also possible to use something
like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space
to the requirements of MY_SESSION.


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"

[Makarius]

On 23/04/17 15:54, Tobias Nipkow wrote:
> The Isabelle regression test system shows up a mistake in a commit of
> yours and you ask what its purpose is? And tell us your rarely look there?

That was a trivial mistake: easy to spot and easy to repair. We don't
need a huge monster like Jenkins for that, with all its waste of resources.


The key problem of the Jenkins project is that the test coverage that is
required to hold up stable Isabelle releases on many platforms dropped
significantly (one 1 ago). I have recovered from that partially, by
working around Jenkins.

In the past 1.5 years, I've spent a lot of time trying to explain how
the Isabelle administration works. If we don't manage to overcome the
"blame game", things will decline further.


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"

[Blanchette, J.C.]

> This means you should see some "Java vomit" on the terminal at startup
> of Isabelle/jEdit, as well as some text popup with a half-decent error
> message. Plugin startup is always a bit fragile.

Yes, it does both I guess. The "half-decent error message" looks like this:

/Users/blanchette/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start: 
*** No such file: 
"/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy"
*** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17 of 
"/Users/blanchette/hgs/isafor/thys/ROOT")
*** No such file: 
"/Users/blanchette/isabelle/src/HOL/Library/Fundamental_Theorem_Algebra.thy"
*** The error(s) above occurred for theory 
"HOL-Lib.Fundamental_Theorem_Algebra" (line 18 of 
"/Users/blanchette/hgs/isafor/thys/ROOT")
*** No such file: 
"/Users/blanchette/isabelle/src/HOL/Library/Polynomial_Factorial.thy"
*** The error(s) above occurred for theory "HOL-Lib.Polynomial_Factorial" (line 
29 of "/Users/blanchette/hgs/isafor/thys/ROOT")
*** The error(s) above occurred in session "HOL-Lib" (line 1 of 
"/Users/blanchette/hgs/isafor/thys/ROOT")

But then I can't use Isabelle/jEdit. I was better off 2 days ago. Back then, 
things worked.

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"

[Tobias Nipkow]

The Isabelle regression test system shows up a mistake in a commit of yours and 
you ask what its purpose is? And tell us your rarely look there?


LOL

Tobias

On 23/04/2017 14:52, Makarius wrote:

On 23/04/17 08:39, Tobias Nipkow wrote:

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


I did not see this, because Jenkins is not "The Isabelle regression test
system" and I am rarely looking what happens there -- I do look
sometimes after significant changes of Isabelle/Scala, because I have no
intention to destroy such experiments on purpose.

Concerning the status of Jenkins wrt. isabelle-dev (not isabelle-group
at TUM), we are still lacking a proper discussion of its purpose and
general approach. When I started to ask some critical questions last
year, I did not get any answers and was merely blamed for that.


If there is anybody *outside* the TUM group, who uses the Jenkins setup
regularly, it would be interesting to discuss some basic things. What is
good about it? What is bad about it?


Makarius





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"

[Makarius]

On 23/04/17 08:39, Tobias Nipkow wrote:
> 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")

I did not see this, because Jenkins is not "The Isabelle regression test
system" and I am rarely looking what happens there -- I do look
sometimes after significant changes of Isabelle/Scala, because I have no
intention to destroy such experiments on purpose.

Concerning the status of Jenkins wrt. isabelle-dev (not isabelle-group
at TUM), we are still lacking a proper discussion of its purpose and
general approach. When I started to ask some critical questions last
year, I did not get any answers and was merely blamed for that.


If there is anybody *outside* the TUM group, who uses the Jenkins setup
regularly, it would be interesting to discuss some basic things. What is
good about it? What is bad about it?


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"

[Makarius]

On 23/04/17 13:43, Blanchette, J.C. wrote:
>>> 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
> 
> I just pulled and updated (f533820e7248) before carrying out any further 
> tests. Now I get the same error as Jenkins:
> 
> $ isabelle build -b HOL
> *** No such file: "/Users/blanchette/isabelle/src/HOL/Main.thy"
> *** The error(s) above occurred for theory "Main" (line 8 of 
> "/Users/blanchette/isabelle/src/HOL/ROOT")
> *** The error(s) above occurred in session "HOL" (line 3 of 
> "/Users/blanchette/isabelle/src/HOL/ROOT")

That is unrelated. I merely made the most basic mistake in Mercurial
usage, see now:

changeset:   65553:006a274cdbc2
user:wenzelm
date:Sun Apr 23 14:15:09 2017 +0200
files:   src/HOL/Main.thy
description:
added missing file (amending f533820e7248);


Concerning the actual problem, I have now made the session_base error
strict (again):

changeset:   65554:a04afc400156
tag: tip
user:wenzelm
date:Sun Apr 23 14:27:22 2017 +0200
files:   src/Tools/jEdit/src/plugin.scala
description:
prefer strict operation (despite 8edca3465758): there might be errors
from all_known = true (ae09b9f5980b);


This means you should see some "Java vomit" on the terminal at startup
of Isabelle/jEdit, as well as some text popup with a half-decent error
message. Plugin startup is always a bit fragile.


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"

[Blanchette, J.C.]

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

I just pulled and updated (f533820e7248) before carrying out any further tests. 
Now I get the same error as Jenkins:

$ isabelle build -b HOL
*** No such file: "/Users/blanchette/isabelle/src/HOL/Main.thy"
*** The error(s) above occurred for theory "Main" (line 8 of 
"/Users/blanchette/isabelle/src/HOL/ROOT")
*** The error(s) above occurred in session "HOL" (line 3 of 
"/Users/blanchette/isabelle/src/HOL/ROOT")

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"

[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-...@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"

[Makarius]

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"

[Blanchette, J.C.]

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

[Makarius]

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"

[Blanchette, J.C.]

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

[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?

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

[Makarius]

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"

[Blanchette, J.C.]

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