Re: [isabelle-dev] Build error (isabelle.Build not found)
On Thu, 10 Jan 2013, Jasmin Christian Blanchette wrote: Am 10.01.2013 um 13:16 schrieb Jasmin Blanchette: I just updated Isabelle to af8ecf09a58c (from a version that was one or two days old) and whenever I try to build HOL, I get this error: isabelle build -c -b HOL Fehler: Hauptklasse isabelle.Build konnte nicht gefunden oder geladen werden 0:00:00 elapsed time, 0:00:00 cpu time Mac OS X 10.6. I haven't changed any settings recently. I did some updates back and forth along the history and strangely enough the problem disappeared once I went back to the above change (af8ecf09a58c). Strange. The root of the problem is here: changeset: 50753:1253fd12ca8a user:wenzelm date:Sun Jan 06 12:44:45 2013 +0100 files: Admin/components/components.sha1 Admin/components/main description: updated to scala-2.10.0; The update from 2.9.2 to 2.10.0 introduces a discontinuity in the JVM bytecode emitted by the scala compiler, since it is a major release step by the EPFL guys. This would be unthinkable for Java, but Scala is still very dynamic, and 2.10.x is indeed a big step forward. My auto-build scripts take source versions into account (via old-fashioned time stamps), but not scala versions. I will rethink this again next time, when there is a new scala release. The -f build option was already introduced some time ago to address any such oddities in the jar build processs. I am doing myself isabelle jedit -b -f quite a lot, e.g. when shuffling components and other administrative scripts. This explains why I did not experience the breakdown myself. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit: type constraints no longer printed by default
On Thu, 10 Jan 2013, Steffen Juilf Smolka wrote: Is this the intended behaviour? It used to be different a couple of month ago. I don't know when it changed exacyly, but I think changeset a6814de45b69 might be responsible for the change. Yes, that change is in the vicinity where I was working on show_markup. See 1301ed115729 for the first occurrence of the corresponding documentation. So with show_markup enabled, type and sort constraints are moved from the text to the markup over the text. This all works surprisingly well for what it does -- it was considered impossible to do such things a few years ago. There might be corner cases where the change of the display leads to odd effects. Are there concrete incidents already that need to be reconsidered before the release? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit: type constraints no longer printed by default
There might be corner cases where the change of the display leads to odd effects. Are there concrete incidents already that need to be reconsidered before the release? We use Syntax.string_of_term when creating Isar proof scripts in Sledgehammer and rely on Type.contstraint to introduce type annotations in terms (this does not work with show_markup set to true). Also, we got the error Malformed YXML: multiple results in certain situations. Both problems are solved as of 0583db803066, simply by setting show_markup to false in Sledgehammer. Steffen ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit: type constraints no longer printed by default
On Fri, 11 Jan 2013, Steffen Juilf Smolka wrote: We use Syntax.string_of_term when creating Isar proof scripts in Sledgehammer and rely on Type.contstraint to introduce type annotations in terms (this does not work with show_markup set to true). Yes, it is correct to set show_markup=false in the context before printing. Note that this is not specific to jedit, but to Isabelle in general. It is just an accident that jedit is right now the only application that enables show_markup routinely. Also, we got the error Malformed YXML: multiple results in certain situations. In which situations? Do you have an exception trace? The message is from YXML.parse, but in most situations one has YXML.parse_body anyway. And in fact, user code should hardly ever come across anything here, at least in theory. Both problems are solved as of 0583db803066, simply by setting show_markup to false in Sledgehammer. BTW, just formally your data (diff over source) and meta-data (log entry) in the changeset have quite an overlap, close to being a parrot. You should not put historical explanation into the source -- it becomes outdated rather quickly and make the text unreadable. The point where you explain what you think you did is the log. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
