RE: [isabelle] Questions about using Isabelle

Thank you, Andrew.

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.

I went back with the Poly/ML and retried again, same error appeared
which did not show up before.

I retried with a blank directory, the error still exits.

I wonder if I missed any step? Thank you.

Peace, joy.

> -----Original Message-----
> From: Andrew Pimlott [mailto:andrew at]
> Sent: November 8, 2005 5:15 PM
> To: Jin Xiaohui
> Cc: isabelle-users at
> Subject: Re: [isabelle] Questions about using Isabelle
> On Mon, Nov 07, 2005 at 04:15:04PM +0100, Jin  Xiaohui wrote:
> > Also, I rebuilt the driver of PolyML according to the possible
> > of "Segmentation faults with Linux" said on the installment webpage,
> > problem still cannot be solved.
> This was my experience as well.  I ended up using SML/NJ instead.  I
> to rebuild the Isabelle libraries with the provided build script.  I
> can't remember everything I did, but I can check later if you have any
> trouble.
> Andrew

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