		Search-engine friendly clone of the ACL2 documentation.

Debugging

Prettygoals

Experimental tool for displaying proof goals in a prettier way.

This tool changes how ACL2 prints proof goals to be ``prettier,'' so that you can more quickly read them and understand why ACL2 is stuck.

Note: this is experimental and may change drastically in the future. It is also an unprincipled tool that may screw up your goals. Please use it with caution. Send any feedback on it to Jared Davis.

Usage

Either manually or via your ACL2::ACL2-customization file, do:

(include-book "tools/prettygoals/top" :dir :system)

Subsequent proof goals will now be made prettier. You can also turn this on an off:

(include-book "tools/prettygoals/top" :dir :system)

(defthm foo ...)          ;; proof goals will be pretty

(set-pretty-goals nil)
(defthm bar ...)          ;; proof goals will be ugly

(set-pretty-goals t)
(defthm baz ...)          ;; proof goals will be pretty

Effects

Readable B* Binders for Structure Accessors

Background: macros like std::defaggregate and fty::defprod introduce fancy b* binders that let you refer to accessors using a concise, dot-style notation like mystudent.name in place of the more verbose (student->name mystudent).

ACL2's ``untranslate'' mechanisms don't know about or preserve this syntax, so when you give it a goal like this:

(defthm xx
  (b* (((student x))
       ((airplane y)))
    (concl (list x.name x.age x.major y.wings y.wheels))))

It prints out all the accessors in full, like this:

*** Key checkpoint at the top level: ***

Goal''
(CONCL (LIST (STUDENT->NAME X)
             (STUDENT->AGE X)
             (STUDENT->MAJOR X)
             (AIRPLANE->WINGS Y)
             (AIRPLANE->WHEELS Y)))

Prettygoals reintroduces the b* binders so you instead see:

*** Key checkpoint at the top level: ***

(B* (((STUDENT X)) ((AIRPLANE Y)))
    (CONCL (LIST X.NAME X.AGE X.MAJOR Y.WINGS Y.WHEELS)))

Type Error Warnings

Occasionally you may submit a theorem with a typo, for instance, notice how we are accessing both (student->... x) and (airplane->... x) in the following goal:

(defthm yy
  (concl (list (student->name x)
               (student->age x)
               (airplane->wings x)
               (airplane->wheels y))))

When pretty goals are enabled and you try to access the same structure in different ways, we may be able to notice and add a warning, e.g.,:

*** Key checkpoint at the top level: ***

Goal
(B* (((STUDENT X))
     ((AIRPLANE X))
     ((AIRPLANE Y)))
    "WARNING: type confusion: ((X STUDENT X) (X AIRPLANE X))"
    (CONCL (LIST X.NAME X.AGE X.WINGS Y.WHEELS)))

Simpler Hyps First

Original Motivation

I was working on a proof when I encountered the following subgoal:

(IMPLIES (AND (SIGNED-BYTE-P (BIGBOUND->SIZE BOUND1)
                             (BIGINT->VAL (BIGEVAL ARG1 ENV)))
              (NOT (BIGBOUND->MIN BOUND1))
              (<= (BIGINT->VAL (BIGEVAL ARG1 ENV))
                  (BIGBOUND->MAX BOUND1))
              (SIGNED-BYTE-P (BIGBOUND->SIZE BOUND2)
                             (BIGINT->VAL (BIGEVAL ARG2 ENV)))
              (<= (BIGBOUND->MIN BOUND2)
                  (BIGINT->VAL (BIGEVAL ARG2 ENV)))
              (NOT (BIGBOUND->MAX BOUND2))
              (BIGBOUND->MAX BOUND1)
              (< 0 (BIGBOUND->MAX BOUND1))
              (BIGBOUND->MIN BOUND2)
              (<= 0 (BIGBOUND->MIN BOUND2))
              (<= (+ 1 (BIGBOUND->MAX BOUND1))
                  (BIGBOUND->SIZE BOUND2)))
         (<= (LOGHEAD (BIGINT->VAL (BIGEVAL ARG1 ENV))
                      (BIGINT->VAL (BIGEVAL ARG2 ENV)))
             (+ -1 (ASH 1 (BIGBOUND->SIZE BOUND1)))))

This goal is really messy and annoying. I at least wanted ACL2 to replace things like (bigbound->min bound1) with bound1.min. After doing that, the goal was still a mess because simple things like bound1.max were jammed between complicated goals, which suggested reordering the hypotheses based on how complex they are. The above goal now prints instead as follows, which I think is a lot more pleasant.

(B* (((BIGBOUND BOUND1))
     ((BIGBOUND BOUND2)))
  (IMPLIES (AND BOUND1.MAX BOUND2.MIN (NOT BOUND1.MIN)
                (NOT BOUND2.MAX)
                (< 0 BOUND1.MAX)
                (<= 0 BOUND2.MIN)
                (<= (+ 1 BOUND1.MAX) BOUND2.SIZE)
                (<= BOUND2.MIN
                    (BIGINT->VAL (BIGEVAL ARG2 ENV)))
                (<= (BIGINT->VAL (BIGEVAL ARG1 ENV))
                    BOUND1.MAX)
                (SIGNED-BYTE-P BOUND1.SIZE
                               (BIGINT->VAL (BIGEVAL ARG1 ENV)))
                (SIGNED-BYTE-P BOUND2.SIZE
                               (BIGINT->VAL (BIGEVAL ARG2 ENV))))
           (<= (LOGHEAD (BIGINT->VAL (BIGEVAL ARG1 ENV))
                        (BIGINT->VAL (BIGEVAL ARG2 ENV)))
               (+ -1 (ASH 1 BOUND1.SIZE)))))

There are probably a lot of other ways to improve this. For instance it might be nice to put hyps about related variables close together, or otherwise try to group up the hyps into a sensible order. We could also look for potential typos in variable names, and so on...