[isabelle-dev] isabelle jedit -l HOL fails
After updating the repository today (and a seemingly good run of 'isabelle components -a') 'isabelle jedit -l HOL' gives me 2013-10-01 20:42:22.345 java[35294:903] *** NSInvocation: warning: object 0x10ad24390 of class 'ThreadUtilities' does not implement methodSignatureForSelector: -- trouble ahead 2013-10-01 20:42:22.348 java[35294:903] *** NSInvocation: warning: object 0x10ad24390 of class 'ThreadUtilities' does not implement doesNotRecognizeSelector: -- abort /Users/ballarin/isabelle/repo/lib/Tools/java: line 1: 35294 Trace/BPT trap $ISABELLE_JDK_HOME/bin/$PRG $@ I'm still on MacOSX 10.6.8 Snow Leopard. Any ideas? Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle jedit -l HOL fails
Try running jedit -bf, if that does not help, manually remove the build artifacts (I.e. the jar files). Sometimes rebuilding of the Java components doors not work reliably. Clemens Ballarin balla...@in.tum.de schrieb: After updating the repository today (and a seemingly good run of 'isabelle components -a') 'isabelle jedit -l HOL' gives me 2013-10-01 20:42:22.345 java[35294:903] *** NSInvocation: warning: object 0x10ad24390 of class 'ThreadUtilities' does not implement methodSignatureForSelector: -- trouble ahead 2013-10-01 20:42:22.348 java[35294:903] *** NSInvocation: warning: object 0x10ad24390 of class 'ThreadUtilities' does not implement doesNotRecognizeSelector: -- abort /Users/ballarin/isabelle/repo/lib/Tools/java: line 1: 35294 Trace/BPT trap $ISABELLE_JDK_HOME/bin/$PRG $@ I'm still on MacOSX 10.6.8 Snow Leopard. Any ideas? Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases
On 09/30/2013 02:41 PM, Makarius wrote: On Mon, 30 Sep 2013, Manuel Eberl wrote: On 30/09/13 11:49, Makarius wrote: On Mon, 23 Sep 2013, Manuel Eberl wrote: I sent my changes to Alexander Krauss last Wednesday so that he can review them. We are now getting very close to the fork-point for the release. So can you just post the changeset here, or send it to me privately? Of course. Here you go. Thanks. This is now Isabelle/d8f7f3d998de. Thanks for taking care of this. When looking at the original code earlier, I was also a bit irritated by the use of term patterns, but then it got lost somehow. Nevertheless, it is also a bit irritating that there seems to be no proper way of adding support for wildcards to fun_cases (and inductive_cases). This should be addressed at some point, but for now we are fine. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testboard
On 09/27/2013 11:49 AM, Lars Noschinski wrote: It might be a good idea to implement a strategy which tests the existing heads in reverse chronological order (commits pushed last get tested first), but I am not sure whether this information is available in Mercurial (we have the commit date, but this is not necessarily related to the push-date). Such a strategy is easy to implement for a single repository. But for multiple repositories (Isabelle+AFP) there is no useful notion of heads (The obvious lifting to products does work theoretically, but not practically, since there are just too many of them...) Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
