Re: [isabelle] installing Isabelle



Hi Clinton,
I am wondering how you installed it the first time around but that
doesn't matter much.

I am no expert on isabelle installations and your terminal output is
formatted strangely on my side but it looks like you do not have the
rights to write/install to usr/local/bin.

Have you tried 
   cd [ISABELLE_HOME]
   ./bin/isatool install -p [your_home]/bin
?

I use this to install to my local bin directory. You can also try
contacting your system administrator.
I do not use the droplet and do not know if the droplet checks there for
executables. You might have to add it to your path if necessary.

Good luck,
Primrose

-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk
[mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of clefort
Sent: Monday, December 11, 2006 11:07 AM
To: cl-isabelle-users at lists.cam.ac.uk
Subject: [isabelle] installing Isabelle


Hello

I have reinstalled Isabelle from http://www.cl.cam.ac.uk/research/hvg/
Isabelle/dist/ Isabelle2005.tar.gz

I placed them in my directory and used UNTAR1.3 to untar the file and
was successful. but  when following the further directions saying:

The installation may be finished as follows:

   cd [ISABELLE_HOME]
   ./bin/isatool install -p /usr/local/bin


I got this from my terminal app:



68-119-241-204:~/Isabelle/Isabelle/ISABELLE_HOME clintonlefort$ ./bin/
isatool install -p /usr/local/bin referring to distribution at
/Users/clintonlefort/Isabelle/Isabelle/
ISABELLE_HOME
installing /usr/local/bin/isatool
/Users/clintonlefort/Isabelle/Isabelle/ISABELLE_HOME/lib/Tools/
install: line 95: /usr/local/bin/isatool: Permission denied Cannot write
file: /usr/local/bin/isatool
68-119-241-204:~/Isabelle/Isabelle/ISABELLE_HOME clintonlefort$


Further when I drop a CCL.thy file on Isabelle droplet I get this
information, which make some think that there are some settings issues:

Unable to find Isabelle.  PATH = /usr/bin:/bin:/usr/sbin:/sbin:/Users/
clintonlefort/isabelle/bin

Can I fix these problems. My goal is to have Isabelle running on my
machine by Christmas 2006. But I've been working on this for three weeks
now (not continually , of course), but I do have the emacs up and
running and have started on the Tutorial. I still need to learn GNU
emacs. I have started my proofs successfully using Otter3.3, but look
forward to learning Isabelle.

Gratefully,

Clinton R. LeFort
Immaculata Publishing
Union, Mo
USA





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