coqPackages: refactor #105877

CohenCyril · 2020-12-04T13:07:23Z

Motivation for this change

Use a mkCoqDerivation function to refactor Coq packages derivations.
This smart builder also allows for easier overriding of the source of the derivation.
See the documentation for more details.

Things done

CohenCyril · 2020-12-11T04:01:06Z

@GrahamcOfBorg build coqPackages coqPackages_8_10 coqPackages_8_12

CohenCyril · 2020-12-11T04:17:44Z

@GrahamcOfBorg build coqPackages coqPackages_8_10 coqPackages_8_12

CohenCyril · 2020-12-12T04:47:02Z

@GrahamcOfBorg build coqPackages coqPackages_8_10 coqPackages_8_12

CohenCyril · 2020-12-12T12:25:07Z

@vbgl @Zimmi48 this is ready modulo the doc.

CohenCyril · 2021-01-07T15:43:56Z

@GrahamcOfBorg build coqPackages.Cheerios coqPackages.CoLoR coqPackages.InfSeqExt coqPackages.QuickChick coqPackages.StructTact coqPackages.Verdi coqPackages.bignums coqPackages.contribs coqPackages.coq coqPackages.coq-bits coqPackages.coq-elpi coqPackages.coq-ext-lib coqPackages.coqeal coqPackages.coqhammer coqPackages.coqprime coqPackages.coquelicot coqPackages.dpdgraph coqPackages.equations coqPackages.flocq coqPackages.gappalib coqPackages.hierarchy-builder coqPackages.interval coqPackages.iris coqPackages.math-classes coqPackages.mathcomp coqPackages.mathcomp-algebra coqPackages.mathcomp-analysis coqPackages.mathcomp-bigenough coqPackages.mathcomp-character coqPackages.mathcomp-field coqPackages.mathcomp-fingroup coqPackages.mathcomp-finmap coqPackages.mathcomp-real-closed coqPackages.mathcomp-solvable coqPackages.mathcomp-ssreflect coqPackages.metalib coqPackages.multinomials coqPackages.paco coqPackages.paramcoq coqPackages.simple-io coqPackages.ssreflect coqPackages.stdpp coqPackages.tlc

CohenCyril · 2021-01-07T15:47:51Z

There is a left-over comment around the github fetcher.
The changes in this PR should be squashed into a single commit.
And then we are good to go!

@vbgl Done, can you double check if I did what you meant?

vbgl · 2021-01-07T16:37:47Z

pkgs/applications/science/logic/coq/default.nix

    "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt";
  csdpPatch = if csdp != null then ''
    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
  '' else "";
+  ocamlPackages = if isNull (args.ocamlPackages or null) then args.ocamlPackages else


I don’t understand this line.

The mkCoq function below always set the ocamlPackages argument, so it is not null, therefore it is ignored and the default ocamlPackages set is computed depending on coq-version.

Suggestion: move the logic for computing the right version of OCaml out of the coq derivation (it thus becomes straightforward to overwrite).

The mkCoq function makes a call to callPackage ../applications/science/logic/coq which leaves out coqPackages indeed, but callPackage provides the ability to override the arguments and hence one can write coq.override {ocamlPackages = whatever;} to change the version of ocaml used by Coq.

oh, I did two mistakes that cancel each other, sorry! And well spot!
I'll push a fix asap.

I fixed my mistake and documented the new instructions... which are using an attribute customOcamlPackages.

https://github.com/NixOS/nixpkgs/blob/14ee56c849763beafce003258fa7ce2ba9512599/doc/languages-frameworks/coq.section.md

I feel like you are inventing yet an other overriding mechanism. I’m glad you did not duplicate all parameters (make & customMake, etc.). But I won’t argue against it.

Thanks for the fix nonetheless.

There are two reasons combined that made me duplicate this predicate that would not possibly make me duplicate any other. 1. it's a scoped argument, which is passed implicitly by callPackage, so I cannot prevent it from being always set whereas I wanted it to be optional. 2. it's the only argument that is both a derivation and needs to change depending on the Coq version.

I don't see how this is yet another overriding mechanism, I'm merly reusing .override provided by callPackage.

Do you see another solution that would make it possible to have the following two derivation build correctly:

coq.override {version = "8.10"};

coq.override {version = "d370a9d1328a4e1cdb9d02ee032f605a9d94ec7a"; customOcamlPackages = ocaml-ng.ocamlPackages_4_09;};

