[acl2/acl2] 9b3a40: Made improvements associated with iprinting, espec...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 9b3a40c1035c1272adea4c9b5543401e3e4de09f
https://github.com/acl2/acl2/commit/9b3a40c1035c1272adea4c9b5543401e3e4de09f
Author: Matt Kaufmann <kauf...@Matts-MBP.attlocal.net>
Date: 2016-07-23 (Sat, 23 Jul 2016)

Changed paths:
M acl2-fns.lisp
M acl2.lisp
M axioms.lisp
M basis-a.lisp
M basis-b.lisp
M books/system/doc/acl2-doc.lisp
M history-management.lisp
M hons-raw.lisp
M hons.lisp
M interface-raw.lisp
M ld.lisp
M other-events.lisp

Log Message:
-----------
Made improvements associated with iprinting, especially new set-iprint keyword, :share; included as a technical improvement is changing the order in *acl2-files*.

Quoting :doc note-7-3:

The iprinting utility has a new keyword option, :share, which causes
iprint indices to be re-used. See [set-iprint]. Thanks to David
Rager for suggesting such an enhancement.

To evaluate a form (set-iprint t :hard-bound N), ACL2 will first
replace t by :reset-enable. This behavior has been expanded to
apply to (set-iprint nil :hard-bound N) and (set-iprint :same
:hard-bound N) as well: the first argument will be converted to
:reset or :reset-enable. See [set-iprint]. This change fixes a bug
in the interaction between hard-bounds and rollovers. For an
example that formerly exhibited this bug, see a comment about
``hard-bounds and rollovers'' in (defxdoc note-7-3 ...) in
community book books/system/doc/acl2-doc.lisp.

Quoting comments in (defxdoc note-7-3 ...):

; We made some technical changes in the implementation of iprinting. For one,
; we no longer compress iprint-ar when exiting a wormhole, since that array is
; already compressed. More important, we fixed a bug in the interaction
; between hard-bounds and rollovers, as noted in the :doc below. The folowing
; caused a hard Lisp error but now works properly.
;
; (set-evisc-tuple (evisc-tuple 3 3 nil nil) :sites :all :iprint t)
; (set-iprint t :hard-bound 3)
; (set-iprint :same :hard-bound 1000)
; (quote ((a b c d) (a b c d)
; (a b c d) e))
; (quote ((a b c d) (a b c d)
; (a b c d) e))
; ; Hard Lisp error:
; (quote ((a b c d) (a b c d)
; (a b c d) e))

; We changed the order of files in *acl2-files*, so that "hons-raw" comes
; immediately after "hons". We think we have seen inlining of hons-related
; functions with under-the-hood raw Lisp code in a tentative implementation of
; eviscerate-stobjs-top, while implementing the set-iprint :share keyword.

[GitHub]

Branch: refs/heads/testing

[Matt Kaufmann]

Hi, acl2-books list --

I want to call your attention to the new :share option of iprinting,
because I think some of you might find it particularly useful.
Suppose for example we start a session by evaluating these:

(set-iprint t :share t)
(set-evisc-tuple (evisc-tuple 2 2 nil nil) :sites :ld)

Then notice the re-use of iprint indices:

