New coq head #26180
New coq head #26180
Conversation
pkgs/top-level/all-packages.nix
Outdated
| @@ -17793,7 +17793,9 @@ with pkgs; | |||
| coq_8_4 = coqPackages_8_4.coq; | |||
| coq_8_5 = coqPackages_8_5.coq; | |||
| coq_8_6 = coqPackages_8_6.coq; | |||
| coq_HEAD = callPackage ../applications/science/logic/coq/HEAD.nix {}; | |||
| coq_HEAD = callPackage ../applications/science/logic/coq { | |||
| version = "8.7pre-2017-05-28"; | |||
There was a problem hiding this comment.
You've been quicker than me :D
There was a problem hiding this comment.
From https://github.com/coq/roadmaps/blob/master/text/roadmap-8.7.md, it is stated that the final version of Coq is scheduled at ~Oct 15 2017, and the current HEAD has yet to reach beta. As there is no tag yet for 8.7, I think the version should still be 8.6-unstable-2017-05-28.
There was a problem hiding this comment.
@rht If there was a tag already I would have used it instead but there is not and this is precisely the point of pre-releases.
Though, if you have a look at the mailing lists such as Coq-Club or Coq-Dev, you'll see that developers are already calling the development version 8.7. More importantly, calling it 8.6-unstable would be plain wrong because the 8.6 branch is still being developed but only regarding bugfixes, while this package really corresponds to what Coq 8.7 will be (modulo a few features still missing - that's why we're not in beta yet - and a lot of bugs to fix).
There was a problem hiding this comment.
@rht This point is especially important given that the coq-version attribute is obtained by taking the first part of the version attribute. Given that there are several breaking changes between 8.6 and this version, one cannot reasonably claim that the coq-version of this snapshot is 8.6.
There was a problem hiding this comment.
Sorry, I meant coq-unstable-2017-05-28 (version is in the date).
I see[1], otherwise it'd be hard to tell if the first rule of Coq-Club were to not talk about pre-release coq-version. I'd say it's still better to wait until the coqdev team have put the 8.7pre tag after (not during) the feature freeze on June 1st.
It is the way a vcs is defined that a repo state can only refer to the previous most-recent repo state, or a checkpoint, rather than a future repo state many commits away from the present.
[1] e.g. https://sympa.inria.fr/sympa/arc/coqdev/2017-05/msg00021.html
There was a problem hiding this comment.
@rht Well, once the tag is put it will be 8.7beta1 not 8.7pre, otherwise I wouldn't have used this here. Moreover, we won't be referring to this new version with variable name coq_HEAD but coq_8_7 (see the history of this derivation).
There was a problem hiding this comment.
For the case of post June 15th, with the 8.7beta1 being added, yes, there will be coq_8_7_beta, but a new snapshot several commits after this tag still resides in coq_HEAD (which is the point of this PR).
For the in-between case, it is not enough to declare a version into a snapshot of a repo when the version hasn't been described in a git tag, only written in a roadmap / spoken unofficially.
e: s|June 15th/June 1st|June 15th| and s|8.7beta1/8.7pre|8.7beta1| because I am not sure if there will be a 8.7pre tag. Besides, the definition of pre-release encompasses the alpha, beta, and rc phase.
There was a problem hiding this comment.
I think citing a version number from a roadmap/mailing-list sounds too manual work, since this has to be parsed by humans rather than having a machine to read a git tag. Package updating is something that is meant to be automated away, and shouldn't be a CAPTCHA/Turing test.
Zimmi48
force-pushed
the
new-coq-head
branch
2 times, most recently
from
c49431f to
e323c86
Compare
|
There were some objections being raised on using a version starting with Now I'd like a proper review on the factoring aspect. Maybe from @jwiegley? |
|
@Zimmi48 I like it! |
|
I think the name of the |
|
@vbgl What do you think of @bjornfor's suggestion in #26173 (comment) to use |
The versions of Coq available through this expression do not actually require camlp5_transitional. We drop this dependency to see if, in the future, the package camlp5_transitional can be removed from nixpkgs.
Motivation for this change
This PR contains one minor unrelated change and one important change, to the Coq derivation definition, so each commit can be reviewed independently.
The main change brought by this PR is to move the definition of
coq_HEADin the file already used forcoq_8_5andcoq_8_6. This has the main advantages of: 1) reducing unnecessary duplication of code, which can btw lead to errors being fixed in one place and not the other 2) make it easier to add new pre-release snapshots in the future.The source is now fetched from GitHub, taking advantage of the versatile archive system allowing to download both commit snapshots and tagged versions in the same way, instead of being fetched from the official download page, but I feel like this shouldn't be a problem because GitHub is the main place of development of Coq anyways (and GitHub endures less down-times than INRIA's website).
Things done
(nix.useSandbox on NixOS,
or option
build-use-sandboxinnix.confon non-NixOS)
nix-shell -p nox --run "nox-review wip"./result/bin/)I tested all the versions of the package which can be built with this file, including the ones that are not included in all-packages.