{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/9295","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/9295/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/9295/comments","events_url":"https://api.github.com/repos/coq/coq/issues/9295/events","html_url":"https://github.com/coq/coq/issues/9295","id":395228420,"node_id":"MDU6SXNzdWUzOTUyMjg0MjA=","number":9295,"title":"Project level option system","user":{"login":"SkySkimmer","id":2461932,"node_id":"MDQ6VXNlcjI0NjE5MzI=","avatar_url":"https://avatars1.githubusercontent.com/u/2461932?v=4","gravatar_id":"","url":"https://api.github.com/users/SkySkimmer","html_url":"https://github.com/SkySkimmer","followers_url":"https://api.github.com/users/SkySkimmer/followers","following_url":"https://api.github.com/users/SkySkimmer/following{/other_user}","gists_url":"https://api.github.com/users/SkySkimmer/gists{/gist_id}","starred_url":"https://api.github.com/users/SkySkimmer/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/SkySkimmer/subscriptions","organizations_url":"https://api.github.com/users/SkySkimmer/orgs","repos_url":"https://api.github.com/users/SkySkimmer/repos","events_url":"https://api.github.com/users/SkySkimmer/events{/privacy}","received_events_url":"https://api.github.com/users/SkySkimmer/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2019-01-02T12:06:20Z","updated_at":"2019-01-02T17:57:49Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"Currently if you want to set some options throughout your project (eg Primitive Projections) you either put `Set Primitive Projections.` at the top of every file, or put `Export Set Primitive Projections.` in some options file and `Require Import myoptions.` at the top of all other files. This is a pain and liable to lead to forgetting to do it for new files. You can also `Global Set` in your options file and require it whenever it isn't already transitively required but this is messy especially if you want people to use you as a library.\r\nAlternatively you could put `-arg -l -arg myoptions.v` in your _CoqProject, but coq_makefile won't register the dependency and there are probably random things breaking.\r\n\r\nMeanwhile if we want to set an option for the stdlib without setting it for everyone else we have no way to do it really (or maybe the -l hack would work).\r\n\r\nCan we come up with some better system? Preferrably something that we can get to work with both coq_makefile and the upcoming dune build systems.\r\ncf #8052, [some WG discussion about _CoqProject format](https://github.com/coq/coq/wiki/CoqWG-2018-12-19)"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/450934773","html_url":"https://github.com/coq/coq/issues/9295#issuecomment-450934773","issue_url":"https://api.github.com/repos/coq/coq/issues/9295","id":450934773,"node_id":"MDEyOklzc3VlQ29tbWVudDQ1MDkzNDc3Mw==","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},"created_at":"2019-01-02T17:57:49Z","updated_at":"2019-01-02T17:57:49Z","author_association":"MEMBER","body":"That's a tricky issue IMHO that goes down to the current libobject design. Dune could support the `-l` approach fine, but it seems quite messy. Using command line parameters/flags could be better [like OCaml does for -safe-string] and indeed you could even save in `dune-package` which options are transitive.\r\n\r\nBut a problem here is that options are really too heterogeneous."}}
{"actor":{"display_login":"ejgallego"}}