diff options
Diffstat (limited to 'pkgs/development/coq-modules')
30 files changed, 77 insertions, 51 deletions
diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix index 46738343431a9..24a7f125599dc 100644 --- a/pkgs/development/coq-modules/CoLoR/default.nix +++ b/pkgs/development/coq-modules/CoLoR/default.nix @@ -23,7 +23,7 @@ with lib; mkCoqDerivation { enableParallelBuilding = false; meta = { - homepage = "http://color.inria.fr/"; + homepage = "https://github.com/fblanqui/color"; description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant."; maintainers = with maintainers; [ jpas jwiegley ]; }; diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/coq-modules/ITree/default.nix index 1ba8080e0b10f..2f7437fd74fd5 100644 --- a/pkgs/development/coq-modules/ITree/default.nix +++ b/pkgs/development/coq-modules/ITree/default.nix @@ -5,7 +5,7 @@ with lib; mkCoqDerivation rec { owner = "DeepSpec"; inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.10" "8.14"; out = "4.0.0"; } + { case = range "8.10" "8.15"; out = "4.0.0"; } ] null; release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm"; releaseRev = v: "${v}"; diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix index 1d2a1a3c05fc8..80aaf506139bb 100644 --- a/pkgs/development/coq-modules/VST/default.nix +++ b/pkgs/development/coq-modules/VST/default.nix @@ -1,5 +1,7 @@ { lib, mkCoqDerivation, coq, compcert, ITree, version ? null }: +with lib; + # A few modules that are not built and installed by default # but that may be useful to some users. # They depend on ITree. @@ -7,12 +9,15 @@ let extra_floyd_files = [ "ASTsize.v" "io_events.v" "powerlater.v" - "printf.v" + ] + # floyd/printf.v is broken in VST 2.9 + ++ optional (!versions.isGe "8.13" coq.coq-version) "printf.v" + ++ [ "quickprogram.v" ]; in -with lib; mkCoqDerivation { +mkCoqDerivation { pname = "coq${coq.coq-version}-VST"; namePrefix = []; displayVersion = { coq = false; }; @@ -20,8 +25,10 @@ with lib; mkCoqDerivation { repo = "VST"; inherit version; defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.13" "8.15"; out = "2.9"; } { case = range "8.12" "8.13"; out = "2.8"; } ] null; + release."2.9".sha256 = "sha256:1adwzbl1pprrrwrm7cm493098fizxanxpv7nyfbvwdhgbhcnv6qf"; release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0="; releaseRev = v: "v${v}"; extraBuildInputs = [ ITree ]; diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix index 9757b3e43c8ba..197f1a96fc4a2 100644 --- a/pkgs/development/coq-modules/compcert/default.nix +++ b/pkgs/development/coq-modules/compcert/default.nix @@ -16,7 +16,8 @@ let compcert = mkCoqDerivation rec { defaultVersion = with versions; switch coq.version [ { case = range "8.8" "8.11"; out = "3.8"; } - { case = range "8.12" "8.14"; out = "3.10"; } + { case = isEq "8.12" ; out = "3.9"; } + { case = range "8.12" "8.15"; out = "3.10"; } ] null; release = { @@ -106,13 +107,18 @@ compcert.overrideAttrs (o: }) ]; } - { cases = [ (isEq "8.14") "3.10" ]; + { cases = [ (range "8.14" "8.15") "3.10" ]; out = [ # Support for Coq 8.14.1 (fetchpatch { url = "https://github.com/AbsInt/CompCert/commit/a79f0f99831aa0b0742bf7cce459cc9353bd7cd0.patch"; sha256 = "sha256:0g20x8gfzvplpad9y9vr1p33k6qv6rsp691x6687v9ffvz7zsz94"; }) + # Support for Coq 8.15.0 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/a882f78c069f7337dd9f4abff117d4df98ef38a6.patch"; + sha256 = "sha256:16i87s608fj9ni7cvd5wrd7gicqniad7w78wi26pxdy0pacl7bjg"; + }) ]; } ] []; diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index 9adcbaaa8c75d..c4055648c5a90 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -6,6 +6,7 @@ with builtins; with lib; let { case = "8.12"; out = { version = "1.12.0"; };} { case = "8.13"; out = { version = "1.13.7"; };} { case = "8.14"; out = { version = "1.13.7"; };} + { case = "8.15"; out = { version = "1.14.1"; };} ] {}); in mkCoqDerivation { pname = "elpi"; @@ -13,11 +14,14 @@ in mkCoqDerivation { owner = "LPCIC"; inherit version; defaultVersion = lib.switch coq.coq-version [ + { case = "8.15"; out = "1.13.0"; } { case = "8.14"; out = "1.11.2"; } { case = "8.13"; out = "1.11.1"; } { case = "8.12"; out = "1.8.3_8.12"; } { case = "8.11"; out = "1.6.3_8.11"; } ] null; + release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n"; + release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY="; release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4"; release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc"; release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk"; diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix index 410e585dce8eb..a6e535e01d86f 100644 --- a/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -5,13 +5,15 @@ with lib; mkCoqDerivation rec { owner = "coq-ext-lib"; inherit version; defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.8" "8.15"; out = "0.11.6"; } { case = range "8.8" "8.14"; out = "0.11.4"; } { case = range "8.8" "8.13"; out = "0.11.3"; } { case = "8.7"; out = "0.9.7"; } { case = "8.6"; out = "0.9.5"; } { case = "8.5"; out = "0.9.4"; } ] null; - release."0.11.4".sha256 = "sha256:0yp8mhrhkc498nblvhq1x4j6i9aiidkjza4wzvrkp9p8rgx5g5y3"; + release."0.11.6".sha256 = "0w6iyrdszz7zc8kaybhy3mwjain2d2f83q79xfd5di0hgdayh7q7"; + release."0.11.4".sha256 = "0yp8mhrhkc498nblvhq1x4j6i9aiidkjza4wzvrkp9p8rgx5g5y3"; release."0.11.3".sha256 = "1w99nzpk72lffxis97k235axss5lmzhy5z3lga2i0si95mbpil42"; release."0.11.2".sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; release."0.10.3".sha256 = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb"; diff --git a/pkgs/development/coq-modules/coq-record-update/default.nix b/pkgs/development/coq-modules/coq-record-update/default.nix index 7c9ee2dca646c..a95f4f6154438 100644 --- a/pkgs/development/coq-modules/coq-record-update/default.nix +++ b/pkgs/development/coq-modules/coq-record-update/default.nix @@ -5,10 +5,11 @@ with lib; mkCoqDerivation rec { owner = "tchajed"; inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.10" "8.14"; out = "0.3.0"; } + { case = range "8.10" "8.15"; out = "0.3.0"; } ] null; release."0.3.0".sha256 = "1ffr21dd6hy19gxnvcd4if2450iksvglvkd6q5713fajd72hmc0z"; releaseRev = v: "v${v}"; + buildFlags = "NO_TEST=1"; meta = { description = "Library to create Coq record update functions"; maintainers = with maintainers; [ ineol ]; diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix index cbbddefffffea..3b8b23618d232 100644 --- a/pkgs/development/coq-modules/coqeal/default.nix +++ b/pkgs/development/coq-modules/coqeal/default.nix @@ -10,7 +10,7 @@ with lib; inherit version; defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.10" "8.14") (isGe "1.12.0") ]; out = "1.1.0"; } + { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.1.0"; } { cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; } { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.0.4"; } { cases = [ (isGe "8.7") "1.10.0" ]; out = "1.0.3"; } diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/coq-modules/corn/default.nix index ee4a39dbd5e54..d3ac8332c11bb 100644 --- a/pkgs/development/coq-modules/corn/default.nix +++ b/pkgs/development/coq-modules/corn/default.nix @@ -5,7 +5,7 @@ with lib; mkCoqDerivation rec { inherit version; defaultVersion = switch coq.coq-version [ { case = "8.6"; out = "8.8.1"; } - { case = (versions.range "8.7" "8.13"); out = "8.13.0"; } + { case = (versions.range "8.7" "8.15"); out = "8.13.0"; } ] null; release = { "8.8.1".sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp"; diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix index 5f5723870938b..9d823c0bf9e6d 100644 --- a/pkgs/development/coq-modules/deriving/default.nix +++ b/pkgs/development/coq-modules/deriving/default.nix @@ -9,7 +9,7 @@ mkCoqDerivation { inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.11" "8.14"; out = "0.1.0"; } + { case = range "8.11" "8.15"; out = "0.1.0"; } ] null; releaseRev = v: "v${v}"; diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix index d8d189ed5c196..82fb6c536d386 100644 --- a/pkgs/development/coq-modules/dpdgraph/default.nix +++ b/pkgs/development/coq-modules/dpdgraph/default.nix @@ -9,6 +9,7 @@ mkCoqDerivation { repo = "coq-dpdgraph"; inherit version; defaultVersion = switch coq.coq-version [ + { case = "8.15"; out = "1.0+8.15"; } { case = "8.14"; out = "1.0+8.14"; } { case = "8.13"; out = "1.0+8.13"; } { case = "8.12"; out = "0.6.8"; } @@ -21,6 +22,7 @@ mkCoqDerivation { { case = "8.5"; out = "0.6"; } ] null; + release."1.0+8.15".sha256 = "sha256:1pxr0gakcz297y8hhrnssv5j07ccd58pv7rh7qv5g7855pfqrkg7"; release."1.0+8.14".sha256 = "sha256:01pmi7jcc77431jii6x6nd4m8jg4vycachiyi1h6dx9rp3a2508s"; release."1.0+8.13".sha256 = "sha256:0f8lj8b99n8nsq2jf5m0snblfs8yz50hmlqqq9nlw4qklq7j4z5z"; release."0.6.9".sha256 = "11mbydpcgk7y8pqzickbzx0ig7g9k9al71i9yfrcscd2xj8fwj8z"; diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix index f563d1728744c..16b358b737795 100644 --- a/pkgs/development/coq-modules/equations/default.nix +++ b/pkgs/development/coq-modules/equations/default.nix @@ -6,8 +6,9 @@ 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.3-8.13"; } + { case = "8.15"; out = "1.3+8.15"; } + { case = "8.14"; out = "1.3+8.14"; } + { case = "8.13"; out = "1.3+8.13"; } { case = "8.12"; out = "1.2.4+coq8.12"; } { case = "8.11"; out = "1.2.4+coq8.11"; } { case = "8.10"; out = "1.2.1+coq8.10-2"; } @@ -44,10 +45,12 @@ 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.13".rev = "v1.3-8.13"; - release."1.3-8.13".sha256 = "1jwjbkkkk4bwf6pz4zzz8fy5bb17aqyf4smkja59rgj9ya6nrdhg"; - release."1.3-8.14".rev = "v1.3-8.14"; - release."1.3-8.14".sha256 = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv"; + release."1.3+8.13".rev = "v1.3-8.13"; + release."1.3+8.13".sha256 = "1jwjbkkkk4bwf6pz4zzz8fy5bb17aqyf4smkja59rgj9ya6nrdhg"; + release."1.3+8.14".rev = "v1.3-8.14"; + release."1.3+8.14".sha256 = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv"; + release."1.3+8.15".rev = "v1.3-8.15"; + release."1.3+8.15".sha256 = "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k"; mlPlugin = true; preBuild = "coq_makefile -f _CoqProject -o Makefile"; diff --git a/pkgs/development/coq-modules/extructures/default.nix b/pkgs/development/coq-modules/extructures/default.nix index c78c6ca03fc34..58c6caa9e6ff6 100644 --- a/pkgs/development/coq-modules/extructures/default.nix +++ b/pkgs/development/coq-modules/extructures/default.nix @@ -10,12 +10,14 @@ with lib; inherit version; defaultVersion = with versions; switch [coq.coq-version ssreflect.version] [ + { cases = [(isGe "8.11") (isGe "1.12.0") ]; out = "0.3.1"; } { cases = [(range "8.11" "8.14") (isLe "1.12.0") ]; out = "0.3.0"; } { cases = [(range "8.10" "8.12") (isLe "1.12.0") ]; out = "0.2.2"; } ] null; releaseRev = v: "v${v}"; + release."0.3.1".sha256 = "sha256-KcuG/11Yq5ACem4FyVnQqHKvy3tNK7hd0ir2SJzzMN0="; release."0.3.0".sha256 = "sha256:14rm0726f1732ldds495qavg26gsn30w6dfdn36xb12g5kzavp38"; release."0.2.2".sha256 = "sha256:1clzza73gccy6p6l95n6gs0adkqd3h4wgl4qg5l0qm4q140grvm7"; diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix index 1ac76b38c72c3..ca82bbbed0691 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -7,9 +7,10 @@ with lib; mkCoqDerivation { domain = "gitlab.inria.fr"; inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.7" "8.14"; out = "3.4.2"; } + { case = range "8.7" "8.15"; out = "3.4.3"; } { case = range "8.5" "8.8"; out = "2.6.1"; } ] null; + release."3.4.3".sha256 = "sha256-YTdWlEmFJjCcHkl47jSOgrGqdXoApJY4u618ofCaCZE="; release."3.4.2".sha256 = "1s37hvxyffx8ccc8mg5aba7ivfc39p216iibvd7f2cb9lniqk1pw"; release."3.3.1".sha256 = "1mk8adhi5hrllsr0hamzk91vf2405sjr4lh5brg9201mcw11abkz"; release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix index 84cd739ed6abd..19d35b4c97ef0 100644 --- a/pkgs/development/coq-modules/fourcolor/default.nix +++ b/pkgs/development/coq-modules/fourcolor/default.nix @@ -7,9 +7,12 @@ mkCoqDerivation { release."1.2.3".rev = "v1.2.3"; release."1.2.3".sha256 = "sha256-gwKfUa74fIP7j+2eQgnLD7AswjCtOFGHGaIWb4qI0n4="; + release."1.2.4".rev = "v1.2.4"; + release."1.2.4".sha256 = "sha256-iSW2O1kuunvOqTolmGGXmsYTxo2MJYCdW3BnEhp6Ksg="; inherit version; defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (isGe "8.11") (isGe "1.11.0") ]; out = "1.2.4"; } { cases = [ (isLe "8.13") (pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; } ] null; diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix index cf52916605e9f..c7c64c9d257ce 100644 --- a/pkgs/development/coq-modules/gaia/default.nix +++ b/pkgs/development/coq-modules/gaia/default.nix @@ -10,7 +10,7 @@ with lib; mkCoqDerivation { inherit version; defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.10" "8.14") (isGe "1.12.0") ]; out = "1.13"; } + { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.13"; } { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; } ] null; diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix index e950741d81ca8..1f5a616bb549e 100644 --- a/pkgs/development/coq-modules/hierarchy-builder/default.nix +++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix @@ -5,10 +5,12 @@ with lib; let hb = mkCoqDerivation { owner = "math-comp"; inherit version; defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.15"; out = "1.2.1"; } { case = range "8.13" "8.14"; out = "1.2.0"; } { case = range "8.12" "8.13"; out = "1.1.0"; } { case = isEq "8.11"; out = "0.10.0"; } ] null; + release."1.2.1".sha256 = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0="; release."1.2.0".sha256 = "0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d"; release."1.1.0".sha256 = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q="; release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp"; diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix index 117eafae92399..b608f3d020508 100644 --- a/pkgs/development/coq-modules/interval/default.nix +++ b/pkgs/development/coq-modules/interval/default.nix @@ -6,11 +6,12 @@ mkCoqDerivation rec { domain = "gitlab.inria.fr"; inherit version; defaultVersion = with lib.versions; lib.switch coq.coq-version [ - { case = range "8.8" "8.14"; out = "4.3.0"; } + { case = isGe "8.8"; out = "4.4.0"; } { case = range "8.8" "8.12"; out = "4.0.0"; } { case = range "8.7" "8.11"; out = "3.4.2"; } { case = range "8.5" "8.6"; out = "3.3.0"; } ] null; + release."4.4.0".sha256 = "sha256-0+9AatTIEsjul0RXoOw6zWGEbGDVmuy7XuyrZNBZ8Kk="; release."4.3.0".sha256 = "sha256-k8DLC4HYYpHeEEgXUafS8jkaECqlM+/CoYaInmUTYko="; release."4.2.0".sha256 = "sha256-SD5thgpirs3wmZBICjXGpoefg9AAXyExb5t8tz3iZhE="; release."4.1.1".sha256 = "sha256-h2NJ6sZt1C/88v7W2xyuftEDoyRt3H6kqm5g2hc1aoU="; diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix index e61019b91c679..0a78191d8b728 100644 --- a/pkgs/development/coq-modules/math-classes/default.nix +++ b/pkgs/development/coq-modules/math-classes/default.nix @@ -4,10 +4,10 @@ with lib; mkCoqDerivation { pname = "math-classes"; inherit version; - defaultVersion = if versions.range "8.11" "8.13" coq.coq-version then "8.13.0" else - if versions.range "8.6" "8.10" coq.coq-version then "8.12.0" else null; + defaultVersion = if versions.range "8.6" "8.15" coq.coq-version then "8.15.0" else null; release."8.12.0".sha256 = "14nd6a08zncrl5yg2gzk0xf4iinwq4hxnsgm4fyv07ydbkxfb425"; release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby"; + release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw"; extraBuildInputs = [ bignums ]; diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/coq-modules/mathcomp-abel/default.nix index 2ada5ee1c91c5..06cfd12b07eb6 100644 --- a/pkgs/development/coq-modules/mathcomp-abel/default.nix +++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix @@ -8,7 +8,7 @@ mkCoqDerivation { inherit version; defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.10" "8.14") (range "1.12.0" "1.13.0") ]; out = "1.2.0"; } + { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.2.0"; } { cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; } ] null; diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix index 5901fe2bb3964..f842bc3b6dbed 100644 --- a/pkgs/development/coq-modules/mathcomp-analysis/default.nix +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -8,6 +8,7 @@ let mca = mkCoqDerivation { pname = "analysis"; owner = "math-comp"; + release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg="; release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI="; release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4="; release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5"; @@ -18,6 +19,7 @@ let mca = mkCoqDerivation { inherit version; defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (isGe "8.13") (isGe "1.12.0") ]; out = "0.3.13"; } { cases = [ (range "8.11" "8.14") (isGe "1.12.0") ]; out = "0.3.10"; } { cases = [ (range "8.11" "8.13") "1.11.0" ]; out = "0.3.4"; } { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; } diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix index 6a72f73a01b8a..744d5ea985142 100644 --- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix +++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix @@ -7,7 +7,7 @@ with lib; mkCoqDerivation { owner = "math-comp"; inherit version; defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ - { cases = [ (isGe "8.10") (range "1.11" "1.13") ]; out = "1.5.1"; } + { cases = [ (isGe "8.10") (isGe "1.11") ]; out = "1.5.1"; } { cases = [ (range "8.7" "8.11") "1.11.0" ]; out = "1.5.0"; } { cases = [ (isEq "8.11") (range "1.8" "1.10") ]; out = "1.4.0+coq-8.11"; } { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ]; out = "1.4.0"; } diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix index b7f613ccfcc1b..67f4c4ef786d7 100644 --- a/pkgs/development/coq-modules/mathcomp-word/default.nix +++ b/pkgs/development/coq-modules/mathcomp-word/default.nix @@ -14,7 +14,7 @@ mkCoqDerivation { inherit version; defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.12" "8.14") (range "1.12" "1.13") ]; out = "1.0"; } + { cases = [ (range "8.12" "8.14") (isGe "1.12") ]; out = "1.0"; } ] null; propagatedBuildInputs = [ mathcomp.algebra ]; diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix index fd3f31d3fe0d1..ce2bd98f3d01a 100644 --- a/pkgs/development/coq-modules/mathcomp-zify/default.nix +++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix @@ -9,7 +9,7 @@ with lib; mkCoqDerivation rec { defaultVersion = with versions; switch [ coq.coq-version mathcomp-algebra.version ] [ - { cases = [ (range "8.13" "8.14") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; } + { cases = [ (range "8.13" "8.15") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; } ] null; release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k"; diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 562d1f949250a..5b41d62d775aa 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -19,7 +19,8 @@ let owner = "math-comp"; withDoc = single && (args.withDoc or false); defaultVersion = with versions; switch coq.coq-version [ - { case = isGe "8.14"; out = "1.13.0"; } + { case = isGe "8.11"; out = "1.14.0"; } + { case = range "8.11" "8.15"; out = "1.13.0"; } { case = range "8.10" "8.13"; out = "1.12.0"; } { case = range "8.7" "8.12"; out = "1.11.0"; } { case = range "8.7" "8.11"; out = "1.10.0"; } @@ -29,6 +30,7 @@ let { case = range "8.5" "8.7"; out = "1.6.4"; } ] null; release = { + "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9"; "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri"; "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix index c29669625a9d3..a74ee17f1c60a 100644 --- a/pkgs/development/coq-modules/multinomials/default.nix +++ b/pkgs/development/coq-modules/multinomials/default.nix @@ -9,7 +9,7 @@ with lib; mkCoqDerivation { inherit version; defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ - { cases = [ (range "8.10" "8.14") (isGe "1.12.0") ]; out = "1.5.4"; } + { cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.5.5"; } { 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"; } @@ -17,6 +17,7 @@ with lib; mkCoqDerivation { { cases = [ "8.6" (range "1.6" "1.7") ]; out = "1.1"; } ] null; release = { + "1.5.5".sha256 = "sha256-VdXA51vr7DZl/wT/15YYMywdD7Gh91dMP9t7ij47qNQ="; "1.5.4".sha256 = "0s4sbh4y88l125hdxahr56325hdhxxdmqmrz7vv8524llyv3fciq"; "1.5.3".sha256 = "1462x40y2qydjd2wcg8r6qr8cx3xv4ixzh2h8vp9h7arylkja1qd"; "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix index 912d523d3bf77..2009034063369 100644 --- a/pkgs/development/coq-modules/odd-order/default.nix +++ b/pkgs/development/coq-modules/odd-order/default.nix @@ -5,11 +5,14 @@ mkCoqDerivation { pname = "odd-order"; owner = "math-comp"; + release."1.13.0".rev = "mathcomp-odd-order.1.13.0"; + release."1.13.0".sha256 = "sha256-EzNKR/JzM8T17sMhPhgZNs14e50X4dY3OwFi133IsT0="; release."1.12.0".rev = "mathcomp-odd-order.1.12.0"; release."1.12.0".sha256 = "sha256-omsfdc294CxKAHNMMeqJCcVimvyRCHgxcQ4NJOWSfNM="; inherit version; defaultVersion = with versions; switch mathcomp.character.version [ + { case = (range "1.12.0" "1.14.0"); out = "1.13.0"; } { case = (range "1.10.0" "1.12.0"); out = "1.12.0"; } ] null; diff --git a/pkgs/development/coq-modules/paramcoq/default.nix b/pkgs/development/coq-modules/paramcoq/default.nix index d73d14c84a0ca..7f65e6643c55e 100644 --- a/pkgs/development/coq-modules/paramcoq/default.nix +++ b/pkgs/development/coq-modules/paramcoq/default.nix @@ -4,10 +4,11 @@ with lib; mkCoqDerivation { pname = "paramcoq"; inherit version; defaultVersion = with versions; switch coq.version [ - { case = range "8.10" "8.14"; out = "1.1.3+coq${coq.coq-version}"; } + { case = range "8.10" "8.15"; out = "1.1.3+coq${coq.coq-version}"; } { case = range "8.7" "8.13"; out = "1.1.2+coq${coq.coq-version}"; } ] null; displayVersion = { paramcoq = "..."; }; + release."1.1.3+coq8.15".sha256 = "0sl7ihznwz05d2x2v78w1zd4q55c1sgy06vxasbcls4v2pkw53hl"; release."1.1.3+coq8.14".sha256 = "00zqq9dc2p5v0ib1jgizl25xkwxrs9mrlylvy0zvb96dpridjc71"; release."1.1.3+coq8.13".sha256 = "06ndly736k4pmdn4baqa7fblp6lx7a9pxm9gvz1vzd6ic51825wp"; release."1.1.3+coq8.12".sha256 = "sha256:10j23ws8ymqpxhapni75sxbzz0dl4n9sgasrx618i7s7b705y2rh"; diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix index 1908c755cd3ab..847ebb7808be3 100644 --- a/pkgs/development/coq-modules/reglang/default.nix +++ b/pkgs/development/coq-modules/reglang/default.nix @@ -10,7 +10,7 @@ mkCoqDerivation { inherit version; defaultVersion = with versions; switch coq.coq-version [ - { case = range "8.10" "8.14"; out = "1.1.2"; } + { case = range "8.10" "8.15"; out = "1.1.2"; } ] null; diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/coq-modules/serapi/default.nix index 383151a1cb5e7..b3bff95b5eaf7 100644 --- a/pkgs/development/coq-modules/serapi/default.nix +++ b/pkgs/development/coq-modules/serapi/default.nix @@ -1,22 +1,9 @@ { lib, fetchzip, mkCoqDerivation, coq, version ? null }: let - ocamlPackages = - coq.ocamlPackages.overrideScope' - (self: super: { - ppxlib = super.ppxlib.override { version = "0.15.0"; }; - # the following does not work - ppx_sexp_conv = super.ppx_sexp_conv.overrideAttrs (_: { - src = fetchzip { - url = "https://github.com/janestreet/ppx_sexp_conv/archive/v0.14.1.tar.gz"; - sha256 = "04bx5id99clrgvkg122nx03zig1m7igg75piphhyx04w33shgkz2"; - }; - }); - }); - release = { - "8.14.0+0.14.0".sha256 = "sha256:1kh80yb791yl771qbqkvwhbhydfii23a7lql0jgifvllm2k8hd8d"; - "8.14+rc1+0.14.0".sha256 = "1w7d7anvcfx8vz51mnrf1jkw6rlpzjkjlr06avf58wlhymww7pja"; + "8.15.0+0.15.0".sha256 = "1vh99ya2dq6a8xl2jrilgs0rpj4j227qx8zvzd2v5xylx0p4bbrp"; + "8.14.0+0.14.0".sha256 = "1kh80yb791yl771qbqkvwhbhydfii23a7lql0jgifvllm2k8hd8d"; "8.13.0+0.13.0".sha256 = "0k69907xn4k61w4mkhwf8kh8drw9pijk9ynijsppihw98j8w38fy"; "8.12.0+0.12.1".sha256 = "048x3sgcq4h845hi6hm4j4dsfca8zfj70dm42w68n63qcm6xf9hn"; "8.11.0+0.11.1".sha256 = "1phmh99yqv71vlwklqgfxiq2vj99zrzxmryj2j4qvg5vav3y3y6c"; @@ -29,9 +16,8 @@ in inherit version release; defaultVersion = with versions; - if isGe "4.12" coq.ocamlPackages.ocaml.version then null - else switch coq.version [ + { case = isEq "8.15"; out = "8.15.0+0.15.0"; } { case = isEq "8.14"; out = "8.14.0+0.14.0"; } { case = isEq "8.13"; out = "8.13.0+0.13.0"; } { case = isEq "8.12"; out = "8.12.0+0.12.1"; } @@ -42,7 +28,7 @@ in useDune2 = true; propagatedBuildInputs = - with ocamlPackages; [ + with coq.ocamlPackages; [ cmdliner findlib # run time dependency of SerAPI ppx_deriving @@ -70,9 +56,6 @@ in let inherit (o) version; in { src = fetchzip { url = - if version == "8.14+rc1+0.14.0" - then "https://github.com/ejgallego/coq-serapi/archive/refs/tags/8.14+rc1+0.14.0.tar.gz" - else "https://github.com/ejgallego/coq-serapi/releases/download/${version}/coq-serapi-${ if version == "8.11.0+0.11.1" then version else builtins.replaceStrings [ "+" ] [ "." ] version |