[isabelle] problem building logics during install of Isabelle2005 on Cygwin




Hello, hoping someone can help...

I've installed Cygwin and SMLNJ as per the instructions on
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/installation_notes_cygwin.html

But I have an error building the logics. I'm trying to build HOL but when it first builds Pure it seems it never writes out the Pure heap anywhere and so the build of HOL fails. The fairly short output of running the build is at the foot of this email.

Anyone have any ideas how to fix this? (I particularly need Isabelle2005, and I think the zip of a Cygwin installation that Viorel Proteasa has online is 2004)

cheers,
Will

               *****************************
               * Welcome to Isabelle build *
               *****************************

Please check /cygdrive/c/whb21_cygwin/Isabelle/Isabelle2005/etc/settings
to make sure that Isabelle's ML system settings and compilation options
are appropriate.

The current values are:

 ML_SYSTEM=smlnj-110
 ML_HOME=/cygdrive/c/whb21_cygwin/Isabelle/Isabelle2005/../smlnj/bin
 ML_OPTIONS= at SMLdebug=/dev/null
 ML_PLATFORM=x86-cygwin

 ISABELLE_USEDIR_OPTIONS=-v true -V outline=/proof,/ML
 HOL_USEDIR_OPTIONS=


Press RETURN to compilation of

 HOL

Started at Tue Apr  4 18:53:01 GMTST 2006 (smlnj-110_x86-cygwin on narani)
make[1]: Entering directory `/cygdrive/c/whb21_cygwin/Isabelle/Isabelle2005/src/Pure'
Building Pure ...
Finished Pure (0:00:02 elapsed time)
make[1]: Leaving directory `/cygdrive/c/whb21_cygwin/Isabelle/Isabelle2005/src/Pure'
Finished at Tue Apr  4 18:53:04 GMTST 2006
0:00:03 total elapsed time







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.