Subject: [clisp-list] Running ACL2 under clisp

From: Ian Clarkson <[email-masked]>
Date: Tue Apr 9 15:39:07 2002

Dear Dr Haible,

Firstly, thanks for making your very useful language available.

I wish to know whether it is possible to run the theorem-proving system 
ACL2 under clisp. When I tried to do this, I got the following message 
almost immediately:

"We are trying to initialize the parameter that specifies the
file extension name used by the local compiler.  For example, in
Allegro Common Lisp, the extension is "fasl" while in Lucid
it is "lbin" or "sbin".  Files with such extensions are understood
to contain compiled code.  We do not recognize this Common Lisp
from its *features*.  Please type as a STRINGP suitable for READ
its compiled file extension name:

It has to READ as a STRINGP!  Put quotation marks around it:"

(This message originates in the ACL2 source, of course.)

The version of ACL2 (which is the only one I have succeeded in 
obtaining) is 1.9. I obtained it by ftp from dirleton.csres.utexas.edu.

This version of ACL2 works under gcl, but I like clisp better!

I would appreciate your help.

Yours faithfully,

Ian Clarkson

---

From: Sam Steingold <[email-masked]>
Date: Tue Apr 9 17:55:24 2002

> * In message <[email-masked]>
> * On the subject of "[clisp-list] Running ACL2 under clisp"
> * Sent on Wed, 10 Apr 2002 08:38:49 +1000
> * Honorable Ian Clarkson <[email-masked]> writes:
>
> I wish to know whether it is possible to run the theorem-proving
> system ACL2 under clisp.

ACL2 supports CLISP starting with version 2.6
See <http://www.cs.utexas.edu/users/moore/acl2>

-- 
Sam Steingold (http://www.podval.org/~sds) running RedHat7.2 GNU/Linux
Keep Jerusalem united! <http://www.onejerusalem.org/Petition.asp>
Read, think and remember! <http://www.iris.org.il> <http://www.memri.org/>
Daddy, why doesn't this magnet pick up this floppy disk?

---

From: Marco Antoniotti <[email-masked]>
Date: Wed Apr 10 08:08:29 2002

> From: Ian Clarkson <[email-masked]>
> Reply-To: [email-masked]
> User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:0.9.4) Gecko/20010914
> X-Accept-Language: en-us
> Content-Type: text/plain; charset=us-ascii; format=flowed
> Sender: [email-masked]
> X-BeenThere: [email-masked]
> X-Mailman-Version: 2.0.9-sf.net
> Precedence: bulk
> List-Help: <mailto:[email-masked]?subject=help>
> List-Post: <mailto:[email-masked]>
> List-Subscribe: <https://lists.sourceforge.net/lists/listinfo/clisp-list>,
> 	<mailto:[email-masked]?subject=subscribe>
> List-Id: CLISP user discussion <clisp-list.lists.sourceforge.net>
> List-Unsubscribe: <https://lists.sourceforge.net/lists/listinfo/clisp-list>,
> 	<mailto:[email-masked]?subject=unsubscribe>
> List-Archive: <http://www.geocrawler.com/redir-sf.php3?list=clisp-list>
> X-Original-Date: Wed, 10 Apr 2002 08:38:49 +1000
> Date: Wed, 10 Apr 2002 08:38:49 +1000
> Content-Length: 1214
> 
> Dear Dr Haible,
> 

The problem seems to be with the underlying assumption by the ACL2
writers that the system must run under GCL.  The above error message
is clearly from a pre CLtL2 and ANSI era, where COMPILED-FILE-PATHNAME
gives you the right information.

I bet you could go in the ACL2 code and excise all that initialization
code by replacing it with a call to COMPILED-FILE-PATHNAME or to

     cl.env:compiled-file-extension

from the CL-ENVIRONMENT library in the CLOCC.

In alternanative, you can use the CLOCC "port" package.

Cheers

-- 
Marco Antoniotti ========================================================
NYU Courant Bioinformatics Group        tel. +1 - 212 - 998 3488
719 Broadway 12th Floor                 fax  +1 - 212 - 995 4122
New York, NY 10003, USA                 http://bioinformatics.cat.nyu.edu
                    "Hello New York! We'll do what we can!"
                           Bill Murray in `Ghostbusters'.