[Gcl-devel] Re: 2.7.0 ANSI ACL2, fyi

[Camm Maguire]

Greetings!

Minor comments here 

1) Yes, please, 2.7.0 cvs tags are for the stout of heart interested
   in helping with testing!  Please keep production work elsewhere if
   possible. 

2) Unless we autoload pcl on demand, using the ansi image will
   definitely bloat acl2 somewhat if it is not needed -- may not make
   a difference though.

3) Beware of the following auto-proclaim pitfall -- if any of your
   functions return a value of form  (funcall (foo)), the sys-proclaim
   mechanism will proclaim (function (...) *), which will disable all
   c stack arg passing into and out of the function at present.  I'm
   occasionally resorting to the ugly workaround of wrapping the above
   in (let ((z (funcall (foo)))) z).

Take care,


Robert Boyer <address@hidden> writes:

> > please let me know
> 
> Here is my advice:  Wait.
> 
> I think that Camm is planning to release a new version of GCL, both ANSI and
> CLTL1, later this summer.  Version 2.8?  After he does, then make double sure
> that ACL2 then builds under that ANSI version.  I really doubt you want to be
> point any random user or sysadmin to 2.7.0 because it changes so very often.
> I think that when I have tried to build GCL under ANSI 2.7.0 some times in
> the past, it has not quit worked, but I know that camm has been doing a lot
> of work on 2.7.0.
> 
> Bob
> 
> P. S.  Have you ever tried Schelter's emit-fn and proclaim-all-files hack on
> ACL2 to see if it might speed up anything?  Probably you've already got
> everything proclaimed that can be proclaimed, but who knows, it might catch
> something.  I think it is a little bit tedious to use, like a multi pass
> compiler.  I think this is how it goes, though I am not much used to it.
> 
> A.  In one GCL, first invoke (compiler::emit-fn t) and then continue the 
> complete
>     compilation of ACL2.  (Generates foo.fn for each foo.o.)
> 
> B.  In a later GCL,
>     a. invoke (compiler::emit-fn t)
>     b. invoke (compiler::make-all-proclaims "*.fn"); 
>           reads all foo.fn and writes sys-proclaim.lisp.
>     c. (load "sys-proclaim.lisp").
>     c. build ACL2, including complete recompilation and saving.
> 
> Bob
> 
> 
> 
> 
> 

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