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 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"
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"
> 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"
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"
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"
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"
> 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. You yourself proposed investigating Jenkins (then Hudson) some while ago, pointing out that e.g. the Scala team is using it. Then, later, when I got started in the Munich group, we talked with e.g. Alex and other stakeholders about Jenkins. Then, later, you came in person and discussed various things. Up until that point in time, I didn't get the impression that you were categorically opposed to the idea of Jenkins. If so, you didn't say it. 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. It is apt that you describe your private testing setup as a "workaround" for the loss of platform support, because that is exactly what it is. Multiple times I attempted to get Windows and OS X support working, by talking to various people who need or have access to our compute resources. You ignored that and worked around it. ___ 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 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"
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"
> 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"
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"
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"
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"
>> 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"
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