{"push_id":798301607,"size":1,"distinct_size":1,"ref":"refs/heads/testing","head":"647a3d60842f1a8e62e6ccd7c67280db197a326b","before":"0476c843181d74b4e0b57259d3278cfb94a9701a","commits":[{"sha":"647a3d60842f1a8e62e6ccd7c67280db197a326b","author":{"email":"420d97235124da5bf24c51a35edb1119f653ce09@kookamara.com","name":"Jared Davis"},"message":"Extend build system to better support Smtlink (half done, help needed)\n\nThis patch adds a new cert_param to cert.pl for Smtlink which should be used\nlike other cert params such as uses-glucose.  That is, in any book whose proofs\nrequire Smtlink to certify, you should add a comment like this:\n\n   ;; cert_param: (uses-smtlink)\n\nThis comment will instruct books/GNUmakefile not to try to certify this book\n(or or any books that transitively depend on it) unless supporting software\nsuch as Z3 is installed.\n\nCurrently implemented:\n\n  - The cert_param has been added to cert.pl\n  - The books/GNUmakefile will properly exclude books that are marked\n  - Various files in workshops/2015/peng-greenstreet/ have cert_param comments\n\nI think this should be good enough to get the testing regression working again.\n\nHOWEVER, there is still work to do because I do not know how to properly detect\nwhether Smtlink's dependencies like Z3 and Python are installed.\n\nCurrently, in books/GNUmakefile, I have just left the following stub.  Someone\nwho knows what they're doing will need to adjust these lines so that\nOS_HAS_SMTLINK will get set to 1 when Z3 and Python and whatever else are\nrequired are indeed available:\n\n  $(info Determining whether Smtlink is supported -- BOZO todo, for now pretending it does not!)\n  # BOZO TODO figure out how to do this right.  For now, just say that SMTLINK\n  OS_HAS_SMTLINK :=\n\nUpdate issue 515.","distinct":true,"url":"https://api.github.com/repos/acl2/acl2/commits/647a3d60842f1a8e62e6ccd7c67280db197a326b"}]}