Re: [isabelle-dev] jEdit
On Fri, 27 Apr 2012, Christian Sternagel wrote: Maybe I should have tried it myself before posting ;). Yes, it works with jdk1.6.0_32. The test website already provides the bundled JDK, which is jdk1.6.0_31 and was produced just before Oracle upgraded to 32 :-( Fortunately there are hardly any significant changes going on the 1.6 branch, so I will probably leave is as is. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Spurious messages
Hi all, With the latest Isabelle (44b33c1e702e), some attributes, e.g. unify_search bound, give pairs of spurious warnings, e.g. ### Ignoring local change of global option unify_search_bound even when they are declared globally, as in the theory below: theory Scratch imports Main begin declare [[unify_search_bound = 55]] declare [[unify_trace_bound = 55]] The declarations are thankfully _not_ ignored. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spurious messages
On Fri, 27 Apr 2012, Jasmin Christian Blanchette wrote: With the latest Isabelle (44b33c1e702e), some attributes, e.g. unify_search bound, give pairs of spurious warnings, e.g. ### Ignoring local change of global option unify_search_bound even when they are declared globally, as in the theory below: declare [[unify_search_bound = 55]] The declarations are thankfully _not_ ignored. This is now addressed in Isabelle/53668571d300, using Context_Position visiblity to restrict output to messages that are considered relevant to the user. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] spass: Internal error: exception Empty raised (line 458 of library.ML)
On Tue, 24 Apr 2012, Makarius wrote: I have also made some more experiments. The Empty exception is from the split_last here http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614 where you don't get any output unexpectedly, bacause /bin/sh has crashed. Ouch! Such things happen on Cygwin. I will try to sort out the physical problem. The situation is still not fully clear. It seems that /bin/sh.exe and especially /bin/perl.exe tend to crash on Cygwin in the way they are used here with src/Pure/Concurrent/bash.ML. I have made a plain C wrapper to replace lib/scripts/process, see Admin/exec_prosess -- this component can be compiled manually with the included build script and initialized in settings or components in the usual way. The idea is to ship that in the Cygwin bundle. Doing this for vmbroy9 seems to improve stabilit significantly. I did not get any crashes of e or spass after 20..40 runs. The remote provers still crash occasionally due to their inherent reliance on perl. It seems that the best times of the rock-solid Larry Wall operating systems are over, at least on this slightly odd Linux variant with MS kernel. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
