On Thu, 31 May 2012, Jasmin Christian Blanchette wrote:
Am 29.05.2012 um 13:46 schrieb Makarius:
* Try to avoid "using" repository versions in the first place. There
must be good reasons to invest the extra effort that is required to
follow the Isabelle development process in every step.
There are good reasons. Steffen recently started as a HiWi and he will
be improving the Isar proof reconstruction code. That code is tightly
interconnected with the rest of Sledgehammer, so this is definitely not
one of those self-contained student projects that can be done in user
space against some stable version of Isabelle.
Depending on your ambitions you can also try to get a feeling from where
the slight instabilities of external ATPs are coming from on
Windows/Cygwin. This affects both local provers like E (with its thick
shell scripts around the C core) and SPASS, and remote ones via perl.
When I helped him set up the repository version last week, the first
thing we did was to "cannibalize" the official components.
Anyway, if you haven't seen the error before, I guess we'll have to
investigate this more closely on Steffen's machine and find out what
went wrong (and let you know).
On Sun, 27 May 2012, Steffen J. Smolka wrote:
I've installed SUN JDK 1.6u32 (64 Bit) and Scala 2.9.2 final, the
ISABELLE_JDK_HOME and SCALA_HOME environment variables are set
accordingly.
My .isabelle/etc/settings file looks like this:
> init_component "/cygdrive/c/Isabelle2012/contrib/scala-2.9.2"
> init_component "..../isabelle/jedit_build-20120414"
You should also try the jdk-6u31_x86-cygwin component from Isabelle2012.
There is a tiny chance that the independently installed JDK 1.6u32 causes
the problem. These things are often just a matter of funny registry
entries etc.
Via isabelle getenv you should check ISABELLE_JDK_HOME, JAVA_HOME,
SCALA_HOME and ensure that they all point to the Isabelle2012/contrib
versions.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
