{"push_id":900878329,"size":5,"distinct_size":0,"ref":"refs/heads/master","head":"1bd5cd06a0b963d88aaa1d1c8f0e7ffc323431bb","before":"b75aa6f67d3a09baed22ea95ee1e979ab17eeb46","commits":[{"sha":"9d2b37f085f5beafffe260af7c8894854f1617bb","author":{"email":"420d97235124da5bf24c51a35edb1119f653ce09@kookamara.com","name":"Jared Davis"},"message":"defrule: add a with-output testing mechanism\n\nThis is essentially a followup to the commit message from\n4f5dc12a0b39faf253389ba6975bc1f26cf7d617.  It adds a new file,\nstd/util/tests/defrule.lisp, which has the test cases from that\ncommit message converted into tests that let you easily see and\ncompare the output from thm vs. rule or defthm vs. defrule in a\nside-by-side manner.\n\nThis is preparation for changing the with-output stuff in\ndefrule.  There are some really bad cases where rule/defrule can\ncompletely hide errors from you.  Before fixing that, I wanted a\ntest suite of sorts (because it's hard to fix one thing without\nscrewing up something else.)","distinct":false,"url":"https://api.github.com/repos/acl2/acl2/commits/9d2b37f085f5beafffe260af7c8894854f1617bb"},{"sha":"3be2be3c2364bf919d8e4b435dd325bbeea9e98e","author":{"email":"420d97235124da5bf24c51a35edb1119f653ce09@kookamara.com","name":"Jared Davis"},"message":"Merge remote-tracking branch 'remotes/origin/testing'","distinct":false,"url":"https://api.github.com/repos/acl2/acl2/commits/3be2be3c2364bf919d8e4b435dd325bbeea9e98e"},{"sha":"9b6efdf3ce6f18fef1891c78d6e52e27e05aa60c","author":{"email":"420d97235124da5bf24c51a35edb1119f653ce09@kookamara.com","name":"Jared Davis"},"message":"defrule: improve with-output handling\n\n - Fix bug with theory invariants being silently suppressed\n - Update defrule tests to note that this is now working","distinct":false,"url":"https://api.github.com/repos/acl2/acl2/commits/9b6efdf3ce6f18fef1891c78d6e52e27e05aa60c"},{"sha":"41f08238966250295daa7d3a0f5e12d331c69fe8","author":{"email":"420d97235124da5bf24c51a35edb1119f653ce09@kookamara.com","name":"Jared Davis"},"message":"define: avoid unnecessary guard declarations\n\nMinor tweak to define's output.  Avoid :guard t declarations\nin the common cases where there are guards coming from other\nplaces.  That is, something like:\n\n  (define f (x) (declare (xargs :guard (natp x))) x)\n\nWould previously expand to:\n\n  (defun f (x)\n    (declare (xargs :guard t))\n    (declare (xargs :guard (natp x)))\n    ...)\n\nBut now we avoid the ugly :guard t form:\n\n  (defun f (x)\n    (declare (xargs :guard (natp x)))\n    ...)","distinct":false,"url":"https://api.github.com/repos/acl2/acl2/commits/41f08238966250295daa7d3a0f5e12d331c69fe8"},{"sha":"1bd5cd06a0b963d88aaa1d1c8f0e7ffc323431bb","author":{"email":"420d97235124da5bf24c51a35edb1119f653ce09@kookamara.com","name":"Jared Davis"},"message":"Define: use fancy pe-table for better :pe displays\n\nFunctions introduced by define previously had ugly :pe displays\nthat showed the __function__ stuff, didn't show the return values\nor any documentation, etc.\n\nThis uses the new extend-pe-table stuff to make it show something\nnicer.  For example, after:\n\n   (define foo\n     :short \"Foo does something very important, indeed.\"\n     ((x integerp \"The first argument\")\n      (y natp     \"Some other argument\"))\n     :returns (mv (ans1 natp :hyp :guard)\n                  (ans2 integerp\n\t\t        \"Not really very useful\"))\n     :verify-guards nil\n     :guard-hints((\"Goal\" :in-theory (enable append)))\n     :guard-debug t\n     (mv y (ifix x)))\n\nRunning (pe 'foo) would formerly print something like this:\n\n   d       4:x(DEFINE FOO :SHORT ...)\n              \\\n>L d           (DEFUN\n                FOO (X Y)\n                (DECLARE (XARGS :GUARD (AND (INTEGERP X) (NATP Y))))\n                (DECLARE\n                    (XARGS :GUARD-DEBUG T\n                           :GUARD-HINTS ((\"Goal\" :IN-THEORY (ENABLE APPEND)))\n                           :VERIFY-GUARDS NIL))\n                (LET ((__FUNCTION__ 'FOO))\n                     (DECLARE (IGNORABLE __FUNCTION__))\n                     (MV Y (IFIX X))))\n\nBut now it will instead print something much more like what you typed:\n\n   d       5:x(DEFINE FOO :SHORT ...)\n              \\\n>L d           (DEFINE FOO\n                       ((X INTEGERP \"The first argument\")\n                        (Y NATP \"Some other argument\"))\n                       :SHORT\n                       \"Foo does something very important, indeed.\"\n                       :RETURNS\n                       (MV (ANS1 NATP :HYP :GUARD)\n                           (ANS2 INTEGERP \"Not really very useful\"))\n                       (MV Y (IFIX X)))\n\nThere may be bugs.  Please report anything you notice that seems\nweird/bad about how this works.","distinct":false,"url":"https://api.github.com/repos/acl2/acl2/commits/1bd5cd06a0b963d88aaa1d1c8f0e7ffc323431bb"}]}