[isabelle-dev] Isabelle release test website

[Makarius]

On Tue, 24 Apr 2012, Jasmin Christian Blanchette wrote:

> Am 23.04.2012 um 17:22 schrieb Makarius:
>
>> Here is an update of the test website for warming up a bit more 
>> http://www4.in.tum.de/~wenzelm/test/website/
>>
>> I've spent this cold and wet weekend to produce a monolitic Windows 
>> application, which bundles both JDK and Cygwin 1.7.9, see the Download 
>> page.  (Cygwin 1.7.9 is important here, because in the later version 
>> from this year Poly/ML multithreading is a bit unstable.)
>
> I use Windows XP on VirtualBox. I downloaded the 
> "Isabelle_23-Apr-2012.exe" file, moved it to my home directory. Then I 
> started "Isabelle.exe" and waited over a minute but nothing happened.

I suppose here that the self-extracting Isabelle_23-Apr-2012.exe archive 
did extract correctly, to something like 850 MB directory structure?


> Then I tried
>
>    ./bin/isabelle tty
>
> but got the message 'Unknown logic "HOL" -- no heap file found in: 
> /cygdrive/c/.../heaps/polyml-undefined_x86-cygwin ...".

> Could it be due to Cygwin somehow? I don't know how to launch a terminal 
> for Cygwin 1.7.9, so I'm still using the old terminal for whatever 
> version of Cygwin I had on the machine already.

Your existing Cygwin is probably relatively old, such that the poly.exe 
cannot be started and produce the required version; cf. the "undefined" 
above.

Starting a terminal for the bundled Isabelle Cygwin now works, but I did 
not update the 7zip SFX yet.  You can do it via 
http://www4.in.tum.de/~wenzelm/test/website/dist/Isabelle_23-Apr-2012_bundle_x86-cygwin.tar.gz 
by untarring that with the existing Cygwin.  Then the directory structure 
can be access via Windows the standard way.

There are now Cygwin-Terminal and Cygwin-Setup batch files to be clicked 
on, which hopefully do the job.


You might still have to do a manual incantation from cmd.exe:

   ...\contrib\cygwin-1.7.9\bin\ash -c /bin/rebaseall

This maintenance step requires all Cygwin stuff to be off.


 	Makarius