{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/229","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/229/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/229/comments","events_url":"https://api.github.com/repos/coq/coq/issues/229/events","html_url":"https://github.com/coq/coq/pull/229","id":162905137,"number":229,"title":"Bytecode compilation in a new 'make byte' rule apart from 'make world' ","user":{"login":"letouzey","id":1541597,"avatar_url":"https://avatars.githubusercontent.com/u/1541597?v=3","gravatar_id":"","url":"https://api.github.com/users/letouzey","html_url":"https://github.com/letouzey","followers_url":"https://api.github.com/users/letouzey/followers","following_url":"https://api.github.com/users/letouzey/following{/other_user}","gists_url":"https://api.github.com/users/letouzey/gists{/gist_id}","starred_url":"https://api.github.com/users/letouzey/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/letouzey/subscriptions","organizations_url":"https://api.github.com/users/letouzey/orgs","repos_url":"https://api.github.com/users/letouzey/repos","events_url":"https://api.github.com/users/letouzey/events{/privacy}","received_events_url":"https://api.github.com/users/letouzey/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/coq/coq/labels/8.6","name":"8.6","color":"0e8a16"}],"state":"closed","locked":false,"assignee":{"login":"maximedenes","id":647105,"avatar_url":"https://avatars.githubusercontent.com/u/647105?v=3","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},"assignees":[{"login":"maximedenes","id":647105,"avatar_url":"https://avatars.githubusercontent.com/u/647105?v=3","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}],"milestone":null,"comments":16,"created_at":"2016-06-29T11:44:44Z","updated_at":"2016-07-05T08:28:08Z","closed_at":"2016-07-04T17:55:53Z","pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/229","html_url":"https://github.com/coq/coq/pull/229","diff_url":"https://github.com/coq/coq/pull/229.diff","patch_url":"https://github.com/coq/coq/pull/229.patch"},"body":"Historically, we're accustomed to build coqtop and coqtop.byte in the same 'make world' run. That might be related with our need of the grammar.cma syntax extension, that used to build anyway the byte version of 50% of coq before the other 50% (the .ml4) could even be parsed. This could also be due to the importance of coqtop.byte and Drop for debugging.\r\n\r\nBut mixing the compilation of native code and byte code leads to delicate issues (races between ocamlc and ocamlopt about some .cmi, more details in the first commit message). \r\n\r\nAnd thanks to @ppedrot, grammar.cma is now completely self-contained.\r\n\r\nSo I think it's time to separate 'make world' (compilation of Coq with the best available OCaml compiler) from a distinct 'make byte' rule, dedicated to coqtop.byte and a few other stuff (bytecode plugins, printers.cma,...). More details in the message of the first commit. In everyday life, the main effect will be to compile with something like : \r\n `make -j && make -j byte`\r\nAnd then possibly: `make install install-byte`\r\nPlease do **not** use the shortcut `make -j world byte` that suffer from the races and crashes mentioned earlier.\r\nIn the second commit, I made corresponding changes to coq_makefile.\r\nBest\r\nPierre"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/230417169","html_url":"https://github.com/coq/coq/pull/229#issuecomment-230417169","issue_url":"https://api.github.com/repos/coq/coq/issues/229","id":230417169,"user":{"login":"silene","id":1674458,"avatar_url":"https://avatars.githubusercontent.com/u/1674458?v=3","gravatar_id":"","url":"https://api.github.com/users/silene","html_url":"https://github.com/silene","followers_url":"https://api.github.com/users/silene/followers","following_url":"https://api.github.com/users/silene/following{/other_user}","gists_url":"https://api.github.com/users/silene/gists{/gist_id}","starred_url":"https://api.github.com/users/silene/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/silene/subscriptions","organizations_url":"https://api.github.com/users/silene/orgs","repos_url":"https://api.github.com/users/silene/repos","events_url":"https://api.github.com/users/silene/events{/privacy}","received_events_url":"https://api.github.com/users/silene/received_events","type":"User","site_admin":false},"created_at":"2016-07-05T08:28:08Z","updated_at":"2016-07-05T08:28:08Z","body":"Note that it is superior but not that much: the way we wrote the Makefile in Why3 fixes the race condition, but it does so by making the bytecode compilation kind of mandatory (for some of the files). Indeed, unless the user were to say so at configure time, we have no way to predict that the user will never perform a bytecode compilation later on, so we have to always account for this possibility. (Fortunately, bytecode compilation is fast enough, so it goes unnoticed when you are not looking at the messages the build process is spewing.)"}}
{"actor":{"display_login":"silene"}}