Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] problem building logics during install of Isab...

Email Gateway (Aug 17 2022 at 14:43):

From: William Billingsley <whb21@cam.ac.uk>
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=@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

Last updated: Nov 21 2024 at 12:39 UTC