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 
   ./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,

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


I have reinstalled Isabelle from
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:

   ./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
installing /usr/local/bin/isatool
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/

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.


Clinton R. LeFort
Immaculata Publishing
Union, Mo

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