[isabelle-dev] Building Isabelle/Scala layer from Repository Version on Windows7 (64 Bit)

[Makarius]

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