gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] Re: hi


From: Camm Maguire
Subject: [Gcl-devel] Re: hi
Date: 05 Jun 2006 17:22:42 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

Greetings!

Robert Boyer <address@hidden> writes:

> Sorry for the sluggish reply.  I have been out of town.
> 
> > Bob, I wanted to test nqthm before committing.  Are there
> > any mods needed when using the ansi build?
> 
> None at all.

Great!  giant-test just passed with the new auto recompilation.

> 
> My *very* few ANSI modifications to ACL2 follow.  I previously
> sent you my current mods to GCL 2.7.0 and will be happy to
> resend them if you'd like.

Thank you!  Will try to get these in or equivalent afer I sync my
local tree.

> 
> (As I suspect you know well, Matt is on the verge of
> releasing ACL2 3.0.0, which I have not yet tried in any way,
> I'm most sorry to say.)
> 
> Look forward to any message from you about a 2.7.0 commit.
> 

Your help in testing is always most appreciated.

Take care,

> Bob
> 
> 
> -------------------------------------------------------------------------------
> 
> This is /u/boyer/patch-acl2.el 
> 
> (require 'cl)
> 
> (defun patch-acl2 ()
>   (interactive "")
> 
>   ; Append stuff to init.lisp.
>   (find-file "/u/boyer/acl2/acl2-sources/init.lisp")
>   (widen)
>   (goto-char (point-min))
>   (cond ((not (search-forward "prependage" nil t))
>          (insert-file "/u/boyer/patch-acl2-init.lisp")
>          (goto-char (point-max))
>          (save-buffer 0)))
> 
>   ; Patch tmp-filename in ld.lisp.
>   (find-file "/u/boyer/acl2/acl2-sources/ld.lisp")
>   (widen)
>   (goto-char (point-min))
>   (cond ((not (search-forward ";; Boyer's ld-patch" nil t))
>          (search-forward "(defun tmp-filename (dir suffix)")
>          (beginning-of-line 1)
>          (insert-file "/u/boyer/patch-acl2-ld.lisp")
>          (save-buffer 0)))
> 
> )
> 
> -------------------------------------------------------------------------------
> 
> This is /u/boyer/patch-acl2-init.lisp
> 
> 
> ;; We prepend the following to acl2-sources/init.lisp when
> ;; we make a fresh copy in /u/boyer/acl2/acl2-sources.
> 
> (in-package "CL-USER")
> 
> #+GCL
> (progn
> 
> ;; Merely for more pleasant hacking:
> (setq system::*enable-eval-in-break* t)
> 
> ;; To speed up compilation, in particular to avoid sometimes
> ;; compiling functions merely one at a time:
> 
> (setq user::*fast-acl2-gcl-build* t)
> (setq cl-user::*fast-acl2-gcl-build* t)
> 
> ;; To get ACL2 to do a CLTL2 build for GCL 2.7.0 ANSI:
> ;; The removal is simply to stop ACL2 from explicitly and
> ;; rightly causing an error because GCL 2.6.7 was not ANSI enough.
> 
> (setq *features* (list* :cltl2 :draft-ansi-cl-2 (remove :ansi-cl *features*)))
> 
> ;; Stop acl2-init.lisp from renaming crucial packages.  When
> ;; ACL2 is released for ANSI GCL, it will probably stop the
> ;; renaming it currently does.
> 
> (cond ((not (get 'cl::rename-package :old-def))
>        (setf (get 'cl::rename-package :old-def)
>              (symbol-function 'cl::rename-package))))
> 
> cl::
> (defun rename-package (&rest r)
>   (cond ((or (eq (find-package (car r))
>                  (find-package "COMMON-LISP"))
>              (eq (find-package (car r))
>                  (find-package "LISP")))
>          nil)
>         (t (apply (get 'rename-package :old-def)
>                   r))))
> )
> 
> ; End of prependage.
> 
> 
> 
> -------------------------------------------------------------------------------
> This is /u/boyer/patch-acl2-ld.lisp 
> 
> 
> ;; We insert this into ld.lisp.
> ;; Boyer's ld-patch of tmp-filename:
> 
> #+GCL
> (defun tmp-filename (dir suffix)
>    (declare (ignore dir suffix))
>    (let ((x (open "|/bin/mktemp /tmp/XXXXXX 2>&1 < /dev/null")))
>      (prog1 (read-line x) (close x))))
> 
> ;; End of insertion except for the next line:
> #-GCL
> 
> 
> 

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah




reply via email to

[Prev in Thread] Current Thread [Next in Thread]