JakeHillion/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

coq_8_14: init at 8.14+rc1

Browse Source
This commit is contained in:
Théo Zimmermann 2021-09-27 21:52:40 +02:00 committed by Vincent Laporte
parent f9203f09e2
commit 3437b543fd
19 changed files with 37 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
pkgs/applications/science/logic/coq/default.nix
View File

@ -44,6 +44,7 @@ let
"8.13.0".sha256 = "0sjbqmz6qcvnz0hv87xha80qbhvmmyd675wyc5z4rgr34j2l1ymd";
"8.13.1".sha256 = "0xx2ns84mlip9bg2mkahy3pmc5zfcgrjxsviq9yijbzy1r95wf0n";
"8.13.2".sha256 = "1884vbmwmqwn9ngibax6dhnqh4cc02l0s2ajc6jb1xgr0i60whjk";
"8.14+rc1".sha256 = "0jrkgj7c2959dsinw4x7q4ril1x24qq08snl25hgx33ls4sym5zb";
};
releaseRev = v: "V${v}";
fetched = import ../../../../build-support/coq/meta-fetch/default.nix
@ -163,7 +164,7 @@ self = stdenv.mkDerivation {
prefixKey = "-prefix ";
buildFlags = [ "revision" "coq" "coqide" "bin/votour" ];
buildFlags = [ "revision" "coq" "coqide" ] ++ optional (!versionAtLeast "8.14") "bin/votour";
enableParallelBuilding = true;
createFindlibDestdir = true;
@ -177,9 +178,11 @@ self = stdenv.mkDerivation {
categories = "Development;Science;Math;IDE;GTK";
});
postInstall = ''
postInstall = let suffix = if versionAtLeast "8.14" then "-core" else ""; in ''
cp bin/votour $out/bin/
ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq
ln -s $out/lib/coq${suffix} $OCAMLFIND_DESTDIR/coq${suffix}
'' + optionalString (versionAtLeast "8.14") ''
ln -s $out/lib/coqide-server $OCAMLFIND_DESTDIR/coqide-server
'' + optionalString buildIde ''
mkdir -p "$out/share/pixmaps"
ln -s "$out/share/coq/coq.png" "$out/share/pixmaps/"

2
pkgs/development/coq-modules/aac-tactics/default.nix
View File

