{"action":"created","issue":{"url":"https://api.github.com/repos/AbsInt/CompCert/issues/223","repository_url":"https://api.github.com/repos/AbsInt/CompCert","labels_url":"https://api.github.com/repos/AbsInt/CompCert/issues/223/labels{/name}","comments_url":"https://api.github.com/repos/AbsInt/CompCert/issues/223/comments","events_url":"https://api.github.com/repos/AbsInt/CompCert/issues/223/events","html_url":"https://github.com/AbsInt/CompCert/issues/223","id":300352698,"number":223,"title":"CompCert 3.2.0 and Coq 8.7.2","user":{"login":"lastland","id":848550,"avatar_url":"https://avatars2.githubusercontent.com/u/848550?v=4","gravatar_id":"","url":"https://api.github.com/users/lastland","html_url":"https://github.com/lastland","followers_url":"https://api.github.com/users/lastland/followers","following_url":"https://api.github.com/users/lastland/following{/other_user}","gists_url":"https://api.github.com/users/lastland/gists{/gist_id}","starred_url":"https://api.github.com/users/lastland/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/lastland/subscriptions","organizations_url":"https://api.github.com/users/lastland/orgs","repos_url":"https://api.github.com/users/lastland/repos","events_url":"https://api.github.com/users/lastland/events{/privacy}","received_events_url":"https://api.github.com/users/lastland/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2018-02-26T18:49:13Z","updated_at":"2018-02-28T14:31:16Z","closed_at":null,"author_association":"NONE","body":"The Makefile of CompCert 3.2.0 does not support Coq 8.7.2 (though it seems simply adding the 8.7.2 version number to the Makefile would make it work?). This causes problems for people who are using Coq 8.7.2 and CompCert 3.2.0, especially if they install CompCert using opam.\r\n\r\nIs it possible to make a release of CompCert that supports Coq 8.7.2? Maybe 3.2.1?"},"comment":{"url":"https://api.github.com/repos/AbsInt/CompCert/issues/comments/369256879","html_url":"https://github.com/AbsInt/CompCert/issues/223#issuecomment-369256879","issue_url":"https://api.github.com/repos/AbsInt/CompCert/issues/223","id":369256879,"user":{"login":"xavierleroy","id":3845810,"avatar_url":"https://avatars0.githubusercontent.com/u/3845810?v=4","gravatar_id":"","url":"https://api.github.com/users/xavierleroy","html_url":"https://github.com/xavierleroy","followers_url":"https://api.github.com/users/xavierleroy/followers","following_url":"https://api.github.com/users/xavierleroy/following{/other_user}","gists_url":"https://api.github.com/users/xavierleroy/gists{/gist_id}","starred_url":"https://api.github.com/users/xavierleroy/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/xavierleroy/subscriptions","organizations_url":"https://api.github.com/users/xavierleroy/orgs","repos_url":"https://api.github.com/users/xavierleroy/repos","events_url":"https://api.github.com/users/xavierleroy/events{/privacy}","received_events_url":"https://api.github.com/users/xavierleroy/received_events","type":"User","site_admin":false},"created_at":"2018-02-28T14:31:16Z","updated_at":"2018-02-28T14:31:16Z","author_association":"CONTRIBUTOR","body":"@lastland is correct that OPAM performs version checks in addition to the checks done by CompCert's configure script.  Because of this, the use of `configure -ignore-coq-version` could be considered. \r\n \r\nHowever, the OPAM dependencies shown above are risky.  They assume that any future \"8.7.x\" version of Coq will not break CompCert.  In the past we've seen minor releases of Coq breaking CompCert.  That's why the configure script of CompCert accepts only versions of Coq that were tested to work with CompCert, and not \"any future minor release of Coq\".\r\n\r\nAlso the menhir dependency is wrong, it should be `>= 20161201`.\r\n\r\nMy preferred approach would be to make a new OPAM package for CompCert 3.2 that includes commit 3593971f9d5ec8fa95344e6d0cd25ec55642b365 as a patch, so that the configure script accepts 8.7.2.\r\n\r\nMy next preferred approach would be to use `configure -ignore-coq-version` but tighten the OPAM dependencies so that the only versions of Coq accepted are those that have been tested  to actually work.  It implies that a new version of the package must be published every time a new, compatible version of Coq is released, just like in the preferred approach above.\r\n"}}
{"actor":{"display_login":"xavierleroy"}}