{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/8667","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/8667/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/8667/comments","events_url":"https://api.github.com/repos/coq/coq/issues/8667/events","html_url":"https://github.com/coq/coq/pull/8667","id":367483580,"node_id":"MDExOlB1bGxSZXF1ZXN0MjIwOTAzNTAz","number":8667,"title":"[RFC] Vendoring of Camlp5","user":{"login":"ejgallego","id":7192257,"node_id":"MDQ6VXNlcjcxOTIyNTc=","avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":17,"created_at":"2018-10-06T18:34:01Z","updated_at":"2018-10-08T11:42:03Z","closed_at":null,"author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/8667","html_url":"https://github.com/coq/coq/pull/8667","diff_url":"https://github.com/coq/coq/pull/8667.diff","patch_url":"https://github.com/coq/coq/pull/8667.patch"},"body":"This is a proposal to vendor `camlp5` as `coq.gramlib`. The idea originated with @ppedrot , as we really don't use a lot of the features Camlp5 provides. This allows to drop the dependency from Camlp5 in order to run Coq, thus testing in newer OCaml versions would become easier. Also, we would be certainly able to optimize the integration with Coq.\r\n\r\nThe vendoring is complete, and it is possible to build Coq without camlp5 as long as you can bootstrap the `ml4` files. Once #8161 is fully implemented, Camlp5 won't be necessary at all [modulo `cLexer.ml4` and `coqide_main.ml4`]\r\n\r\nFor now, the regular make-based system uses `camlp5`, and the Dune build uses the vendored one."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/427802767","html_url":"https://github.com/coq/coq/pull/8667#issuecomment-427802767","issue_url":"https://api.github.com/repos/coq/coq/issues/8667","id":427802767,"node_id":"MDEyOklzc3VlQ29tbWVudDQyNzgwMjc2Nw==","user":{"login":"gares","id":1013846,"node_id":"MDQ6VXNlcjEwMTM4NDY=","avatar_url":"https://avatars2.githubusercontent.com/u/1013846?v=4","gravatar_id":"","url":"https://api.github.com/users/gares","html_url":"https://github.com/gares","followers_url":"https://api.github.com/users/gares/followers","following_url":"https://api.github.com/users/gares/following{/other_user}","gists_url":"https://api.github.com/users/gares/gists{/gist_id}","starred_url":"https://api.github.com/users/gares/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gares/subscriptions","organizations_url":"https://api.github.com/users/gares/orgs","repos_url":"https://api.github.com/users/gares/repos","events_url":"https://api.github.com/users/gares/events{/privacy}","received_events_url":"https://api.github.com/users/gares/received_events","type":"User","site_admin":false},"created_at":"2018-10-08T11:42:03Z","updated_at":"2018-10-08T11:42:03Z","author_association":"MEMBER","body":"@Zimmi48 what I propose (rename the files) is orthogonal to the status of `coq.gramlib`. \r\n\r\nBe it maintained in Coq or outside Coq, the OCaml module names conflicts with camlp5, so it won't be possible to link both camlp5.gramlib and coq.gramlib (it is a limitation of OCaml) in the same application.\r\nThis may be a necessity (example of elpi).\r\n\r\nI frankly don't care much how coq.gramlib is maintained, in both cases I wont to get rid of the extensible parser of elpi. I considered it acceptable to use camlp5 in the first place just because my target was Coq and Matita, and both already use it. FTR it was not me that wrote the parser of elpi ;-)"}}
{"actor":{"display_login":"gares"}}