Re: Odd behavior with accumulated-persistence and disable
5 views
Skip to first unread message
Matt Kaufmann
Nov 29, 2016, 10:33:13 AM11/29/16
to acl2-...@googlegroups.com
Hi, David --
[Replying here to acl2-books.]
Thanks for highlighting that. Now that the author of the arithmetic-5
books is no longer active in the ACL2 community, I hope that you or
others who are using it will feel free to improve it.
-- Matt
> Authentication-Results: ironmaiden.mail.utexas.edu; dkim=neutral (message not signed) header.i=none
> From: David Hardin <david....@rockwellcollins.com>
> Date: Tue, 29 Nov 2016 09:21:41 -0600
> Cc: ACL2 Help <acl2...@utlists.utexas.edu>
>
>
> [1:text/plain Hide]
>
> Grant,
>
> Thanks for the prompt response. I could've done a grep on the ACL2 sources
> to find boil-that-dustspeck, etc., but I thought that it was worth
> highlighting as a perhaps-less-than-useful warning message. :-)
>
>
> David Hardin
>
>
> On Mon, Nov 28, 2016 at 5:31 PM, Grant Olney Passmore <
> grant.p...@cl.cam.ac.uk> wrote:
>
> > Hi, David --
> >
> > I believe your disabling of BUBBLE-DOWN-+-MATCH-3 is violating an
> > arithmetic-5 theory invariant ( http://www.cs.utexas.edu/
> > users/moore/acl2/v7-2/manual/index.html?topic=ACL2____THEORY-INVARIANT )
> > defined in arithmetic-5/basic-ops/collect.lisp (
> > https://github.com/acl2/acl2/blob/master/books/arithmetic-
> > 5/lib/basic-ops/collect.lisp#L566-L573 ):
> >
> > (theory-invariant
> > (if (active-runep '(:definition boil-that-dustspeck))
> > (and (active-runep '(:rewrite bubble-down-+-bubble-down))
> > (active-runep '(:rewrite bubble-down-+-match-1))
> > (active-runep '(:rewrite bubble-down-+-match-2))
> > (active-runep '(:rewrite bubble-down-+-match-3)))
> > t)
> > :error nil)
> >
> > Since it has :error nil, a warning will be printed if the theory invariant
> > is violated, but an error shouldn't be caused.
> >
> > The (hilarious) definition of boil-that-dustspeck is here:
> > https://github.com/acl2/acl2/blob/master/books/
> > arithmetic-5/lib/basic-ops/we-are-here.lisp#L17-L20
> >
> > As far as I can tell, the rune (:definition boil-that-dustspeck) is only
> > used in arithmetic-5 theory invariants, so there should be no harm for you
> > disabling it if you want to avoid seeing that specific warning.
> >
> > Grant
> >
> > On Mon, Nov 28, 2016 at 11:08 PM David Hardin <
> > david....@rockwellcollins.com> wrote:
> >
> >> I've been using accumulated-persistence as one normally does to speed up
> >> a proof. I like to look at the :frames-f outptut, and disable rules that
> >> are truly useless.
> >>
> >> I came along the following output from (show-accumulated-persistence
> >> :frames-f)
> >> (BTW, I'm using an ACL2 7.2-plus snapshot, (git commit hash:
> >> c94c55ad208dc5ef4fb34253dc30df46f65786ec):
> >>
> >> --------------------------------
> >> 2706 146 ( 18.53) (:REWRITE BUBBLE-DOWN-+-MATCH-3)
> >> 0 0 [useful]
> >> 2706 146 [useless]
> >> --------------------------------
> >>
> >> OK, not a lot of frames -- we're down to the tail end of the list here,
> >> but I was trying to be as lean and mean as possible, so I tried to disable
> >> it:
> >>
> >> (in-theory (disable BUBBLE-DOWN-+-MATCH-3))
> >>
> >>
> >> ACL2 responded with a very odd message:
> >>
> >> ACL2 Warning [Theory]: Theory invariant 12 failed on the theory produced
> >> by the current event. Theory invariant 12 is
> >> (IF (ACTIVE-RUNEP '(:DEFINITION BOIL-THAT-DUSTSPECK))
> >> (AND (ACTIVE-RUNEP '(:REWRITE BUBBLE-DOWN-+-BUBBLE-DOWN))
> >> (ACTIVE-RUNEP '(:REWRITE BUBBLE-DOWN-+-MATCH-1))
> >> (ACTIVE-RUNEP '(:REWRITE BUBBLE-DOWN-+-MATCH-2))
> >> (ACTIVE-RUNEP '(:REWRITE BUBBLE-DOWN-+-MATCH-3)))
> >> T).
> >>
> >>
> >> While I appreciate the Seussian reference, it doesn't help me understand
> >> what's going on here. Keeping this rule enabled doesn't hurt anything --
> >> I'm just curious.
> >>
> >>
> >> David Hardin
> >>
> >>
>
> [2:text/html Show]
>
[Replying here to acl2-books.]
Thanks for highlighting that. Now that the author of the arithmetic-5
books is no longer active in the ACL2 community, I hope that you or
others who are using it will feel free to improve it.
-- Matt
> Authentication-Results: ironmaiden.mail.utexas.edu; dkim=neutral (message not signed) header.i=none
> From: David Hardin <david....@rockwellcollins.com>
> Date: Tue, 29 Nov 2016 09:21:41 -0600
> Cc: ACL2 Help <acl2...@utlists.utexas.edu>
>
>
> [1:text/plain Hide]
>
> Grant,
>
> Thanks for the prompt response. I could've done a grep on the ACL2 sources
> to find boil-that-dustspeck, etc., but I thought that it was worth
> highlighting as a perhaps-less-than-useful warning message. :-)
>
>
> David Hardin
>
>
> On Mon, Nov 28, 2016 at 5:31 PM, Grant Olney Passmore <
> grant.p...@cl.cam.ac.uk> wrote:
>
> > Hi, David --
> >
> > I believe your disabling of BUBBLE-DOWN-+-MATCH-3 is violating an
> > arithmetic-5 theory invariant ( http://www.cs.utexas.edu/
> > users/moore/acl2/v7-2/manual/index.html?topic=ACL2____THEORY-INVARIANT )
> > defined in arithmetic-5/basic-ops/collect.lisp (
> > https://github.com/acl2/acl2/blob/master/books/arithmetic-
> > 5/lib/basic-ops/collect.lisp#L566-L573 ):
> >
> > (theory-invariant
> > (if (active-runep '(:definition boil-that-dustspeck))
> > (and (active-runep '(:rewrite bubble-down-+-bubble-down))
> > (active-runep '(:rewrite bubble-down-+-match-1))
> > (active-runep '(:rewrite bubble-down-+-match-2))
> > (active-runep '(:rewrite bubble-down-+-match-3)))
> > t)
> > :error nil)
> >
> > Since it has :error nil, a warning will be printed if the theory invariant
> > is violated, but an error shouldn't be caused.
> >
> > The (hilarious) definition of boil-that-dustspeck is here:
> > https://github.com/acl2/acl2/blob/master/books/
> > arithmetic-5/lib/basic-ops/we-are-here.lisp#L17-L20
> >
> > As far as I can tell, the rune (:definition boil-that-dustspeck) is only
> > used in arithmetic-5 theory invariants, so there should be no harm for you
> > disabling it if you want to avoid seeing that specific warning.
> >
> > Grant
> >
> > On Mon, Nov 28, 2016 at 11:08 PM David Hardin <
> > david....@rockwellcollins.com> wrote:
> >
> >> I've been using accumulated-persistence as one normally does to speed up
> >> a proof. I like to look at the :frames-f outptut, and disable rules that
> >> are truly useless.
> >>
> >> I came along the following output from (show-accumulated-persistence
> >> :frames-f)
> >> (BTW, I'm using an ACL2 7.2-plus snapshot, (git commit hash:
> >> c94c55ad208dc5ef4fb34253dc30df46f65786ec):
> >>
> >> --------------------------------
> >> 2706 146 ( 18.53) (:REWRITE BUBBLE-DOWN-+-MATCH-3)
> >> 0 0 [useful]
> >> 2706 146 [useless]
> >> --------------------------------
> >>
> >> OK, not a lot of frames -- we're down to the tail end of the list here,
> >> but I was trying to be as lean and mean as possible, so I tried to disable
> >> it:
> >>
> >> (in-theory (disable BUBBLE-DOWN-+-MATCH-3))
> >>
> >>
> >> ACL2 responded with a very odd message:
> >>
> >> ACL2 Warning [Theory]: Theory invariant 12 failed on the theory produced
> >> by the current event. Theory invariant 12 is
> >> (IF (ACTIVE-RUNEP '(:DEFINITION BOIL-THAT-DUSTSPECK))
> >> (AND (ACTIVE-RUNEP '(:REWRITE BUBBLE-DOWN-+-BUBBLE-DOWN))
> >> (ACTIVE-RUNEP '(:REWRITE BUBBLE-DOWN-+-MATCH-1))
> >> (ACTIVE-RUNEP '(:REWRITE BUBBLE-DOWN-+-MATCH-2))
> >> (ACTIVE-RUNEP '(:REWRITE BUBBLE-DOWN-+-MATCH-3)))
> >> T).
> >>
> >>
> >> While I appreciate the Seussian reference, it doesn't help me understand
> >> what's going on here. Keeping this rule enabled doesn't hurt anything --
> >> I'm just curious.
> >>
> >>
> >> David Hardin
> >>
> >>
>
> [2:text/html Show]
>
Keshav Kini
Dec 2, 2016, 2:47:13 PM12/2/16
to acl2-...@googlegroups.com
Hi all,
Since, as Matt pointed out, the author of arithmetic-5 is inactive, I went ahead and changed the name of that definition from boil-that-dustspeck to arith-5-active-flag, similar to David Hardin's suggestion. Hopefully that makes the warning message more enlightening.
Thanks,
Keshav
On Tue, Nov 29, 2016 at 7:33 AM, Matt Kaufmann <kauf...@cs.utexas.edu> wrote:
Hi, David --
[Replying here to acl2-books.]
Thanks for highlighting that. Now that the author of the arithmetic-5
books is no longer active in the ACL2 community, I hope that you or
others who are using it will feel free to improve it.
-- Matt
> Authentication-Results: ironmaiden.mail.utexas.edu; dkim=neutral (message not signed) header.i=none
> From: David Hardin <david.hardin@rockwellcollins.com>
--
--
ACL2-books help:
To post new messages: acl2-...@googlegroups.com
To unsubscribe: acl2-books-unsubscribe@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+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
Matt Kaufmann
Dec 3, 2016, 4:19:22 PM12/3/16
to acl2-...@googlegroups.com
To acl2-books (kind of related to a message I just sent to acl2-help):
In short: clean your books. Details:
I've just pushed a change to github that improves theory-invariant
warnings but changes the shape of a related record in the
implementation. Also, the pushed changes modify *acl2-exports*. For
both of those reasons, you might need to clean all of your books when
updating.
-- Matt
> From: Keshav Kini <krk...@utexas.edu>
> Date: Fri, 2 Dec 2016 11:47:10 -0800
> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
>
>
> [1:text/plain Hide]
> > To unsubscribe: acl2-books-...@googlegroups.com
> To unsubscribe: acl2-books-...@googlegroups.com
> [2:text/html Show]
>
In short: clean your books. Details:
I've just pushed a change to github that improves theory-invariant
warnings but changes the shape of a related record in the
implementation. Also, the pushed changes modify *acl2-exports*. For
both of those reasons, you might need to clean all of your books when
updating.
-- Matt
> From: Keshav Kini <krk...@utexas.edu>
> Date: Fri, 2 Dec 2016 11:47:10 -0800
> Reply-To: acl2-...@googlegroups.com
> Mailing-list: list acl2-...@googlegroups.com; contact acl2-boo...@googlegroups.com
>
>
> [1:text/plain Hide]
>
> Hi all,
>
> Since, as Matt pointed out, the author of arithmetic-5 is inactive, I went
> ahead and changed the name of that definition from boil-that-dustspeck to
> arith-5-active-flag, similar to David Hardin's suggestion. Hopefully that
> makes the warning message more enlightening.
>
> Thanks,
> Keshav
>
>
> On Tue, Nov 29, 2016 at 7:33 AM, Matt Kaufmann <kauf...@cs.utexas.edu>
> wrote:
>
> > Hi, David --
> >
> > [Replying here to acl2-books.]
> >
> > Thanks for highlighting that. Now that the author of the arithmetic-5
> > books is no longer active in the ACL2 community, I hope that you or
> > others who are using it will feel free to improve it.
> >
> > -- Matt
> > > Authentication-Results: ironmaiden.mail.utexas.edu; dkim=neutral
> > (message not signed) header.i=none
> > > From: David Hardin <david....@rockwellcollins.com>
> Hi all,
>
> Since, as Matt pointed out, the author of arithmetic-5 is inactive, I went
> ahead and changed the name of that definition from boil-that-dustspeck to
> arith-5-active-flag, similar to David Hardin's suggestion. Hopefully that
> makes the warning message more enlightening.
>
> Thanks,
> Keshav
>
>
> On Tue, Nov 29, 2016 at 7:33 AM, Matt Kaufmann <kauf...@cs.utexas.edu>
> wrote:
>
> > Hi, David --
> >
> > [Replying here to acl2-books.]
> >
> > Thanks for highlighting that. Now that the author of the arithmetic-5
> > books is no longer active in the ACL2 community, I hope that you or
> > others who are using it will feel free to improve it.
> >
> > -- Matt
> > > Authentication-Results: ironmaiden.mail.utexas.edu; dkim=neutral
> > (message not signed) header.i=none
> > 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.
> >
> > ---
> > 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
> 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.
>
> ---
> You received this message because you are subscribed to the Google Groups "acl2-books" group.
> [2:text/html Show]
>
Reply all
Reply to author
Forward
0 new messages