@ -6,6 +6,7 @@ mkCoqDerivation {
releaseRev = v: "v${v}";
release."8.14.0".sha256 = "04x47ngb95m1h4jw2gl0v79s5im7qimcw7pafc34gkkf51pyhakp";
release."8.13.0".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTY=";
release."8.12.0".sha256 = "sha256-dPNA19kZo/2t3rbyX/R5yfGcaEfMhbm9bo71Uo4ZwoM=";
release."8.11.0".sha256 = "sha256-CKKMiJLltIb38u+ZKwfQh/NlxYawkafp+okY34cGCYU=";
@ -17,6 +18,7 @@ mkCoqDerivation {
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = "8.14"; out = "8.14.0"; }
{ case = "8.13"; out = "8.13.0"; }
{ case = "8.12"; out = "8.12.0"; }
{ case = "8.11"; out = "8.11.0"; }

1
pkgs/development/coq-modules/bignums/default.nix
View File

@ -8,6 +8,7 @@ with lib; mkCoqDerivation {
defaultVersion = if versions.isGe "8.5" coq.coq-version
then "${coq.coq-version}.0" else null;
release."8.14.0".sha256 = "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06";
release."8.13.0".sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y";
release."8.12.0".sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8";
release."8.11.0".sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp";

3
pkgs/development/coq-modules/equations/default.nix
View File

@ -6,6 +6,7 @@ with lib; mkCoqDerivation {
repo = "Coq-Equations";
inherit version;
defaultVersion = switch coq.coq-version [
{ case = "8.14"; out = "1.3-8.14"; }
{ case = "8.13"; out = "1.2.4+coq8.13"; }
{ case = "8.12"; out = "1.2.4+coq8.12"; }
{ case = "8.11"; out = "1.2.4+coq8.11"; }
@ -43,6 +44,8 @@ with lib; mkCoqDerivation {
release."1.2.4+coq8.12".sha256 = "1n0w8is464qcq8mk2mv7amaf0khbjz5mpc9phf0rhpjm0lb22cb3";
release."1.2.4+coq8.13".rev = "v1.2.4-8.13";
release."1.2.4+coq8.13".sha256 = "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q";
release."1.3-8.14".rev = "v1.3-8.14";
release."1.3-8.14".sha256 = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv";
mlPlugin = true;
preBuild = "coq_makefile -f _CoqProject -o Makefile";

4
pkgs/development/coq-modules/fourcolor/default.nix
View File

@ -9,8 +9,8 @@ mkCoqDerivation {
release."1.2.3".sha256 = "sha256-gwKfUa74fIP7j+2eQgnLD7AswjCtOFGHGaIWb4qI0n4=";
inherit version;
defaultVersion = with versions; switch mathcomp.version [
{ case = pred.inter (isGe "1.11.0") (isLt "1.13"); out = "1.2.3"; }
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
{ cases = [ (isLe "8.13") (pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
] null;
propagatedBuildInputs = [ mathcomp.algebra ];

2
pkgs/development/coq-modules/goedel/default.nix
View File

@ -10,7 +10,7 @@ mkCoqDerivation {
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.11"; out = "8.12.0"; }
{ case = range "8.11" "8.13"; out = "8.12.0"; }
] null;
propagatedBuildInputs = [ hydra-battles pocklington ];

2
pkgs/development/coq-modules/graph-theory/default.nix
View File

@ -12,7 +12,7 @@ mkCoqDerivation {
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.13"; out = "0.9"; }
{ case = isEq "8.13"; out = "0.9"; }
] null;
propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap hierarchy-builder ];

4
pkgs/development/coq-modules/hierarchy-builder/default.nix
View File

@ -5,8 +5,8 @@ with lib; mkCoqDerivation {
owner = "math-comp";
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.12"; out = "1.1.0"; }
{ case = range "8.11" "8.12"; out = "0.10.0"; }
{ case = range "8.12" "8.13"; out = "1.1.0"; }
{ case = isEq "8.11"; out = "0.10.0"; }
] null;
release."1.1.0".sha256 = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q=";
release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp";

4
pkgs/development/coq-modules/iris/default.nix
View File

@ -6,8 +6,8 @@ with lib; mkCoqDerivation rec {
owner = "iris";
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.11"; out = "3.4.0"; }
{ case = range "8.9" "8.11"; out = "3.3.0"; }
{ case = range "8.11" "8.13"; out = "3.4.0"; }
{ case = range "8.9" "8.10"; out = "3.3.0"; }
] null;
release."3.4.0".sha256 = "0vdc2mdqn5jjd6yz028c0c6blzrvpl0c7apx6xas7ll60136slrb";
release."3.3.0".sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp";

2
pkgs/development/coq-modules/itauto/default.nix
View File

@ -9,7 +9,7 @@ mkCoqDerivation rec {
release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.13"; out = "8.13+no"; }
{ case = isEq "8.13"; out = "8.13+no"; }
] null;
mlPlugin = true;

2
pkgs/development/coq-modules/multinomials/default.nix
View File

@ -9,7 +9,7 @@ with lib; mkCoqDerivation {
inherit version;
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
{ cases = [ (range "8.10" "8.13") "1.12.0" ]; out = "1.5.4"; }
{ cases = [ (range "8.10" "8.14") "1.12.0" ]; out = "1.5.4"; }
{ cases = [ (range "8.10" "8.12") "1.12.0" ]; out = "1.5.3"; }
{ cases = [ (range "8.7" "8.12") "1.11.0" ]; out = "1.5.2"; }
{ cases = [ (range "8.7" "8.11") (range "1.8" "1.10") ]; out = "1.5.0"; }

4
pkgs/development/coq-modules/paco/default.nix
View File

@ -5,8 +5,8 @@ with lib; mkCoqDerivation {
owner = "snu-sf";
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.6"; out = "4.0.2"; }
{ case = range "8.5" "8.8"; out = "1.2.8"; }
{ case = range "8.6" "8.13"; out = "4.0.2"; }
{ case = isEq "8.5"; out = "1.2.8"; }
] null;
release."4.0.2".sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b";
release."1.2.8".sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb";

2
pkgs/development/coq-modules/parsec/default.nix
View File

@ -11,7 +11,7 @@ mkCoqDerivation {
releaseRev = (v: "v${v}");
inherit version;
defaultVersion = if versions.isGe "8.12" coq.version then "0.1.0" else null;
defaultVersion = if versions.range "8.12" "8.13" coq.version then "0.1.0" else null;
release."0.1.0".sha256 = "sha256:01avfcqirz2b9wjzi9iywbhz9szybpnnj3672dgkfsimyg9jgnsr";
meta = {

2
pkgs/development/coq-modules/reglang/default.nix
View File

@ -10,7 +10,7 @@ mkCoqDerivation {
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = range "8.10" "8.13"; out = "1.1.2"; }
{ case = range "8.10" "8.14"; out = "1.1.2"; }
] null;

10
pkgs/development/coq-modules/relation-algebra/default.nix
View File

@ -15,11 +15,11 @@ mkCoqDerivation {
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.13"; out = "1.7.5"; }
{ case = isGe "8.12"; out = "1.7.4"; }
{ case = isGe "8.11"; out = "1.7.3"; }
{ case = isGe "8.10"; out = "1.7.2"; }
{ case = isGe "8.9"; out = "1.7.1"; }
{ case = isEq "8.13"; out = "1.7.5"; }
{ case = isEq "8.12"; out = "1.7.4"; }
{ case = isEq "8.11"; out = "1.7.3"; }
{ case = isEq "8.10"; out = "1.7.2"; }
{ case = isEq "8.9"; out = "1.7.1"; }
] null;
mlPlugin = true;

3
pkgs/development/coq-modules/semantics/default.nix
View File

@ -15,8 +15,7 @@ mkCoqDerivation rec {
inherit version;
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.13"; out = "8.13.0"; }
{ case = "8.11"; out = "8.11.1"; }
{ case = range "8.10" "8.13"; out = "8.13.0"; }
{ case = "8.9"; out = "8.9.0"; }
{ case = "8.8"; out = "8.8.0"; }
{ case = "8.7"; out = "8.7.0"; }

4
pkgs/development/coq-modules/stdpp/default.nix
View File

@ -6,8 +6,8 @@ with lib; mkCoqDerivation rec {
domain = "gitlab.mpi-sws.org";
owner = "iris";
defaultVersion = with versions; switch coq.coq-version [
{ case = isGe "8.11"; out = "1.5.0"; }
{ case = range "8.8" "8.11"; out = "1.4.0"; }
{ case = range "8.11" "8.13"; out = "1.5.0"; }
{ case = range "8.8" "8.10"; out = "1.4.0"; }
] null;
release."1.5.0".sha256 = "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf";
release."1.4.0".sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r";

1
pkgs/top-level/all-packages.nix
View File

@ -31068,6 +31068,7 @@ with pkgs;
coqPackages_8_11 coq_8_11
coqPackages_8_12 coq_8_12
coqPackages_8_13 coq_8_13
coqPackages_8_14 coq_8_14
coqPackages coq
;

2
pkgs/top-level/coq-packages.nix
View File

@ -131,6 +131,7 @@ in rec {
coq_8_11 = mkCoq "8.11";
coq_8_12 = mkCoq "8.12";
coq_8_13 = mkCoq "8.13";
coq_8_14 = mkCoq "8.14";
coqPackages_8_5 = mkCoqPackages coq_8_5;
coqPackages_8_6 = mkCoqPackages coq_8_6;
@ -141,6 +142,7 @@ in rec {
coqPackages_8_11 = mkCoqPackages coq_8_11;
coqPackages_8_12 = mkCoqPackages coq_8_12;
coqPackages_8_13 = mkCoqPackages coq_8_13;
coqPackages_8_14 = mkCoqPackages coq_8_14;
coqPackages = recurseIntoAttrs coqPackages_8_13;
coq = coqPackages.coq;