[Gcl-devel] Re: autoproclaiming and tempus fugit

[Camm Maguire]

Greetings!

OK, the preliminary autoproclamation stuff is in -- self-build,
ansi-tests, and maxima work.

Right now, there is a variable compiler::*compiler-auto-proclaim*
which defaults to t which turns this on.  If notes are not suppressed,
a note will be issued indicating the signature that is being
asserted.  In all cases, a warning will be issued if either the arg or
ret types deduced differ from those previously proclaimed as in
sys-proclaim.lisp.  The former override the latter.  If a call is
compiled to a function with no explicit (manual) proclaim  issued
ahead of time, the call will be a low generic call at this moment.  I
am working now on having the subsequent compilation of the callee
trigger a recompile of the caller.

So the upshot is that since acl2 proclaims everything anyway, the
performance should be unchanged.  This infrastructure will open up
performance improvement possibilities in the hopefully near future,
however. 

Please let me know of any problems.

Take care,



Robert Boyer <address@hidden> writes:

> Wonderful to hear of the progress on auto proclaiming.  We
> will be well served by your going with your favorite
> approach.
> 
> Of some minor relevance to COMPILE, there exist Gnu-Linux
> system calls for making guaranteed-to-be-unique temp files.
> There are several possibilities.  For example, 'mktemp'
> exists even as a shell command.
> 
> You will eventually want to use such a facility for
> COMPILE's gazonk-name to get even more reliably unique temp
> files, even in preference to the recent, and much
> appreciated, process id naming in compiler::gazonk-name.
> 
> In a parallel environment, it is possible that the process
> id naming technique will not suffice because of multiple
> processors accessing the same directory from different
> machines while running processes with the same process id.
> One might add some machine identification for uniqueness,
> but this may become harder with multiple cores.  There seems
> to be a better way.
> 
> 'tmpfile' makes a unique temporary file that even disappears
> when the process terminates normally.  (It would be nice to
> be able to have such a stream/file at the GCL level, too.)
> 
> I still don't see how best to solve the problem of temp
> files well because one needs guaranteed unique temp files
> for which the .lisp, .c, .h. .data, .o, and Lord knows what
> other file types, are also unique.  One could create a
> unique temporary directory for all these with 'mktemp' and
> use that for the auxiliary files, but then one would not
> enjoy the feature of tmp files disappearing when the process
> dies that one enjoys with 'tmpfile', which does not seem to
> permit one to create directories rather than files.
> 
> Bob
> 
> 
> 
> 
> 

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