Now I tried those two commands, I realize that the second one does not work anymore since I started using fetchzip everywhere. See my next comment.

What I meant about this overriding scheme being ad-hoc, is that there is an argument whose only purpose is overriding. Notice that now there are two ways to override the ocamlPackages set: either by setting customOCamlPackages or by overriding, say, ocamlPackages_4_10.

CohenCyril · 2021-01-07T18:24:08Z

@GrahamcOfBorg build coqPackages.Cheerios coqPackages.CoLoR coqPackages.InfSeqExt coqPackages.QuickChick coqPackages.StructTact coqPackages.Verdi coqPackages.bignums coqPackages.contribs coqPackages.coq coqPackages.coq-bits coqPackages.coq-elpi coqPackages.coq-ext-lib coqPackages.coqeal coqPackages.coqhammer coqPackages.coqprime coqPackages.coquelicot coqPackages.dpdgraph coqPackages.equations coqPackages.flocq coqPackages.gappalib coqPackages.hierarchy-builder coqPackages.interval coqPackages.iris coqPackages.math-classes coqPackages.mathcomp coqPackages.mathcomp-algebra coqPackages.mathcomp-analysis coqPackages.mathcomp-bigenough coqPackages.mathcomp-character coqPackages.mathcomp-field coqPackages.mathcomp-fingroup coqPackages.mathcomp-finmap coqPackages.mathcomp-real-closed coqPackages.mathcomp-solvable coqPackages.mathcomp-ssreflect coqPackages.metalib coqPackages.multinomials coqPackages.paco coqPackages.paramcoq coqPackages.simple-io coqPackages.ssreflect coqPackages.stdpp coqPackages.tlc

CohenCyril · 2021-01-07T18:28:20Z

@GrahamcOfBorg build coqPackages_8_10 coqPackages_8_12 coqPackages_8_13

doc/languages-frameworks/coq.section.md

CohenCyril · 2021-01-08T01:57:25Z

@GrahamcOfBorg build coqPackages.Cheerios coqPackages.CoLoR coqPackages.InfSeqExt coqPackages.QuickChick coqPackages.StructTact coqPackages.Verdi coqPackages.bignums coqPackages.contribs coqPackages.coq coqPackages.coq-bits coqPackages.coq-elpi coqPackages.coq-ext-lib coqPackages.coqeal coqPackages.coqhammer coqPackages.coqprime coqPackages.coquelicot coqPackages.dpdgraph coqPackages.equations coqPackages.flocq coqPackages.gappalib coqPackages.hierarchy-builder coqPackages.interval coqPackages.iris coqPackages.math-classes coqPackages.mathcomp coqPackages.mathcomp-algebra coqPackages.mathcomp-analysis coqPackages.mathcomp-bigenough coqPackages.mathcomp-character coqPackages.mathcomp-field coqPackages.mathcomp-fingroup coqPackages.mathcomp-finmap coqPackages.mathcomp-real-closed coqPackages.mathcomp-solvable coqPackages.mathcomp-ssreflect coqPackages.metalib coqPackages.multinomials coqPackages.paco coqPackages.paramcoq coqPackages.simple-io coqPackages.ssreflect coqPackages.stdpp coqPackages.tlc

CohenCyril · 2021-01-08T01:57:40Z

@GrahamcOfBorg build coqPackages_8_10 coqPackages_8_12 coqPackages_8_13

pkgs/applications/science/logic/coq/default.nix

CohenCyril · 2021-01-08T15:09:01Z

Since I started using fetchzip everywhere, I lost the ability to fetch arbitrary sources without providing a hash, for unreleased versions. There are two ways I could fix this:

for unreleased versions, revert to fetchTarball in the default fetcher, which supports downloads without hashes,
make it necessary to provide a hash even for unreleased version, using e.g.

   mathcomp.override {version = "#682"; sha256 = "<the sha256>";}

but this comes with extra burden for the casual users since there will be no more easy setups mentioning only a branch...

@vbgl and @Zimmi48 what do you think? Do you see other solutions?

EDIT: I opted for 1. in a quite compact way, we'll see what comes out of this...

CohenCyril · 2021-01-08T18:02:54Z

