{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/7257","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/7257/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/7257/comments","events_url":"https://api.github.com/repos/coq/coq/issues/7257/events","html_url":"https://github.com/coq/coq/pull/7257","id":314417894,"node_id":"MDExOlB1bGxSZXF1ZXN0MTgxNzAwMjg0","number":7257,"title":"Fixing yet a source of dependency on alphabetic order in unification.","user":{"login":"herbelin","id":460771,"node_id":"MDQ6VXNlcjQ2MDc3MQ==","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},"labels":[{"id":485985650,"node_id":"MDU6TGFiZWw0ODU5ODU2NTA=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20fix","name":"kind: fix","color":"d93f0b","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":832236574,"node_id":"MDU6TGFiZWw4MzIyMzY1NzQ=","url":"https://api.github.com/repos/coq/coq/labels/part:%20elaboration","name":"part: elaboration","color":"dddddd","default":false},{"id":698064744,"node_id":"MDU6TGFiZWw2OTgwNjQ3NDQ=","url":"https://api.github.com/repos/coq/coq/labels/part:%20tactics","name":"part: tactics","color":"dddddd","default":false},{"id":869900904,"node_id":"MDU6TGFiZWw4Njk5MDA5MDQ=","url":"https://api.github.com/repos/coq/coq/labels/part:%20unification","name":"part: unification","color":"dddddd","default":false}],"state":"open","locked":false,"assignee":{"login":"ppedrot","id":1202327,"node_id":"MDQ6VXNlcjEyMDIzMjc=","avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"assignees":[{"login":"ppedrot","id":1202327,"node_id":"MDQ6VXNlcjEyMDIzMjc=","avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/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":115,"closed_issues":435,"state":"open","created_at":"2017-07-18T15:03:25Z","updated_at":"2018-09-14T08:07:11Z","due_on":null,"closed_at":null},"comments":7,"created_at":"2018-04-15T13:58:26Z","updated_at":"2018-09-14T08:44:54Z","closed_at":null,"author_association":"MEMBER","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/7257","html_url":"https://github.com/coq/coq/pull/7257","diff_url":"https://github.com/coq/coq/pull/7257.diff","patch_url":"https://github.com/coq/coq/pull/7257.patch"},"body":"<!-- Keep what applies -->\r\n**Kind:** bug fix\r\n\r\nFixes #7256, refining c24bcae8 (PR #924) and 6304c843:\r\n- c24bcae8 fixed the order in the heuristic governed by the `choose` flag\r\n- 6304c843 improved the order by preferring projections\r\n\r\nThere remained a dependency in the alphabetic order in selecting unification candidates. This PR fixes it by radically changing the representation of the substitution to invert, using a map indexed on the rank in the signature rather than on the name of the variable. Note that more could be done to use numbers further, e.g. for representing aliases (but not a priority at the moment).\r\n\r\n~~Added note: The fix seems to break things elsewhere. To be investigated.~~ ~~This PR now depends on PR #7274 for the compilation of the test-suite.~~ (Updated 28 July 2018)"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/421276776","html_url":"https://github.com/coq/coq/pull/7257#issuecomment-421276776","issue_url":"https://api.github.com/repos/coq/coq/issues/7257","id":421276776,"node_id":"MDEyOklzc3VlQ29tbWVudDQyMTI3Njc3Ng==","user":{"login":"herbelin","id":460771,"node_id":"MDQ6VXNlcjQ2MDc3MQ==","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-09-14T08:44:54Z","updated_at":"2018-09-14T08:44:54Z","author_association":"MEMBER","body":"@ CI experts: cross-crypto has an instance of unification which depends on the ASCII order, and which this PR fixes. The incompatibility is in the submodule FCF. Is there a way to make an overlay for a submodule or do I need instead to let upstream FCF first merge the (backwards-compatible) [fix](https://github.com/herbelin/fcf/tree/master%2Bfix-coq7257-ascii-sensitive-unification) I made?"}}
{"actor":{"display_login":"herbelin"}}