[Gcl-devel] Re: acl2 && 2.7.0

[Camm Maguire]

Greetings, and thank you so much again!  Bingo.  Compile is proceeding
now.  Will let you know if I have problems with the regression.

Take care,

Matt Kaufmann <address@hidden> writes:

> Hi --
> 
> I think I see where the bug probably lies.  Below is an abbreviated
> version of that definition that may give you a clue -- see "OUCH".
> 
> (defun raw-ev-fncall (fn args latches hard-error-returns-nilp)
>   (the #+acl2-mv-as-values (values t t t)
>        #-acl2-mv-as-values t
>        (let* ((w (w *the-live-state*))
>               (throw-raw-ev-fncall-flg t)
>               (*1*fn (*1*-symbol fn))
>               (applied-fn [comes out to *1*fn])
>               [uninteresting binding]
>               (val (catch 'raw-ev-fncall
>                      [omitted stuff]
>                      (prog1
>                          [basically, (apply applied-fn args)]
>                        (setq throw-raw-ev-fncall-flg nil))))
>               (w (w *the-live-state*)))
>          (cond
>           (throw-raw-ev-fncall-flg ;;; OUCH -- erroneously non-nil???
>            (mv t (ev-fncall-msg val w) latches))
>           (t [non-error case])))))
> 
> I've written a much longer reply with a lot of background info and a
> tracing suggestion.  Let me know if you'd like me to clean it up a bit
> and send it along.  But based on the backtrace, I'm reasonably
> confident that throw-raw-ev-fncall-flg is getting the wrong value
> above.  A less likely possibility is that the (apply applied-fn args)
> above is doing a throw to 'raw-ev-fncall, but that seems impossible
> unless the compilation has gone completely goofy for this:
> 
> (defun-*1* cons (x y)
>   (cons x y))
> 
> I'll explain if you like, but if I say any more it will probably be
> just a distraction.
> 
> -- Matt
>    From: Camm Maguire <address@hidden>
>    Date: Wed, 03 Sep 2008 18:55:20 -0400
>    X-SpamAssassin-Status: No, hits=-2.6 required=5.0
>    X-UTCS-Spam-Status: No, hits=-152 required=165
> 
>    Greetings!  That helped a lot, and revealed a subtle compiler bug, now
>    fixed.  Now I'm at:
> 
> 
>    HARD ACL2 ERROR in RAW-EV-FNCALL:  An unrecognized value, ("ACL2"),
>    was thrown to 'raw-ev-fncall.  To debug see :DOC print-gv, see :DOC
>    trace, and see :DOC wet.
> 
> 
>    Error: ERROR "The tag RAW-EV-FNCALL is undefined."
>    Signalled by THROW-RAW-EV-FNCALL.
> 
>    Raw Lisp Break.
>    ERROR "The tag RAW-EV-FNCALL is undefined."
> 
>    Broken at THROW-RAW-EV-FNCALL.  Type :H for Help.
>    ACL2>>:bt
> 
>    #0   THROW-RAW-EV-FNCALL {loc0=illegal,loc1=raw-ev-fncall} [ihs=30]
>    #1   HARD-ERROR {loc0=raw-ev-fncall,loc1="An unrecognized value, ~x0, was 
> thrown to 'raw-ev-fnca...} [ihs=29]
>    #2   ILLEGAL {loc0=raw-ev-fncall,loc1="An unrecognized value, ~x0, was 
> thrown to 'raw-ev-fnca...} [ihs=28]
>    #3   EV-FNCALL-MSG {loc0=("ACL2"),loc1=((command-landmark global-value 0 
> ...) (event-landmark globa...} [ihs=27]
>    #4   RAW-EV-FNCALL {loc0=cons,loc1=("ACL2" nil),loc2=nil,loc3=nil} [ihs=26]
>    #5   EV-FNCALL-REC {loc0=cons,loc1=("ACL2" nil),loc2=((command-landmark 
> global-value 0 ...) (event-...} [ihs=25]
>    #6   EV-REC {loc0=(cons str (quote nil)),loc1=((str . 
> "ACL2")),loc2=((command-landmark globa...} [ihs=24]
>    #7   EV-REC-LST {loc0=((cons str (quote nil))),loc1=((str . 
> "ACL2")),loc2=((command-landmark glo...} [ihs=23]
>    #8   EV-REC-LST {loc0=((quote quote) (cons str (quote nil))),loc1=((str . 
> "ACL2")),loc2=((comman...} [ihs=22]
>    #9   EV-REC {loc0=(cons (quote quote) (cons str (quote nil))),loc1=((str . 
> "ACL2")),loc2=((c...} [ihs=21]
>    #10   EV-REC-LST {loc0=((cons (quote quote) (cons str #1=#)) (cons (quote 
> state) #1#)),loc1=((str...} [ihs=20]
>    #11   EV-REC {loc0=(cons (cons (quote quote) (cons str #1=#)) (cons (quote 
> state) #1#)),loc1=...} [ihs=19]
>    #12   EV-REC-LST {loc0=((cons (cons # #) (cons # #1=#))),loc1=((str . 
> "ACL2")),loc2=((command-lan...} [ihs=18]
>    #13   EV-REC-LST {loc0=((quote in-package-fn) (cons (cons # #) (cons # 
> #1=#))),loc1=((str . "ACL2...} [ihs=17]
>    #14   EV-REC {loc0=(cons (quote in-package-fn) (cons (cons # #) (cons # 
> #1=#))),loc1=((str . ...} [ihs=16]
>    #15   EV {loc0=(cons (quote in-package-fn) (cons (cons # #) (cons # 
> #1=#))),loc1=((str . ...} [ihs=15]
>    #16   MACROEXPAND1 {loc0=(in-package 
> "ACL2"),loc1=top-level,loc2=acl2_invisible::|The Live State It...} [ihs=14]
>    #17   TRANSLATE11 {loc0=(in-package 
> "ACL2"),loc1=:stobjs-out,loc2=((:stobjs-out . :stobjs-out)),lo...} [ihs=13]
>    #18   TRANSLATE1 {state=(in-package 
> "ACL2"),loc1=:stobjs-out,loc2=((:stobjs-out . :stobjs-out)),l...} [ihs=12]
>    #19   TRANS-EVAL {loc0=(in-package 
> "ACL2"),loc1=top-level,loc2=acl2_invisible::|The Live State It...} [ihs=11]
>    #20   LD-READ-EVAL-PRINT {loc0=acl2_invisible::|The Live State 
> Itself|,loc1=(acl2_invisible::|The Live St...} [ihs=10]
>    #21   LD-LOOP {loc0=acl2_invisible::|The Live State Itself|} [ihs=9]
>    #22   LD-FN-BODY {loc0=((in-package "ACL2") (defconst 
> *common-lisp-symbols-from-main-lisp-package...} [ihs=8]
>    #23   LD-FN {loc0=((standard-oi (in-package "ACL2") (defconst 
> *common-lisp-symbols-from-main...} [ihs=7]
>    #24   INITIALIZE-ACL2 
> {pass-2-ld-skip-proofsp=include-book,acl2-pass-2-files=("axioms" 
> "hons"),distrib...} [ihs=6]
>    #25   EVAL {loc0=nil,loc1=nil,loc2=nil,loc3=#<compiled-function 
> initialize-acl2>} [ihs=5]
>    #26   EVAL {loc0=(initialize-acl2 (quote include-book) 
> *acl2-pass-2-files*),loc1=(initializ...} [ihs=4]
>    #27   SAVE-ACL2 {loc0=((do-not-save-gcl nil) (other-info "saved_acl2") 
> (mode (initialize-acl2 # ...} [ihs=3]
>    #28   EVAL {loc0=nil,loc1=nil,loc2=nil,loc3=#<interpreted-function 
> (lisp:lambda-block save-...} [ihs=2]
>    ACL2>>wisdom.m.enhanced.com:~$ 
> 
>    Suggestions?
> 
>    Take care,
> 
>    Matt Kaufmann <address@hidden> writes:
> 
>    > Wow -- that's an odd one.  I'll say what I can think of and maybe it
>    > will help... feel free to query further.
>    >
>    > I see this in axioms.lisp, which should have the effect that
>    > (f-get-global 'ld-level *the-live-state*) is 0 -- it can go up and
>    > down after that, but should never be nil.
>    >
>    > #-acl2-loop-only
>    > (dolist (pair *initial-global-table*)
>    >         (f-put-global (car pair) (cdr pair) *the-live-state*))
>    >
>    > In your email though you say (f-get-global 'ld-level) -- probably you
>    > just omitted the second (state, or *the-live-state*) argument, but if
>    > something f-get-global is called on one argument, that's certainly
>    > wrong.  (But I don't see that in the sources.)
>    >
>    > By the way, we call such variables "state globals" -- notice:
>    >
>    >   ACL2>(macroexpand '(f-get-global 'ld-level *the-live-state*))
>    >
>    >   (LET ()
>    >     (DECLARE (SPECIAL ACL2_GLOBAL_ACL2::LD-LEVEL))
>    >     ACL2_GLOBAL_ACL2::LD-LEVEL)
>    >   T
>    >
>    >   ACL2>
>    >
>    > If you can reproduce the error on the UT CS file system and would like
>    > me to poke around trying to do the build and trying to see how
>    > ld-level could possibly be nil, I'd be willing to give it a try.
>    >
>    > Or, if you just send me the entire log, maybe something will occur to
>    > me.  The key though is probably to figure out how state global
>    > 'ld-level, i.e. special variable ACL2_GLOBAL_ACL2::LD-LEVEL, could
>    > have value nil -- hard to imagine how that could happen.  Maybe you
>    > could set a watch point for that in gdb somehow?  Notice by the way
>    > that this is a different variable than *ld-level*, which however
>    > should also never be nil.
>    >
>    > -- Matt
>    >    From: Camm Maguire <address@hidden>
>    >    Date: Mon, 01 Sep 2008 13:55:10 -0400
>    >    X-SpamAssassin-Status: No, hits=-2.6 required=5.0
>    >    X-UTCS-Spam-Status: No, hits=-112 required=165
>    >
>    >    Greetings!  Just cleaning up a few 2.7.0 bugs revealed in the acl2
>    >    build.  Do you have a suggestion for chasing down the following?
>    >
>    >    After this point:
>    >
>    >    ACL2 loading 
>    >    '((IN-PACKAGE "ACL2")
>    >      (DEFCONST *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*
>    >         '(&ALLOW-OTHER-KEYS *PRINT-MISER-WIDTH*
>    >                             &AUX *PRINT-PPRINT-DISPATCH*
>    >                             &BODY *PRINT-PRETTY* &ENVIRONMENT ...))
>    >      (DEFCONST
>    >       *ACL2-FILES*
>    >       '("axioms" "hons" "basis" "parallel"
>    >           "translate" "type-set-a" "linear-a" ...)
>    >       "*acl2-files* is the list of all the files necessary to build
>    >    ACL2 from scratch.")
>    >      (DEFCONST *COMMON-LISP-SPECIALS-AND-CONSTANTS*
>    >         '(* ** *** *BREAK-ON-SIGNALS*
>    >             *COMPILE-FILE-PATHNAME*
>    >             *COMPILE-FILE-TRUENAME*
>    >             *COMPILE-PRINT* ...))
>    >      (DEFCONST *STOBJ-INLINE-DECLARE* '(DECLARE #))
>    >      (DEFMACRO MAKE-PACKAGE-ENTRY
>    >         (&KEY NAME IMPORTS HIDDEN-P
>    >               BOOK-PATH DEFPKG-EVENT-FORM TTERM)
>    >         (CONS 'LIST* (CONS NAME #)))
>    >      (DEFMACRO FIND-PACKAGE-ENTRY
>    >         (NAME KNOWN-PACKAGE-ALIST)
>    >         (CONS 'ASSOC-EQUAL (CONS NAME #)))
>    >      ...).
>    >
>    >    I get an error in ld-read-eval-print, as (f-get-global 'ld-level) is
>    >    returning nil, and the call to >= is expecting an integer.  I've
>    >    checked the state, and there is no such flag in the global table.  And
>    >    there is not call to put-global with same save the initial call
>    >    putting 0.  Anyway, if you have some acceleration pointers about where
>    >    to look, I can chase this down.
>    >
>    >    Take care,
>    >
>    >    -- 
>    >    Camm Maguire                                          address@hidden
>    >    
> ==========================================================================
>    >    "The earth is but one country, and mankind its citizens."  --  
> Baha'u'llah
>    >
>    >
>    >
>    >
> 
>    -- 
>    Camm Maguire                                               address@hidden
>    ==========================================================================
>    "The earth is but one country, and mankind its citizens."  --  Baha'u'llah
> 
> 
> 

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