[Gcl-devel] Re: 2.7.0

[Camm Maguire]

Greetings, and thanks as always! Should be fixed now.

I'd dearly love to dispense with this nested algorithm in favor of a
single pass if I could figure out how to do it.  Right now, the
exponential behavior is capped via the variable compiler::*dlbsrl*,
and you can see the effects on compile time via

(in-package 'compiler)
        (push :acl2-mv-as-values *features*)
        (push :CLTL2 *features*)
        (setq *features* (remove :ansi-cl *features*))
        (time (let ((*dlbsrl* 0)) ; set this to 0 1 2 ...
                (load "init.lisp")
                (funcall (find-symbol "COMPILE-ACL2" (find-package "ACL2")))))

Currently the default is 2, but we'd get full benefit at 0.  Soon
(hopefully), we will benefit from higher values as follows:

; i Autodeclared as long-float at *dlbsrl* 0
(let ((i 1.0))
    (setq i (* i 2))) ;or any other mod preserving type

; i Autodeclared as long-float at *dlbsrl* 1
(let ((i 1.0))
    (let ((v i))    ; or any other long-float binding depending on i
            (setq i (* v 2))) ;or any other mod preserving type

; i Autodeclared as long-float at *dlbsrl* 2
(let ((i 1.0))
    (let ((v i))    ; or any other long-float binding depending on i
            (let ((k v))    ; or any other long-float binding depending on v
                    (setq i (* k 2))) ;or any other mod preserving type

Right now, only constant bindings are autodeclared, though this is
easily remedied.

The nesting works like this: process the let form in trial mode, then
if the type is discernible, declare it and process it for real.  This
is exponential with base 2.

A one pass algorithm might look like this:

 option a) declare all let bindings according to their init form, and
 when an inconsistent setq is found, throw back to a catch set at the
 beginning of the let.

 option b) collect a set of functions expressing the type dependencies
 as the let is processed.  When an inconsistent setq is found, fire
 the functions resetting the var types until completion.  

Both of these are for simple flow of control and need come
modification in the presence of go tags and catch forms.

Here are the compile timings for acl2 with mv in features:

*dlbsrl* 0
real time       :    216.520 secs
run-gbc time    :     13.730 secs
child run time  :    198.350 secs
gbc time        :      3.150 secs

*dlbsrl* 1
real time       :    238.800 secs
run-gbc time    :     30.000 secs
child run time  :    197.970 secs
gbc time        :      9.290 secs

*dlbsrl* 2
real time       :    394.390 secs
run-gbc time    :    121.860 secs
child run time  :    239.260 secs
gbc time        :     31.470 secs


Suggestions as always most welcome.

BTW, if you discover any function showing the nqthm slowdown, I'd be
most interested.

Take care,
 


Robert Boyer <address@hidden> writes:

> > If you have a moment and can pin it down to a function
> > (maybe trace compiler::t1defun...), that would be helpful
> 
> It is the compilation of the function INCLUDE-BOOK-FN in the file
> other-events.lisp that is the problem.  Just runs forever.
> 
> Bob
> 
> You can see a 4mb transcript at
> 
>    http://www.cs.utexas.edu/users/boyer/foo.text
> 
> It smells just like the problem that was making eternal the compilation of
> CHK-ACCEPTABLE-DEFUNS in defuns.lisp.
> 
> That transcript includes all that one needs to get to the bug or problem,
> starting with a wget.
> 
> Bob
> 
> 
> 
> 

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