@GrahamcOfBorg build coqPackages.Cheerios coqPackages.CoLoR coqPackages.InfSeqExt coqPackages.QuickChick coqPackages.StructTact coqPackages.Verdi coqPackages.bignums coqPackages.contribs coqPackages.coq coqPackages.coq-bits coqPackages.coq-elpi coqPackages.coq-ext-lib coqPackages.coqeal coqPackages.coqhammer coqPackages.coqprime coqPackages.coquelicot coqPackages.dpdgraph coqPackages.equations coqPackages.flocq coqPackages.gappalib coqPackages.hierarchy-builder coqPackages.interval coqPackages.iris coqPackages.math-classes coqPackages.mathcomp coqPackages.mathcomp-algebra coqPackages.mathcomp-analysis coqPackages.mathcomp-bigenough coqPackages.mathcomp-character coqPackages.mathcomp-field coqPackages.mathcomp-fingroup coqPackages.mathcomp-finmap coqPackages.mathcomp-real-closed coqPackages.mathcomp-solvable coqPackages.mathcomp-ssreflect coqPackages.metalib coqPackages.multinomials coqPackages.paco coqPackages.paramcoq coqPackages.simple-io coqPackages.ssreflect coqPackages.stdpp coqPackages.tlc

CohenCyril · 2021-01-08T18:03:04Z

@GrahamcOfBorg build coqPackages_8_10 coqPackages_8_12 coqPackages_8_13

Zimmi48 · 2021-01-08T21:34:21Z

I'm definitely in favor of option 1, i.e. not making the hash compulsory. However, I missed the reason why you didn't use fetchTarball for everything.

CohenCyril · 2021-01-08T23:32:21Z

I'm definitely in favor of option 1, i.e. not making the hash compulsory. However, I missed the reason why you didn't use fetchTarball for everything.

@Zimmi48 cf #105877 (comment) and subsequent discussion
fetchTarball prevents evaluation by GrahamcOfBorg for some reason.

CohenCyril · 2021-01-08T23:33:53Z

@vbgl I guess everything should be solved now...

siraben · 2021-01-10T07:56:26Z

It appears that it is not rendering correctly in the generated documentation (huge wall of text rather than being a list), https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq

ofborg bot added 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux labels Dec 4, 2020

CohenCyril force-pushed the mathcomp_refactoring branch from dafb736 to f945d78 Compare December 4, 2020 17:24

CohenCyril changed the title ~~Mathcomp refactoring~~ coqPackages refactoring Dec 5, 2020

ofborg bot added the 2.status: merge conflict This PR has merge conflicts with the target branch label Dec 5, 2020

vbgl added the 6.topic: coq "A formal proof management system" label Dec 5, 2020

CohenCyril force-pushed the mathcomp_refactoring branch 3 times, most recently from 2602d63 to 8f4db8c Compare December 9, 2020 03:31

vbgl mentioned this pull request Dec 9, 2020

coq_8_13: init at 8.13+β1 #106427

Merged

10 tasks

CohenCyril force-pushed the mathcomp_refactoring branch 4 times, most recently from 5bf33fa to 82015e8 Compare December 10, 2020 12:58

CohenCyril force-pushed the mathcomp_refactoring branch 3 times, most recently from ca77b6e to d19ecc9 Compare December 11, 2020 04:00

CohenCyril force-pushed the mathcomp_refactoring branch from d19ecc9 to cef1d2d Compare December 11, 2020 04:05

CohenCyril force-pushed the mathcomp_refactoring branch from b7fbfc0 to ac573b1 Compare December 12, 2020 04:46

This comment has been minimized.

Sign in to view

CohenCyril changed the title ~~coqPackages refactoring~~ coqPackages: refactor Jan 7, 2021

ofborg bot requested a review from vbgl January 7, 2021 16:14

vbgl reviewed Jan 7, 2021

View reviewed changes

CohenCyril force-pushed the mathcomp_refactoring branch 2 times, most recently from 8c83d77 to 14ee56c Compare January 7, 2021 18:18

ofborg bot requested a review from vbgl January 7, 2021 18:44

Zimmi48 reviewed Jan 7, 2021

View reviewed changes

doc/languages-frameworks/coq.section.md Outdated Show resolved Hide resolved

CohenCyril force-pushed the mathcomp_refactoring branch from 14ee56c to c958992 Compare January 8, 2021 01:57

ofborg bot requested a review from Zimmi48 January 8, 2021 02:06

vbgl reviewed Jan 8, 2021

View reviewed changes

