Greetings! Robert Boyer <[EMAIL PROTECTED]> 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 [EMAIL PROTECTED] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list Gcl-devel@gnu.org http://lists.gnu.org/mailman/listinfo/gcl-devel
