{"push_id":2345715738,"size":44,"distinct_size":6,"ref":"refs/heads/unit-test-suite","head":"1557b8639acdb5113f199914772ccf7b0d18e52b","before":"d80ab92eff00b07f0e949f9c787552497238730c","commits":[{"sha":"568dffcc32cfdec78e7824fa6875d892fb9cfd5a","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"Remove dir-locals and ship suggested helper hooks instead.\n\n.dir-locals led to issues with unsafe local variable warnings. With\nthis method the user is opting in to running this code so there are no warnings.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/568dffcc32cfdec78e7824fa6875d892fb9cfd5a"},{"sha":"e82bbbb5181e04d00696f9bb2d352766b305886b","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"Fix ci-all target","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/e82bbbb5181e04d00696f9bb2d352766b305886b"},{"sha":"e4529a4349110c2edb6bd08f873175db71363a84","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"coqdev.el: add installation instructions.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/e4529a4349110c2edb6bd08f873175db71363a84"},{"sha":"20e654c5b1995e04d103e099bc806d27f797b640","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"Merge anomaly-traces-parser.el into coqdev.el.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/20e654c5b1995e04d103e099bc806d27f797b640"},{"sha":"68935660fbfdec2e357e123ed999073ed3b8fc26","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[engine] Remove ghost parameter from `Proofview.Goal.t`\n\nIn current code, `Proofview.Goal.t` uses a phantom type to indicate\nwhether the goal was properly substituted wrt current `evar_map` or\nnot.\n\nAfter the introduction of `EConstr`, this distinction should have\nbecome unnecessary, thus we remove the phantom parameter from\n`'a Proofview.Goal.t`. This may introduce some minor incompatibilities\nat the typing level. Code-wise, things should remain the same.\n\nWe thus deprecate `assume`. In a next commit, we will remove\nnormalization as much as possible from the code.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/68935660fbfdec2e357e123ed999073ed3b8fc26"},{"sha":"9997f9aec01abdb59852ec5706ef36ce56311109","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"coqdev.el: stop using when-let for emacs<25 compatibility.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/9997f9aec01abdb59852ec5706ef36ce56311109"},{"sha":"fbe9d252ef31f49a75225b8c71be56a38bc51a3d","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"coqdev.el: shell-quote-argument the directory for make -C","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/fbe9d252ef31f49a75225b8c71be56a38bc51a3d"},{"sha":"d5c771138a3b2ce753f458396d82eef9a4557e20","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"coqdev.el: fix \"compilate\"-command typo","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/d5c771138a3b2ce753f458396d82eef9a4557e20"},{"sha":"d9cb50d8f9b2bb16ddf7c27c146e09d7de33b90f","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"coqdev.el: wait for 'compile to touch compilation-error-regexp-alist\n\n(and alist-alist)","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/d9cb50d8f9b2bb16ddf7c27c146e09d7de33b90f"},{"sha":"d643abd6bc67ed6fb3064316cdca19d5f1564418","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[build] Fix VM dynamic linking prep in byte builds.\n\nWe correctly set the path of `libcoqrun` in non-local builds. This bug\nwas introduced by #6038.\n\nc.f. #6475 , #5992.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/d643abd6bc67ed6fb3064316cdca19d5f1564418"},{"sha":"20916bd558a355b597337101e3281bb5ebbfcd36","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"detype_case predicate is not optional","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/20916bd558a355b597337101e3281bb5ebbfcd36"},{"sha":"8cd6ddb98c12b6aba002781158180ffb68aba02f","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Abstract further the type of VM bytecode compilation.\n\nThis reduces the possibility to wreak havoc while making the API nicer.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/8cd6ddb98c12b6aba002781158180ffb68aba02f"},{"sha":"8fa3c26adb1bc2c0201a61adede278a0e889eef4","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Move the call to the computation of bytecode inside Cemitcodes.\n\nThis shouldn't matter because the tcode_of_code function is pure, its only\neffect being allocating a string and filling it with the translated bytecode.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/8fa3c26adb1bc2c0201a61adede278a0e889eef4"},{"sha":"96a4c2a8e2b3de327331e55a9663d230027210e9","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Remove the unsafe bytes conversion function in Cemitcodes.\n\nThis is actually not needed, as the only thing we do with this Bytes.t is to\npass it to a C function which will use it in a read-only way.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/96a4c2a8e2b3de327331e55a9663d230027210e9"},{"sha":"7d4a5f3774ef730a55e6199addcc7dc104f5b9c6","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Do not use global variables for VM bytecode compilation in Cemitcodes.\n\nInstead we thread a buffer.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/7d4a5f3774ef730a55e6199addcc7dc104f5b9c6"},{"sha":"da659eeeb413c488f5efae0269c5d37837c62dc2","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Use a more compact representation for bytecode relocations stored on disk.\n\nThe previous implementation used a list of pairs, which has size 9n where n\nis the number of relocations. We instead use two arrays for a total memory\ncost of 2n + 5 words.\n\nThe use of arrays may turn out to be problematic on 32-bit machines, I am unsure\nif we will hit this limitation in practice.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/da659eeeb413c488f5efae0269c5d37837c62dc2"},{"sha":"745696124240963616a38f41b1a20f199646c5dc","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Factorize the relocations in the on-disk VM representation.\n\nInstead of using a linear representation, we simply use a table that maps\nevery kind of relocation to the list of positions it needs to be applied to.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/745696124240963616a38f41b1a20f199646c5dc"},{"sha":"99d44ff26e2e822b331546fc8e362c2d73155fdf","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"Remove unused argument in Record.declare_structure\n\nThis was for autoinstance.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/99d44ff26e2e822b331546fc8e362c2d73155fdf"},{"sha":"4bc9529ece085441121678a07e4b269c7633471c","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[ide] Localize a IDE-specific flag.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/4bc9529ece085441121678a07e4b269c7633471c"},{"sha":"ed18f926e4695acc730218925ca156abe56ba5fc","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[toplevel] Make toplevel state into a record.\n\nWe organize the toplevel execution as a record and pass it\naround. This will be used by future PRs as to for example decouple\ngoal printing from the classifier.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/ed18f926e4695acc730218925ca156abe56ba5fc"}]}
{"actor":{"display_login":"psteckler"}}