pkgs/applications/science/logic/coq/default.nix Outdated Show resolved Hide resolved

pkgs/applications/science/logic/coq/default.nix Outdated Show resolved Hide resolved

coqPackages: refactor

90b7ca2

CohenCyril force-pushed the mathcomp_refactoring branch from c958992 to 90b7ca2 Compare January 8, 2021 18:02

ofborg bot requested a review from vbgl January 8, 2021 18:11

vbgl merged commit 9ffd16b into NixOS:master Jan 9, 2021

CohenCyril mentioned this pull request Jan 10, 2021

coqPackages: doc #108937

Merged

10 tasks

SkySkimmer mentioned this pull request Sep 23, 2021

coq_8_14: init at 8.14+rc1 #138274

Merged

12 tasks

Zimmi48 mentioned this pull request Feb 14, 2022

Coq master builds fail using the simple CI workflow coq-community/coq-nix-toolbox#95

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

coqPackages: refactor #105877

coqPackages: refactor #105877

CohenCyril commented Dec 4, 2020 •

edited

Loading

CohenCyril commented Dec 11, 2020

CohenCyril commented Dec 11, 2020

CohenCyril commented Dec 12, 2020

CohenCyril commented Dec 12, 2020 •

edited

Loading

This comment has been minimized.

CohenCyril commented Jan 7, 2021

CohenCyril commented Jan 7, 2021 •

edited

Loading

vbgl Jan 7, 2021

CohenCyril Jan 7, 2021 •

edited

Loading

CohenCyril Jan 7, 2021

CohenCyril Jan 7, 2021

CohenCyril Jan 7, 2021

vbgl Jan 8, 2021

CohenCyril Jan 8, 2021 •

edited

Loading

vbgl Jan 9, 2021

CohenCyril commented Jan 7, 2021

CohenCyril commented Jan 7, 2021

CohenCyril commented Jan 8, 2021

CohenCyril commented Jan 8, 2021

CohenCyril commented Jan 8, 2021 •

edited

Loading

CohenCyril commented Jan 8, 2021

CohenCyril commented Jan 8, 2021

Zimmi48 commented Jan 8, 2021

CohenCyril commented Jan 8, 2021 •

edited

Loading

CohenCyril commented Jan 8, 2021

siraben commented Jan 10, 2021

coqPackages: refactor #105877

coqPackages: refactor #105877

Conversation

CohenCyril commented Dec 4, 2020 • edited Loading

Motivation for this change

Things done

CohenCyril commented Dec 11, 2020

CohenCyril commented Dec 11, 2020

CohenCyril commented Dec 12, 2020

CohenCyril commented Dec 12, 2020 • edited Loading

This comment has been minimized.

CohenCyril commented Jan 7, 2021

CohenCyril commented Jan 7, 2021 • edited Loading

vbgl Jan 7, 2021

Choose a reason for hiding this comment

CohenCyril Jan 7, 2021 • edited Loading

Choose a reason for hiding this comment

CohenCyril Jan 7, 2021

Choose a reason for hiding this comment

CohenCyril Jan 7, 2021

Choose a reason for hiding this comment

CohenCyril Jan 7, 2021

Choose a reason for hiding this comment

vbgl Jan 8, 2021

Choose a reason for hiding this comment

CohenCyril Jan 8, 2021 • edited Loading

Choose a reason for hiding this comment

vbgl Jan 9, 2021

Choose a reason for hiding this comment

CohenCyril commented Jan 7, 2021

CohenCyril commented Jan 7, 2021

CohenCyril commented Jan 8, 2021

CohenCyril commented Jan 8, 2021

CohenCyril commented Jan 8, 2021 • edited Loading

CohenCyril commented Jan 8, 2021

CohenCyril commented Jan 8, 2021

Zimmi48 commented Jan 8, 2021

CohenCyril commented Jan 8, 2021 • edited Loading

CohenCyril commented Jan 8, 2021

siraben commented Jan 10, 2021

CohenCyril commented Dec 4, 2020 •

edited

Loading

CohenCyril commented Dec 12, 2020 •

edited

Loading

CohenCyril commented Jan 7, 2021 •

edited

Loading

CohenCyril Jan 7, 2021 •

edited

Loading

CohenCyril Jan 8, 2021 •

edited

Loading

CohenCyril commented Jan 8, 2021 •

edited

Loading

CohenCyril commented Jan 8, 2021 •

edited

Loading