{"push_id":3402306676,"size":23,"distinct_size":23,"ref":"refs/heads/relaxed-ambiguous-paths","head":"5c388bb330afab9b87ab68ee94e4dc1055bf66f9","before":"271ac6fc31246bb0b58a1afa6b5d21ce7cc656d6","commits":[{"sha":"18bdabf7211508e72ece347bbc619f16e79e3678","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[dune] [ide] Don't install the internal CoqIDE UI library.\n\nThis library is unstable and not meant to be consumed by anyone. We\nthus make it private.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/18bdabf7211508e72ece347bbc619f16e79e3678"},{"sha":"c0948de203f6eccb42c47c2e818cf8234f09ec79","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[dune] [checker] Don't install internal checker library.\n\nThis library is private and shouldn't be exposed to plugins.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/c0948de203f6eccb42c47c2e818cf8234f09ec79"},{"sha":"7d436786e79b79643999cddff70f5fbf3b4c3ad9","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove unused Retroknowledge.Register_inline\n\nThis operation is done directly in Safe_typing.register_inline and has\nnothing to do with retroknowledge afaict.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/7d436786e79b79643999cddff70f5fbf3b4c3ad9"},{"sha":"ab1fd660db052741a3d9aed871251dc3dbee63ca","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Nicer error for bad primitive types (through type_errors etc)","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/ab1fd660db052741a3d9aed871251dc3dbee63ca"},{"sha":"3597a7f32fa1e01504adcd34fed4927c15edbda4","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Fix undefined gramlib_MLLIB_DEPENDENCIES in make install","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/3597a7f32fa1e01504adcd34fed4927c15edbda4"},{"sha":"0e2bb26240b785d4ca618cfbc042b13c613fa78f","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Don't coqchk the test suite prerequisites\n\nThis causes the makefile to break due to dependencies when it fails,\nand it's not worth adding a whole mess of code to catch the failure\nfor these files.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/0e2bb26240b785d4ca618cfbc042b13c613fa78f"},{"sha":"288a9d42df805064adfb26daa488fb55d034707a","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[dune] [configure] Fix `gramlib` path for hardcoded includes.\n\nThe regular make build uses a non-standard header path for their files\n[as a way to workaround the ugliness of the non-hygienic build]\n\nThis breaks in Dune as it uses the regular object file pack, so\n`coq_makefile` won't find it. We cherry pick a change from #8729 which\nfixes the updated version of bug #9735 , even tho `coq_makefile`\nshould stop relying on hardcoded paths and use findlib instead.\n\nCloses #9735","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/288a9d42df805064adfb26daa488fb55d034707a"},{"sha":"430851db6db8ba30280f024ccbca5f6124287ab7","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[dune] Add shim for coqtop.byte\n\nWe add a shim for running the byte version of coqtop. This fixes the\nCoq part of #9727 , the Dune part is still open at\nhttps://github.com/ocaml/dune/issues/108 but this PR includes a\nworkaround.\n\nUnfortunately we have to introduce a small inefficiency in the build\nprocess as we build both byte and native versions of plugins for this\nwork reliable.\n\nAs this is a choice done during bootstrap it won't be easy to fix\nuntil we have our own `dune coqtop` command and we can control the\nrules depending on the final target.\n\nThis should affect the `check` target so still fast builds should be\npossible, but if this is a problem we could add a `byteboot` target to\nhelp.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/430851db6db8ba30280f024ccbca5f6124287ab7"},{"sha":"a249cc95c1345442c67e240e881fb653579ee386","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"[refman] Add 'warn' option to coqtop directive.\n\nFix semantic conflict between #9389 and #9654.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/a249cc95c1345442c67e240e881fb653579ee386"},{"sha":"e341c36cdc2aa2220152b2a3745bf3255316cdf3","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"Merge PR #9627: Small retroknowledge/primitive cleanup\n\nAck-by: SkySkimmer\nReviewed-by: ppedrot\nReviewed-by: vbgl","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/e341c36cdc2aa2220152b2a3745bf3255316cdf3"},{"sha":"6c20e7d284280d7c3927aab6ea9b46b86998a00e","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"[refman] Fix other newly emitted warnings.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/6c20e7d284280d7c3927aab6ea9b46b86998a00e"},{"sha":"59d8aea2665828619d42a012ec1650ccac5c4c94","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"[refman] Remove warning silencing by fixing the underlying issue.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/59d8aea2665828619d42a012ec1650ccac5c4c94"},{"sha":"1eb1fe7cee6f8381c5c715430eba0c5994f0b3a4","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"[refman] Fix Sphinx-translation regression in Arguments command.","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/1eb1fe7cee6f8381c5c715430eba0c5994f0b3a4"},{"sha":"915192abdf1bdb3129fd28f05cee6340d5a8c464","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Merge PR #9748: [dune] Add shim for coqtop.byte\n\nReviewed-by: Zimmi48\nReviewed-by: gares","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/915192abdf1bdb3129fd28f05cee6340d5a8c464"},{"sha":"63362b21a4fbb5e921ffca723d4eba923fb4e62d","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr"},"message":"Merge PR #9739: [dune] [configure] Fix `gramlib` path for hardcoded includes.\n\nReviewed-by: gares","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/63362b21a4fbb5e921ffca723d4eba923fb4e62d"},{"sha":"f16fca89aa98fc4d8360df7045e932800edcb9ea","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr"},"message":"Merge PR #9723: Fix undefined gramlib_MLLIB_DEPENDENCIES in make install\n\nReviewed-by: gares","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/f16fca89aa98fc4d8360df7045e932800edcb9ea"},{"sha":"425c02cb6dc4578aebc62ff94c656a904e5d6299","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"Merge PR #9757: [refman] Add 'warn' option to coqtop directive.\n\nReviewed-by: cpitclaudel","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/425c02cb6dc4578aebc62ff94c656a904e5d6299"},{"sha":"27ab0d69e87fa3ce414cdaa205f7f6266693e263","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr"},"message":"Merge PR #9736: Don't coqchk the test suite prerequisites\n\nReviewed-by: gares","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/27ab0d69e87fa3ce414cdaa205f7f6266693e263"},{"sha":"8ea0039ff69491b9e672bc3c522a356085d89c22","author":{"name":"Chantal Keller","email":"cf43de92e885c828939e8d77803882703881910e@inria.fr"},"message":"Exposes Coq_micromega.dump_proof_term to allow a use independent from tactics","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/8ea0039ff69491b9e672bc3c522a356085d89c22"},{"sha":"d07f718785414e643c69a77e38bfa43792d877f3","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Merge PR #9700: [dune] [checker] Don't install internal checker library.\n\nReviewed-by: Zimmi48\nReviewed-by: ppedrot","distinct":true,"url":"https://api.github.com/repos/pi8027/coq/commits/d07f718785414e643c69a77e38bfa43792d877f3"}]}
{"actor":{"display_login":"pi8027"}}