[Top][All Lists]

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

[Gcl-devel] Re: GCL profiling with ACL2

From: Camm Maguire
Subject: [Gcl-devel] Re: GCL profiling with ACL2
Date: 22 Mar 2005 09:12:16 -0500
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

Greetings!  si::*system-directory* is used in a number of places, all
with the central purpose of trying to find files that should be
present in a GCL installation.  As GCL's general portable design is to
allow images to work where there is no such installation, it might not
make sense for ACL2 to rely on this variable.  If the variable is set,
it is persistent -- if unset it will default to the directory location
of the image if memory serves.  There is also a little utility
si::reset-sys-paths which I use in multi image builds (like axiom) to
make sure the paths are all right even when one moves the image around
to temporary directories and the like.

In general, I think the best way forward is for GCL to:

1) dump the large si::*cmpinclude-string* into every C file when the
   variable is set, which is the case in any default 'saved_' image.
2) Always toggle the init_ name, and expand our currently crude
   translation to ensure that we always come up with a valid C
   identifier.  (Right now, we only translate - to _)
3) Allow lisp init data format to be governed purely by
4) Keep the traditional :system-p behavior for backward compatibility,
   but no longer require it for ld generated images.

If there are no objections, I'll put this into CVS head.

Take care,

<address@hidden> writes:

> Matt Kaufmann <address@hidden> wrote:
> > Camm, David --
> >
> > My apologies for how ACL2 was, I gather, not doing the right thing with 
> > -dir.
> >
> > So, should the saved_acl2 script not include -dir, since without that 
> > setting,
> > the underlying gcl on which ACL2 is built will presumably have the correct
> > value of SI::*SYSTEM-DIRECTORY*?
> Well, deleting the -dir from saved_acl2 sure worked for me, both for 
> certifying the distributed ACL2 books, as well as
> for certifying my own books.  However, I have to wonder why you had decided 
> to include -dir in saved_acl2 to begin with,
> and if some ACL2 developers (maybe even some here at Rockwell Collins ;-) 
> depend on that setting.
> Best Regards,
> David Hardin
> P.S.  In building the distributed books for profiling, I found that having a 
> file named @whatever.lisp (as in
> books/ihs/@logops.lisp) is a bad idea.  In particular, the init function is 
> given the name address@hidden(), which is not
> a legal C identifier.

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]