{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/186","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/186/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/186/comments","events_url":"https://api.github.com/repos/coq/coq/issues/186/events","html_url":"https://github.com/coq/coq/pull/186","id":158124283,"node_id":"MDExOlB1bGxSZXF1ZXN0NzIzMzQyMzc=","number":186,"title":"[RFC] Coqlib cleanup","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":[{"id":661181694,"node_id":"MDU6TGFiZWw2NjExODE2OTQ=","url":"https://api.github.com/repos/coq/coq/labels/help%20wanted","name":"help wanted","color":"fff06a","default":true},{"id":485985791,"node_id":"MDU6TGFiZWw0ODU5ODU3OTE=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20cleanup","name":"kind: cleanup","color":"3366ff","default":false},{"id":396673733,"node_id":"MDU6TGFiZWwzOTY2NzM3MzM=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20redesign","name":"kind: redesign","color":"0052cc","default":false},{"id":777223550,"node_id":"MDU6TGFiZWw3NzcyMjM1NTA=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20benchmarking","name":"needs: benchmarking","color":"c2e0c6","default":false},{"id":395008245,"node_id":"MDU6TGFiZWwzOTUwMDgyNDU=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20fixing","name":"needs: fixing","color":"e99695","default":false},{"id":394846778,"node_id":"MDU6TGFiZWwzOTQ4NDY3Nzg=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20progress","name":"needs: progress","color":"ffd062","default":false},{"id":394846679,"node_id":"MDU6TGFiZWwzOTQ4NDY2Nzk=","url":"https://api.github.com/repos/coq/coq/labels/needs:%20review","name":"needs: review","color":"f9d0c4","default":false}],"state":"open","locked":false,"assignee":{"login":"mattam82","id":98373,"node_id":"MDQ6VXNlcjk4Mzcz","avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","gravatar_id":"","url":"https://api.github.com/users/mattam82","html_url":"https://github.com/mattam82","followers_url":"https://api.github.com/users/mattam82/followers","following_url":"https://api.github.com/users/mattam82/following{/other_user}","gists_url":"https://api.github.com/users/mattam82/gists{/gist_id}","starred_url":"https://api.github.com/users/mattam82/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mattam82/subscriptions","organizations_url":"https://api.github.com/users/mattam82/orgs","repos_url":"https://api.github.com/users/mattam82/repos","events_url":"https://api.github.com/users/mattam82/events{/privacy}","received_events_url":"https://api.github.com/users/mattam82/received_events","type":"User","site_admin":false},"assignees":[{"login":"mattam82","id":98373,"node_id":"MDQ6VXNlcjk4Mzcz","avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","gravatar_id":"","url":"https://api.github.com/users/mattam82","html_url":"https://github.com/mattam82","followers_url":"https://api.github.com/users/mattam82/followers","following_url":"https://api.github.com/users/mattam82/following{/other_user}","gists_url":"https://api.github.com/users/mattam82/gists{/gist_id}","starred_url":"https://api.github.com/users/mattam82/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mattam82/subscriptions","organizations_url":"https://api.github.com/users/mattam82/orgs","repos_url":"https://api.github.com/users/mattam82/repos","events_url":"https://api.github.com/users/mattam82/events{/privacy}","received_events_url":"https://api.github.com/users/mattam82/received_events","type":"User","site_admin":false}],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/7","html_url":"https://github.com/coq/coq/milestone/7","labels_url":"https://api.github.com/repos/coq/coq/milestones/7/labels","id":2647743,"node_id":"MDk6TWlsZXN0b25lMjY0Nzc0Mw==","number":7,"title":"8.9+beta1","description":"The date of the feature freeze has not been announced yet.","creator":{"login":"Zimmi48","id":1108325,"node_id":"MDQ6VXNlcjExMDgzMjU=","avatar_url":"https://avatars2.githubusercontent.com/u/1108325?v=4","gravatar_id":"","url":"https://api.github.com/users/Zimmi48","html_url":"https://github.com/Zimmi48","followers_url":"https://api.github.com/users/Zimmi48/followers","following_url":"https://api.github.com/users/Zimmi48/following{/other_user}","gists_url":"https://api.github.com/users/Zimmi48/gists{/gist_id}","starred_url":"https://api.github.com/users/Zimmi48/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Zimmi48/subscriptions","organizations_url":"https://api.github.com/users/Zimmi48/orgs","repos_url":"https://api.github.com/users/Zimmi48/repos","events_url":"https://api.github.com/users/Zimmi48/events{/privacy}","received_events_url":"https://api.github.com/users/Zimmi48/received_events","type":"User","site_admin":false},"open_issues":123,"closed_issues":204,"state":"open","created_at":"2017-07-18T15:03:25Z","updated_at":"2018-06-08T14:10:22Z","due_on":null,"closed_at":null},"comments":32,"created_at":"2016-06-02T12:02:18Z","updated_at":"2018-06-08T14:52:21Z","closed_at":null,"author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/186","html_url":"https://github.com/coq/coq/pull/186","diff_url":"https://github.com/coq/coq/pull/186.diff","patch_url":"https://github.com/coq/coq/pull/186.patch"},"body":"# Patch description and motivation:\n\nThis patch modifies the API for requesting library-defined symbols from the ML side. It enables the use of Coq without its standard library. It is a port to trunk of PR #145, see comments there.\n\nCurrently, ML code wanting to access to library-defined constants use [Coqlib.find_reference module id] to get a reference to a symbol in .v files.\n\nIMO, the current API to map library-provided symbols has a few weak points:\n- It is closely tied to file-system layout.\n- It uses non-deterministic search sometimes.\n- It doesn't handle optional dependencies well (Anomalies...)\n- The rules for symbol lifetime are not very clear (Lazy vs delayed)\n- It provides redundant entry points.\n- It provides \"hardcoded constants\".\n- The symbol namespace is not easily discoverable/extensible.\n- It is not easy for plugin/library writers to extend the global namespace in such a way that other plugins can rely on it.\n# Current changes/Status.\n\nThe current patch introduces a new API to access library-defined symbols.\n\nIt is pretty much work in progress and not ready to be merged yet; with some caveats, it enables the compilation of HoTT and math-comp without the standard library [1].\n\nThe main change is a modification of the coqlib API such that objects are referenced now using a \"domain.object.property\".\n\nThe new functions are:\n\n``` ocaml\nval lib_ref    : string -> global_reference\nval add_ref    : string -> global_reference -> unit\n```\n\nExample namespaces are:\n\n```\n  \"core.eq.type\"   -> reference to current eq type\n  \"core.bool.type\" -> reference to current bool type\n  \"core.bool.true\" -> reference to true constructor\n\n  \"omega.bool.type\" -> plugin-specific namespace, omega may want to\n                       allow rebinding of bool, etc...\n```\n\nStatic references are not allowed, as they depend on which libraries are loaded.\n\nThe contract for callers of `lib_ref` is pretty liberal. Users _must_ handle Not_found gracefully; also, the result of `lib_ref` will be altered by library loading, thus each time a current reference is desired `lib_ref` must be called again.\n\nPlugins are free to cache references, but they are then responsible of managing reference lifetime.\n\nThe main parts of Coq have been ported to the new API. Coq stdlib, math-comp and HoTT work, but a flag is still needed to tweak a couple of settings.\n\nIn order to remove the flag, a new vernacular is necessary:\n\n``` coq\nDeclare Lib Object \"dom.obj.prop\" name.\n```\n\nThen, libraries could rebind references and the rest of hardcoded paths in `coqlib.ml` would go away.\n\nTest suite passes but for micromega and omega that I didn't port, [waiting for some more feedback as the porting effort is large].\n\nMost of the patch is pretty straightforward; the kernel is not affected. There are a couple of delicate things thou:\n- Coqlib has been moved to pretyping now. This is needed as program.ml was requesting access to library-defined symbols.\n  I don't have a particular opinion on this.\n- The old coqlib was using smartlocate, but as a consequence of the above change, reference finding had to be moved back to using Nametab. I don't know what the impact of this change is.\n- hipattern and equality.ml want to use \"globals\", that is uninitialized references to library symbols. You can see the two particular places by doing \"git grep glob_jmeq\".\n  The logic here is delicate and I'd need a bit of help to understand what would be the right choice.\n# TODO:\n\nApart from checking if people would be OK with this change, there are\nstill quite a few things to do:\n- Removal of glob_\\* in coqlib:\n  - the last uses are in hipattern.ml and equality.ml, but they are a bit tricky and require having a good understanding of the logic.\n- Implement the Declare Lib Object vernacular.\n- Port the syntax plugins\n- removal of *_module exports in coqlib.ml\n- removal of the rest of exports from coqlib.\n- Finish porting all other plugins.\n  - In particular Tauto.v depends on Coq.Init.Logic.{iff,not}.\n\n[1] See:\n- https://github.com/ejgallego/HoTT/tree/no-stdlib\n- https://github.com/ejgallego/math-comp/tree/no-stdlib\n"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/395785774","html_url":"https://github.com/coq/coq/pull/186#issuecomment-395785774","issue_url":"https://api.github.com/repos/coq/coq/issues/186","id":395785774,"node_id":"MDEyOklzc3VlQ29tbWVudDM5NTc4NTc3NA==","user":{"login":"maximedenes","id":647105,"node_id":"MDQ6VXNlcjY0NzEwNQ==","avatar_url":"https://avatars1.githubusercontent.com/u/647105?v=4","gravatar_id":"","url":"https://api.github.com/users/maximedenes","html_url":"https://github.com/maximedenes","followers_url":"https://api.github.com/users/maximedenes/followers","following_url":"https://api.github.com/users/maximedenes/following{/other_user}","gists_url":"https://api.github.com/users/maximedenes/gists{/gist_id}","starred_url":"https://api.github.com/users/maximedenes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/maximedenes/subscriptions","organizations_url":"https://api.github.com/users/maximedenes/orgs","repos_url":"https://api.github.com/users/maximedenes/repos","events_url":"https://api.github.com/users/maximedenes/events{/privacy}","received_events_url":"https://api.github.com/users/maximedenes/received_events","type":"User","site_admin":false},"created_at":"2018-06-08T14:52:21Z","updated_at":"2018-06-08T14:52:21Z","author_association":"MEMBER","body":"@ejgallego Having a look now. If I fix the build, can I push to your tree?"}}
{"actor":{"display_login":"maximedenes"}}