[Paco] trace$ing thru simplify-clause resets the trace level

[kazarmy]

After the following commands:

ACL2 !>(include-book "projects/paco/paco" :dir :system)

Summary
Form:  ( INCLUDE-BOOK "projects/paco/paco" ...)
Rules: NIL
Time:  4.85 seconds (prove: 0.00, print: 0.01, other: 4.83)
 "/home/kazarmy/tar/acl2-8.4/books/projects/paco/paco.lisp"
ACL2 !>:paco
 "PACO"
PACO !>(ACL2::TABLE ACL2::THEORY-INVARIANT-TABLE NIL NIL :CLEAR)  ; Crude workaround for #1380

Summary
Form:  ( ACL2::TABLE ACL2::THEORY-INVARIANT-TABLE ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 ACL2::THEORY-INVARIANT-TABLE
PACO !>(acl2::trace$ defthm-fn
              (prove :entry (list 'PROVE term)
                     :exit (list 'PROVE (access proof-attempt (car acl2::values) :output-signal)))
              (apply-waterfall-process
               :entry (list 'APPLY-WATERFALL-PROCESS process cl hist)
               :exit (append '(APPLY-WATERFALL-PROCESS)
                             (acl2::take (if (eq (car acl2::values) 'HIT) 2 1) acl2::values))))
 ((DEFTHM-FN)
  (PROVE :ENTRY (LIST 'PROVE TERM)
         :EXIT (LIST 'PROVE
                     (ACCESS PROOF-ATTEMPT (CAR COMMON-LISP::VALUES)
                             :OUTPUT-SIGNAL)))
  (APPLY-WATERFALL-PROCESS
       :ENTRY (LIST 'APPLY-WATERFALL-PROCESS
                    PROCESS CL HIST)
       :EXIT (APPEND '(APPLY-WATERFALL-PROCESS)
                     (ACL2::TAKE (IF (EQ (CAR COMMON-LISP::VALUES) 'HIT)
                                     2 1)
                                 COMMON-LISP::VALUES))))

the tracing output is a bit strange:

PACO !>(dthm true t :rule-classes nil)
1> (ACL2_*1*_PACO::DEFTHM-FN TRUE
                             T 10 ACL2::|*the-live-state*| NIL NIL)
  2> (DEFTHM-FN TRUE
                T 10 ACL2::|*the-live-state*| NIL NIL)

Computing and transferring the ACL2 environment to Paco...

Done.
    3> (PROVE 'T)
      4> (APPLY-WATERFALL-PROCESS APPLY-HINTS-CLAUSE ('T)
                                  NIL)
      <4 (APPLY-WATERFALL-PROCESS MISS)
      4> (APPLY-WATERFALL-PROCESS SIMPLIFY-CLAUSE ('T)
                                  NIL)
Subgoal NIL
'T
Simplify to produce 0 goals.

                  <0 (APPLY-WATERFALL-PROCESS HIT NIL)
(SUMMARY)
                  <0 (PROVE HIT)

Summary
Form:  ( ACL2::DEFAXIOM TRUE ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
                  <-1 (DEFTHM-FN NIL
          :QED ACL2::|*the-live-state*|)
                  <-2 (ACL2_*1*_PACO::DEFTHM-FN NIL
                       :QED ACL2::|*the-live-state*|)
 :QED

specifically the trace level goes to 0 here:

      4> (APPLY-WATERFALL-PROCESS SIMPLIFY-CLAUSE ('T)
                                  NIL)
Subgoal NIL
'T
Simplify to produce 0 goals.

                  <0 (APPLY-WATERFALL-PROCESS HIT NIL)
(SUMMARY)
                  <0 (PROVE HIT)

and then after that it heads into negative territory.

This is apparently not a significant problem but curious to know what's causing it.

[kazarmy]

This is with ACL2 8.4.

[MattKaufmann]

That's a good question, and I don't have an answer. I see though that the macro (file books/projects/paco/output-module.lisp), which is called in the code for apply-waterfall-process (file books/projects/paco/prove.lisp), invokes the wormhole macro, and there are many calls of wormhole-eval in output-module.lisp as well. Wormholes are strange tricky things, and it wouldn't surprise me if they interact oddly with tracing.

I'll put this on my list of things to investigate, but I don't expect to get to it any time soon unless perhaps I'm told that it's causing significant problems. If anyone else cares to tackle this, they should contact me and we can coordinate.

[kazarmy]

The problem appears to be that ld-fn sets *trace-level* to 0, and this happens to be a global variable of the underlying Lisp implementation. I have a fix for this that involves redefining wormhole1, and will email you the patch hopefully before the weekend ends.

[MattKaufmann]

Good catch! It will be interesting to see your proposed patch (no hurry). Thanks!

[MattKaufmann]

Below is another way that the resetting of trace-level by ld-fn is causing bad behavior due to a wormhole. Notice that just under :go, the trace-level is 1 instead of 4. I expect a fix will go into github master today.

ACL2 !>:monitor! (:definition binary-append) t
 T
ACL2 !>(trace$ (rewrite :entry (list 'rewrite term) :exit (cadr values)))
 ((REWRITE :ENTRY (LIST 'REWRITE TERM)
       :EXIT (CADR VALUES)))
ACL2 !>(thm (equal (append (append x y) z) (append x y z)))
1> (REWRITE (EQUAL (BINARY-APPEND (BINARY-APPEND X Y) Z)
	       (BINARY-APPEND X (BINARY-APPEND Y Z))))
  2> (REWRITE (BINARY-APPEND (BINARY-APPEND X Y) Z))
3> (REWRITE (BINARY-APPEND X Y))
  4> (REWRITE X)
  <4 X
  4> (REWRITE Y)
  <4 Y

(1 Breaking (:DEFINITION BINARY-APPEND) on (BINARY-APPEND X Y):
1 ACL2 >:go
1> (REWRITE (IF (CONSP X)
	    (CONS (CAR X) (BINARY-APPEND (CDR X) Y))
	    Y))
  2> (REWRITE X)
  <2 X
  2> (REWRITE (CONS (CAR X)
		(BINARY-APPEND (CDR X) Y)))
3> (REWRITE (CAR X))
  4> (REWRITE X)
  <4 X
<3 (CAR X)
3> (REWRITE (BINARY-APPEND (CDR X) Y))
  4> (REWRITE (CDR X))
    5> (REWRITE X)
    <5 X
  <4 (CDR X)
  4> (REWRITE Y)
  <4 Y
<3 (BINARY-APPEND (CDR X) Y)
  <2 (CONS (CAR X) (BINARY-APPEND (CDR X) Y))
  2> (REWRITE Y)
  <2 Y
<1 (IF (CONSP X)
   (CONS (CAR X) (BINARY-APPEND (CDR X) Y))
   Y)

1x (:DEFINITION BINARY-APPEND) failed because the :REWRITTEN-RHS is
judged heuristically unattractive.
1)
	      <0 (BINARY-APPEND X Y)
	      0> (REWRITE Z)
	      <0 Z

(1 Breaking (:DEFINITION BINARY-APPEND) on 
(BINARY-APPEND (BINARY-APPEND X Y) Z):
1 ACL2 >

[MattKaufmann]

I think this issue is settled by my recent push to github master (4862383), but I'll leave it to @kazarmy to close it.

[kazarmy]

Thanks for the fix!