[Top][All Lists]
[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
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Gcl-devel] Re: hi,
Camm Maguire <=