RE: [isabelle] Questions about using Isabelle



Hello, Andrew, thank you for your nice help.

I tried several times running the build file, and fixed one problem with move the SML/NJ directory, and then came to the following error message:


Please check /usr/local/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=/usr/local/Isabelle2005/contrib/smlnj/bin
  ML_OPTIONS= at SMLdebug=/dev/null
  ML_PLATFORM=x86-linux

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


Press RETURN to compilation of

  HOL

Started at Mon Nov 14 21:53:36 CET 2005 (smlnj-110_x86-linux on linux)
make[1]: Entering directory `/usr/local/Isabelle2005/src/Pure'
Building Pure ...
Finished Pure (0:00:00 elapsed time)
make[1]: Leaving directory `/usr/local/Isabelle2005/src/Pure'
make: *** No rule to make target `/usr/local/Isabelle2005/heaps/smlnj-110_x86-linux/Pure', needed by `/usr/local/Isabelle2005/heaps/smlnj-110_x86-linux/HOL'.  Stop.
Finished at Mon Nov 14 21:53:36 CET 2005

Do you know how to solve this? Thank you again.

Peace, joy.
Jenny


-----Original Message-----
From: Andrew Pimlott [mailto:andrew at pimlott.net]
Sent: Fri 11/11/2005 10:41 PM
To: Jin  Xiaohui
Cc: isabelle-users at cl.cam.ac.uk
Subject: Re: [isabelle] Questions about using Isabelle
 
On Fri, Nov 11, 2005 at 06:26:43PM +0100, Jin  Xiaohui wrote:
> I tried to install Isabelle with SML/NJ. When start Isabelle after the
> installment, an error message of "unknown logic "HOL", no heap file
> found in... " came up. I did more tries, such as exchange the installing
> order for the files, etc., the error just stays.

Run the script /usr/local/Isabelle/build.

Andrew






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