{"push_id":830171606,"size":71,"distinct_size":0,"ref":"refs/heads/master","head":"88becefc05609176a30cf748f0a6aabf3db14924","before":"e34b51d2c0be29edbaf2c79bdc44dc85123ff65c","commits":[{"sha":"f5bfcfcb77dabe3b2a1b8a0af068decc18133e54","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Work in progress for the word-count proof","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/f5bfcfcb77dabe3b2a1b8a0af068decc18133e54"},{"sha":"f444b5881f3d214fb56f8fef32055464fcbad1db","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Some more progress towards the word-count proof.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/f444b5881f3d214fb56f8fef32055464fcbad1db"},{"sha":"45cf8181d98b6fb8772d1ee81810ac88d14f4d78","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Finished the word-count proof. Clean-up pending.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/45cf8181d98b6fb8772d1ee81810ac88d14f4d78"},{"sha":"c8e1a00b937756b2221c8a872e1d162e24bae645","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Minor edits to wc proof.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/c8e1a00b937756b2221c8a872e1d162e24bae645"},{"sha":"5135013d56f6803c9cda9957d2f9b1a7b40d4d19","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Added dataCopy program to tools/execution/examples. Also organized the\ncontents of this directory. Started working on the proof of\ncorrectness of the dataCopy program.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/5135013d56f6803c9cda9957d2f9b1a7b40d4d19"},{"sha":"deaf7388c25beabd7ab2329d2c3097c66143aecf","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Proved copy properties of the loop in the dataCopy program.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/deaf7388c25beabd7ab2329d2c3097c66143aecf"},{"sha":"72c8d7a9b8dc15405b6f10344fae1b44426770b7","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Merge back","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/72c8d7a9b8dc15405b6f10344fae1b44426770b7"},{"sha":"65e3f302cdbda00a4815fe7bbeec031ebeec8b26","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Some more progress with the dataCopy proof.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/65e3f302cdbda00a4815fe7bbeec031ebeec8b26"},{"sha":"1bf05fb08f95aea1e1b0f50c0d6adef2d2584c2c","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Merge","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/1bf05fb08f95aea1e1b0f50c0d6adef2d2584c2c"},{"sha":"a02e833e741f75c7aa6e66ae33f5932b3f6350fb","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Proved that the dataCopy program correctly copies data from the source\narray to the destination array.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/a02e833e741f75c7aa6e66ae33f5932b3f6350fb"},{"sha":"85f320cb599249c5101e88aecc912024d393f32b","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Finished the proof of correctness of dataCopy program.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/85f320cb599249c5101e88aecc912024d393f32b"},{"sha":"507305a26845c553c672574b00b67fdf82a75810","author":{"email":"6c5f8d76635c682fbfbfe94b3e951001b5cf4bc0@gmail.com","name":"Jared C. Davis"},"message":"Add preferred topics to fixtypes\n\nIn the golden age of cutil and std/util, the closest thing to a type\nwas a recognizer, so recognizers like widget-p ended up being the\n\"main\" topic for a type.\n\nNow, with FTY, we tend to instead use the type name (e.g., widget) as\nthe main topic.  Pages like widget-p, widget-fix, widget-equiv, and\neat-widget being found underneath widget.  This is fine and seems to\nbe we want to standardize on going forward, so I'll call it the\n\"typename topic convention.\"\n\nHowever, in the documentation produced by macros like defprod, where\nwe want to provide links to the types of each field, we were still\nlinking to recognizers, i.e., for vl-gateinst we were producing things\nlike this:\n\n     type     --- vl-gatetype-p  ...\n     name     --- maybe-stringp  ...\n     atts     --- vl-atts-p      ...\n\nWhereas really we should instead be linking to topics like vl-gatetype\nand vl-atts.\n\nThis would be easy if everything followed the typename topic\nconvention, but various base types like nat/string/etc. don't follow\nthe convention, so in those cases we probably still want to link to\nthe recognizers, i.e., natp, stringp, etc.\n\nTo resolve this, we add a new TOPIC field to each fixtype, which can\nbe chosen at DEFFIXTYPE time, and which indicates the preferred topic\nto link to when referring to this type.  The defaults topic is just\nthe type name (i.e., by default types are expected to follow the\ntypename topic convention), but for cases like natp/stringp we can\ninstead configure the TOPIC to point to the recognizer (or whatever\nelse is appropriate) instead of having to introduce new topics.\n\nThe idea is that macros like DEFPROD can now use this TOPIC field when\ncreating links to the type so that the documentation points to the\nmain page for each type, instead of just pointing to the (much less\ndescriptive) recognizer pages.\n\nThis patch tweaks DEFPROD to do this; it may be that other FTY macros\nshould also be similarly extended.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/507305a26845c553c672574b00b67fdf82a75810"},{"sha":"82616c9afd82be7875c8682236192b5b85e72e4c","author":{"email":"6c5f8d76635c682fbfbfe94b3e951001b5cf4bc0@gmail.com","name":"Jared C. Davis"},"message":"Ensure a tshell is available for xdoc::save.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/82616c9afd82be7875c8682236192b5b85e72e4c"},{"sha":"75168abd9efc71a69c86f22ceffbe5cad14ad014","author":{"email":"6c5f8d76635c682fbfbfe94b3e951001b5cf4bc0@gmail.com","name":"Jared C. Davis"},"message":"Various fixes to FTY and VL documentation\n\n - Fix some problems with generated docs for defoption\n - Update some fixtypes to use the new :topic feature\n - Edit various VL topics","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/75168abd9efc71a69c86f22ceffbe5cad14ad014"},{"sha":"d854dd50438b4e5a63d3e45bb61ca7e3af2d8b87","author":{"email":"6c5f8d76635c682fbfbfe94b3e951001b5cf4bc0@gmail.com","name":"Jared C. Davis"},"message":"FTY: fixes to autogenerated docs for deftranssum","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/d854dd50438b4e5a63d3e45bb61ca7e3af2d8b87"},{"sha":"9614f0e3b59f6cc9c06807e0f3a11d99ee96c736","author":{"email":"d57ab9ef26948e212f0246a6891e128e06bf652e@cs.utexas.edu","name":"Shilpi Goel"},"message":"Clean up of dataCopy proof.","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/9614f0e3b59f6cc9c06807e0f3a11d99ee96c736"},{"sha":"67da317f0f5fb05f00e16ab02105a833c94304e7","author":{"email":"6c5f8d76635c682fbfbfe94b3e951001b5cf4bc0@gmail.com","name":"Jared C. Davis"},"message":"VL documentation work","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/67da317f0f5fb05f00e16ab02105a833c94304e7"},{"sha":"c7b8855df5d768078fca0f5138d5f1df538e5e6e","author":{"email":"6c5f8d76635c682fbfbfe94b3e951001b5cf4bc0@gmail.com","name":"Jared C. Davis"},"message":"Merge remote-tracking branch 'remotes/origin/master'","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/c7b8855df5d768078fca0f5138d5f1df538e5e6e"},{"sha":"5851fecf731af6718250ecfd4b28dbf02f4f9427","author":{"email":"b3527ff7b4d8dd1f2a0ead5c4a72f45b44cc8ae0@gmail.com","name":"nadezhin"},"message":"Limited floating-point support in JVM M5 model","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/5851fecf731af6718250ecfd4b28dbf02f4f9427"},{"sha":"a612abf0ac59cd98c0fec777f2793853412b03e1","author":{"email":"b3527ff7b4d8dd1f2a0ead5c4a72f45b44cc8ae0@gmail.com","name":"nadezhin"},"message":"cp-make functions fix their argument","distinct":false,"url":"https://api.github.com/repos/ragerdl/acl2/commits/a612abf0ac59cd98c0fec777f2793853412b03e1"}]}