[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: 2.7.0 ANSI ACL2, fyi
From: |
Camm Maguire |
Subject: |
[Gcl-devel] Re: 2.7.0 ANSI ACL2, fyi |
Date: |
09 Aug 2005 01:52:08 -0400 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
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