Re: [Gcl-devel] Re: GCL profiling with ACL2

[Camm Maguire]

Greetings!

OK, just made a moderately large commit to 2.6.7pre implementing
unique init names.  Please test as thoroughly as possible.  If you
have any suggestions as to the name formats, these are also welcome. 

Will prepare same for cvs head shortly.

Take care,

<address@hidden> writes:

> Camm Maguire <address@hidden> wrote:
> > Greetings!  GCL carries around its own modules in libgcl.a for use in
> > compiler::link and the like.  Using an absolute pathname for these
> > modules makes no sense, as they will be extracted from the archive in
> > the current directory.  I propose reserving the designator "gcl_" at
> > the start of the pathname-name to indicate that truename init-names
> > are not to be used.  The rest of the namespace would belong to the
> > user and write the full pathname of the source in the initname.
> > I.e. this will fail if the user has two files identically named
> > gcl_.... at two distinct locations in their source tree.  Does this
> > sound acceptable?
> Camm,
> The general idea sounds OK to me -- I don't see any files so named in our 
> code base, nor in the ACL2 2.9.2 distribution.
> Thanks,
> David Hardin

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