> > 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 _)
> >
> > Would that solve David Hardin's problem, as follows?
> >
>
> Yes. If you'd like, I can post a simple patch achieving these
three
> points.
> > 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.
> >
> > P.P.S. A similar situation exists for the "near+"
files found, for
> > example, in books/rtl/rel4...
> >
Camm,
As you're going about this work, keep in mind that
files in different ACL2 books can have the same simple name, e.g. top.lisp
occurs in several of the distributed ACL2 books. I have been bitten
by this one today in my attempts to perform a COMPILER::LINK made up of
multiple books from many directories.
Thanks again for trying to simplify this whole area
for users -- I think it will pay dividends in the long term.