diff options
Diffstat (limited to 'pkgs/development/coq-modules')
7 files changed, 121 insertions, 26 deletions
diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix index 524427c109a..8362c704d95 100644 --- a/pkgs/development/coq-modules/contribs/default.nix +++ b/pkgs/development/coq-modules/contribs/default.nix @@ -42,7 +42,7 @@ let mkContrib = repo: revs: param: sha256 = "18f5vbq6nx9gz2gcj5p7v2gmjczpspc5dmlj6by4jqv07iirzsz2"; }; - additions = mkContrib "additions" [ "8.6" "8.7" ] { + additions = mkContrib "additions" [ "8.6" ] { version = "v8.5.0-9-gbec504e"; rev = "bec504e7822747376159aaa2156cf7453dbbd2b4"; sha256 = "1vvkqjnqrf6m726krhlm2viza64ha2081xgc5wb9y5sygd0baaz7"; diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix new file mode 100644 index 00000000000..ed6118dbb55 --- /dev/null +++ b/pkgs/development/coq-modules/coq-bits/default.nix @@ -0,0 +1,38 @@ +{ stdenv, fetchFromGitHub, coq, mathcomp-algebra }: + +let + version = "20190812"; +in + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-coq-bits-${version}"; + + src = fetchFromGitHub { + owner = "coq-community"; + repo = "coq-bits"; + rev = "f74498a6c67e97d9565e139d62be8eaae7111f06"; + sha256 = "1ibg37qxgkmpbpvc78qcb179bcnzl149z1kzwdm8n98xk5ibavrf"; + }; + + buildInputs = [ coq ]; + propagatedBuildInputs = [ mathcomp-algebra ]; + + enableParallelBuilding = true; + + installPhase = '' + make -f Makefile CoqMakefile + make -f CoqMakefile COQLIB=$out/lib/coq/${coq.coq-version}/ install + ''; + + meta = with stdenv.lib; { + homepage = https://github.com/coq-community/coq-bits; + description = "A formalization of bitset operations in Coq"; + license = licenses.asl20; + maintainers = with maintainers; [ ptival ]; + platforms = coq.meta.platforms; + }; + + passthru = { + compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" ]; + }; +} diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index c689cea1a82..defe52987aa 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -1,10 +1,10 @@ { stdenv, fetchFromGitHub, which, coq }: let params = { - "8.10" = { - version = "master"; - rev = "bc7134deba1aacc7ecd2f5d1032bdf05b125c568"; - sha256 = "188avk9irwjsbs5ya4ka01mpk3vw4397kv2rmsncqrrrsa1pdddk"; + "8.10" = rec { + version = "1.1.0"; + rev = "v${version}"; + sha256 = "06jyw7n27ylg02jvlaa3hs13hg8qgx47yn4dxhg9as1xri9a2rvm"; }; }; param = params.${coq.coq-version}; diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix index 898272d402b..588172aea61 100644 --- a/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -5,8 +5,8 @@ let params = "8.5" = { version = "0.9.4"; sha256 = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; }; "8.6" = { version = "0.9.5"; sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; }; "8.7" = { version = "0.9.7"; sha256 = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag"; }; - "8.8" = { version = "0.9.8"; sha256 = "0z1ix855kdjl7zw5ca664h5njd1x8mmvf5wi37fck4dj9dgamwlz"; }; - "8.9" = { version = "0.10.1"; sha256 = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95"; }; + "8.8" = { version = "0.10.3"; sha256 = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb"; }; + "8.9" = { version = "0.10.3"; sha256 = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb"; }; }; param = params.${coq.coq-version}; in @@ -33,7 +33,7 @@ stdenv.mkDerivation rec { meta = with stdenv.lib; { homepage = https://github.com/coq-ext-lib/coq-ext-lib; description = "A collection of theories and plugins that may be useful in other Coq developments"; - maintainers = with maintainers; [ jwiegley ]; + maintainers = with maintainers; [ jwiegley ptival ]; platforms = coq.meta.platforms; }; diff --git a/pkgs/development/coq-modules/coq-extensible-records/default.nix b/pkgs/development/coq-modules/coq-extensible-records/default.nix index 513b046c0fe..3b93b6b2de2 100644 --- a/pkgs/development/coq-modules/coq-extensible-records/default.nix +++ b/pkgs/development/coq-modules/coq-extensible-records/default.nix @@ -1,13 +1,39 @@ { stdenv, fetchFromGitHub, coq }: -stdenv.mkDerivation { - name = "coq${coq.coq-version}-coq-extensible-records-1.2.0"; +let + versions = { + pre_8_9 = { + owner = "gmalecha"; + rev = "1.2.0"; + version = "1.2.0"; + sha256 = "0h5m04flqfk0v577syw0v1dw2wf7xrx6jaxv5gpmqzssf5hxafy4"; + }; + post_8_9 = { + owner = "Ptival"; + rev = "bd7082a3571ee3c111096ff6b5eb28c8d3a99ce5"; + version = "1.2.0+8.9-fix"; + sha256 = "0625qd8pyxi0v704fwnawrfw5fk966vnk120il0g6qv42siyck95"; + }; + }; + params = + { + "8.5" = versions.pre_8_9; + "8.6" = versions.pre_8_9; + "8.7" = versions.pre_8_9; + "8.8" = versions.pre_8_9; + "8.9" = versions.post_8_9; + "8.10" = versions.post_8_9; + }; + param = params.${coq.coq-version}; +in + +stdenv.mkDerivation rec { + inherit (param) version; + name = "coq${coq.coq-version}-coq-extensible-records-${version}"; src = fetchFromGitHub { - owner = "gmalecha"; + inherit (param) owner rev sha256; repo = "coq-extensible-records"; - rev = "1.2.0"; - sha256 = "0h5m04flqfk0v577syw0v1dw2wf7xrx6jaxv5gpmqzssf5hxafy4"; }; buildInputs = [ coq ]; @@ -27,6 +53,6 @@ stdenv.mkDerivation { }; passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" ]; + compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" ]; }; } diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/coq-modules/ltac2/default.nix index 80b167aaa98..67441e9cdd8 100644 --- a/pkgs/development/coq-modules/ltac2/default.nix +++ b/pkgs/development/coq-modules/ltac2/default.nix @@ -11,11 +11,16 @@ let params = { rev = "0.1"; sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7"; }; - "8.9" = { - version = "0.1"; - rev = "a69551a49543b22a7d4e6a2484356b56bd05068e"; + "8.9" = rec { + version = "0.2"; + rev = version; sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73"; }; + "8.10" = rec { + version = "0.3"; + rev = version; + sha256 = "0pzs5nsakh4l8ffwgn4ryxbnxdv2x0r1i7bc598ij621haxdirrr"; + }; }; param = params.${coq.coq-version}; in @@ -31,7 +36,10 @@ stdenv.mkDerivation rec { }; nativeBuildInputs = [ which ]; - buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib ]) + ++ stdenv.lib.optional (!stdenv.lib.versionAtLeast coq.coq-version "8.10") + coq.ocamlPackages.camlp5 + ; installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix index 86a1301d3c7..fee6de7b35b 100644 --- a/pkgs/development/coq-modules/paco/default.nix +++ b/pkgs/development/coq-modules/paco/default.nix @@ -1,13 +1,36 @@ -{stdenv, fetchurl, coq, unzip}: +{stdenv, fetchFromGitHub, coq, unzip}: + +let + versions = { + pre_8_6 = rec { + rev = "v${version}"; + version = "1.2.8"; + sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb"; + }; + post_8_6 = rec { + rev = "v${version}"; + version = "4.0.0"; + sha256 = "1ncrdyijkgf0s2q4rg1s9r2nrcb17gq3jz63iqdlyjq3ylv8gyx0"; + }; + }; + params = { + "8.5" = versions.pre_8_6; + "8.6" = versions.post_8_6; + "8.7" = versions.post_8_6; + "8.8" = versions.post_8_6; + "8.9" = versions.post_8_6; + }; + param = params.${coq.coq-version}; +in stdenv.mkDerivation rec { - + inherit (param) version; name = "coq-paco-${coq.coq-version}-${version}"; - version = "1.2.8"; - src = fetchurl { - url = "http://plv.mpi-sws.org/paco/paco-${version}.zip"; - sha256 = "1lcmdr0y2d7gzyvr8dal3pi7fibbd60bpi1l32fw89xiyrgqhsqy"; + src = fetchFromGitHub { + inherit (param) rev sha256; + owner = "snu-sf"; + repo = "paco"; }; buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ]; @@ -24,12 +47,12 @@ stdenv.mkDerivation rec { meta = with stdenv.lib; { homepage = http://plv.mpi-sws.org/paco/; description = "A Coq library implementing parameterized coinduction"; - maintainers = with maintainers; [ jwiegley ]; + maintainers = with maintainers; [ jwiegley ptival ]; platforms = coq.meta.platforms; }; passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ]; + compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" ]; }; } |