using ACL2 in emacs

From: Kemin Yang
Subject: using ACL2 in emacs
Date: Mon, 31 Mar 2003 18:18:12 +0000
Message-ID: <Pine.GSO.4.50.0303311316350.29546-100000@gaia.cc.gatech.edu>

Can anybody give a step by step directions for using ACL2 in emacs?
Thanks!
kemin

Re: using ACL2 in emacs Matthew Danish
Re: using ACL2 in emacs Peter Seibel
Re: using ACL2 in emacs Eric Marsden

From: Matthew Danish
Subject: Re: using ACL2 in emacs
Date: Mon, 31 Mar 2003 21:44:23 +0000
Message-ID: <20030331164423.A13181@lain.cheme.cmu.edu>

On Mon, Mar 31, 2003 at 01:18:12PM -0500, Kemin Yang wrote:
> Can anybody give a step by step directions for using ACL2 in emacs?
> Thanks!

I can't give you step-by-step directions but I can direct you to a
source of links: http://www.cliki.net/ACL2

Presuming you mean ACL2 as in A Computational Logic for Applicative
Common Lisp.  I do not know what you mean by "in emacs" but I will let
you know that ACL2 is not written in Emacs Lisp.

-- 
; Matthew Danish <·······@andrew.cmu.edu>
; OpenPGP public key: C24B6010 on keyring.debian.org
; Signed or encrypted mail welcome.
; "There is no dark side of the moon really; matter of fact, it's all dark."

From: Peter Seibel
Subject: Re: using ACL2 in emacs
Date: Mon, 31 Mar 2003 21:13:40 +0000
Message-ID: <m3n0jbw8ao.fsf@localhost.localdomain>

Kemin Yang <·····@gaia.cc.gatech.edu> writes:

> Can anybody give a step by step directions for using ACL2 in emacs?

If by ACL you mean Allegro Common Lisp (I'm not sure what the 2 is
about) you have two choices, ILISP[1], a general purpose mode for
interacting with various flavors of Lisp from emacs, or ELI[2],
Franz's own version of the same idea that comes with ACL. In either
case, you should read the fine manual that comes which the software.

-Peter


[1] <http://sourceforge.net/projects/ilisp/>
[2] <http://www.franz.com/support/documentation/6.0/doc/eli.htm>

-- 
Peter Seibel                                      ·····@javamonkey.com

  The intellectual level needed   for  system design is  in  general
  grossly  underestimated. I am  convinced  more than ever that this
  type of work is very difficult and that every effort to do it with
  other than the best people is doomed to either failure or moderate
  success at enormous expense. --Edsger Dijkstra

From: Eric Marsden
Subject: Re: using ACL2 in emacs
Date: Tue, 01 Apr 2003 08:11:44 +0000
Message-ID: <wziwuieab7j.fsf@melbourne.laas.fr>

>>>>> "ky" == Kemin Yang <·····@gaia.cc.gatech.edu> writes:

  ky> Can anybody give a step by step directions for using ACL2 in
  ky> emacs?

there is an emacs directory in the ACL2 distribution that contains a
file named emacs-acl2.el -- this augments shell mode with some
keybindings for interacting with the prover.

There is also some basic support for ACL2 in the Emacs-based
ProofGeneral interface to proof assistants; see

   <URL:http://www.proofgeneral.org/>

-- 
Eric Marsden                          <URL:http://www.laas.fr/~emarsden/>