New coq head #26180

Zimmi48 · 2017-05-28T13:26:12Z

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_HEAD in the file already used for coq_8_5 and coq_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

Tested using sandboxing
(nix.useSandbox on NixOS,
or option build-use-sandbox in nix.conf
on non-NixOS)
Built on platform(s)
- NixOS
- macOS
- Linux
Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
Tested execution of all binary files (usually in ./result/bin/)
Fits CONTRIBUTING.md.

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.

mention-bot · 2017-05-28T13:26:14Z

@Zimmi48, thanks for your PR! By analyzing the history of the files in this pull request, we identified @jwiegley, @vbgl and @rht to be potential reviewers.

FRidh · 2017-05-28T13:31:22Z

pkgs/top-level/all-packages.nix

@@ -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";


#26108 and #26173

You've been quicker than me :D

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.

@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).

@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.

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

@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).

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.

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 · 2017-06-01T21:00:41Z

There were some objections being raised on using a version starting with 8.7pre as no 8.7 version of Coq has been released yet. So I've followed @bjornfor's suggestion in #26173 to use a version number based on git describe. For the coq-version attribute, since I think it would be wrong to use 8.6, I put trunk which is in fact the version info that Coq provides for this version (because it is the development branch).

Now I'd like a proper review on the factoring aspect. Maybe from @jwiegley?

jwiegley · 2017-06-02T06:59:45Z

@Zimmi48 I like it!

vbgl · 2017-06-02T07:49:49Z

I think the name of the coq_HEAD package should be different (the manual and current practice suggest coq-git or coq-unstable). Otherwise, update commands like nix-env -u will propose to install coq_HEAD instead of coq.

Zimmi48 · 2017-06-02T08:02:54Z

@vbgl What do you think of @bjornfor's suggestion in #26173 (comment) to use lowPrio?

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.

Zimmi48 · 2017-06-06T13:05:14Z

I don't want to delay uselessly this PR on naming issues so I went back to the conventional naming as dictated in the manual.

@jwiegley @vbgl Feel free to merge. I don't think there is any issue left to discuss.

Zimmi48 force-pushed the new-coq-head branch from 5780614 to 65ebec7 Compare May 28, 2017 13:29

FRidh reviewed May 28, 2017

View reviewed changes

Zimmi48 force-pushed the new-coq-head branch 2 times, most recently from c49431f to e323c86 Compare June 1, 2017 20:55

Zimmi48 force-pushed the new-coq-head branch from e323c86 to 02bdb1b Compare June 2, 2017 07:45

Zimmi48 added 3 commits June 6, 2017 14:59

coq: use camlp5_strict

4783b69

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.

coq: adding myself to the maintainers

4c93f23

coq_HEAD: derivation using coq/default.nix

1d02726

Zimmi48 force-pushed the new-coq-head branch from 02bdb1b to 1d02726 Compare June 6, 2017 12:59

Zimmi48 closed this Jun 21, 2017

Zimmi48 deleted the new-coq-head branch January 5, 2018 13:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New coq head #26180

New coq head #26180

Zimmi48 commented May 28, 2017 •

edited

mention-bot commented May 28, 2017

FRidh May 28, 2017

Zimmi48 May 28, 2017

rht May 29, 2017 •

edited

Zimmi48 May 29, 2017

Zimmi48 May 29, 2017

rht May 30, 2017

Zimmi48 May 30, 2017

rht May 30, 2017 •

edited

rht May 30, 2017 •

edited

Zimmi48 commented Jun 1, 2017

jwiegley commented Jun 2, 2017

vbgl commented Jun 2, 2017

Zimmi48 commented Jun 2, 2017

Zimmi48 commented Jun 6, 2017

New coq head #26180

New coq head #26180

Conversation

Zimmi48 commented May 28, 2017 • edited

Motivation for this change

Things done

mention-bot commented May 28, 2017

FRidh May 28, 2017

Choose a reason for hiding this comment

Zimmi48 May 28, 2017

Choose a reason for hiding this comment

rht May 29, 2017 • edited

Choose a reason for hiding this comment

Zimmi48 May 29, 2017

Choose a reason for hiding this comment

Zimmi48 May 29, 2017

Choose a reason for hiding this comment

rht May 30, 2017

Choose a reason for hiding this comment

Zimmi48 May 30, 2017

Choose a reason for hiding this comment

rht May 30, 2017 • edited

Choose a reason for hiding this comment

rht May 30, 2017 • edited

Choose a reason for hiding this comment

Zimmi48 commented Jun 1, 2017

jwiegley commented Jun 2, 2017

vbgl commented Jun 2, 2017

Zimmi48 commented Jun 2, 2017

Zimmi48 commented Jun 6, 2017

Zimmi48 commented May 28, 2017 •

edited

rht May 29, 2017 •

edited

rht May 30, 2017 •

edited

rht May 30, 2017 •

edited