Re: [isabelle-dev] canonical left-fold combinator for lists
On Fri, 13 Jan 2012, Brian Huffman wrote: I am writing about the following recent changeset, which adds another left-fold operator to HOL/List.thy. author haftmann Fri Jan 06 10:19:49 2012 +0100 (6 days ago) changeset 46133 d9fe85d3d2cd parent 461325a29dbf4c155 child 46134 4b9d4659228a incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r) http://isabelle.in.tum.de/repos/isabelle/rev/d9fe85d3d2cd I would like to take issue with a couple of things here. First, I don't understand why it should be called canonical. What mainstream programming language has a left-fold operation with this particular type signature? The only place I have ever seen this variety of fold is in src/Pure/General/basics.ML in the Isabelle distribution. Canonical is a technical term from the Isabelle/ML culture. The idea behind it is already firmly established for many years, the name is there for quite a few years as well. The Isabelle/Isar Implementation Manual privides some text on this in section 0.3. (Does anybody have a PDF to Stone-Tablet-Printer?) I've never claimed myself that the HOL library or any other language out there is or has to be canonical in that sense, although it would do them good. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: Loading theories does not work
Hi, lately, Isabelle/jEdit stopped working for me on my work laptop. The Isabelle process is started (the usual startup phrase is displayed in the log windows), but the status is displayed as startup. In particular, no parsing, syntax coloring or proof checking happens; the polyml processes seem to be mostly idle. I bisected the problem down to the following commit: changeset: 46121:30a69cd8a9a0c9d539fceba286bb93bc0c3154ca Author: wenzelm Date: Thu Jan 05 14:15:37 2012 +0100 prefer raw_message for protocol implementation; As for the dependencies, * scala-2.8.2-final (but happens with 2.9.1-final and 2.8.1-final, too) * my systems java is 1.6.0_26 from Sun * jedit_build-20110622 (but happens with jedit_build-20111217, too) * the contrib/ directory is the one from Isabelle2011-1 I could not reproduce this problem on my other machine, which (apart from scala-2.8.1) uses the same components. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] JinjaThreads
On Thu, 12 Jan 2012, Lukas Bulwahn wrote: On 01/11/2012 09:29 PM, Alexander Krauss wrote: The real problem is in fact JinjaThreads. AFAIK, the only machine at TUM where it can still build (in principle) is lxbroy10, but as Lukas pointed out there are still some failures, cf. http://isabelle.in.tum.de/reports/Isabelle/report/628b2a4bd3f94f478b929b72f811c5af. I hope that we can get further data on whether this is a repeatable problem in the next days. NB: JinjaThreads has been failing in the mira testing of the configuration AFP-big since the beginning of testing on lxbroy10. Up to now, we don't know which system configurations is actually causing this failure. But nobody has spent much time to investigate this sofar. I haven't been aware of that. The configuration goes back to myself, in private communication with Alex. I did not check it later. In 4a892432e8f1 it is now more conventional, also tested manually to some extend. But there is another problem with JinjaThreads right now: Isabelle/d43ddad41d81 AFP/3dcc6b9eae2b thys/JinjaThreads/Framework/FWDeadlock.thy line 251: blast does not terminate and fills up memory It looks like another set vs. pred thing stemming from coinductive_set deadlocked further above. An expert of having a set-back should know what to do here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Loading theories does not work
On 13.01.2012 13:49, Lars Noschinski wrote: Hi, lately, Isabelle/jEdit stopped working for me on my work laptop. The Isabelle process is started (the usual startup phrase is displayed in the log windows), but the status is displayed as startup. In particular, no parsing, syntax coloring or proof checking happens; the polyml processes seem to be mostly idle. I bisected the problem down to the following commit: Please ignore this for now; if found an error in my test setup. Will try again on monday. Sorry, Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JinjaThreads
On 01/13/2012 06:24 PM, Makarius wrote: I haven't been aware of that. The configuration goes back to myself, in private communication with Alex. I did not check it later. In 4a892432e8f1 it is now more conventional, also tested manually to some extend. 4a892432e8f1 merely modifies the setup for the Isabelle_makeall run. The AFP settings are here http://afp.hg.sourceforge.net/hgweb/afp/afp/file/3dcc6b9eae2b/admin/mira.py#l33 and they match the ones from regular isatest. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