ACL2 !>'(1 (2 3 4 5) 6)
(1 (2 3 . #@1#) . #@2#)
ACL2 !>'(1 (2 3 4 5) 6)
(1 (2 3 . #@1#) . #@2#)
ACL2 !>

So for example, if you run a proof, then do some stuff, and then try
the proof again, then you can get information about equal subterms in
corresponding checkpoints.

I'm tempted to make :share t the default, but I worry a bit about that
because this "iprint sharing" is implemented by hons-copying values
that are elided, and these values might be big, in which case
hons-copy might be slow or use a lot of space. Perhaps only experts
create such big terms and use iprinting, and experts can overcome
defaults; but I'm not quite sure about that, so the default remains
:share nil.

I've updated
http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html
-- so you can see the updated :doc set-iprint there.

-- Matt
> Date: Sat, 23 Jul 2016 17:07:46 -0700
> From: GitHub <nor...@github.com>
> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
>
>
> [1:text/plain Hide]

> --
> --
> ACL2-books help:
> To post new messages: acl2-...@googlegroups.com
> To unsubscribe: acl2-books-...@googlegroups.com
> More options: http://groups.google.com/group/acl2-books?hl=en
>
> ---
> You received this message because you are subscribed to the Google Groups "acl2-books" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[David L. Rager]

Hi Matt,

Very cool! This should help a lot when we have to compare versions of
very large circuits that are fundamentally the same.

Now for your next trick, can you make it dynamically print up to
n-levels deeper, when it determines that there's a shared term within
those n-levels? That'd make compare-windows even more useful! I
expect that to be a different type of solution than what's currently
implemented and probably not worth the time (unless something quick
and clever comes to mind). Though, if it were only a factor of 10 or
100 slower, I can imagine cases where I'd turn it on and use it.

As one potential solution,. I can imagine that preprocessing a term
with an equals consequence to generate a tree that records matches
could be pretty cool.

I can't think of a useful application for this "next trick" outside of
SVex recomposition proofs, so that's even more reason not to worry
about it for now. Maybe during proofs with gag-mode disabled, users
would prefer to hide parts (via iprinting) that aren't changing. It's
kind of like the dynamic diff'ing and matching I did over a decade
ago..., but we don't run ACL2 without gag mode that often these
days....

Thanks,
David

[Matt Kaufmann]

Hi, David --

Please see comments and questions below. Ultimately, it might be most
efficient for you if you don't bother to answer my questions (below)
now, but rather, to use the new capability awhile and then get back to
me (perhaps directly, outside the acl2-books list, though I'm fine
with including anyone who'd like to be in such a thread).

> From: "David L. Rager" <rag...@gmail.com>
> Date: Mon, 25 Jul 2016 19:06:41 -0500
> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
>

> Hi Matt,
>
> Very cool! This should help a lot when we have to compare versions of
> very large circuits that are fundamentally the same.

Excellent.

> Now for your next trick, can you make it dynamically print up to
> n-levels deeper, when it determines that there's a shared term within
> those n-levels? That'd make compare-windows even more useful! I

I don't understand the request. Suppose for example that we evaluate
the following three forms.

(defun make-tree (leaf n)
(declare (type (integer 0 *) n))
(if (zp n)
leaf
(let ((x (make-tree leaf (1- n))))
(cons x x))))

(set-iprint t :share t)
(set-evisc-tuple (evisc-tuple 2 2 nil nil) :sites :ld)

Currently we then have:

ACL2 !>(cons (list (make-tree 'a 10)) '(b c d e f))
((#@1#) B . #@2#)
ACL2 !>(cons (list (make-tree 'a 10)) '(b c d e f))
((#@1#) B . #@2#)
ACL2 !>

Are you saying that you'd like the second #@1 and #@2 replaced to show
more structure, for example? If so, then I don't see why that would
be helpful. If not, it might be best to give me your own concrete
example.

> expect that to be a different type of solution than what's currently
> implemented and probably not worth the time (unless something quick
> and clever comes to mind).

You might be right about "not worth the time". It took me
surprisingly long (almost 16 hours) to add the :share keyword
(including documentation). Perhaps it would be best for you to let me
know when you run into cases with the existing tool where you feel
additional features would be useful to you.

> Though, if it were only a factor of 10 or
> 100 slower, I can imagine cases where I'd turn it on and use it.

Showing me such a case might help me to understand better what you
have in mind.

> As one potential solution,. I can imagine that preprocessing a term
> with an equals consequence to generate a tree that records matches
> could be pretty cool.

Sorry, I didn't understand the three lines just above.

> I can't think of a useful application for this "next trick" outside of
> SVex recomposition proofs, so that's even more reason not to worry
> about it for now. Maybe during proofs with gag-mode disabled, users
> would prefer to hide parts (via iprinting) that aren't changing. It's
> kind of like the dynamic diff'ing and matching I did over a decade
> ago..., but we don't run ACL2 without gag mode that often these
> days....

I continue to believe that in almost all cases, watching an ACL2 proof
evolve is much more of a distraction than it is helpful. In those few
cases where focusing on checkpoints isn't the optimal output, I think
that almost all of those would be cases where large case splits might
be identified by looking at "Splitter note" output.

> Thanks,
> David

Thanks for being a possible early adopter, and even more, thanks for
the original idea!

What I imagined as a typical use of :share t is the following. One
tries a proof -- perhaps, as you mentioned, some SVex recomposition
proof -- and it fails. So you prove some lemmas or change the hints,
and then try again. You might want to know if the lemmas or hints
were effective. By comparing checkpoints in the two proof attempts,
you could see quickly whether your lemmas or hints had any effect.

-- Matt

[Matt Kaufmann]

P.S. Something just occurred to me....

Perhaps you were under the impression that when you invoke set-iprint
with :share t, then every expression encountered that is already
associated with an iprint index is printed using that index. That
might be a good idea, but it's not the case. Consider for example
first evaluating the following two forms, with the ensuing log as
shown.

(set-iprint t :share t)
(set-evisc-tuple (evisc-tuple 2 2 nil nil) :sites :ld)

ACL2 !>'(1 2 3 4 5)
(1 2 . #@1#)
ACL2 !>'(2 3 4 5)
(2 3 . #@2#)
ACL2 !>

Maybe you would have rather seen the following as the second result:

(2 . #@1#)

But the way :share t works is that the usual algorithm applies for
eviscerated printing, except that when a term is to be elided,
and a new iprint index would ordinarily be associated with the
term and printed -- like #@2# in the result above -- then at
that point, ACL2 re-uses an existing iprint index. So continuing
the example above, at the point we would otherwise print the
last three elements of the result, we re-use #@1# instead of
generating (and printing with) a new iprint index, in this case
#@3#:

ACL2 !>'(1 2 3 4 5)
(1 2 . #@1#)
ACL2 !>

If anyone would find the stronger kind of sharing to be useful, I
could look into implementing it; I suspect it would be very easy (not
sure). But maybe it would be good to try the existing version first,
to see if such an enhancement is really of much help.

-- Matt
> Date: Mon, 25 Jul 2016 19:52:32 -0500
> From: Matt Kaufmann <kauf...@cs.utexas.edu>

[Keshav Kini]

On 07/25/2016 10:49 PM, Matt Kaufmann wrote:
> P.S. Something just occurred to me....
>
> Perhaps you were under the impression that when you invoke set-iprint
> with :share t, then every expression encountered that is already
> associated with an iprint index is printed using that index. That
> might be a good idea, but it's not the case.

Just as a datapoint, I had this misconception too :)

-Keshav

[Matt Kaufmann]

Thanks, Keshav. I'm working today on implementing the stronger kind
of sharing, which will probably be invoked with (set-iprint t :share
:eager). As part of that I expect that I'll clarify about the two
kinds of sharing in the :doc.

-- Matt
> From: Keshav Kini <krk...@utexas.edu>
> Organization: University of Texas at Austin
> Date: Tue, 26 Jul 2016 14:28:17 -0500

> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
>

[Keshav Kini]

On 07/26/2016 02:31 PM, Matt Kaufmann wrote:
> Thanks, Keshav. I'm working today on implementing the stronger kind
> of sharing, which will probably be invoked with (set-iprint t :share
> :eager). As part of that I expect that I'll clarify about the two
> kinds of sharing in the :doc.

Cool!

If I may venture to guess what David was looking for -- maybe he wants a
variant of evisc-tuple's print-level, call it shared-print-level, such
that if there exists a shared term within shared-print-level levels from
the top, then iprint will print down to whatever level the shared term
is at, but if such a shared term is not found, iprint will print down to
the normal print-level level instead. Presumably the user would
typically set shared-print-level to be larger than print-level.

But that doesn't seem to make that much sense to me. Suppose you have
print-level set to 5 and shared-print-level set to 15. I imagine that
if you have two terms, foo and bar, which share some value at level,
say, 10, you'd want to use this mechanism in order to see that shared
value printed with the same iprint index in both. But ACL2 will
necessarily print one of these, say foo, before the other. In that
case, the "shared" term won't actually be shared with anything yet, so
iprint will only print down to level 5. Then, even if ACL2 remembers
that value from level 10 in foo when it's reading bar (which would mean
that ACL2 was routinely allocating iprint indices that it never used),
that won't help the user much since the "shared" iprint value will only
ever actually be visible in the output for the second value, bar.

David, any thoughts?

-Keshav

[David L. Rager]

Hi Keshav,

Close!

What I mean is suppose a shared term, foo, is at print-level 10 in the lhs (of an equality) and print-level 11 in the rhs (of an equality).  Then in a dream world, ACL2 would automatically figure out that it "needs" to print to level 10 when printing the lhs and that it "needs" to print to level 11 when printing the rhs.  And then it would elide the shared term via the iprinting-based abbreviation.  Combined with compare-windows, such a feature would make it trivial to browse diffs between terms.

Indeed, as you point out, figuring out what parts are equal and worth hiding/iprinting probably would require some pre-processing.

Best,

David

-Keshav

[Matt Kaufmann]

Hi, David --

Thanks for the clarification, though at this point a bunch of
questions start occurring to me.

1. If the print-level is smaller than 10, would your example not get
special treatment?

2. What happens if a subterm of your shared expression occurs by
itself in the equality at a not-very-deep level?

3. If the print-level is a bit bigger than 11, so that both
occurrences of your expression would be printed today with proper
subterms eviscerated, then do we print the first occurrence
normally and then print the second one the same as the first?
(Probably.)

4. Do we do the same thing for other calls besides equal? How about
calls of equal that aren't at the top level?

Please don't bother answering -- I have a feeling there are lots more
questions where those come from! My real point is that this might be
a big job, so it might be best to wait till you (and others) use the
new utility for awhile so that we can have a better idea just what
sorts of improvements would be both useful and feasible.

I'm almost done with the new :share :eager option, by the way; I hope
to get that pushed to github first thing tomorrow morning after some
overnight testing.

Thanks --
-- Matt

> From: "David L. Rager" <rag...@gmail.com>

> Date: Tue, 26 Jul 2016 15:39:54 -0500

> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
>
>

> [1:text/plain Hide]

> [2:text/html Show]
>