Skip to content

Commit

Permalink
coqPackages.mathcomp: 1.6.1 -> 1.6.4, for Coq versions 8.6 and 8.7
Browse files Browse the repository at this point in the history
  • Loading branch information
@jwiegley
jwiegley committed Nov 11, 2017
1 parent f1caf10 commit 462b5e0
Showing 1 changed file with 26 additions and 4 deletions.
30 changes: 26 additions & 4 deletions pkgs/development/coq-modules/mathcomp/default.nix
View file
Expand Up @@ -2,10 +2,32 @@

let param =
{
version = "1.6.1";
url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
}; in
"8.4" = {
version = "1.6.1";
url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
};

"8.5" = {
version = "1.6.1";
url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.1.tar.gz;
sha256 = "1j9ylggjzrxz1i2hdl2yhsvmvy5z6l4rprwx7604401080p5sgjw";
};

"8.6" = {
version = "1.6.4";
url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.4.tar.gz;
sha256 = "0qmjjb6jsxmmf4gpw10r30rmrvwqgzirvvgyy41mz2vhgwis8wn6";
};

"8.7" = {
version = "1.6.4";
url = https://github.com/math-comp/math-comp/archive/mathcomp-1.6.4.tar.gz;
sha256 = "0qmjjb6jsxmmf4gpw10r30rmrvwqgzirvvgyy41mz2vhgwis8wn6";
};

}."${coq.coq-version}"
; in

callPackage ./generic.nix {
name = "coq${coq.coq-version}-mathcomp-${param.version}";
Expand Down

3 comments on commit 462b5e0

@vbgl
Copy link
Contributor

@vbgl vbgl commented on 462b5e0 Nov 11, 2017 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@jwiegley It would be nice if the versions of coqPackages.ssreflect and coqPackages.mathcomp were the same.

Also, according to the release notes, version 1.6.4 should work with Coq 8.5.

Also, there are some discussions scattered around PR comments (e.g., #31368); it seems that to avoid unneeded complexity, the legacy and half-broken coqPackages_8_4 attribute set should be removed.

@jwiegley
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@vbgl Indeed. One thing that makes this a bit tricky is that Coq 8.7 now includes ssreflect too.

@Zimmi48
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some people told me that the ssreflect package is more than what Coq ships. But I haven't checked.

Please sign in to comment.