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
The current values are:
ML_OPTIONS= at SMLdebug=/dev/null
ISABELLE_USEDIR_OPTIONS=-v true -V outline=/proof,/ML
Press RETURN to compilation of
Started at Mon Nov 14 21:53:36 CET 2005 (smlnj-110_x86-linux on linux)
make: Entering directory `/usr/local/Isabelle2005/src/Pure'
Building Pure ...
Finished Pure (0:00:00 elapsed time)
make: 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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and