[isabelle-dev] Isabelle release test website

Makarius makarius at sketis.net
Tue Apr 24 16:41:13 CEST 2012

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" 

Starting a terminal for the bundled Isabelle Cygwin now works, but I did 
not update the 7zip SFX yet.  You can do it via 
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.


More information about the isabelle-dev mailing list