coqPackages.coqeal: master, add dependency

[proux01]

In order to include matrix normal forms in CoqEAL (coq-community/coqeal#54) we add a dependency on mathcomp-real-closed for master.

Motivation for this change

Things done

• Built on platform(s)
  • x86_64-linux
  • aarch64-linux
  • x86_64-darwin
  • aarch64-darwin
• For non-Linux: Is sandbox = true set in nix.conf? (See Nix manual)
• Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
• Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review wip"
• Tested execution of all binary files (usually in ./result/bin/)
• 21.11 Release Notes (or backporting 21.05 Release notes)
  • (Package updates) Added a release notes entry if the change is major or breaking
  • (Module updates) Added a release notes entry if the change is significant
  • (Module addition) Added a release notes entry if adding a new NixOS module
• Fits CONTRIBUTING.md.

[proux01]

@cohen of @vbgl I may need your help here

[Zimmi48]

I would tend to disagree with @CohenCyril on the unconditional dependency addition. Here is an example package which adds a dependency depending on the version that is being built: https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/extructures/default.nix

However, instead of using versionAtLeast ..., use lib.versions.isGt "1.0" o.version || o.version == "dev" (assuming that the next version of CoqEAL will be at least 1.1 given the feature addition).

[CohenCyril]

However, instead of using versionAtLeast ..., use lib.versions.isGt "1.0" o.version || o.version == "dev" (assuming that the next version of CoqEAL will be at least 1.1 given the feature addition).

Yes, I just had the problem with it, and I did not have the patience to explain how to solve it. Sorry.
cf https://github.com/math-comp/math-comp/pull/817/files#diff-df12f6cc542a582b603c601e5ecc0a28dc39259b8484f153ee2f181800ebd389

[SuperSandro2000]

Suggested change

	propagatedBuildInputs =
	[ mathcomp.algebra bignums paramcoq multinomials mathcomp-real-closed ];
	propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials mathcomp-real-closed ];

Please use nixpkgs-fmt instead of nix-fmt.

[Zimmi48]

@SuperSandro2000 I'm very much in favor of using an auto-formatter, but could you make sure that this recommendation is documented in the contributing guidelines? For now, there is nothing on Nix formatting in https://github.com/NixOS/nixpkgs/blob/master/CONTRIBUTING.md nor in https://nixos.org/manual/nixpkgs/unstable/#idm140737315817472.

[proux01]

Thanks, done (this changed quite a bit more though)

[proux01]

Thanks @Zimmi48 for the explanation, done

[vbgl]

I believe that dropping the second commit will solve the conflicts…

[proux01]

Let's try that