{"push_id":3638061652,"size":10,"distinct_size":2,"ref":"refs/heads/btc","head":"6aaa065cf5745bf9dda6c17e1ef2ccc40e8afbbf","before":"ce62586fd047b3c6f4f8116516df93dc86eb291f","commits":[{"sha":"5de31e5e4b6b3453079df9e198957285c8fc1dad","author":{"name":"David L. Rager","email":"48c9d777490d75eff3299fbd20c03e45a7856f15@gmail.com"},"message":"Changing startjob from bash alias to env variable\n\nI don't know how the bash alias ever worked, but changing it to\r\nan environment variable should do the trick.","distinct":false,"url":"https://api.github.com/repos/acoglio/acl2/commits/5de31e5e4b6b3453079df9e198957285c8fc1dad"},{"sha":"388d219ed6826ee88027b46a2fe30d4c07580e3d","author":{"name":"David L. Rager","email":"48c9d777490d75eff3299fbd20c03e45a7856f15@gmail.com"},"message":"Merge pull request #997 from acl2/ragerdl-startjob\n\nChanging startjob from bash alias to env variable","distinct":false,"url":"https://api.github.com/repos/acoglio/acl2/commits/388d219ed6826ee88027b46a2fe30d4c07580e3d"},{"sha":"8ad68513809f8d6a07c0e6938eb8032e51467073","author":{"name":"David L. Rager","email":"48c9d777490d75eff3299fbd20c03e45a7856f15@gmail.com"},"message":"Use env var for startjob in jenkins multi script\n\nUse environment variable for startjob in jenkin's multiple lisp script.","distinct":false,"url":"https://api.github.com/repos/acoglio/acl2/commits/8ad68513809f8d6a07c0e6938eb8032e51467073"},{"sha":"8cce1061c3c961e72bca7397c7f91581f22abe86","author":{"name":"David L. Rager","email":"48c9d777490d75eff3299fbd20c03e45a7856f15@gmail.com"},"message":"Merge pull request #998 from acl2/ragerdl-patch-1\n\nUse env var for startjob in jenkins multi script","distinct":false,"url":"https://api.github.com/repos/acoglio/acl2/commits/8cce1061c3c961e72bca7397c7f91581f22abe86"},{"sha":"b997b5ce9e24d016fc18d928444edbe68a9c0888","author":{"name":"Matt Kaufmann","email":"0e8571cdea8dfcd394fe3e7a6fd70cfe66e52b6d@cs.utexas.edu"},"message":"Fix (by J) for a hard Lisp error for definition rules introducing recursion.\n\nQuoting :doc note-8-3 -- this fix was done by J:\n\n  A hard Lisp error has been fixed that could occur (probably only\n  rarely) after adding rules of class :[definition] that introduce\n  recursion.\n\nJ sent me a message that included the following before he fixed the\nbug; it can serve as a test case.  I've edited out all but one of his\ncomments (which were partly about some other work he was doing).\n\n(include-book \"projects/apply/top\" :dir :system)\n\n(defun$ m (x)\n  (if (consp x)\n      (+ 1 (m (car x)) (m (cdr x)))\n      1))\n\n(defun flagged-foo (flg x)\n  (declare (xargs :measure (+ (if flg 1 0) (m x))))\n  (if flg\n      (cond ((atom x) 2)\n            (t (flagged-foo nil x)))\n      (if (endp x)\n          0\n          (+ (fix (flagged-foo t (car x)))\n             (flagged-foo nil (cdr x))))))\n\n(defwarrant flagged-foo)\n\n(defun$ foo (x) (flagged-foo t x))\n\n(encapsulate\n  nil\n  (local\n   (defthm lemma\n     (implies (warrant foo)\n              (equal (flagged-foo flg x)\n                     (if flg\n                         (cond ((atom x) 2)\n                               (t (loop$ for e in x sum (foo e))))\n                         (loop$ for e in x sum (foo e)))))))\n\n  (defthm alternative-foo\n    (implies (warrant foo)\n             (equal (foo x)\n                    (cond ((atom x) 2)\n                          (t (loop$ for e in x sum (foo e))))))\n    :rule-classes :definition))\n\n(in-theory (disable foo))\n\n(defun foo-induction (x)\n  (if (endp x)\n      x\n      (list (foo-induction (car x))\n            (foo-induction (cdr x)))))\n\n(defthm foo-induction-hint\n  t\n  :rule-classes ((:induction :pattern (foo x)\n                             :scheme (foo-induction x))))\n\n; This should succeed but causes a hard error!  If :induct t is replaced by\n; :induct (foo-induction x) it succeeds.\n\n(set-debugger-enable t)\n\n(defthm integerp-foo\n  (implies (warrant foo)\n           (integerp (foo x)))\n  :hints ((\"Goal\" :induct t)))","distinct":false,"url":"https://api.github.com/repos/acoglio/acl2/commits/b997b5ce9e24d016fc18d928444edbe68a9c0888"},{"sha":"b79948d6c3fbb5fdb49a9b659d7a4051928c8c63","author":{"name":"David L. Rager","email":"48c9d777490d75eff3299fbd20c03e45a7856f15@gmail.com"},"message":"Update some markup for the jenkins read\n\nReally, this is to test jenkin's ability to auto-merge from testing to master.","distinct":false,"url":"https://api.github.com/repos/acoglio/acl2/commits/b79948d6c3fbb5fdb49a9b659d7a4051928c8c63"},{"sha":"ccbdc67a6646113833dfb4965703a75864b6e06e","author":{"name":"Matt Kaufmann","email":"ec40743754137ee363bbb55e78fb292c86850f89@gmail.com"},"message":"Removed the restriction that the evaluator can't be ancestral in a metafunction or clause-processor.\n\nQuoting :doc note-8-3:\n\n  It is now permitted for an evaluator to be ancestral in a\n  metafunction or clause-processor.  See [evaluator-restrictions], or\n  see the source code comment ``Essay on Correctness of Meta\n  Reasoning'', for discussion of the remaining restrictions.  Thanks\n  to Sol Swords for requesting this improvement and for many helpful\n  discussions.  Moreover, he found a bug in a proof in the above\n  Essay, which has been been fixed; he made a key observation that\n  led to completion of that fix.  Also thanks to Rob Sumners for\n  helpful discussions.\n\nAlso updated the date in bin/purity.sh.","distinct":false,"url":"https://api.github.com/repos/acoglio/acl2/commits/ccbdc67a6646113833dfb4965703a75864b6e06e"},{"sha":"0c00b18c9fa497c84aec9395c8613ea43d8d2f54","author":{"name":"Shilpi Goel","email":"d57ab9ef26948e212f0246a6891e128e06bf652e@gmail.com"},"message":"[GL] Make add[remove]-gl-rewrite throw an error if given a non-existing rune","distinct":false,"url":"https://api.github.com/repos/acoglio/acl2/commits/0c00b18c9fa497c84aec9395c8613ea43d8d2f54"},{"sha":"7261bab4488bd7fdba693117a2cfe05bc79e6f47","author":{"name":"Alessandro Coglio","email":"1ef9ed097c6a8977a4052c2c50305fb13ab50140@kestrel.edu"},"message":"[Bitcoin] Weaken a few guards in BIP 32.\n\nThese functions with quantifiers can be defined on slightly weaker guards, which\nfacilitates the proof of equivalence with upcoming executable versions of these\nfunctions.","distinct":true,"url":"https://api.github.com/repos/acoglio/acl2/commits/7261bab4488bd7fdba693117a2cfe05bc79e6f47"},{"sha":"6aaa065cf5745bf9dda6c17e1ef2ccc40e8afbbf","author":{"name":"Alessandro Coglio","email":"1ef9ed097c6a8977a4052c2c50305fb13ab50140@kestrel.edu"},"message":"[Bitcoin] Rename a fixing function in BIP 32.","distinct":true,"url":"https://api.github.com/repos/acoglio/acl2/commits/6aaa065cf5745bf9dda6c17e1ef2ccc40e8afbbf"}]}
{"actor":{"display_login":"acoglio"}}