[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
cmulisp and Nqthm
This note is a report on the use of Nqthm (the Boyer-Moore prover)
under the beta release of cmulisp, a public domain Common Lisp that
has recently been released. I wanted to see what would happen
compiling the now 3-years-old, released Nqthm sources under cmulisp,
which incorporates some CLTL2 features. (cmulisp may be entirely
CLTL2 compatible for all I know.) Information on how to get cmulisp
may be found at the very end of this message. *HURRAY and THANKS* to
CMU for building and distributing a public domain Common Lisp.
Summary. To happily use Nqthm (the one and only released version, the
one available by anonymous ftp from cli.com) under cmulisp, it
suffices to do the two following extra things:
a. Immediately after each call of (load "nqthm.lisp") (i.e., during
installation, both compilation and loading) execute
(defun provide (x) x)
b. Immediately after each call of (load-nqthm) (i.e., during
loading), execute
(load "allegro-patch.lisp").
If you don't understand when or where you are supposed to execute
(load "nqthm.lisp") or (load-nqthm), see the installation instructions
for Nqthm, either in the users manual (the book "A Computational Logic
Handbook", Boyer and Moore, Academic Press) or the file
installation.guide distributed with the Nqthm sources.
I have only run Nqthm through the first main ``proveall'' in
basic.events, but that's a pretty lengthy test.
** DETAILS worth ignoring **
Here are some detailed reports on the very few dubious matters
encoutered during compilation, which required the foregoing deviations
from the standard Nqthm operating instructions.
** COMPILE-UNCOMPILED-DEFNS **
The line
(COMPILE-FILE FN-FILE)
should really be
(COMPILE-FILE FN-FILE-NAME)
because FN-FILE is a stream, but COMPILE-FILE in cmulisp wants
somethingd else better, e.g., a string or symbol. Some Lisps are
willing to extract the name from a stream, but not cmulisp. This
error has previously raised its head, and is already fixed by the file
allegro-patch.lisp, now distributed with Nqthm. Also, this patch
causes files created by COMPILE-UNCOMPILED-DEFNS to be smashed even if
they exist, as one probably hopes, rather than the ``tender'' default
treatment that cmulisp uses, and which may be the CLTL2 default for
all I know.
** SLOOP problems **
Sloop is Bill Schelter's excellent version of the MIT Loop macro.
Sloop is distributed with Nqthm. Since something like the MIT Loop
macro has become standard with CLTL2/ANSI, perhaps eventually we
should cause Nqthm to use the default LOOP. But to retain CLTL1
compatibility, or even consistent Nqthm behavior, that may be a bad
idea.
For all I know, these problems are solved in later versions of sloop.
** PROVIDE is a function that is flushed by CLTL2 and presumably the
final ANSI standard. A call to PROVIDE is found in the file
sloop.lisp distributed with Nqthm. One possible fix is just to delete
the line that contains the call to PROVIDE. This would retain CLTL1
compatibility. However, I have suggested the silly idea of doing a
(defun provide (x) nil) in my instructions above just to avoid anyone
having to commit the venial sin of violating Schelter's prohibition
against changing the sloop.lisp sources.
** Here are some presumably inconsequential sloop compilation errors.
In: DEFUN MAKE-NEW-NAME
(ITERATE FOR I FROM 1 ...)
--> SLOOP:SLOOP LET MACROLET BLOCK
==>
(TAGBODY
SLOOP::NEXT-LOOP (OR (NULL #) (SLOOP:LOCAL-FINISH))
NIL
(OR (< I 536870910) (TYPE-ERROR)) ...)
Error: Repeated tagbody tag: NIL.
In: DEFUN MAKE-NEW-NAME
(ITERATE FOR I FROM 1 ...)
--> SLOOP:SLOOP LET MACROLET BLOCK
==>
(TAGBODY
SLOOP::NEXT-LOOP (OR (NULL #) (SLOOP:LOCAL-FINISH))
NIL
(OR (< I 536870910) (TYPE-ERROR)) ...)
Error: Repeated tagbody tag: NIL.
** Long Term Package Issue **
A long term Nqthm/CLTL2 issue, is the USER package. (Damn packages,
they always get you.) Apparently, the official user package for ANSI
Common Lisp will be COMMON-LISP-USER. In the meantime, for a long
time, I think that CLTL2/CLTL1 compatible systems such as cmulisp will
continue to provide the good old USER package. But if this should
stop, a possible fix is to replace all instances of USER as a package
name with COMMON-LISP-USER. But this would lose CLTL1 compatibility.
Probably a better, because simpler fix, is before loading nqthm.lisp
to check that if the package USER does not exist then it is created,
``using'' COMMON-LISP. Anyway, this is not currently a cmulisp
problem.
** CMU Lisp announcement **
From: ram+@cs.cmu.edu
Subject: Re: Beta release of SunOS/SPARC CMU Common Lisp
Newsgroups: comp.lang.lisp
>This message announces a general beta release of CMU Common Lisp for
>SPARCstation or Sun4 machines running SunOS. The rest of this message
>is derived from the cmucl(1) man page and README file.
>
> Robert A. MacLachlan (ram@cs.cmu.edu)
>________________________________________________________________________
>
>Sun Release 4.1 1
>
>CMUCL(1) USER COMMANDS CMUCL(1)
>
>NAME
> CMU Common Lisp
>
>DESCRIPTION
> CMU Common Lisp is public domain "industrial strength" Com-
> mon Lisp programming environment. Many of the X3j13 changes
> have been incorporated into CMU CL. Wherever possible, this
> has been done so as to transparently allow use of either
> CLtL1 or proposed ANSI CL. Probably the new features most
> interesting to users are SETF functions, LOOP and the WITH-
> COMPILATION-UNIT macro.
>
>HARDWARE REQUIREMENTS
> CMU CL is currently available for Sparcstations and DECsta-
> tions (pmaxes) running Mach (or OSF/1). We are beta-testing
> a SunOS SPARC version and an IBM RT Mach version. At least
> 16 megabytes of memory and 25 megabytes of disk space are
> recommended. As usual, more is better.
>
>SUPPORT
> Bug reports should be sent to cmucl-bugs@cs.cmu.edu. Please
> consult your local CMU CL maintainer or Common Lisp expert
> to verify that the problem really is a bug before sending to
> this list.
>
> We have insufficient staffing to provide extensive support
> to people outside of CMU. We are looking for university and
> industrial affiliates to help us with porting and mainte-
> nance for hardware and software that is not widely used at
> CMU.
>
>OVERVIEW
> When compared other Common Lisp implementations (such as
> Allegro), CMU CL has two broad advantages:
>
> -- The new CMU CL compiler (Python) is more sophisticated
> than other Common Lisp compilers. It both produces
> better code and is easier to use.
>
> -- The programming environment based on the Hemlock editor
> is better integrated than gnu-emacs based environments.
> (Though you can still use GNU if you want.)
>
> CMU CL also has significant non-technical advantages:
>
> -- It has good local support for CMU users, and is well
> integrated with the CMU CS environment.
>
> -- It is public domain, and is freely available to non-CMU
> sites that aren't able to afford a site-license for a
> commercial Lisp.
>
>COMPILER FEATURES
> The `Advanced Compiler' chapter of the User's manual exten-
> sively discusses Python's optimization capabilities (See
> DOCUMENTATION below.) Here are a few high points:
>
> -- Good efficiency and type-checking at the same time. Com-
> piling code safe gives a 2x speed reduction at worst.
>
> -- In safe code, type declarations are verified, allowing
> declarations to be debugged in safe code. When you go to
> compile unsafe, you know the declarations are right.
>
> -- Full source level debugging of compiled code, including
> display of the exact call that got an error.
>
> -- Good efficiency notes that tell you why an operation
> can't be open coded or where you are number-consing, and
> that provide unprecedented source context
>
> -- Block compilation, partial evaluation, lightweight func-
> tions and proper tail-recursion allow low-cost use of
> function call abstraction.
>
>___________________________________________________________________________
>
>This software is "as is", and has no warranty of any kind. CMU and the
>authors assume no responsibility for the consequences of any use of this
>software.
>
>This is a general beta release, meaning that anyone can FTP it, but we won't
>be very sympathetic about catastrophes resulting from your dependence on CMU
>CL. After the bug reports die down, we will announce a full release, and will
>then try to be sympathetic toward desperate users.
>
>See "man cmucl" (man/cmucl.1) for other general information.
>
>Distribution:
>
>CMU Common Lisp is only available via anonymous FTP. We don't have the
>manpower to make tapes. All of our files are in the AFS file system. Here
>are some suggested gateway machines:
> lisp-rt1.slisp.cs.cmu.edu
> lisp-rt2.slisp.cs.cmu.edu
>
>Log in with the user "anonymous" and your real userid as password. Due to the
>way anonymous FTP access control is done, it is important to "cd" to the
>source directory with a single command, and then do a "get" operation. If you
>have any trouble with FTP access, please send mail to slisp@cs.cmu.edu.
>
>The binary release area is /afs/cs.cmu.edu/project/clisp/release. This
>directory holds compressed tar files with names of the form:
> <version>-<machine>_<os>.tar.Z
>
>FTP compressed tar archives in binary mode. To extract, "cd" to the
>directory that is to be the root of the tree, then type:
> uncompress <file.tar.Z | tar xf - .
>
>The latest SunOS Sparc release is:
> 15a-sun4c_41.tar.Z
>This tar file is 10 megabytes, and the resulting tree is 23 megabytes.
>
>Major release announcements will be made to comp.lang.lisp until there is
>enough volume to warrant a comp.lang.lisp.cmu.
>
>SunOS credit:
>
>The SunOS support was written by Miles Bader and Ted Dunning.
>
>SPARC Notes:
>
>We have not done any SPARC-specific tuning yet. Performance will improve from
>10-30% when we add instruction scheduling and register windows.
>
>Source availability:
>
>Lisp and documentation sources are available via anonymous FTP. [See the
>README file.] All CMU written code is public domain, but CMU CL also makes
>use of several imported packages: PCL, CLX and XP. Although these packages
>are copyrighted, they may be freely distributed without any licensing
>agreement or fee.