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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 >

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

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

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

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

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

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

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

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.

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

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

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

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