{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/6698","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/6698/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/6698/comments","events_url":"https://api.github.com/repos/coq/coq/issues/6698/events","html_url":"https://github.com/coq/coq/pull/6698","id":294516542,"number":6698,"title":"Use record of Printing options, issue #6560","user":{"login":"psteckler","id":2244648,"avatar_url":"https://avatars0.githubusercontent.com/u/2244648?v=4","gravatar_id":"","url":"https://api.github.com/users/psteckler","html_url":"https://github.com/psteckler","followers_url":"https://api.github.com/users/psteckler/followers","following_url":"https://api.github.com/users/psteckler/following{/other_user}","gists_url":"https://api.github.com/users/psteckler/gists{/gist_id}","starred_url":"https://api.github.com/users/psteckler/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/psteckler/subscriptions","organizations_url":"https://api.github.com/users/psteckler/orgs","repos_url":"https://api.github.com/users/psteckler/repos","events_url":"https://api.github.com/users/psteckler/events{/privacy}","received_events_url":"https://api.github.com/users/psteckler/received_events","type":"User","site_admin":false},"labels":[{"id":723611231,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20enhancement","name":"kind: enhancement","color":"0e8a16","default":false},{"id":485986179,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20feature","name":"kind: feature","color":"0e8a16","default":false},{"id":394846679,"url":"https://api.github.com/repos/coq/coq/labels/needs:%20review","name":"needs: review","color":"f9d0c4","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/5","html_url":"https://github.com/coq/coq/milestone/5","labels_url":"https://api.github.com/repos/coq/coq/milestones/5/labels","id":2550427,"number":5,"title":"8.8","description":"","creator":{"login":"maximedenes","id":647105,"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},"open_issues":142,"closed_issues":347,"state":"open","created_at":"2017-05-30T13:02:47Z","updated_at":"2018-02-16T22:07:58Z","due_on":null,"closed_at":null},"comments":116,"created_at":"2018-02-05T19:37:49Z","updated_at":"2018-02-17T00:08:21Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/6698","html_url":"https://github.com/coq/coq/pull/6698","diff_url":"https://github.com/coq/coq/pull/6698.diff","patch_url":"https://github.com/coq/coq/pull/6698.patch"},"body":"<!-- Thank you for your contribution.\r\n     Make sure you read the contributing guide and fill this template. -->\r\n\r\nThis PR is an attempt to have `Set Printing All` work as the composition of Printing options, rather than working as its own option. That way, `Set Printing All` followed by, for example, `Unset Printing Implicit` means that implicits won't be printed.\r\n\r\nThe printing options are stored in a single globally-accessible record, rather than as refs scattered throughout the code, as before. The behavior of `Unset Printing All` changes: it negates the options of `Set Printing All`. Before, the `Unset` changed the `raw_print` flag. To compensate for that a bit, there's a new command, `Set Printing Defaults`, which restores the startup options.\r\n\r\n`Set Printing All` also prints universes, which it didn't before.\r\n\r\n`Set Printing Universes` also affected the printing of universe inconsistency explanations, which is somewhat different to printing universes in terms, so the PR adds the command `Set Printing Universe Explanations`, on by default. Maybe the explanations should always be printed, with no option involved.\r\n\r\nOne test-suite file, `output/Cases.v` and the corresponding `.out` file are changed a bit, because of the printing of universes.\r\n\r\nThis PR does not go as far as the request of @ejgallego to pass the record of printing options. That could be added, if there's agreement that the idea in this PR is OK. There were some places where it wasn't clear how the `raw_print` flag was representing other printing options.\r\n\r\nAn alternative to this PR would be to make clear in the documentation that `Set Printing All` is its own separate option, and in the code, make clear which options the `raw_print` flag represents. For example, instead of looking at `raw_print` directly when printing implicits, there could be a predicate `do_print_implicits`, which is the `or` of `raw_print` and the ref for the `Printing Implicit` option. If that cleanup is preferred, there are places in the code where the refs for particular options are aliased, which seems prone to confusion. Even if this PR is not adopted, it would still might be good to gather all the printing option refs in one place.\r\n\r\n<!-- Keep what applies -->\r\n**Kind:** feature\r\n\r\n\r\n<!-- If this is a bug fix, make sure the bug was reported beforehand. -->\r\nFixes #6560 .\r\n\r\n<!-- If this is a feature pull request / breaks compatibility: -->\r\n<!-- (Otherwise, remove these lines.) -->\r\n- [x] Corresponding documentation was added / updated.\r\n- [x] Entry added in CHANGES.\r\n"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/366394325","html_url":"https://github.com/coq/coq/pull/6698#issuecomment-366394325","issue_url":"https://api.github.com/repos/coq/coq/issues/6698","id":366394325,"user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars1.githubusercontent.com/u/460771?v=4","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"created_at":"2018-02-17T00:08:21Z","updated_at":"2018-02-17T00:08:21Z","author_association":"OWNER","body":"> I believe the option we were considering relates to the second bullet point in your conclusion.\r\n\r\nActually I don't know. It really depends on how we think at records, primitive or defined. However, with respect to the PR, I believe that it is consistent to replace the use of `raw_print` with a check at the `Printing Records` option."}}
{"actor":{"display_login":"herbelin"}}