> 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.