[Gcl-devel] Re: Building ACL2

[Camm Maguire]

Greetings, and sorry for the burst of traffic of late.

Looking for a little advice here -- there are now two places where we
intern proxy symbols to hold related functions -- 

1) "setf" functions, (i.e. (defun (setf foo) ...), which is indexed by
   a symbol stored in the 'si::setf-function property of 'foo.

and 

2) the automatic state function conversion for mutually recursive
   functions, not yet in production but hopefully to be automated
   soon.  (i.e. the takr example discussed previously).

The main issue requiring the interned symbol is that I don't see a way
to use an uninterned symbol to name the function, define it, compile
it, and then load it into the held uninterned symbol.  The function
name must be read from the data file, so the symbol will never match
unless it is interned.  THe problem with this, of course, is that when
one redefines the functions, the old interned symbol will hold on the
the old code in the gc.  Is there a better way, or must I find a way
to unintern the proxy symbols on function redefinition?

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