diff options
author | Alyssa Ross <hi@alyssa.is> | 2021-08-04 10:43:07 +0000 |
---|---|---|
committer | Alyssa Ross <hi@alyssa.is> | 2021-08-04 10:43:07 +0000 |
commit | 62614cbef7da005c1eda8c9400160f6bcd6546b8 (patch) | |
tree | c2630f69080637987b68acb1ee8676d2681fe304 /pkgs/development/coq-modules | |
parent | d9c82ed3044c72cecf01c6ea042489d30914577c (diff) | |
parent | e24069138dfec3ef94f211f1da005bb5395adc11 (diff) | |
download | nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.gz nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.bz2 nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.lz nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.xz nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.zst nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.zip |
Merge branch 'nixpkgs-update' into master
Diffstat (limited to 'pkgs/development/coq-modules')
64 files changed, 1601 insertions, 2204 deletions
diff --git a/pkgs/development/coq-modules/Cheerios/default.nix b/pkgs/development/coq-modules/Cheerios/default.nix index 194a1a0752a..6c5216f0d01 100644 --- a/pkgs/development/coq-modules/Cheerios/default.nix +++ b/pkgs/development/coq-modules/Cheerios/default.nix @@ -1,32 +1,13 @@ -{ stdenv, fetchFromGitHub, coq, StructTact }: +{ lib, mkCoqDerivation, coq, StructTact, version ? null }: -let param = - { - version = "20200201"; - rev = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d"; - sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1"; - }; -in - -stdenv.mkDerivation { - name = "coq${coq.coq-version}-Cheerios-${param.version}"; - - src = fetchFromGitHub { - owner = "uwplse"; - repo = "cheerios"; - inherit (param) rev sha256; - }; - - buildInputs = [ coq ]; +with lib; mkCoqDerivation { + pname = "cheerios"; + owner = "uwplse"; + inherit version; + defaultVersion = if versions.isGe "8.6" coq.coq-version then "20200201" else null; + release."20200201".rev = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d"; + release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1"; propagatedBuildInputs = [ StructTact ]; - enableParallelBuilding = true; - preConfigure = "patchShebangs ./configure"; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" ]; - }; } diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix index 1d3e5a07b03..46738343431 100644 --- a/pkgs/development/coq-modules/CoLoR/default.nix +++ b/pkgs/development/coq-modules/CoLoR/default.nix @@ -1,58 +1,30 @@ -{ stdenv, fetchFromGitHub, coq, bignums }: +{ lib, mkCoqDerivation, coq, bignums, version ? null }: -let - coqVersions = { - "8.6" = "1.4.0"; - "8.7" = "1.4.0"; - "8.8" = "1.6.0"; - "8.9" = "1.6.0"; - "8.10" = "1.7.0"; - "8.11" = "1.7.0"; - }; - params = { - "1.4.0" = { - version = "1.4.0"; - rev = "168c6b86c7d3f87ee51791f795a8828b1521589a"; - sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm"; - }; - "1.6.0" = { - version = "1.6.0"; - rev = "328aa06270584b578edc0d2925e773cced4f14c8"; - sha256 = "07sy9kw1qlynsqy251adgi8b3hghrc9xxl2rid6c82mxfsp329sd"; - }; - "1.7.0" = { - version = "1.7.0"; - rev = "08b5481ed6ea1a5d2c4c068b62156f5be6d82b40"; - sha256 = "1w7fmcpf0691gcwq00lm788k4ijlwz3667zj40j5jjc8j8hj7cq3"; - }; - }; - param = params.${coqVersions.${coq.coq-version}}; -in +with lib; mkCoqDerivation { + pname = "color"; + owner = "fblanqui"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + {case = range "8.12" "8.13"; out = "1.8.1"; } + {case = range "8.10" "8.11"; out = "1.7.0"; } + {case = range "8.8" "8.9"; out = "1.6.0"; } + {case = range "8.6" "8.7"; out = "1.4.0"; } + ] null; -stdenv.mkDerivation { - name = "coq${coq.coq-version}-CoLoR-${param.version}"; - - src = fetchFromGitHub { - owner = "fblanqui"; - repo = "color"; - inherit (param) rev sha256; - }; + release."1.8.1".sha256 = "0knhca9fffmyldn4q16h9265i7ih0h4jhcarq4rkn0wnn7x8w8yw"; + release."1.7.0".rev = "08b5481ed6ea1a5d2c4c068b62156f5be6d82b40"; + release."1.7.0".sha256 = "1w7fmcpf0691gcwq00lm788k4ijlwz3667zj40j5jjc8j8hj7cq3"; + release."1.6.0".rev = "328aa06270584b578edc0d2925e773cced4f14c8"; + release."1.6.0".sha256 = "07sy9kw1qlynsqy251adgi8b3hghrc9xxl2rid6c82mxfsp329sd"; + release."1.4.0".rev = "168c6b86c7d3f87ee51791f795a8828b1521589a"; + release."1.4.0".sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm"; - buildInputs = [ coq bignums ]; + extraBuildInputs = [ bignums ]; enableParallelBuilding = false; - installPhase = '' - make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install - ''; - - meta = with stdenv.lib; { + meta = { homepage = "http://color.inria.fr/"; 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 ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v coqVersions; }; } diff --git a/pkgs/development/coq-modules/HoTT/default.nix b/pkgs/development/coq-modules/HoTT/default.nix index 7b52838505e..706943cf8d0 100644 --- a/pkgs/development/coq-modules/HoTT/default.nix +++ b/pkgs/development/coq-modules/HoTT/default.nix @@ -1,18 +1,14 @@ -{ stdenv, fetchFromGitHub, autoconf, automake, coq }: +{ lib, mkCoqDerivation, autoconf, automake, coq, version ? null }: -stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-HoTT-${version}"; - version = "20170921"; +with lib; mkCoqDerivation { + pname = "HoTT"; + owner = "HoTT"; + inherit version; + defaultVersion = if coq.coq-version == "8.6" then "20170921" else null; + release."20170921".rev = "e3557740a699167e6adb1a65855509d55a392fa1"; + release."20170921".sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v"; - src = fetchFromGitHub { - owner = "HoTT"; - repo = "HoTT"; - rev = "e3557740a699167e6adb1a65855509d55a392fa1"; - sha256 = "0zwfp8g62b50vmmbb2kmskj3v6w7qx1pbf43yw0hr7asdz2zbx5v"; - }; - - buildInputs = [ autoconf automake coq ]; - enableParallelBuilding = true; + extraBuildInputs = [ autoconf automake ]; preConfigure = '' patchShebangs ./autogen.sh @@ -44,18 +40,9 @@ stdenv.mkDerivation rec { rmdir $out/share ''; - installFlags = [ - "COQBIN=${coq}/bin" - ]; - - meta = with stdenv.lib; { + meta = { homepage = "http://homotopytypetheory.org/"; description = "Homotopy type theory"; maintainers = with maintainers; [ siddharthist ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: v == "8.6"; }; } diff --git a/pkgs/development/coq-modules/ITree/default.nix b/pkgs/development/coq-modules/ITree/default.nix new file mode 100644 index 00000000000..95174d9547e --- /dev/null +++ b/pkgs/development/coq-modules/ITree/default.nix @@ -0,0 +1,17 @@ +{ lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }: + +with lib; mkCoqDerivation rec { + pname = "InteractionTrees"; + owner = "DeepSpec"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.10" "8.13"; out = "4.0.0"; } + ] null; + release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm"; + releaseRev = v: "${v}"; + propagatedBuildInputs = [ coq-ext-lib paco ]; + meta = { + description = "A Library for Representing Recursive and Impure Programs in Coq"; + maintainers = with maintainers; [ larsr ]; + }; +} diff --git a/pkgs/development/coq-modules/InfSeqExt/default.nix b/pkgs/development/coq-modules/InfSeqExt/default.nix index e97b4499901..8236705b58f 100644 --- a/pkgs/development/coq-modules/InfSeqExt/default.nix +++ b/pkgs/development/coq-modules/InfSeqExt/default.nix @@ -1,31 +1,11 @@ -{ stdenv, fetchFromGitHub, coq }: - -let param = - { - version = "20200131"; - rev = "203d4c20211d6b17741f1fdca46dbc091f5e961a"; - sha256 = "0xylkdmb2dqnnqinf3pigz4mf4zmczcbpjnn59g5g76m7f2cqxl0"; - }; -in - -stdenv.mkDerivation { - name = "coq${coq.coq-version}-InfSeqExt-${param.version}"; - - src = fetchFromGitHub { - owner = "DistributedComponents"; - repo = "InfSeqExt"; - inherit (param) rev sha256; - }; - - buildInputs = [ coq ]; - - enableParallelBuilding = true; - +{ lib, mkCoqDerivation, coq, version ? null }: + +mkCoqDerivation { + pname = "InfSeqExt"; + owner = "DistributedComponents"; + inherit version; + defaultVersion = if lib.versions.isGe "8.5" coq.coq-version then "20200131" else null; + release."20200131".rev = "203d4c20211d6b17741f1fdca46dbc091f5e961a"; + release."20200131".sha256 = "0xylkdmb2dqnnqinf3pigz4mf4zmczcbpjnn59g5g76m7f2cqxl0"; preConfigure = "patchShebangs ./configure"; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" ]; - }; } diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix index a167b7988dc..6490391eb63 100644 --- a/pkgs/development/coq-modules/QuickChick/default.nix +++ b/pkgs/development/coq-modules/QuickChick/default.nix @@ -1,96 +1,48 @@ -{ stdenv, fetchFromGitHub, coq, ssreflect, coq-ext-lib, simple-io }: - -let params = - { - "8.5" = { - version = "20170512"; - rev = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03"; - sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg"; - }; - - "8.6" = { - version = "20171102"; - rev = "0fdb769e1dc87a278383b44a9f5102cc7ccbafcf"; - sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17"; - }; - - "8.8" = { - version = "20190311"; - rev = "22af9e9a223d0038f05638654422e637e863b355"; - sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq"; - }; - - "8.9" = rec { - version = "1.1.0"; - rev = "v${version}"; - sha256 = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3"; - }; - - "8.10" = rec { - version = "1.2.1"; - rev = "v${version}"; - sha256 = "17vz88xjzxh3q7hs6hnndw61r3hdfawxp5awqpgfaxx4w6ni8z46"; - }; - - "8.11" = rec { - version = "1.3.2"; - rev = "v${version}"; - sha256 = "0lciwaqv288dh2f13xk2x0lrn6zyrkqy6g4yy927wwzag2gklfrs"; - }; - - "8.12" = rec { - version = "1.4.0"; - rev = "v${version}"; - sha256 = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc"; - }; - }; - param = params.${coq.coq-version}; -in - -let inherit (stdenv.lib) maintainers optional optionals versionAtLeast; in - -let recent = versionAtLeast coq.coq-version "8.8"; in - -stdenv.mkDerivation { - - name = "coq${coq.coq-version}-QuickChick-${param.version}"; - - src = fetchFromGitHub { - owner = "QuickChick"; - repo = "QuickChick"; - inherit (param) rev sha256; - }; - - preConfigure = stdenv.lib.optionalString recent +{ lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io }: +with lib; +let recent = versions.isGe "8.7" coq.coq-version; in +mkCoqDerivation { + pname = "QuickChick"; + owner = "QuickChick"; + defaultVersion = with versions; switch [ coq.coq-version ssreflect.version ] [ + { cases = [ "8.13" pred.true ]; out = "1.5.0"; } + { cases = [ "8.12" pred.true ]; out = "1.4.0"; } + { cases = [ "8.11" pred.true ]; out = "1.3.2"; } + { cases = [ "8.10" pred.true ]; out = "1.2.1"; } + { cases = [ "8.9" pred.true ]; out = "1.1.0"; } + { cases = [ "8.8" pred.true ]; out = "20190311"; } + { cases = [ "8.7" isLe "1.8" ]; out = "1.0.0"; } + { cases = [ "8.6" pred.true ]; out = "20171102"; } + { cases = [ "8.5" pred.true ]; out = "20170512"; } + ] null; + release."1.5.0".sha256 = "1lq8x86vd3vqqh2yq6hvyagpnhfq5wmk5pg2z0xq7b7dcw7hyfkw"; + release."1.4.0".sha256 = "068p48pm5yxjc3yv8qwzp25bp9kddvxj81l31mjkyx3sdrsw3kyc"; + release."1.3.2".sha256 = "0lciwaqv288dh2f13xk2x0lrn6zyrkqy6g4yy927wwzag2gklfrs"; + release."1.2.1".sha256 = "17vz88xjzxh3q7hs6hnndw61r3hdfawxp5awqpgfaxx4w6ni8z46"; + release."1.1.0".sha256 = "1c34v1k37rk7v0xk2czv5n79mbjxjrm6nh3llg2mpfmdsqi68wf3"; + release."1.0.0".sha256 = "1gqy9a4yavd0sa7kgysf9gf2lq4p8dmn4h89y8081f2j8zli0w5y"; + release."20190311".rev = "22af9e9a223d0038f05638654422e637e863b355"; + release."20190311".sha256 = "00rnr19lg6lg0haq1sy4ld38p7imzand6fc52fvfq27gblxkp2aq"; + release."20171102".rev = "0fdb769e1dc87a278383b44a9f5102cc7ccbafcf"; + release."20171102".sha256 = "0fri4nih40vfb0fbr82dsi631ydkw48xszinq43lyinpknf54y17"; + release."20170512".rev = "31eb050ae5ce57ab402db9726fb7cd945a0b4d03"; + release."20170512".sha256 = "033ch10i5wmqyw8j6wnr0dlbnibgfpr1vr0c07q3yj6h23xkmqpg"; + releaseRev = v: "v${v}"; + + preConfigure = optionalString recent "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native"; - buildInputs = [ coq ] - ++ (with coq.ocamlPackages; [ ocaml findlib ]) - ++ optionals (recent && !versionAtLeast coq.coq-version "8.10") - (with coq.ocamlPackages; [ camlp5 ocamlbuild ]) - ++ optional recent coq.ocamlPackages.num - ; + mlPlugin = true; + extraBuildInputs = optional recent coq.ocamlPackages.num; propagatedBuildInputs = [ ssreflect ] - ++ optionals recent [ coq-ext-lib simple-io ] - ++ optional (versionAtLeast coq.coq-version "8.10") - coq.ocamlPackages.ocamlbuild - ; + ++ optionals recent [ coq-ext-lib simple-io ] + ++ optional recent coq.ocamlPackages.ocamlbuild; + extraInstallFlags = [ "-f Makefile.coq" ]; enableParallelBuilding = false; - installPhase = '' - make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install - ''; - meta = { - homepage = "https://github.com/QuickChick/QuickChick"; description = "Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck"; maintainers = with maintainers; [ jwiegley ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; }; - } diff --git a/pkgs/development/coq-modules/StructTact/default.nix b/pkgs/development/coq-modules/StructTact/default.nix index 798aaabe677..9770b9fb9c4 100644 --- a/pkgs/development/coq-modules/StructTact/default.nix +++ b/pkgs/development/coq-modules/StructTact/default.nix @@ -1,31 +1,11 @@ -{ stdenv, fetchFromGitHub, coq }: - -let param = - { - version = "20181102"; - rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510"; - sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v"; - }; -in - -stdenv.mkDerivation { - name = "coq${coq.coq-version}-StructTact-${param.version}"; - - src = fetchFromGitHub { - owner = "uwplse"; - repo = "StructTact"; - inherit (param) rev sha256; - }; - - buildInputs = [ coq ]; - - enableParallelBuilding = true; - +{ lib, mkCoqDerivation, coq, version ? null }: + +with lib; mkCoqDerivation { + pname = "StructTact"; + owner = "uwplse"; + inherit version; + defaultVersion = if versions.isGe "8.5" coq.coq-version then "20181102" else null; + release."20181102".rev = "82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510"; + release."20181102".sha256 = "08zry20flgj7qq37xk32kzmg4fg6d4wi9m7pf9aph8fd3j2a0b5v"; preConfigure = "patchShebangs ./configure"; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - passthru = { - compatibleCoqVersions = v: stdenv.lib.versionAtLeast v "8.5"; - }; } diff --git a/pkgs/development/coq-modules/VST/default.nix b/pkgs/development/coq-modules/VST/default.nix new file mode 100644 index 00000000000..5ee1df77418 --- /dev/null +++ b/pkgs/development/coq-modules/VST/default.nix @@ -0,0 +1,38 @@ +{ lib, mkCoqDerivation, coq, compcert, version ? null }: + +with lib; mkCoqDerivation { + pname = "coq${coq.coq-version}-VST"; + namePrefix = []; + displayVersion = { coq = false; }; + owner = "PrincetonUniversity"; + repo = "VST"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.12" "8.13"; out = "2.8"; } + ] null; + release."2.8".sha256 = "sha256-cyK88uzorRfjapNQ6XgQEmlbWnDsiyLve5po1VG52q0="; + releaseRev = v: "v${v}"; + propagatedBuildInputs = [ compcert ]; + + preConfigure = "patchShebangs util"; + + makeFlags = [ + "BITSIZE=64" + "COMPCERT=inst_dir" + "COMPCERT_INST_DIR=${compcert.lib}/lib/coq/${coq.coq-version}/user-contrib/compcert" + "INSTALLDIR=$(out)/lib/coq/${coq.coq-version}/user-contrib/VST" + ]; + + postInstall = '' + for d in msl veric floyd sepcomp progs64 + do + cp -r $d $out/lib/coq/${coq.coq-version}/user-contrib/VST/ + done + ''; + + meta = { + description = "Verified Software Toolchain"; + homepage = "https://vst.cs.princeton.edu/"; + inherit (compcert.meta) platforms; + }; +} diff --git a/pkgs/development/coq-modules/Velisarios/default.nix b/pkgs/development/coq-modules/Velisarios/default.nix index 92c9b2569ca..08322fb7fc4 100644 --- a/pkgs/development/coq-modules/Velisarios/default.nix +++ b/pkgs/development/coq-modules/Velisarios/default.nix @@ -1,41 +1,14 @@ -{ stdenv, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -let params = - { - "8.6" = { - version = "20180221"; - rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; - sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; - }; +with lib; mkCoqDerivation { + pname = "Velisarios"; + owner = "vrahli"; + inherit version; + defaultVersion = if versions.range "8.6" "8.8" coq.coq-version then "20180221" else null; - "8.7" = { - version = "20180221"; - rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; - sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; - }; - - "8.8" = { - version = "20180221"; - rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; - sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; - }; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation { - name = "coq${coq.coq-version}-Velisarios-${param.version}"; - - src = fetchFromGitHub { - owner = "vrahli"; - repo = "Velisarios"; - inherit (param) rev sha256; - }; - - buildInputs = [ - coq coq.ocaml coq.camlp5 coq.findlib - ]; - enableParallelBuilding = true; + release."20180221".rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; + release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; + mlPlugin = true; buildPhase = "make -j$NIX_BUILD_CORES"; preBuild = "./create-makefile.sh"; @@ -43,8 +16,4 @@ stdenv.mkDerivation { mkdir -p $out/lib/coq/${coq.coq-version}/Velisarios cp -pR model/*.vo $out/lib/coq/${coq.coq-version}/Velisarios ''; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ]; - }; } diff --git a/pkgs/development/coq-modules/Verdi/default.nix b/pkgs/development/coq-modules/Verdi/default.nix index 1fd06a9c556..d3769eb2c4d 100644 --- a/pkgs/development/coq-modules/Verdi/default.nix +++ b/pkgs/development/coq-modules/Verdi/default.nix @@ -1,37 +1,19 @@ -{ stdenv, fetchFromGitHub, coq, Cheerios, InfSeqExt, ssreflect }: +{ lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }: + + +with lib; mkCoqDerivation { + pname = "verdi"; + owner = "uwplse"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.7"; out = "20200131"; } + { case = isEq "8.6"; out = "20181102"; } + ] null; + release."20200131".rev = "fdb4ede19d2150c254f0ebcfbed4fb9547a734b0"; + release."20200131".sha256 = "1a2k19f9q5k5djbxplqmmpwck49kw3lrm3aax920h4yb40czkd8m"; + release."20181102".rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564"; + release."20181102".sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z"; -let param = - if stdenv.lib.versionAtLeast coq.coq-version "8.7" then - { - version = "20200131"; - rev = "fdb4ede19d2150c254f0ebcfbed4fb9547a734b0"; - sha256 = "1a2k19f9q5k5djbxplqmmpwck49kw3lrm3aax920h4yb40czkd8m"; - } else { - version = "20181102"; - rev = "25b79cf1be5527ab8dc1b8314fcee93e76a2e564"; - sha256 = "1vw47c37k5vaa8vbr6ryqy8riagngwcrfmb3rai37yi9xhdqg55z"; - }; -in - -stdenv.mkDerivation { - name = "coq${coq.coq-version}-verdi-${param.version}"; - - src = fetchFromGitHub { - owner = "uwplse"; - repo = "verdi"; - inherit (param) rev sha256; - }; - - buildInputs = [ coq ]; propagatedBuildInputs = [ Cheerios InfSeqExt ssreflect ]; - - enableParallelBuilding = true; - preConfigure = "patchShebangs ./configure"; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" ]; - }; } diff --git a/pkgs/development/coq-modules/aac-tactics/default.nix b/pkgs/development/coq-modules/aac-tactics/default.nix new file mode 100644 index 00000000000..445a0422446 --- /dev/null +++ b/pkgs/development/coq-modules/aac-tactics/default.nix @@ -0,0 +1,46 @@ +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; + +mkCoqDerivation { + pname = "aac-tactics"; + + releaseRev = v: "v${v}"; + + 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="; + release."8.10.0".sha256 = "sha256-Ny3AgfLAzrz3FnoUqejXLApW+krlkHBmYlo3gAG0JsM="; + release."8.9.0".sha256 = "sha256-6Pp0dgYEnVaSnkJR/2Cawt5qaxWDpBI4m0WAbQboeWY="; + release."8.8.0".sha256 = "sha256-mwIKp3kf/6i9IN3cyIWjoRtW8Yf8cc3MV744zzFM3u4="; + release."8.6.1".sha256 = "sha256-PfovQ9xJnzr0eh/tO66yJ3Yp7A5E1SQG46jLIrrbZFg="; + release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = "8.13"; out = "8.13.0"; } + { case = "8.12"; out = "8.12.0"; } + { case = "8.11"; out = "8.11.0"; } + { case = "8.10"; out = "8.10.0"; } + { case = "8.9"; out = "8.9.0"; } + { case = "8.8"; out = "8.8.0"; } + { case = "8.6"; out = "8.6.1"; } + { case = "8.5"; out = "8.5.0"; } + ] null; + + mlPlugin = true; + + meta = { + description = "Coq plugin providing tactics for rewriting universally quantified equations"; + longDescription = '' + This Coq plugin provides tactics for rewriting universally quantified + equations, modulo associativity and commutativity of some operator. + The tactics can be applied for custom operators by registering the + operators and their properties as type class instances. Many common + operator instances, such as for Z binary arithmetic and booleans, are + provided with the plugin. + ''; + maintainers = with maintainers; [ siraben ]; + license = licenses.gpl3Plus; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch b/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch deleted file mode 100644 index dde0e2e03eb..00000000000 --- a/pkgs/development/coq-modules/autosubst/0001-changes-to-work-with-Coq-8.6.patch +++ /dev/null @@ -1,134 +0,0 @@ -From 5b40a32e35fe446cda20ed34c756a010856f39ce Mon Sep 17 00:00:00 2001 -From: Theo Giannakopoulos <theo.giannakopoulos@baesystems.com> -Date: Wed, 5 Apr 2017 15:48:55 -0400 -Subject: [PATCH] changes to work with Coq 8.6 - ---- - theories/Autosubst_Derive.v | 12 ++++++++++++ - theories/Autosubst_MMap.v | 3 ++- - 2 files changed, 14 insertions(+), 1 deletion(-) - -diff --git a/theories/Autosubst_Derive.v b/theories/Autosubst_Derive.v -index 61995de..cf87f67 100644 ---- a/theories/Autosubst_Derive.v -+++ b/theories/Autosubst_Derive.v -@@ -18,6 +18,7 @@ Hint Extern 0 (Ids _) => derive_Ids : derive. - - Ltac derive_Rename := - match goal with [ |- Rename ?term ] => -+ let inst := fresh "inst" in - hnf; fix inst 2; change _ with (Rename term) in inst; - intros xi s; change (annot term s); destruct s; - match goal with -@@ -66,6 +67,7 @@ Ltac has_var s := - Ltac derive_Subst := - match goal with [ |- Subst ?term ] => - require_instance (Rename term); -+ let inst := fresh "inst" in - hnf; fix inst 2; change _ with (Subst term) in inst; - intros sigma s; change (annot term s); destruct s; - match goal with -@@ -107,6 +109,7 @@ Hint Extern 0 (Subst _) => derive_Subst : derive. - Ltac derive_HSubst := - match goal with [ |- HSubst ?inner ?outer ] => - require_instance (Subst inner); -+ let inst := fresh "inst" in - hnf; fix inst 2; change _ with (HSubst inner outer) in inst; - intros sigma s; change (annot outer s); destruct s; - match goal with -@@ -327,6 +330,7 @@ Ltac derive_SubstLemmas := - assert (up_upren_n : - forall xi n, upn n (ren xi) = ren (iterate upren n xi)) by - (apply up_upren_n_internal, up_upren); -+ let ih := fresh "ih" in - fix ih 2; intros xi s; destruct s; try reflexivity; simpl; f_equal; - try apply mmap_ext; intros; rewrite ?up_upren, ?up_upren_n; apply ih); - -@@ -337,6 +341,7 @@ Ltac derive_SubstLemmas := - (apply up_id_internal; reflexivity); - assert (up_id_n : forall n, upn n ids = ids) by - (apply up_id_n_internal, up_id); -+ let ih := fresh "ih" in - fix ih 1; intros s; destruct s; simpl; f_equal; try reflexivity; - rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; apply ih); - -@@ -344,6 +349,7 @@ Ltac derive_SubstLemmas := - - assert (ren_subst_comp : - forall xi sigma (s : term), (rename xi s).[sigma] = s.[xi >>> sigma]) by( -+ let ih := fresh "ih" in - fix ih 3; intros xi sigma s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?up_comp_ren_subst, ?up_comp_ren_subst_n, ?mmap_comp; - try apply mmap_ext; intros; apply ih); -@@ -357,6 +363,7 @@ Ltac derive_SubstLemmas := - assert (up_comp_subst_ren_n : - forall sigma xi n, upn n (sigma >>> rename xi) = upn n sigma >>> rename (iterate upren n xi)) - by (apply up_comp_subst_ren_n_internal; apply up_comp_subst_ren); -+ let ih := fresh "ih" in - fix ih 3; intros sigma xi s; destruct s; try reflexivity; simpl; - f_equal; rewrite ?up_comp_subst_ren, ?up_comp_subst_ren_n, ?mmap_comp; - try (rewrite hcomp_ren_internal; [|apply rename_subst]); -@@ -368,6 +375,7 @@ Ltac derive_SubstLemmas := - by (apply up_comp_internal; [reflexivity|apply ren_subst_comp|apply subst_ren_comp]); - assert (up_comp_n : forall sigma tau n, upn n (sigma >> tau) = upn n sigma >> upn n tau) - by (apply up_comp_n_internal; apply up_comp); -+ let ih := fresh "ih" in - fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?up_comp, ?up_comp_n, ?mmap_comp, ?hcomp_dist_internal; - try apply mmap_ext; intros; apply ih); -@@ -382,6 +390,7 @@ Ltac derive_HSubstLemmas := - let ids := constr:(ids : var -> inner) in - - assert (hsubst_id : forall (s : outer), s.|[ids] = s) by ( -+ let ih := fresh "ih" in - fix ih 1; intros s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?up_id, ?up_id_n; try apply mmap_id_ext; intros; - (apply subst_id || apply ih) -@@ -390,6 +399,7 @@ Ltac derive_HSubstLemmas := - assert (hsubst_comp : forall (theta eta : var -> inner) (s : outer), - s.|[theta].|[eta] = s.|[theta >> eta]) - by ( -+ let ih := fresh "ih" in - fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; - rewrite <- ?up_comp, <- ?up_comp_n, ?mmap_comp; try apply mmap_ext; intros; - (apply subst_comp || apply ih) -@@ -405,6 +415,7 @@ Ltac derive_SubstHSubstComp := - assert (ren_hsubst_comp : forall xi (theta : var -> inner) (s : outer), - rename xi s.|[theta] = (rename xi s).|[theta] - ) by ( -+ let ih := fresh "ih" in - fix ih 3; intros xi theta s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?mmap_comp; try apply mmap_ext; intros; simpl; apply ih - ); -@@ -421,6 +432,7 @@ Ltac derive_SubstHSubstComp := - apply up_hcomp_n_internal; apply up_hcomp - ); - -+ let ih := fresh "ih" in - fix ih 3; intros sigma tau s; destruct s; try reflexivity; simpl; f_equal; - rewrite ?up_hcomp, ?up_hcomp_n, ?hcomp_lift_n_internal, ?mmap_comp; - try apply mmap_ext; intros; apply ih -diff --git a/theories/Autosubst_MMap.v b/theories/Autosubst_MMap.v -index f8387e7..7af7902 100644 ---- a/theories/Autosubst_MMap.v -+++ b/theories/Autosubst_MMap.v -@@ -23,7 +23,7 @@ Arguments mmap {A B _} f !s /. - Class MMapExt (A B : Type) `{MMap A B} := - mmap_ext : forall f g, - (forall t, f t = g t) -> forall s, mmap f s = mmap g s. --Arguments mmap_ext {A B _ _ f g} H s. -+Arguments mmap_ext {A B H' _ f g} H s : rename. - - Class MMapLemmas (A B : Type) `{MMap A B} := { - mmap_id x : mmap id x = x; -@@ -123,6 +123,7 @@ Tactic Notation "msimpl" "in" "*" := (in_all msimplH); msimpl. - - Ltac derive_MMap := - hnf; match goal with [ |- (?A -> ?A) -> ?B -> ?B ] => -+ let map := fresh "map" in - intros f; fix map 1; intros xs; change (annot B xs); destruct xs; - match goal with - | [ |- annot _ ?ys ] => --- -2.13.2 - diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix index 9507dc6751a..a5f7cbb2f0b 100644 --- a/pkgs/development/coq-modules/autosubst/default.nix +++ b/pkgs/development/coq-modules/autosubst/default.nix @@ -1,33 +1,23 @@ -{ stdenv, fetchgit, coq, mathcomp }: +{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }: +with lib; -stdenv.mkDerivation rec { +mkCoqDerivation { + pname = "autosubst"; - name = "coq-autosubst-${coq.coq-version}-${version}"; - version = "5b40a32e"; + release."1.7".rev = "v1.7"; + release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI="; - src = fetchgit { - url = "git://github.com/uds-psl/autosubst.git"; - rev = "1c3bb3bbf5477e3b33533a0fc090399f45fe3034"; - sha256 = "06pcjbngzwqyncvfwzz88j33wvdj9kizxyg5adp7y6186h8an341"; - }; - - buildInputs = [ coq ]; - propagatedBuildInputs = [ mathcomp ]; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.10"; out = "1.7"; } + ] null; - patches = [./0001-changes-to-work-with-Coq-8.6.patch]; + propagatedBuildInputs = [ mathcomp-ssreflect ]; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { + meta = { homepage = "https://www.ps.uni-saarland.de/autosubst/"; description = "Automation for de Bruijn syntax and substitution in Coq"; - maintainers = with maintainers; [ jwiegley ]; - platforms = coq.meta.platforms; + maintainers = with maintainers; [ siraben jwiegley ]; + license = licenses.mit; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" ]; - }; - - } diff --git a/pkgs/development/coq-modules/bignums/default.nix b/pkgs/development/coq-modules/bignums/default.nix index 88d7e461a31..84dc92a3cd5 100644 --- a/pkgs/development/coq-modules/bignums/default.nix +++ b/pkgs/development/coq-modules/bignums/default.nix @@ -1,58 +1,25 @@ -{ stdenv, fetchFromGitHub, coq }: - -let params = { - "8.6" = { - rev = "v8.6.0"; - sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj"; - }; - "8.7" = { - rev = "V8.7.0"; - sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl"; - }; - "8.8" = { - rev = "V8.8.0"; - sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg"; - }; - "8.9" = { - rev = "V8.9.0"; - sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01"; - }; - "8.10" = { - rev = "V8.10.0"; - sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"; - }; - "8.11" = { - rev = "V8.11.0"; - sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"; - }; - "8.12" = { - rev = "V8.12.0"; - sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8"; - }; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation { - - name = "coq${coq.coq-version}-bignums"; - - src = fetchFromGitHub { - owner = "coq"; - repo = "bignums"; - inherit (param) rev sha256; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { - license = licenses.lgpl2; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; - }; +{ lib, mkCoqDerivation, coq, version ? null }: + +with lib; mkCoqDerivation { + pname = "bignums"; + owner = "coq"; + displayVersion = { bignums = ""; }; + inherit version; + defaultVersion = if versions.isGe "8.5" coq.coq-version + then "${coq.coq-version}.0" else null; + + release."8.13.0".sha256 = "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"; + release."8.12.0".sha256 = "14ijb3qy2hin3g4djx437jmnswxxq7lkfh3dwh9qvrds9a015yg8"; + release."8.11.0".sha256 = "1xcd7c7qlvs0narfba6px34zq0mz8rffnhxw0kzhhg6i4iw115dp"; + release."8.10.0".sha256 = "0bpb4flckn4nqxbs3wjiznyx1k7r8k93qdigp3qwmikp2lxvcbw5"; + release."8.9.0".sha256 = "03qz1w2xb2j5p06liz5yyafl0fl9vprcqm6j0iwi7rxwghl00p01"; + release."8.8.0".sha256 = "1ymxyrvjygscxkfj3qkq66skl3vdjhb670rzvsvgmwrjkrakjnfg"; + release."8.7.0".sha256 = "11c4sdmpd3l6jjl4v6k213z9fhrmmm1xnly3zmzam1wrrdif4ghl"; + release."8.6.0".rev = "v8.6.0"; + release."8.6.0".sha256 = "0553pcsy21cyhmns6k9qggzb67az8kl31d0lwlnz08bsqswigzrj"; + releaseRev = v: "V${v}"; + + mlPlugin = true; + + meta = { license = licenses.lgpl2; }; } diff --git a/pkgs/development/coq-modules/category-theory/default.nix b/pkgs/development/coq-modules/category-theory/default.nix index 1178b1558ff..339bcb9d6b0 100644 --- a/pkgs/development/coq-modules/category-theory/default.nix +++ b/pkgs/development/coq-modules/category-theory/default.nix @@ -1,54 +1,26 @@ -{ stdenv, fetchgit, coq, ssreflect, equations }: +{ lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }: -let - params = - let - v20180709 = { - version = "20180709"; - rev = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead"; - sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs"; - }; - v20190414 = { - version = "20190414"; - rev = "706fdb4065cc2302d92ac2bce62cb59713253119"; - sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay"; - }; - in { - "8.6" = v20180709; - "8.7" = v20180709; - "8.8" = v20190414; - "8.9" = v20190414; - }; - param = params.${coq.coq-version}; -in +with lib; mkCoqDerivation { -stdenv.mkDerivation { + pname = "category-theory"; + owner = "jwiegley"; - name = "coq${coq.coq-version}-category-theory-${param.version}"; + release."20190414".rev = "706fdb4065cc2302d92ac2bce62cb59713253119"; + release."20190414".sha256 = "16lg4xs2wzbdbsn148xiacgl4wq4xwfqjnjkdhfr3w0qh1s81hay"; + release."20180709".rev = "3b9ba7b26a64d49a55e8b6ccea570a7f32c11ead"; + release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs"; - src = fetchgit { - url = "git://github.com/jwiegley/category-theory.git"; - inherit (param) rev sha256; - }; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.8" "8.9"; out = "20190414"; } + { case = range "8.6" "8.7"; out = "20180709"; } + ] null; - buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ]); + mlPlugin = true; propagatedBuildInputs = [ ssreflect equations ]; - buildFlags = [ "JOBS=$(NIX_BUILD_CORES)" ]; - - installPhase = '' - make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install - ''; - - meta = with stdenv.lib; { - homepage = "https://github.com/jwiegley/category-theory"; + meta = { description = "A formalization of category theory in Coq for personal study and practical work"; maintainers = with maintainers; [ jwiegley ]; - platforms = coq.meta.platforms; }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; - }; - } diff --git a/pkgs/development/coq-modules/compcert/default.nix b/pkgs/development/coq-modules/compcert/default.nix new file mode 100644 index 00000000000..3b94a8087d3 --- /dev/null +++ b/pkgs/development/coq-modules/compcert/default.nix @@ -0,0 +1,110 @@ +{ lib, fetchzip, mkCoqDerivation, coq, flocq, compcert +, ocamlPackages, fetchpatch, makeWrapper, coq2html +, stdenv, tools ? stdenv.cc +, version ? null +}: + +with lib; + +let compcert = mkCoqDerivation rec { + + pname = "compcert"; + owner = "AbsInt"; + + inherit version; + releaseRev = v: "v${v}"; + + defaultVersion = with versions; switch coq.version [ + { case = range "8.8" "8.11"; out = "3.8"; } + { case = range "8.12" "8.13"; out = "3.9"; } + ] null; + + release = { + "3.8".sha256 = "1gzlyxvw64ca12qql3wnq3bidcx9ygsklv9grjma3ib4hvg7vnr7"; + "3.9".sha256 = "1srcz2dqrvmbvv5cl66r34zqkm0hsbryk7gd3i9xx4slahc9zvdb"; + }; + + nativeBuildInputs = [ makeWrapper ]; + buildInputs = with ocamlPackages; [ ocaml findlib menhir menhirLib ] ++ [ coq coq2html ]; + propagatedBuildInputs = [ flocq ]; + + enableParallelBuilding = true; + + postPatch = '' + substituteInPlace ./configure \ + --replace \$\{toolprefix\}ar 'ar' \ + --replace '{toolprefix}gcc' '{toolprefix}cc' + ''; + + configurePhase = '' + ./configure -clightgen \ + -prefix $out \ + -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \ + -toolprefix ${tools}/bin/ \ + -use-external-Flocq \ + ${if stdenv.isDarwin then "x86_64-macosx" else "x86_64-linux"} + ''; + + installTargets = "documentation install"; + postInstall = '' + # move man into place + mkdir -p $man/share + mv $out/share/man/ $man/share/ + + # move docs into place + mkdir -p $doc/share/doc/compcert + mv doc/html $doc/share/doc/compcert/ + + # wrap ccomp to undefine _FORTIFY_SOURCE; ccomp invokes cc1 which sets + # _FORTIFY_SOURCE=2 by default, but undefines __GNUC__ (as it should), + # which causes a warning in libc. this suppresses it. + for x in ccomp clightgen; do + wrapProgram $out/bin/$x --add-flags "-U_FORTIFY_SOURCE" + done + ''; + + outputs = [ "out" "lib" "doc" "man" ]; + + meta = with lib; { + description = "Formally verified C compiler"; + homepage = "https://compcert.org"; + license = licenses.inria-compcert; + platforms = [ "x86_64-linux" "x86_64-darwin" ]; + maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ]; + }; +}; in +compcert.overrideAttrs (o: + { + patches = with versions; switch [ coq.version o.version ] [ + { cases = [ (range "8.12.2" "8.13.2") "3.8" ]; + out = [ + # Support for Coq 8.12.2 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/06956421b4307054af221c118c5f59593c0e67b9.patch"; + sha256 = "1f90q6j3xfvnf3z830bkd4d8526issvmdlrjlc95bfsqs78i1yrl"; + }) + # Support for Coq 8.13.0 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/0895388e7ebf9c9f3176d225107e21968919fb97.patch"; + sha256 = "0qhkzgb2xl5kxys81pldp3mr39gd30lvr2l2wmplij319vp3xavd"; + }) + # Support for Coq 8.13.1 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/6bf310dd678285dc193798e89fc2c441d8430892.patch"; + sha256 = "026ahhvpj5pksy90f8pnxgmhgwfqk4kwyvcf8x3dsanvz98d4pj5"; + }) + # Drop support for Coq < 8.9 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/7563a5df926a4c6fb1489a7a4c847641c8a35095.patch"; + sha256 = "05vkslzy399r3dm6dmjs722rrajnyfa30xsyy3djl52isvn4gyfb"; + }) + # Support for Coq 8.13.2 + (fetchpatch { + url = "https://github.com/AbsInt/CompCert/commit/48bc183167c4ce01a5c9ea86e49d60530adf7290.patch"; + sha256 = "0j62lppfk26d1brdp3qwll2wi4gvpx1k70qivpvby5f7dpkrkax1"; + }) + ]; + } + ] []; + } +) diff --git a/pkgs/development/coq-modules/contribs/default.nix b/pkgs/development/coq-modules/contribs/default.nix index d2787f0948e..cb6dedca355 100644 --- a/pkgs/development/coq-modules/contribs/default.nix +++ b/pkgs/development/coq-modules/contribs/default.nix @@ -1,27 +1,16 @@ -{ stdenv, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, callPackage }: -let mkContrib = repo: revs: param: - stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-${repo}-${version}"; - version = param.version; - - src = fetchFromGitHub { +with lib; let mkContrib = pname: coqs: param: + let contribVersion = {version ? null}: mkCoqDerivation ({ + inherit pname version; owner = "coq-contribs"; - repo = repo; - rev = param.rev; - sha256 = param.sha256; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; - - installFlags = - stdenv.lib.optional (stdenv.lib.versionAtLeast coq.coq-version "8.9") "-f Makefile.coq" - ++ [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - passthru = { - compatibleCoqVersions = v: builtins.elem v revs; - }; - }; in + mlPlugin = true; + } // optionalAttrs (builtins.elem coq.coq-version coqs) ({ + defaultVersion = param.version; + release = { "${param.version}" = { inherit (param) rev sha256; }; }; + } // (removeAttrs param [ "version" "rev" "sha256" ])) + ); in + makeOverridable contribVersion {} ; in { aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] { "8.7" = { @@ -353,10 +342,10 @@ let mkContrib = repo: revs: param: sha256 = "02jcp74i5icv92xkq3mcx91786d56622ghgnjiz3b51wfqs6ldic"; }; - firing-squad = mkContrib "firing-squad" [ "8.6" "8.7" ] { - version = "v8.5.0-9-gbe728cd"; - rev = "be728cddbee58088809b51c25425d2a4bdf9b823"; - sha256 = "0i0v5x6lncjasxk22pras3644ff026q8jai45dbimf2fz73312c9"; + firing-squad = mkContrib "firing-squad" [ "8.6" ] { + version = "v8.5.0-9-gbe728cd"; + rev = "be728cddbee58088809b51c25425d2a4bdf9b823"; + sha256 = "0i0v5x6lncjasxk22pras3644ff026q8jai45dbimf2fz73312c9"; }; float = mkContrib "float" [ "8.7" ] { @@ -525,6 +514,7 @@ let mkContrib = repo: revs: param: version = "v8.6.0"; rev = "6279ed83244dc4aec2e23ffb4c87e3f10a50326d"; sha256 = "1yvlnqwa7ka4a0yg0j7zrzvayhsm1shvsjjawjv552sxc9519aag"; + installFlags = [ "COQBIN=$(out)/lib/coq/${coq.coq-version}/bin/" ]; # hack }; ipc = mkContrib "ipc" [ "8.6" "8.7" ] { @@ -635,12 +625,6 @@ let mkContrib = repo: revs: param: sha256 = "19csz50846gvfwmhhc37nmlvf70g53cpb1kpmcnjlj82y8r63ajz"; }; - math-classes = mkContrib "math-classes" [ "8.6" ] { - version = "v8.6.0-19-ge2c6453"; - rev = "e2c6453e2f6cc1b7f0e1371675f4a76b19fab2c7"; - sha256 = "0das56i8wi7v0s30lbadjlfqas1jlq0mm13yxq6s7zqqbdl5r0bk"; - }; - maths = mkContrib "maths" [ "8.5" "8.6" "8.7" ] { version = "v8.6.0"; rev = "75a2f84990c1dc83a18ee7decc1445c122664222"; diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix index 9665c5400d8..410280925dc 100644 --- a/pkgs/development/coq-modules/coq-bits/default.nix +++ b/pkgs/development/coq-modules/coq-bits/default.nix @@ -1,38 +1,24 @@ -{ stdenv, fetchFromGitHub, coq, mathcomp-algebra }: +{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: -let - version = "20190812"; -in +with lib; mkCoqDerivation { + pname = "coq-bits"; + repo = "bits"; + inherit version; + defaultVersion = if versions.isGe "8.7" coq.version then "20190812" else null; -stdenv.mkDerivation { - name = "coq${coq.coq-version}-coq-bits-${version}"; + release."20190812".rev = "1.0.0"; + release."20190812".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl"; - src = fetchFromGitHub { - owner = "coq-community"; - repo = "bits"; - rev = "1.0.0"; - sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl"; - }; - - buildInputs = [ coq ]; - propagatedBuildInputs = [ mathcomp-algebra ]; - - enableParallelBuilding = true; + propagatedBuildInputs = [ mathcomp.algebra ]; 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/bits"; + meta = { 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" "8.11" "8.12" ]; }; } diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index e58e51c63ae..5bf0cd8f835 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -1,43 +1,52 @@ -{ stdenv, fetchFromGitHub, which, coq }: +{ lib, mkCoqDerivation, which, coq, version ? null }: -let params = { - "8.11" = rec { - version = "1.5.0"; - rev = "v${version}"; - sha256 = "0dlw869j6ib58i8fhbr7x3hq2cy088arihhfanv8i08djqml6g8x"; - }; - "8.12" = rec { - version = "1.5.1"; - rev = "v${version}"; - sha256 = "1znjc8c8rivsawmz5bgm9ddl69p62p2pwxphvpap1gfmi5cp8lwi"; - }; -}; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-elpi-${param.version}"; - - src = fetchFromGitHub { - owner = "LPCIC"; - repo = "coq-elpi"; - inherit (param) rev sha256; - }; +with builtins; with lib; let + elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [ + { case = "8.11"; out = { version = "1.11.4"; };} + { case = "8.12"; out = { version = "1.12.0"; };} + { case = "8.13"; out = { version = "1.13.5"; };} + ] {}); +in mkCoqDerivation { + pname = "elpi"; + repo = "coq-elpi"; + owner = "LPCIC"; + inherit version; + defaultVersion = lib.switch coq.coq-version [ + { case = "8.13"; out = "1.10.1"; } + { case = "8.12"; out = "1.8.3_8.12"; } + { case = "8.11"; out = "1.6.3_8.11"; } + ] null; + release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk"; + release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1"; + release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6"; + release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq"; + release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z"; + release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07"; + release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557"; + release."1.8.3_8.12".version = "1.8.3"; + release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y"; + release."1.8.2_8.12".version = "1.8.2"; + release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r"; + release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1"; + release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8"; + release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp"; + release."1.6.3_8.11".version = "1.6.3"; + release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn"; + release."1.6.2_8.11".version = "1.6.2"; + release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53"; + release."1.6.1_8.11".version = "1.6.1"; + release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq"; + release."1.6.0_8.11".version = "1.6.0"; + release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; + releaseRev = v: "v${v}"; nativeBuildInputs = [ which ]; - buildInputs = [ coq coq.ocaml ] ++ (with coq.ocamlPackages; [ findlib elpi ]); - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + mlPlugin = true; + extraBuildInputs = [ elpi ]; meta = { description = "Coq plugin embedding ELPI."; - maintainers = [ stdenv.lib.maintainers.cohencyril ]; - license = stdenv.lib.licenses.lgpl21; - inherit (coq.meta) platforms; - inherit (src.meta) homepage; - }; - - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; + maintainers = [ maintainers.cohencyril ]; + license = licenses.lgpl21Plus; }; } diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix index 9cf30e277f3..6ba798ac328 100644 --- a/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -1,46 +1,29 @@ -{ stdenv, fetchFromGitHub, coq }: - -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.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - "8.9" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - "8.10" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - "8.11" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - "8.12" = { version = "0.11.2"; sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; }; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation rec { - - name = "coq${coq.coq-version}-coq-ext-lib-${version}"; - inherit (param) version; - - src = fetchFromGitHub { - owner = "coq-ext-lib"; - repo = "coq-ext-lib"; - rev = "v${param.version}"; - inherit (param) sha256; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 ]; - propagatedBuildInputs = [ coq ]; - - enableParallelBuilding = true; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { - homepage = "https://github.com/coq-ext-lib/coq-ext-lib"; +{ lib, mkCoqDerivation, coq, version ? null }: + +with lib; mkCoqDerivation rec { + pname = "coq-ext-lib"; + owner = "coq-ext-lib"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { 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.3".sha256 = "1w99nzpk72lffxis97k235axss5lmzhy5z3lga2i0si95mbpil42"; + release."0.11.2".sha256 = "0iyka81g26x5n99xic7kqn8vxqjw8rz7vw9rs27iw04lf137vzv6"; + release."0.10.3".sha256 = "0795gs2dlr663z826mp63c8h2zfadn541dr8q0fvnvi2z7kfyslb"; + release."0.11.1".sha256 = "0dmf1p9j8lm0hwaq0af18jxdwg869xi2jm8447zng7krrq3kvkg5"; + release."0.10.2".sha256 = "1b150rc5bmz9l518r4m3vwcrcnnkkn9q5lrwygkh0a7mckgg2k9f"; + release."0.10.1".sha256 = "0r1vspad8fb8bry3zliiz4hfj4w1iib1l2gm115a94m6zbiksd95"; + release."0.10.0".sha256 = "1kxi5bmjwi5zqlqgkyzhhxwgcih7wf60cyw9398k2qjkmi186r4a"; + release."0.9.7".sha256 = "00v4bm4glv1hy08c8xsm467az6d1ashrznn8p2bmbmmp52lfg7ag"; + release."0.9.5".sha256 = "1b4cvz3llxin130g13calw5n1zmvi6wdd5yb8a41q7yyn2hd3msg"; + release."0.9.4".sha256 = "1y66pamgsdxlq2w1338lj626ln70cwj7k53hxcp933g8fdsa4hp0"; + releaseRev = v: "v${v}"; + + meta = { description = "A collection of theories and plugins that may be useful in other Coq developments"; maintainers = with maintainers; [ jwiegley ptival ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; }; } diff --git a/pkgs/development/coq-modules/coq-haskell/default.nix b/pkgs/development/coq-modules/coq-haskell/default.nix index 7c86a7d55f3..7caf754ae50 100644 --- a/pkgs/development/coq-modules/coq-haskell/default.nix +++ b/pkgs/development/coq-modules/coq-haskell/default.nix @@ -1,60 +1,21 @@ -{ stdenv, fetchgit, coq, ssreflect }: +{ lib, mkCoqDerivation, coq, ssreflect, version ? null }: -let params = - { - "8.5" = { - version = "20171215"; - rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; - sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; - }; +with lib; mkCoqDerivation { - "8.6" = { - version = "20171215"; - rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; - sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; - }; + pname = "coq-haskell"; + owner = "jwiegley"; + inherit version; + defaultVersion = if versions.range "8.5" "8.8" coq.coq-version then "20171215" else null; + release."20171215".rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; + release."20171215".sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; - "8.7" = { - version = "20171215"; - rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; - sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; - }; - - "8.8" = { - version = "20171215"; - rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; - sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; - }; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation { - - name = "coq${coq.coq-version}-coq-haskell-${param.version}"; - - src = fetchgit { - url = "git://github.com/jwiegley/coq-haskell.git"; - inherit (param) rev sha256; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib ]; + mlPlugin = true; + extraInstallFlags = [ "-f Makefile.coq" ]; propagatedBuildInputs = [ coq ssreflect ]; - enableParallelBuilding = false; - installPhase = '' - make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install - ''; - - meta = with stdenv.lib; { - homepage = "https://github.com/jwiegley/coq-haskell"; + meta = { description = "A library for formalizing Haskell types and functions in Coq"; maintainers = with maintainers; [ jwiegley ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; }; } diff --git a/pkgs/development/coq-modules/coqeal/default.nix b/pkgs/development/coq-modules/coqeal/default.nix new file mode 100644 index 00000000000..615c200c633 --- /dev/null +++ b/pkgs/development/coq-modules/coqeal/default.nix @@ -0,0 +1,26 @@ +{ coq, mkCoqDerivation, mathcomp, bignums, paramcoq, multinomials, + lib, which, version ? null }: + +with lib; mkCoqDerivation { + + pname = "CoqEAL"; + owner = "CoqEAL"; + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { 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"; } + ] null; + + release."1.0.5".sha256 = "0cmvky8glb5z2dy3q62aln6qbav4lrf2q1589f6h1gn5bgjrbzkm"; + release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk"; + release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24"; + + extraBuildInputs = [ which ]; + propagatedBuildInputs = [ mathcomp.algebra bignums paramcoq multinomials ]; + + meta = { + description = "CoqEAL - The Coq Effective Algebra Library"; + license = licenses.mit; + }; +} diff --git a/pkgs/development/coq-modules/coqhammer/default.nix b/pkgs/development/coq-modules/coqhammer/default.nix index 56fce9ac526..93582745564 100644 --- a/pkgs/development/coq-modules/coqhammer/default.nix +++ b/pkgs/development/coq-modules/coqhammer/default.nix @@ -1,43 +1,37 @@ -{ stdenv, fetchFromGitHub, coq }: - -let - params = { - "8.8" = { - version = "1.1"; - sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; - buildInputs = [ coq.ocamlPackages.camlp5 ]; - }; - "8.9" = { - version = "1.1.1"; - sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; - buildInputs = [ coq.ocamlPackages.camlp5 ]; - }; - "8.10" = { - version = "1.3"; - sha256 = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd"; - }; - "8.11" = { - version = "1.3"; - sha256 = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b"; - }; - "8.12" = { - version = "1.3"; - sha256 = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8"; - }; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation rec { - inherit (param) version; - name = "coq${coq.coq-version}-coqhammer-${version}"; - - src = fetchFromGitHub { - owner = "lukaszcz"; - repo = "coqhammer"; - rev = "v${version}-coq${coq.coq-version}"; - inherit (param) sha256; - }; +{ lib, mkCoqDerivation, coq, version ? null }: + +with lib; mkCoqDerivation { + inherit version; + pname = "coqhammer"; + owner = "lukaszcz"; + defaultVersion = with versions; switch coq.coq-version [ + { case = "8.13"; out = "1.3.1-coq8.13"; } + { case = "8.12"; out = "1.3.1-coq8.12"; } + { case = "8.11"; out = "1.3.1-coq8.11"; } + { case = "8.10"; out = "1.3.1-coq8.10"; } + { case = "8.9"; out = "1.1.1-coq8.9"; } + { case = "8.8"; out = "1.1-coq8.8"; } + ] null; + release."1.3.1-coq8.13".sha256 = "033j6saw24anb1lqbgsg1zynxi2rnxq7pgqwh11k8r8y3xisz78w"; + release."1.3.1-coq8.12".sha256 = "0xy3vy4rv8w5ydwb9nq8y4dcimd91yr0hak2j4kn02svssg1kv1y"; + release."1.3.1-coq8.11".sha256 = "0i9nlcayq0ac95vc09d1w8sd221gdjs0g215n086qscqjwimnz8j"; + release."1.3.1-coq8.10".sha256 = "0aq9qwqx680lkidhb77fmyq403rvfcdxch849x1pzy6a48rz5yra"; + release."1.3-coq8.12".sha256 = "1q1y3cwhd98pkm98g71fsdjz85bfwgcz2xn7s7wwmiraifv5l6z8"; + release."1.3-coq8.11".sha256 = "08zf8qfna7b9p2myfaz4g7bas3a1q1156x78n5isqivlnqfrjc1b"; + release."1.3-coq8.10".sha256 = "1fj8497ir4m79hyrmmmmrag01001wrby0h24wv6525vz0w5py3cd"; + release."1.1.1-coq8.9".sha256 = "1knjmz4hr8vlp103j8n4fyb2lfxysnm512gh3m2kp85n6as6fvb9"; + release."1.1-coq8.8".sha256 = "0ms086wp4jmrzyglb8wymchzyflflk01nsfsk4r6qv8rrx81nx9h"; + + release."1.3.1-coq8.13".version = "1.3.1"; + release."1.3.1-coq8.12".version = "1.3.1"; + release."1.3.1-coq8.11".version = "1.3.1"; + release."1.3.1-coq8.10".version = "1.3.1"; + release."1.3-coq8.12".version = "1.3"; + release."1.3-coq8.11".version = "1.3"; + release."1.3-coq8.10".version = "1.3"; + release."1.1.1-coq8.9".version = "1.1.1"; + release."1.1-coq8.9".version = "1.1"; + releaseRev = v: "v${v}"; postPatch = '' substituteInPlace Makefile.coq.local --replace \ @@ -46,26 +40,16 @@ stdenv.mkDerivation rec { substituteInPlace Makefile.coq.local --replace 'g++' 'c++' --replace 'gcc' 'cc' ''; - buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ - ocaml findlib - ]) ++ (param.buildInputs or []); - preInstall = '' mkdir -p $out/bin ''; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + mlPlugin = true; meta = { homepage = "http://cl-informatik.uibk.ac.at/cek/coqhammer/"; description = "Automation for Dependent Type Theory"; - license = stdenv.lib.licenses.lgpl21; - inherit (coq.meta) platforms; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; + license = licenses.lgpl21; + maintainers = [ maintainers.vbgl ]; }; - } diff --git a/pkgs/development/coq-modules/coqprime/default.nix b/pkgs/development/coq-modules/coqprime/default.nix index 0ead97ffbf0..d738041d5d2 100644 --- a/pkgs/development/coq-modules/coqprime/default.nix +++ b/pkgs/development/coq-modules/coqprime/default.nix @@ -1,56 +1,29 @@ -{ stdenv, which, fetchFromGitHub, coq, bignums }: - -let - params = - let v_8_8 = { - version = "8.8"; - sha256 = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5"; - }; - v_8_10 = { - version = "8.10"; - sha256 = "0r9gnh5a5ykiiz5h1i8xnzgiydpwc4z9qhndxyya85xq0f910qaz"; - }; - in - { - "8.7" = { - version = "8.7.2"; - sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k"; - }; - "8.8" = v_8_8; - "8.9" = v_8_8; - "8.10" = v_8_10; - "8.11" = v_8_10; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation rec { - - inherit (param) version; - name = "coq${coq.coq-version}-coqprime-${version}"; - - src = fetchFromGitHub { - owner = "thery"; - repo = "coqprime"; - rev = "v${version}"; - inherit (param) sha256; - }; - - buildInputs = [ which coq ]; - +{ which, lib, mkCoqDerivation, coq, bignums, version ? null }: + +with lib; mkCoqDerivation { + + pname = "coqprime"; + owner = "thery"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.12" "8.13"; out = "8.12"; } + { case = range "8.10" "8.11"; out = "8.10"; } + { case = range "8.8" "8.9"; out = "8.8"; } + { case = "8.7"; out = "8.7.2"; } + ] null; + + release."8.12".sha256 = "1slka4w0pya15js4drx9frj7lxyp3k2lzib8v23givzpnxs8ijdj"; + release."8.10".sha256 = "0r9gnh5a5ykiiz5h1i8xnzgiydpwc4z9qhndxyya85xq0f910qaz"; + release."8.8".sha256 = "075yjczk79pf1hd3lgdjiz84ilkzfxjh18lgzrhhqp7d3kz5lxp5"; + release."8.7.2".sha256 = "15zlcrx06qqxjy3nhh22wzy0rb4npc8l4nx2bbsfsvrisbq1qb7k"; + releaseRev = v: "v${v}"; + + extraBuildInputs = [ which ]; propagatedBuildInputs = [ bignums ]; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { + meta = with lib; { description = "Library to certify primality using Pocklington certificate and Elliptic Curve Certificate"; license = licenses.lgpl21; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - inherit (coq.meta) platforms; - inherit (src.meta) homepage; - }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; + maintainers = [ maintainers.vbgl ]; }; } diff --git a/pkgs/development/coq-modules/coqtail-math/default.nix b/pkgs/development/coq-modules/coqtail-math/default.nix new file mode 100644 index 00000000000..891d1fae62c --- /dev/null +++ b/pkgs/development/coq-modules/coqtail-math/default.nix @@ -0,0 +1,19 @@ +{ lib, mkCoqDerivation, coq, version ? null }: + +with lib; + +mkCoqDerivation { + pname = "coqtail-math"; + owner = "coq-community"; + inherit version; + defaultVersion = if versions.range "8.11" "8.13" coq.coq-version then "20201124" else null; + release."20201124".rev = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e"; + release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ="; + + buildInputs = with coq.ocamlPackages; [ ocaml findlib ]; + + meta = { + license = licenses.lgpl3Only; + maintainers = [ maintainers.siraben ]; + }; +} diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix index e45077f89fd..b7f5802b9d4 100644 --- a/pkgs/development/coq-modules/coquelicot/default.nix +++ b/pkgs/development/coq-modules/coquelicot/default.nix @@ -1,43 +1,29 @@ -{ stdenv, fetchurl, which, coq, ssreflect }: +{ lib, mkCoqDerivation, which, autoconf, + coq, ssreflect, version ? null }: -let param = - if stdenv.lib.versionAtLeast coq.coq-version "8.8" - then { - version = "3.1.0"; - uid = "38287"; - sha256 = "07436wkvnq9jyf7wyhp77bpl157s3qhba1ay5xrkxdi26qdf3h14"; - } else { - version = "3.0.2"; - uid = "37523"; - sha256 = "1biia7nfqf7vaqq5gmykl4rwjyvrcwss6r2jdf0in5pvp2rnrj2w"; - } -; in +with lib; mkCoqDerivation { + pname = "coquelicot"; + owner = "coquelicot"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.8" ; out = "3.2.0"; } + { case = range "8.8" "8.13"; out = "3.1.0"; } + { case = range "8.5" "8.9"; out = "3.0.2"; } + ] null; + release."3.2.0".sha256 = "07w7dbl8x7xxnbr2q39wrdh054gvi3daqjpdn1jm53crsl1fjxm4"; + release."3.1.0".sha256 = "02i0djar13yk01hzaqprcldhhscn9843x9nf6x3jkv4wv1jwnx9f"; + release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl"; + releaseRev = v: "coquelicot-${v}"; -stdenv.mkDerivation { - name = "coq${coq.coq-version}-coquelicot-${param.version}"; - src = fetchurl { - url = "https://gforge.inria.fr/frs/download.php/file/${param.uid}/coquelicot-${param.version}.tar.gz"; - inherit (param) sha256; - }; - - nativeBuildInputs = [ which ]; - buildInputs = [ coq ]; + nativeBuildInputs = [ which autoconf ]; propagatedBuildInputs = [ ssreflect ]; - - configureFlags = [ "--libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Coquelicot" ]; - buildPhase = "./remake"; - installPhase = "./remake install"; + useMelquiondRemake.logpath = "Coquelicot"; meta = { homepage = "http://coquelicot.saclay.inria.fr/"; description = "A Coq library for Reals"; - license = stdenv.lib.licenses.lgpl3; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - inherit (coq.meta) platforms; + license = licenses.lgpl3; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; - }; - } diff --git a/pkgs/development/coq-modules/corn/default.nix b/pkgs/development/coq-modules/corn/default.nix index 14ff74506f3..6910f487c64 100644 --- a/pkgs/development/coq-modules/corn/default.nix +++ b/pkgs/development/coq-modules/corn/default.nix @@ -1,38 +1,27 @@ -{ stdenv, fetchFromGitHub, coq, bignums, math-classes }: +{ lib, mkCoqDerivation, coq, bignums, math-classes, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation rec { pname = "corn"; - version = "8.8.1"; - name = "coq${coq.coq-version}-${pname}-${version}"; - src = fetchFromGitHub { - owner = "coq-community"; - repo = pname; - rev = version; - sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp"; + inherit version; + defaultVersion = switch coq.coq-version [ + { case = "8.6"; out = "8.8.1"; } + { case = (versions.range "8.7" "8.12"); out = "8.12.0"; } + ] null; + release = { + "8.8.1".sha256 = "0gh32j0f18vv5lmf6nb87nr5450w6ai06rhrnvlx2wwi79gv10wp"; + "8.12.0".sha256 = "0b92vhyzn1j6cs84z2182fn82hxxj0bqq7hk6cs4awwb3vc7dkhi"; }; - buildInputs = [ coq ]; - preConfigure = "patchShebangs ./configure.sh"; configureScript = "./configure.sh"; dontAddPrefix = true; propagatedBuildInputs = [ bignums math-classes ]; - enableParallelBuilding = true; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - meta = { homepage = "http://c-corn.github.io/"; - license = stdenv.lib.licenses.gpl2; + license = licenses.gpl2; description = "A Coq library for constructive analysis"; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - inherit (coq.meta) platforms; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" ]; - }; - } diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix index 689745003df..203b8bb1b2b 100644 --- a/pkgs/development/coq-modules/dpdgraph/default.nix +++ b/pkgs/development/coq-modules/dpdgraph/default.nix @@ -1,83 +1,60 @@ -{ stdenv, fetchFromGitHub, autoreconfHook, coq }: - -let params = { - "8.11" = { - version = "0.6.7"; - sha256 = "01vpi7scvkl4ls1z2k2x9zd65wflzb667idj759859hlz3ps9z09"; - }; - "8.10" = { - version = "0.6.6"; - sha256 = "1gjrm5zjzw4cisiwdr5b3iqa7s4cssa220xr0k96rwgk61rcjd8w"; - }; - "8.9" = { - version = "0.6.5"; - sha256 = "1f34z24yg05b1096gqv36jr3vffkcjkf9qncii3pzhhvagxd0w2f"; - }; - "8.8" = { - version = "0.6.3"; - rev = "0acbd0a594c7e927574d5f212cc73a486b5305d2"; - sha256 = "0c95b0bz2kjm6swr5na4gs06lxxywradszxbr5ldh2zx02r3f3rx"; - }; - "8.7" = { - version = "0.6.2"; - rev = "d76ddde37d918569945774733b7997e8b24daf51"; - sha256 = "04lnf4b25yarysj848cfl8pd3i3pr3818acyp9hgwdgd1rqmhjwm"; - }; - "8.6" = { - version = "0.6.1"; - rev = "c3b87af6bfa338e18b83f014ebd0e56e1f611663"; - sha256 = "1jaafkwsb5450378nprjsds1illgdaq60gryi8kspw0i25ykz2c9"; - }; - "8.5" = { - version = "0.6"; - sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n"; - }; -}; -param = params.${coq.coq-version}; -in - -let hasWarning = stdenv.lib.versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in - -stdenv.mkDerivation { - name = "coq${coq.coq-version}-dpdgraph-${param.version}"; - src = fetchFromGitHub { - owner = "Karmaki"; - repo = "coq-dpdgraph"; - rev = param.rev or "v${param.version}"; - inherit (param) sha256; - }; +{ lib, mkCoqDerivation, autoreconfHook, coq, version ? null }: + +with lib; +let hasWarning = versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in + +mkCoqDerivation { + pname = "dpdgraph"; + owner = "Karmaki"; + repo = "coq-dpdgraph"; + inherit version; + defaultVersion = switch coq.coq-version [ + { case = "8.13"; out = "0.6.9"; } + { case = "8.12"; out = "0.6.8"; } + { case = "8.11"; out = "0.6.7"; } + { case = "8.10"; out = "0.6.6"; } + { case = "8.9"; out = "0.6.5"; } + { case = "8.8"; out = "0.6.3"; } + { case = "8.7"; out = "0.6.2"; } + { case = "8.6"; out = "0.6.1"; } + { case = "8.5"; out = "0.6"; } + ] null; + + release."0.6.9".sha256 = "11mbydpcgk7y8pqzickbzx0ig7g9k9al71i9yfrcscd2xj8fwj8z"; + release."0.6.8".sha256 = "1mj6sknsd53xfb387sp3kdwvl4wn80ck24bfzf3s6mgw1a12vyps"; + release."0.6.7".sha256 = "01vpi7scvkl4ls1z2k2x9zd65wflzb667idj759859hlz3ps9z09"; + release."0.6.6".sha256 = "1gjrm5zjzw4cisiwdr5b3iqa7s4cssa220xr0k96rwgk61rcjd8w"; + release."0.6.5".sha256 = "1f34z24yg05b1096gqv36jr3vffkcjkf9qncii3pzhhvagxd0w2f"; + release."0.6.3".rev = "0acbd0a594c7e927574d5f212cc73a486b5305d2"; + release."0.6.3".sha256 = "0c95b0bz2kjm6swr5na4gs06lxxywradszxbr5ldh2zx02r3f3rx"; + release."0.6.2".rev = "d76ddde37d918569945774733b7997e8b24daf51"; + release."0.6.2".sha256 = "04lnf4b25yarysj848cfl8pd3i3pr3818acyp9hgwdgd1rqmhjwm"; + release."0.6.1".rev = "c3b87af6bfa338e18b83f014ebd0e56e1f611663"; + release."0.6.1".sha256 = "1jaafkwsb5450378nprjsds1illgdaq60gryi8kspw0i25ykz2c9"; + release."0.6".sha256 = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n"; + releaseRev = v: "v${v}"; nativeBuildInputs = [ autoreconfHook ]; - buildInputs = [ coq ] - ++ (with coq.ocamlPackages; [ ocaml camlp5 findlib ocamlgraph ]); + mlPlugin = true; + extraBuildInputs = [ coq.ocamlPackages.ocamlgraph ]; # dpd_compute.ml uses deprecated Pervasives.compare # Versions prior to 0.6.5 do not have the WARN_ERR build flag - preConfigure = stdenv.lib.optionalString hasWarning '' + preConfigure = optionalString hasWarning '' substituteInPlace Makefile.in --replace "-warn-error +a " "" ''; - buildFlags = stdenv.lib.optional hasWarning "WARN_ERR="; + buildFlags = optional hasWarning "WARN_ERR="; preInstall = '' mkdir -p $out/bin ''; - installFlags = [ - "COQLIB=$(out)/lib/coq/${coq.coq-version}/" - "BINDIR=$(out)/bin" - ]; + extraInstallFlags = [ "BINDIR=$(out)/bin" ]; meta = { description = "Build dependency graphs between Coq objects"; - license = stdenv.lib.licenses.lgpl21; - homepage = "https://github.com/Karmaki/coq-dpdgraph/"; - maintainers = with stdenv.lib.maintainers; [ vbgl ]; - platforms = coq.meta.platforms; + license = licenses.lgpl21; + maintainers = with maintainers; [ vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; - }; - } diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix index 5a07d537536..d19d3826c74 100644 --- a/pkgs/development/coq-modules/equations/default.nix +++ b/pkgs/development/coq-modules/equations/default.nix @@ -1,79 +1,55 @@ -{ stdenv, fetchFromGitHub, coq }: - -let - params = { - "8.6" = { - version = "1.0"; - rev = "v1.0"; - sha256 = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj"; - }; - - "8.7" = { - version = "1.0"; - rev = "v1.0-8.7"; - sha256 = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h"; - }; - - "8.8" = { - version = "1.2"; - rev = "v1.2-8.8"; - sha256 = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx"; - }; - - "8.9" = { - version = "1.2.1"; - rev = "v1.2.1-8.9"; - sha256 = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij"; - }; - - "8.10" = { - version = "1.2.1"; - rev = "v1.2.1-8.10-2"; - sha256 = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68"; - }; - - "8.11" = { - version = "1.2.3"; - rev = "v1.2.3-8.11"; - sha256 = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"; - }; - - "8.12" = { - version = "1.2.3"; - rev = "v1.2.3-8.12"; - sha256 = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643"; - }; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation rec { - - name = "coq${coq.coq-version}-equations-${version}"; - version = param.version; - - src = fetchFromGitHub { - owner = "mattam82"; - repo = "Coq-Equations"; - rev = param.rev; - sha256 = param.sha256; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ]; - +{ lib, mkCoqDerivation, coq, version ? null }: + +with lib; mkCoqDerivation { + pname = "equations"; + owner = "mattam82"; + repo = "Coq-Equations"; + inherit version; + defaultVersion = switch coq.coq-version [ + { 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"; } + { case = "8.10"; out = "1.2.1+coq8.10-2"; } + { case = "8.9"; out = "1.2.1+coq8.9"; } + { case = "8.8"; out = "1.2+coq8.8"; } + { case = "8.7"; out = "1.0+coq8.7"; } + { case = "8.6"; out = "1.0+coq8.6"; } + ] null; + + release."1.0+coq8.6".version = "1.0"; + release."1.0+coq8.6".rev = "v1.0"; + release."1.0+coq8.6".sha256 = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj"; + release."1.0+coq8.7".version = "1.0"; + release."1.0+coq8.7".rev = "v1.0-8.7"; + release."1.0+coq8.7".sha256 = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h"; + release."1.2+coq8.8".version = "1.2"; + release."1.2+coq8.8".rev = "v1.2-8.8"; + release."1.2+coq8.8".sha256 = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx"; + release."1.2.1+coq8.9".version = "1.2.1"; + release."1.2.1+coq8.9".rev = "v1.2.1-8.9"; + release."1.2.1+coq8.9".sha256 = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij"; + release."1.2.1+coq8.10-2".version = "1.2.1"; + release."1.2.1+coq8.10-2".rev = "v1.2.1-8.10-2"; + release."1.2.1+coq8.10-2".sha256 = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68"; + release."1.2.3+coq8.11".version = "1.2.3"; + release."1.2.3+coq8.11".rev = "v1.2.3-8.11"; + release."1.2.3+coq8.11".sha256 = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf"; + release."1.2.3+coq8.12".version = "1.2.3"; + release."1.2.3+coq8.12".rev = "v1.2.3-8.12"; + release."1.2.3+coq8.12".sha256 = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643"; + release."1.2.4+coq8.11".rev = "v1.2.4-8.11"; + release."1.2.4+coq8.11".sha256 = "01fihyav8jbjinycgjc16adpa0zy5hcav5mlkf4s9zvqxka21i52"; + release."1.2.4+coq8.12".rev = "v1.2.4-8.12"; + 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"; + + mlPlugin = true; preBuild = "coq_makefile -f _CoqProject -o Makefile"; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - meta = with stdenv.lib; { + meta = { homepage = "https://mattam82.github.io/Coq-Equations/"; description = "A plugin for Coq to add dependent pattern-matching"; maintainers = with maintainers; [ jwiegley ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; }; - } diff --git a/pkgs/development/coq-modules/fiat/HEAD.nix b/pkgs/development/coq-modules/fiat/HEAD.nix index fd3ade0c64b..47f097a34b2 100644 --- a/pkgs/development/coq-modules/fiat/HEAD.nix +++ b/pkgs/development/coq-modules/fiat/HEAD.nix @@ -1,17 +1,17 @@ -{stdenv, fetchgit, coq, python27}: +{lib, mkCoqDerivation, coq, python27, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation rec { + pname = "fiat"; + owner = "mit-plv"; + repo = "fiat"; + displayVersion = { fiat = v: "unstable-${v}"; }; + inherit version; + defaultVersion = if coq.coq-version == "8.5" then "2016-10-24" else null; + release."2016-10-24".rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a"; + release."2016-10-24".sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; - name = "coq-fiat-${coq.coq-version}-unstable-${version}"; - version = "2016-10-24"; - - src = fetchgit { - url = "https://github.com/mit-plv/fiat.git"; - rev = "7feb6c64be9ebcc05924ec58fe1463e73ec8206a"; - sha256 = "0griqc675yylf9rvadlfsabz41qy5f5idya30p5rv6ysiakxya64"; - }; - - buildInputs = [ coq python27 ] ++ (with coq.ocamlPackages; [ ocaml camlp5 ]); + mlPlugin = true; + extraBuildInputs = [ python27 ]; prePatch = "patchShebangs etc/coq-scripts"; @@ -26,14 +26,9 @@ stdenv.mkDerivation rec { cp -pR src/* $COQLIB/user-contrib/Fiat ''; - meta = with stdenv.lib; { + meta = { homepage = "http://plv.csail.mit.edu/fiat/"; description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications"; maintainers = with maintainers; [ jwiegley ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: v == "8.5"; }; } diff --git a/pkgs/development/coq-modules/flocq/default.nix b/pkgs/development/coq-modules/flocq/default.nix index c5d3a295f2b..2598d4e233e 100644 --- a/pkgs/development/coq-modules/flocq/default.nix +++ b/pkgs/development/coq-modules/flocq/default.nix @@ -1,49 +1,26 @@ -{ stdenv, bash, which, autoconf, automake, fetchzip, coq }: - -let params = - if stdenv.lib.versionAtLeast coq.coq-version "8.7" then { - version = "3.3.1"; - sha256 = "0k1nfgiszmai5dihhpfa5mgq9rwigl0n38dw10jn79x89xbdpyh5"; - } else { - version = "2.6.1"; - sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; - } -; in - -stdenv.mkDerivation rec { - - name = "coq${coq.coq-version}-flocq-${version}"; - inherit (params) version; - - src = fetchzip { - url = "https://gitlab.inria.fr/flocq/flocq/-/archive/flocq-${version}.tar.gz"; - inherit (params) sha256; - }; - - nativeBuildInputs = [ bash which autoconf automake ]; - buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ - ocaml camlp5 - ]); - - buildPhase = '' - ${bash}/bin/bash autogen.sh || autoconf - ${bash}/bin/bash configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Flocq - ./remake - ''; - - installPhase = '' - ./remake install - ''; - - meta = with stdenv.lib; { - homepage = "http://flocq.gforge.inria.fr/"; +{ lib, bash, which, autoconf, automake, + mkCoqDerivation, coq, version ? null }: + +with lib; mkCoqDerivation { + pname = "flocq"; + owner = "flocq"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.7"; out = "3.3.1"; } + { case = range "8.5" "8.8"; out = "2.6.1"; } + ] null; + release."3.3.1".sha256 = "1mk8adhi5hrllsr0hamzk91vf2405sjr4lh5brg9201mcw11abkz"; + release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj"; + releaseRev = v: "flocq-${v}"; + + nativeBuildInputs = [ bash which autoconf ]; + mlPlugin = true; + useMelquiondRemake.logpath = "Flocq"; + + meta = { description = "A floating-point formalization for the Coq system"; license = licenses.lgpl3; maintainers = with maintainers; [ jwiegley ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.5" "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; }; } diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix new file mode 100644 index 00000000000..4de6e2da8b5 --- /dev/null +++ b/pkgs/development/coq-modules/fourcolor/default.nix @@ -0,0 +1,24 @@ +{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: +with lib; + +mkCoqDerivation { + pname = "fourcolor"; + owner = "math-comp"; + + release."1.2.3".rev = "v1.2.3"; + 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"; } + ] null; + + propagatedBuildInputs = [ mathcomp.algebra ]; + + meta = { + description = "Formal proof of the Four Color Theorem "; + maintainers = with maintainers; [ siraben ]; + license = licenses.cecill-b; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/coq-modules/gappalib/default.nix index eb431b9faf2..a835d53fded 100644 --- a/pkgs/development/coq-modules/gappalib/default.nix +++ b/pkgs/development/coq-modules/gappalib/default.nix @@ -1,30 +1,24 @@ -{ stdenv, fetchurl, which, coq, flocq }: +{ which, lib, mkCoqDerivation, autoconf, coq, flocq, version ? null }: -stdenv.mkDerivation { - name = "coq${coq.coq-version}-gappalib-1.4.3"; - src = fetchurl { - url = "https://gforge.inria.fr/frs/download.php/file/38302/gappalib-coq-1.4.3.tar.gz"; - sha256 = "108k9dks04wbcqz38pf0zz11hz5imbzimpnkgjrk5gp1hifih370"; - }; +with lib; mkCoqDerivation { + pname = "gappalib"; + repo = "coq"; + owner = "gappa"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = if versions.isGe "8.8" coq.coq-version then "1.4.5" else null; + release."1.4.5".sha256 = "081hib1d9wfm29kis390qsqch8v6fs3q71g2rgbbzx5y5cf48n9k"; + release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l"; + releaseRev = v: "gappalib-coq-${v}"; - nativeBuildInputs = [ which ]; - buildInputs = [ coq coq.ocamlPackages.ocaml ]; + nativeBuildInputs = [ which autoconf ]; + mlPlugin = true; propagatedBuildInputs = [ flocq ]; - - configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Gappa"; - buildPhase = "./remake"; - installPhase = "./remake install"; + useMelquiondRemake.logpath = "Gappa"; meta = { description = "Coq support library for Gappa"; - license = stdenv.lib.licenses.lgpl21; - homepage = "http://gappa.gforge.inria.fr/"; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - inherit (coq.meta) platforms; + license = licenses.lgpl21; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.8" "8.9" "8.10" "8.11" ]; - }; - } diff --git a/pkgs/development/coq-modules/goedel/default.nix b/pkgs/development/coq-modules/goedel/default.nix new file mode 100644 index 00000000000..f6ed9491e98 --- /dev/null +++ b/pkgs/development/coq-modules/goedel/default.nix @@ -0,0 +1,24 @@ +{ lib, mkCoqDerivation, coq, hydra-battles, pocklington, version ? null }: +with lib; + +mkCoqDerivation { + pname = "goedel"; + owner = "coq-community"; + + release."8.12.0".rev = "v8.12.0"; + release."8.12.0".sha256 = "sha256-4lAwWFHGUzPcfHI9u5b+N+7mQ0sLJ8bH8beqQubfFEQ="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.11"; out = "8.12.0"; } + ] null; + + propagatedBuildInputs = [ hydra-battles pocklington ]; + + meta = { + description = "The Gödel-Rosser 1st incompleteness theorem in Coq"; + maintainers = with maintainers; [ siraben ]; + license = licenses.mit; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix index d0445c83ca5..4bf9139b494 100644 --- a/pkgs/development/coq-modules/heq/default.nix +++ b/pkgs/development/coq-modules/heq/default.nix @@ -1,30 +1,23 @@ -{stdenv, fetchurl, coq, unzip}: - -stdenv.mkDerivation rec { - - name = "coq-heq-${coq.coq-version}-${version}"; - version = "0.92"; - - src = fetchurl { - url = "https://www.mpi-sws.org/~gil/Heq/download/Heq-${version}.zip"; - sha256 = "03y71c4qs6cmy3s2hjs05g7pcgk9sqma6flj15394yyxbvr9is1p"; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ]; +{lib, fetchzip, mkCoqDerivation, coq, version ? null }: + +with lib; mkCoqDerivation { + pname = "heq"; + repo = "Heq"; + owner = "gil"; + domain = "mpi-sws.org"; + inherit version fetcher; + defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null; + release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74"; + + mlPlugin = true; propagatedBuildInputs = [ coq ]; + extraInstallFlags = [ "COQLIB=$out/lib/coq/${coq.coq-version}" ]; preBuild = "cd src"; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}" ]; - - meta = with stdenv.lib; { + meta = { homepage = "https://www.mpi-sws.org/~gil/Heq/"; description = "Heq : a Coq library for Heterogeneous Equality"; maintainers = with maintainers; [ jwiegley ]; - platforms = coq.meta.platforms; - }; - - passthru = { - compatibleCoqVersions = v: !stdenv.lib.versionAtLeast v "8.8"; }; } diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix index 9be8459ee9f..491ff959ece 100644 --- a/pkgs/development/coq-modules/hierarchy-builder/default.nix +++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix @@ -1,43 +1,30 @@ -{ stdenv, fetchFromGitHub, which, coq, coq-elpi }: +{ lib, mkCoqDerivation, which, coq, coq-elpi, version ? null }: -let - versions = { - "0.10.0" = { - rev = "v0.10.0"; - sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h"; - }; - }; - version = x: versions.${x} // {version = x;}; - params = { - "8.11" = version "0.10.0"; - "8.12" = version "0.10.0"; - }; - param = params.${coq.coq-version}; -in +with lib; mkCoqDerivation { + pname = "hierarchy-builder"; + 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"; } + ] null; + release."1.1.0".sha256 = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q="; + release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp"; + release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h"; + releaseRev = v: "v${v}"; -stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-hierarchy-builder-${param.version}"; - - src = fetchFromGitHub { - owner = "math-comp"; - repo = "hierarchy-builder"; - inherit (param) rev sha256; - }; + nativeBuildInputs = [ which ]; propagatedBuildInputs = [ coq-elpi ]; - buildInputs = [ coq coq.ocaml coq.ocamlPackages.elpi ]; - installPhase = ''make -f Makefile.coq VFILES=structures.v COQLIB=$out/lib/coq/${coq.coq-version}/ install''; + mlPlugin = true; - meta = { - description = "Coq plugin embedding ELPI."; - maintainers = [ stdenv.lib.maintainers.cohencyril ]; - license = stdenv.lib.licenses.lgpl21; - inherit (coq.meta) platforms; - inherit (src.meta) homepage; - }; + installFlags = [ "DESTDIR=$(out)" "COQMF_COQLIB=lib/coq/${coq.coq-version}" ]; + extraInstallFlags = [ "VFILES=structures.v" ]; - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; + meta = { + description = "High level commands to declare a hierarchy based on packed classes"; + maintainers = with maintainers; [ cohencyril siraben ]; + license = licenses.mit; }; } diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix new file mode 100644 index 00000000000..a74eec4b64f --- /dev/null +++ b/pkgs/development/coq-modules/hydra-battles/default.nix @@ -0,0 +1,29 @@ +{ lib, mkCoqDerivation, coq, mathcomp, equations, paramcoq, version ? null }: +with lib; + +mkCoqDerivation { + pname = "hydra-battles"; + owner = "coq-community"; + + release."0.3".rev = "v0.3"; + release."0.3".sha256 = "sha256-rXP/vJqVEg2tN/I9LWV13YQ1+C7M6lzGu3oI+7pSZzg="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.11"; out = "0.3"; } + ] null; + + propagatedBuildInputs = [ mathcomp equations paramcoq ]; + + meta = { + description = "Variations on Kirby & Paris' hydra battles and other entertaining math in Coq"; + longDescription = '' + Variations on Kirby & Paris' hydra battles and other + entertaining math in Coq (collaborative, documented, includes + exercises) + ''; + maintainers = with maintainers; [ siraben ]; + license = licenses.mit; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix index e72fe7845c8..cdb90452365 100644 --- a/pkgs/development/coq-modules/interval/default.nix +++ b/pkgs/development/coq-modules/interval/default.nix @@ -1,62 +1,29 @@ -{ stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp -, bignums ? null }: - -let params = - let - v3_3 = { - version = "3.3.0"; - uid = "37077"; - sha256 = "08fdcf3hbwqphglvwprvqzgkg0qbimpyhnqsgv3gac4y1ap0f903"; - }; - v3_4 = { - version = "3.4.2"; - uid = "38288"; - sha256 = "00bgzbji0gkazwxhs4q8gz4ccqsa1y1r0m0ravr18ps2h8a8qva5"; - }; - v4_0 = { - version = "4.0.0"; - uid = "38339"; - sha256 = "19sbrv7jnzyxji7irfslhr9ralc0q3gx20nymig5vqbn3vssmgpz"; - }; - in { - "8.5" = v3_3; - "8.6" = v3_3; - "8.7" = v3_4; - "8.8" = v4_0; - "8.9" = v4_0; - "8.10" = v4_0; - "8.11" = v4_0; - "8.12" = v4_0; - }; - param = params."${coq.coq-version}"; -in - -stdenv.mkDerivation { - name = "coq${coq.coq-version}-interval-${param.version}"; - - src = fetchurl { - url = "https://gforge.inria.fr/frs/download.php/file/${param.uid}/interval-${param.version}.tar.gz"; - inherit (param) sha256; - }; - - nativeBuildInputs = [ which ]; - buildInputs = [ coq ]; +{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, bignums ? null, version ? null }: + +with lib; mkCoqDerivation { + pname = "interval"; + owner = "coqinterval"; + domain = "gitlab.inria.fr"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.8" ; out = "4.1.1"; } + { 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.1.1".sha256 = "sha256-h2NJ6sZt1C/88v7W2xyuftEDoyRt3H6kqm5g2hc1aoU="; + release."4.0.0".sha256 = "1hhih6zmid610l6c8z3x4yzdzw9jniyjiknd1vpkyb2rxvqm3gzp"; + release."3.4.2".sha256 = "07ngix32qarl3pjnm9d0vqc9fdrgm08gy7zp306hwxjyq7h1v7z0"; + release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz"; + releaseRev = v: "interval-${v}"; + + nativeBuildInputs = [ which autoconf ]; propagatedBuildInputs = [ bignums coquelicot flocq ]; + useMelquiondRemake.logpath = "Interval"; - configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Interval"; - buildPhase = "./remake"; - installPhase = "./remake install"; - - meta = with stdenv.lib; { - homepage = "http://coq-interval.gforge.inria.fr/"; + meta = with lib; { description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant"; license = licenses.cecill-c; maintainers = with maintainers; [ vbgl ]; - platforms = coq.meta.platforms; }; - - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; - }; - } diff --git a/pkgs/development/coq-modules/iris/default.nix b/pkgs/development/coq-modules/iris/default.nix index 6826e07d613..d2d9870f320 100644 --- a/pkgs/development/coq-modules/iris/default.nix +++ b/pkgs/development/coq-modules/iris/default.nix @@ -1,33 +1,23 @@ -{ stdenv, fetchFromGitLab, coq, stdpp }: +{ lib, mkCoqDerivation, coq, stdpp, version ? null }: -stdenv.mkDerivation rec { - version = "3.3.0"; - name = "coq${coq.coq-version}-iris-${version}"; - src = fetchFromGitLab { - domain = "gitlab.mpi-sws.org"; - owner = "iris"; - repo = "iris"; - rev = "iris-${version}"; - sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp"; - }; +with lib; mkCoqDerivation rec { + pname = "iris"; + domain = "gitlab.mpi-sws.org"; + 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"; } + ] null; + release."3.4.0".sha256 = "0vdc2mdqn5jjd6yz028c0c6blzrvpl0c7apx6xas7ll60136slrb"; + release."3.3.0".sha256 = "0az4gkp5m8sq0p73dlh0r7ckkzhk7zkg5bndw01bdsy5ywj0vilp"; + releaseRev = v: "iris-${v}"; - buildInputs = [ coq ]; propagatedBuildInputs = [ stdpp ]; - enableParallelBuilding = true; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - meta = { - homepage = "https://gitlab.mpi-sws.org/FP/iris-coq"; description = "The Coq development of the Iris Project"; - inherit (coq.meta) platforms; - license = stdenv.lib.licenses.bsd3; - maintainers = [ stdenv.lib.maintainers.vbgl ]; + license = licenses.bsd3; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.9" "8.10" "8.11" "8.12" ]; - }; - } diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix new file mode 100644 index 00000000000..66791b13061 --- /dev/null +++ b/pkgs/development/coq-modules/itauto/default.nix @@ -0,0 +1,24 @@ +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; + +mkCoqDerivation rec { + pname = "itauto"; + owner = "fbesson"; + domain = "gitlab.inria.fr"; + + 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"; } + ] null; + + mlPlugin = true; + extraBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); + enableParallelBuilding = false; + + meta = { + description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support"; + maintainers = with maintainers; [ siraben ]; + license = licenses.gpl3Plus; + }; +} diff --git a/pkgs/development/coq-modules/ltac2/default.nix b/pkgs/development/coq-modules/ltac2/default.nix index 92484f169c1..1d0d03fb7f7 100644 --- a/pkgs/development/coq-modules/ltac2/default.nix +++ b/pkgs/development/coq-modules/ltac2/default.nix @@ -1,57 +1,28 @@ -{ stdenv, fetchFromGitHub, which, coq }: +{ lib, mkCoqDerivation, which, coq, version ? null }: -let params = { - "8.7" = { - version = "0.1"; - rev = "v0.1-8.7"; - sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0"; - }; - "8.8" = { - version = "0.1"; - rev = "0.1"; - sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7"; - }; - "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 - -stdenv.mkDerivation rec { - inherit (param) version; - name = "coq${coq.coq-version}-ltac2-${version}"; - - src = fetchFromGitHub { - owner = "coq"; - repo = "ltac2"; - inherit (param) rev sha256; - }; +with lib; mkCoqDerivation { + pname = "ltac2"; + owner = "coq"; + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = "8.10"; out = "0.3"; } + { case = "8.9"; out = "0.2"; } + { case = "8.8"; out = "0.1"; } + { case = "8.7"; out = "0.1-8.7"; } + ] null; + release."0.3".sha256 = "0pzs5nsakh4l8ffwgn4ryxbnxdv2x0r1i7bc598ij621haxdirrr"; + release."0.2".sha256 = "0xby1kb26r9gcvk5511wqj05fqm9paynwfxlfqkmwkgnfmzk0x73"; + release."0.1".sha256 = "1zz26cyv99whj7rrpgnhhm9dfqnpmrx5pqizn8ihf8jkq8d4drz7"; + release."0.1-8.7".version = "0.1"; + release."0.1-8.7".rev = "v0.1-8.7"; + release."0.1-8.7".sha256 = "0l6wiwi4cvd0i324fb29i9mdh0ijlxzggw4mrjjy695l2qdnlgg0"; nativeBuildInputs = [ which ]; - 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}/" ]; + mlPlugin = true; meta = { description = "A robust and expressive tactic language for Coq"; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - license = stdenv.lib.licenses.lgpl21; - inherit (coq.meta) platforms; - inherit (src.meta) homepage; - }; - - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; + maintainers = [ maintainers.vbgl ]; + license = licenses.lgpl21; }; } diff --git a/pkgs/development/coq-modules/math-classes/default.nix b/pkgs/development/coq-modules/math-classes/default.nix index 73e420b326d..e61019b91c6 100644 --- a/pkgs/development/coq-modules/math-classes/default.nix +++ b/pkgs/development/coq-modules/math-classes/default.nix @@ -1,30 +1,19 @@ -{ stdenv, fetchFromGitHub, coq, bignums }: +{ lib, mkCoqDerivation, coq, bignums, version ? null }: -stdenv.mkDerivation rec { +with lib; mkCoqDerivation { - name = "coq${coq.coq-version}-math-classes-${version}"; - version = "8.11.0"; + 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; + release."8.12.0".sha256 = "14nd6a08zncrl5yg2gzk0xf4iinwq4hxnsgm4fyv07ydbkxfb425"; + release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby"; - src = fetchFromGitHub { - owner = "coq-community"; - repo = "math-classes"; - rev = version; - sha256 = "1hjgncvm1m46lw6264w4dqsy8dbh74vhmzq52x0fba2yqlvy94sf"; - }; - - buildInputs = [ coq bignums ]; - enableParallelBuilding = true; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; + extraBuildInputs = [ bignums ]; - meta = with stdenv.lib; { + meta = { homepage = "https://math-classes.github.io"; description = "A library of abstract interfaces for mathematical structures in Coq."; maintainers = with maintainers; [ siddharthist jwiegley ]; - platforms = coq.meta.platforms; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" ]; - }; - } diff --git a/pkgs/development/coq-modules/mathcomp-abel/default.nix b/pkgs/development/coq-modules/mathcomp-abel/default.nix new file mode 100644 index 00000000000..2a8c006b27c --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-abel/default.nix @@ -0,0 +1,23 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-real-closed, lib, version ? null }: + +mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "abel"; + owner = "math-comp"; + + release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3"; + + inherit version; + defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.10" "8.13") (range "1.11.0" "1.12.0") ]; out = "1.0.0"; } + ] null; + + propagatedBuildInputs = [ mathcomp.field mathcomp-real-closed ]; + + meta = with lib; { + description = "Abel - Galois and Abel - Ruffini Theorems"; + license = licenses.cecill-b; + maintainers = [ maintainers.cohencyril ]; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix new file mode 100644 index 00000000000..b06f057f82e --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-analysis/default.nix @@ -0,0 +1,44 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, mathcomp-real-closed, + hierarchy-builder, lib, version ? null }: + +with lib; +let mca = mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "analysis"; + owner = "math-comp"; + + release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4="; + release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5"; + release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c"; + release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867"; + release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; + release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; + + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (range "8.11" "8.13") "1.12.0" ]; out = "0.3.9"; } + { 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"; } + { cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; } + { cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; } + ] null; + + propagatedBuildInputs = + [ mathcomp.ssreflect mathcomp.field + mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ]; + + meta = { + description = "Analysis library compatible with Mathematical Components"; + maintainers = [ maintainers.cohencyril ]; + license = licenses.cecill-c; + }; +}; in +mca.overrideAttrs (o: + let ext = { propagatedBuildInputs = o.propagatedBuildInputs + ++ [ hierarchy-builder ]; }; + in with versions; switch o.version [ + {case = "dev"; out = ext;} + {case = isGe "0.3.4"; out = ext;} + ] {} +) diff --git a/pkgs/development/coq-modules/mathcomp-bigenough/default.nix b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix new file mode 100644 index 00000000000..296bd738928 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-bigenough/default.nix @@ -0,0 +1,19 @@ +{ coq, mkCoqDerivation, mathcomp, lib, version ? null }: + +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "bigenough"; + owner = "math-comp"; + + release = { "1.0.0".sha256 = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg"; }; + inherit version; + defaultVersion = "1.0.0"; + + propagatedBuildInputs = [ mathcomp.ssreflect ]; + + meta = { + description = "A small library to do epsilon - N reasonning"; + license = licenses.cecill-b; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix new file mode 100644 index 00000000000..c506d07e457 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix @@ -0,0 +1,36 @@ +{ coq, mkCoqDerivation, mathcomp, lib, version ? null }: + +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "finmap"; + owner = "math-comp"; + inherit version; + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (isGe "8.10") (range "1.11" "1.12") ]; 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"; } + { cases = [ (range "8.7" "8.11.0") (range "1.8" "1.10") ]; out = "1.3.4"; } + { cases = [ (range "8.7" "8.9") "1.7.0" ]; out = "1.1.0"; } + { cases = [ (range "8.6" "8.7") (range "1.6.1" "1.7") ]; out = "1.0.0"; } + ] null; + release = { + "1.5.1".sha256 = "0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7"; + "1.5.0".sha256 = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq"; + "1.4.1".sha256 = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p"; + "1.4.0+coq-8.11".sha256 = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb"; + "1.4.0".sha256 = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd"; + "1.3.4".sha256 = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii"; + "1.2.1".sha256 = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf"; + "1.1.0".sha256 = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a"; + "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa"; + }; + + propagatedBuildInputs = [ mathcomp.ssreflect ]; + + meta = { + description = "A finset and finmap library"; + license = licenses.cecill-b; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix new file mode 100644 index 00000000000..dbd1550c6a7 --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix @@ -0,0 +1,33 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-bigenough, + lib, version ? null }: + +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "real-closed"; + owner = "math-comp"; + inherit version; + release = { + "1.1.2".sha256 = "0907x4nf7nnvn764q3x9lx41g74rilvq5cki5ziwgpsdgb98pppn"; + "1.1.1".sha256 = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b"; + "1.0.5".sha256 = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2"; + "1.0.4".sha256 = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b"; + "1.0.3".sha256 = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb"; + "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg"; + }; + + defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ + { cases = [ (isGe "8.10") "1.12.0" ]; out = "1.1.2"; } + { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.1.1"; } + { cases = [ (isGe "8.7") (range "1.9.0" "1.10.0") ]; out = "1.0.4"; } + { cases = [ (isGe "8.7") "1.8.0" ]; out = "1.0.3"; } + { cases = [ (isGe "8.7") "1.7.0" ]; out = "1.0.1"; } + ] null; + + propagatedBuildInputs = [ mathcomp.ssreflect mathcomp.field mathcomp-bigenough ]; + + meta = { + description = "Mathematical Components Library on real closed fields"; + license = licenses.cecill-c; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix new file mode 100644 index 00000000000..65af999d08f --- /dev/null +++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix @@ -0,0 +1,22 @@ +{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }: + +with lib; mkCoqDerivation rec { + pname = "mathcomp-zify"; + repo = "mczify"; + owner = "math-comp"; + inherit version; + + defaultVersion = with versions; + switch [ coq.coq-version mathcomp-algebra.version ] [ + { cases = [ (isEq "8.13") (isEq "1.12") ]; out = "1.0.0+1.12+8.13"; } + ] null; + + release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k"; + + propagatedBuildInputs = [ mathcomp-algebra ]; + + meta = { + description = "Micromega tactics for Mathematical Components"; + maintainers = with maintainers; [ cohencyril ]; + }; +} diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index 8cf502a1943..4637edebdb7 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -1,263 +1,117 @@ -############################# -# Main derivation: mathcomp # -######################################################################## -# This file mainly provides the `mathcomp` derivation, which is # -# essentially a meta-package containing all core mathcomp libraries # -# (ssreflect fingroup algebra solvable field character). They can be # -# accessed individually through the paththrough attributes of mathcomp # -# bearing the same names (mathcomp.ssreflect, etc). # -# # -# Do not use overrideAttrs, but overrideMathcomp instead, which # -# regenerate a full mathcomp derivation with sub-derivations, and # -# behave the same as `mathcomp_`, described below. # -######################################################################## - -############################################################ -# Compiling a custom version of mathcomp using `mathcomp_` # -############################################################################## -# The prefered way to compile a custom version of mathcomp (other than a # -# released version which should be added to `mathcomp-config-initial` # -# and pushed to nixpkgs), is to apply the function `coqPackages.mathcomp_` # -# to either: # -# - a string without slash, which is interpreted as a github revision, # -# i.e. either a tag, a branch or a commit hash # -# - a string with slashes "owner/p_1/.../p_n", which is interpreted as # -# github owner "owner" and revision "p_1/.../p_n". # -# - a path which is interpreted as a local source for the repository, # -# the name of the version is taken to be the basename of the path # -# i.e. if the path is /home/you/git/package/branch/, # -# then "branch" is the name of the version # -# - an attribute set which overrides some attributes (e.g. the src) # -# if the version is updated, the name is automatically regenerated using # -# the conventional schema "coq${coq.coq-version}-${pkgname}-${version}" # -# - a "standard" override function (old: new_attrs) to override the default # -# attribute set, so that you can use old.${field} to patch the derivation. # -############################################################################## - -######################################################################### -# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix # -######################################################################### - -################################# -# Adding a new mathcomp version # -############################################################################# -# When adding a new version of mathcomp, add an attribute to `sha256` (use # -# ```sh # -# nix-prefetch-url --unpack # -# https://github.com/math-comp/math-comp/archive/version.tar.gz # -# ``` # -# to get the corresponding `sha256`) and to `coq-version` (read the release # -# notes to check which versions of coq it is compatible with). Then add # -# it in `preference version`, if not all mathcomp-extra packages are # -# ready, you might want to give new release secondary priority. # -############################################################################# - - -{ stdenv, fetchFromGitHub, ncurses, which, graphviz, - recurseIntoAttrs, withDoc ? false, - coqPackages, - mathcomp_, mathcomp, mathcomp-config, -}: -with builtins // stdenv.lib; +############################################################################ +# This file mainly provides the `mathcomp` derivation, which is # +# essentially a meta-package containing all core mathcomp libraries # +# (ssreflect fingroup algebra solvable field character). They can be # +# accessed individually through the passthrough attributes of mathcomp # +# bearing the same names (mathcomp.ssreflect, etc). # +############################################################################ +# Compiling a custom version of mathcomp using `mathcomp.override`. # +# This is the replacement for the former `mathcomp_ config` function. # +# See the documentation at doc/languages-frameworks/coq.section.md. # +############################################################################ + +{ lib, ncurses, which, graphviz, lua, fetchzip, + mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, + coqPackages, coq, ocamlPackages, version ? null }@args: +with builtins // lib; let - mathcomp-config-initial = rec { - ####################################################################### - # CONFIGURATION (please edit this), it is exported as mathcomp-config # - ####################################################################### - # sha256 of released mathcomp versions - sha256 = { - "1.11.0" = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; - "1.11+beta1" = "12i3zznwajlihzpqsiqniv20rklj8d8401lhd241xy4s21fxkkjm"; - "1.10.0" = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; - "1.9.0" = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; - "1.8.0" = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp"; - "1.7.0" = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; - "1.6.1" = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; - }; - # versions of coq compatible with released mathcomp versions - coq-versions = { - "1.11.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; - "1.11+beta1" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; - "1.10.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ]; - "1.9.0" = flip elem [ "8.7" "8.8" "8.9" "8.10" ]; - "1.8.0" = flip elem [ "8.7" "8.8" "8.9" ]; - "1.7.0" = flip elem [ "8.6" "8.7" "8.8" "8.9" ]; - "1.6.1" = flip elem [ "8.5"]; - }; - - # sets the default version of mathcomp given a version of Coq - # this is currently computed using version-perference below - # but it can be set to a fixed version number - preferred-version = let v = head ( - filter (mc: mathcomp-config.coq-versions.${mc} coq.coq-version) - mathcomp-config.version-preferences ++ ["0.0.0"]); - in if v == "0.0.0" then head mathcomp-config.version-preferences else v; - - # mathcomp preferred versions by decreasing order - # (the first version in the list will be tried first) - version-preferences = - [ "1.10.0" "1.11.0" "1.9.0" "1.8.0" "1.7.0" "1.6.1" ]; - - # list of core mathcomp packages sorted by dependency order - packages = _version: # unused in current versions of mathcomp - # because the following list of packages is fixed for - # all versions of mathcomp up to 1.11.0 - [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; - - # compute the dependencies of the core package pkg - # (assuming the total ordering above, change if necessary) - deps = version: pkg: if pkg == "single" then [] else - (pred-split-list (x: x == pkg) (mathcomp-config.packages version)).left; - }; - - ############################################################## - # COMPUTED using the configuration above (edit with caution) # - ############################################################## - - # generic split function (TODO: move to lib?) - pred-split-list = pred: l: - let loop = v: l: if l == [] then {left = v; right = [];} - else let hd = builtins.head l; tl = builtins.tail l; in - if pred hd then {left = v; right = tl;} else loop (v ++ [hd]) tl; - in loop [] l; - - pkgUp = l: r: l // r // { - meta = (l.meta or {}) // (r.meta or {}); - passthru = (l.passthru or {}) // (r.passthru or {}); + repo = "math-comp"; + owner = "math-comp"; + withDoc = single && (args.withDoc or false); + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.13"; out = "1.12.0"; } # lower version of coq to 8.10 when all mathcomp packages are ported + { case = range "8.7" "8.12"; out = "1.11.0"; } + { case = range "8.7" "8.11"; out = "1.10.0"; } + { case = range "8.7" "8.11"; out = "1.9.0"; } + { case = range "8.7" "8.9"; out = "1.8.0"; } + { case = range "8.6" "8.9"; out = "1.7.0"; } + { case = range "8.5" "8.7"; out = "1.6.4"; } + ] null; + release = { + "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; + "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; + "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; + "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; + "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp"; + "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; + "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz"; + "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; }; + releaseRev = v: "mathcomp-${v}"; - coq = coqPackages.coq; - mathcomp-deps = mathcomp-config.deps mathcomp.config.preferred-version; + # list of core mathcomp packages sorted by dependency order + packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; - # default set of attributes given a 'package' name. - # this attribute set will be extended using toOverrideFun - default-attrs = package: - let + mathcomp_ = package: let + mathcomp-deps = if package == "single" then [] + else map mathcomp_ (head (splitList (pred.equal package) packages)); pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; - pkgname = if package == "single" then "mathcomp" else "mathcomp-${package}"; + pname = if package == "single" then "mathcomp" else "mathcomp-${package}"; pkgallMake = '' echo "all.v" > Make echo "-I ." >> Make echo "-R . mathcomp.all" >> Make ''; - in - rec { - version = "master"; - name = "coq${coq.coq-version}-${pkgname}-${version}"; + derivation = mkCoqDerivation ({ + inherit version pname defaultVersion release releaseRev repo owner; - nativeBuildInputs = optionals withDoc [ graphviz ]; - buildInputs = [ ncurses which ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); - propagatedBuildInputs = [ coq ]; - enableParallelBuilding = true; + nativeBuildInputs = optionals withDoc [ graphviz lua ]; + mlPlugin = versions.isLe "8.6" coq.coq-version; + extraBuildInputs = [ ncurses which ]; + propagatedBuildInputs = mathcomp-deps; buildFlags = optional withDoc "doc"; - COQBIN = "${coq}/bin/"; - preBuild = '' - patchShebangs etc/utils/ssrcoqdep || true + if [[ -f etc/utils/ssrcoqdep ]] + then patchShebangs etc/utils/ssrcoqdep + fi + if [[ -f etc/buildlibgraph ]] + then patchShebangs etc/buildlibgraph + fi + '' + '' cd ${pkgpath} '' + optionalString (package == "all") pkgallMake; - installPhase = '' - make -f Makefile.coq COQLIB=$out/lib/coq/${coq.coq-version}/ install - '' + optionalString withDoc '' - make -f Makefile.coq install-doc DOCDIR=$out/share/coq/${coq.coq-version}/ - ''; - - meta = with stdenv.lib; { + meta = { homepage = "https://math-comp.github.io/"; license = licenses.cecill-b; - maintainers = [ maintainers.vbgl maintainers.jwiegley maintainers.cohencyril ]; - platforms = coq.meta.platforms; - }; - - passthru = { - mathcompDeps = mathcomp-deps package; - inherit package mathcomp-config; - compatibleCoqVersions = _: true; - }; - }; - - # converts a string, path or attribute set into an override function - toOverrideFun = overrides: - if isFunction overrides then overrides else old: - let - pkgname = if old.passthru.package == "single" then "mathcomp" - else "mathcomp-${old.passthru.package}"; - - string-attrs = if hasAttr overrides mathcomp-config.sha256 then - let version = overrides; - in { - inherit version; - src = fetchFromGitHub { - owner = "math-comp"; - repo = "math-comp"; - rev = "mathcomp-${version}"; - sha256 = mathcomp-config.sha256.${version}; - }; - passthru = old.passthru // { - compatibleCoqVersions = mathcomp-config.coq-versions.${version}; - mathcompDeps = mathcomp-config.deps version old.passthru.package; - }; - } - else - let splitted = filter isString (split "/" overrides); - owner = head splitted; - ref = concatStringsSep "/" (tail splitted); - version = head (reverseList splitted); - in if length splitted == 1 then { - inherit version; - src = fetchTarball "https://github.com/math-comp/math-comp/archive/${version}.tar.gz"; - } else { - inherit version; - src = fetchTarball "https://github.com/${owner}/math-comp/archive/${ref}.tar.gz"; - }; - - attrs = - if overrides == null || overrides == "" then _: {} - else if isString overrides then string-attrs - else if isPath overrides then { version = baseNameOf overrides; src = overrides; } - else if isAttrs overrides then pkgUp old overrides - else let overridesStr = toString overrides; in - abort "${overridesStr} not a legitimate overrides"; - in - attrs // (if attrs?version && ! (attrs?name) - then { name = "coq${coq.coq-version}-${pkgname}-${attrs.version}"; } else {}); - - # generates {ssreflect = «derivation ...» ; ... ; character = «derivation ...», ...} - mkMathcompGenSet = pkgs: o: - fold (pkg: pkgs: pkgs // {${pkg} = mkMathcompGen pkg o;}) {} pkgs; - # generates the derivation of one mathcomp package. - mkMathcompGen = package: overrides: - let - up = x: o: x // (toOverrideFun o x); - fixdeps = attrs: - let version = attrs.version or "master"; - mcdeps = if package == "single" then {} - else mkMathcompGenSet (filter isString attrs.passthru.mathcompDeps) overrides; - allmc = mkMathcompGenSet (mathcomp-config.packages version ++ [ "single" ]) overrides; - in { - propagatedBuildInputs = [ coq ] - ++ filter isDerivation attrs.passthru.mathcompDeps - ++ attrValues mcdeps - ; - passthru = allmc // - { overrideMathcomp = o: mathcomp_ (old: up (up old overrides) o); }; + maintainers = with maintainers; [ vbgl jwiegley cohencyril ]; }; - in - stdenv.mkDerivation (up (up (default-attrs package) overrides) fixdeps); + } // optionalAttrs (package != "single") + { passthru = genAttrs packages mathcomp_; } + // optionalAttrs withDoc { + htmldoc_template = + fetchzip { + url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip"; + sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8"; + }; + postBuild = '' + cp -rf _build_doc/* . + rm -r _build_doc + ''; + postInstall = + let tgt = "$out/share/coq/${coq.coq-version}/"; in + optionalString withDoc '' + mkdir -p ${tgt} + cp -r htmldoc ${tgt} + cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/ + ''; + buildTargets = "doc"; + extraInstallFlags = [ "-f Makefile.coq" ]; + }); + patched-derivation1 = derivation.overrideAttrs (o: + optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && + o.version != null && o.version != "dev" && versions.isLt "1.7" o.version) + { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; } + ); + patched-derivation = patched-derivation1.overrideAttrs (o: + optionalAttrs (versions.isLe "8.7" coq.coq-version || + (o.version != "dev" && versions.isLe "1.7" o.version)) + { + installFlags = o.installFlags ++ [ "-f Makefile.coq" ]; + } + ); + in patched-derivation; in -{ - mathcomp-config = mathcomp-config-initial; - mathcomp_ = mkMathcompGen "all"; - mathcomp = mathcomp_ mathcomp-config.preferred-version; - # mathcomp-single = mathcomp.single; - ssreflect = mathcomp.ssreflect; - mathcomp-ssreflect = mathcomp.ssreflect; - mathcomp-fingroup = mathcomp.fingroup; - mathcomp-algebra = mathcomp.algebra; - mathcomp-solvable = mathcomp.solvable; - mathcomp-field = mathcomp.field; - mathcomp-character = mathcomp.character; -} +mathcomp_ (if single then "single" else "all") diff --git a/pkgs/development/coq-modules/mathcomp/extra.nix b/pkgs/development/coq-modules/mathcomp/extra.nix deleted file mode 100644 index 6a2dfcda345..00000000000 --- a/pkgs/development/coq-modules/mathcomp/extra.nix +++ /dev/null @@ -1,391 +0,0 @@ -########################################################## -# Main derivation: # -# mathcomp-finmap mathcomp-analysis mathcomp-bigenough # -# mathcomp-multinomials mathcomp-real-closed coqeal # -# Additionally: # -# mathcomp-extra-all contains all the extra packages # -# mathcomp-extra-fast contains the one not marked slow # -######################################################################## -# This file mainly provides the above derivations, which are packages # -# extra mathcomp libraries based on mathcomp. # -######################################################################## - -##################################################### -# Compiling customs versions using `mathcomp-extra` # -############################################################################## -# The prefered way to compile a custom version of mathcomp extra packages # -# (other than released versions which should be added to # -# `rec-mathcomp-extra-config` and pushed to nixpkgs, see below), # -# is to use `coqPackages.mathcomp-extra name version` where # -# 1. `name` is a string representing the name of a declared package # -# OR undeclared package. # -# 2. `version` is either: # -# - a string without slash, which is interpreted as a github revision, # -# i.e. either a tag, a branch or a commit hash # -# - a string with slashes "owner/p_1/.../p_n", which is interpreted as # -# github owner "owner" and revision "p_1/.../p_n". # -# - a path which is interpreted as a local source for the repository, # -# the name of the version is taken to be the basename of the path # -# i.e. if the path is /home/you/git/package/branch/, # -# then "branch" is the name of the version # -# - an attribute set which overrides some attributes (e.g. the src) # -# if the version is updated, the name is automatically regenerated using # -# the conventional schema "coq${coq.coq-version}-${pkgname}-${version}" # -# - a "standard" override function (old: new_attrs) to override the default # -# attribute set, so that you can use old.${field} to patch the derivation. # -# # -# Should you choose to use `pkg.overrideAttrs` instead, we provide the # -# function mathcomp-extra-override which takes a name and a version exactly # -# as above and returns an override function. # -############################################################################## - -######################################################################### -# Example of use: https://github.com/math-comp/math-comp/wiki/Using-nix # -######################################################################### - -########################################### -# Adding a new package or package version # -################################################################################ -# 1. Update or add a `package` entry to `initial`, it must be a function # -# taking the version as argument and returning an attribute set. Everything # -# is optional and the default for the sources of the repository and the # -# homepage will be https://github.com/math-comp/${package}. # -# # -# 2. Update or add a `package` entry to `sha256` for each release. # -# You may use # -# ```sh # -# nix-prefetch-url --unpack # -# https://github.com/math-comp/math-comp/archive/version.tar.gz # -# ``` # -# # -# 3. Update or create a new consistent set of extra packages. # -# /!\ They must all be co-compatible. /!\ # -# Do not use versions that may disappear: it must either be # -# - a tag from the main repository (e.g. version or tag), or # -# - a revision hash that has been *merged in master* # -################################################################################ - -{ stdenv, fetchFromGitHub, recurseIntoAttrs, - which, mathcomp, coqPackages, - mathcomp-extra-config, mathcomp-extra-override, - mathcomp-extra, current-mathcomp-extra, -}: -with builtins // stdenv.lib; -let - ############################## - # CONFIGURATION, please edit # - ############################## - ############################ - # Packages base delaration # - ############################ - rec-mathcomp-extra-config = { - initial = { - mathcomp-finmap = {version, coqPackages}: { - meta = { - description = "A finset and finmap library"; - repo = "finmap"; - homepage = "https://github.com/math-comp/finmap"; - }; - passthru.compatibleCoqVersions = flip elem [ "8.8" "8.9" "8.10" "8.11" ]; - }; - - mathcomp-bigenough = {version, coqPackages}: { - meta = { - description = "A small library to do epsilon - N reasonning"; - repo = "bigenough"; - homepage = "https://github.com/math-comp/bigenough"; - }; - passthru.compatibleCoqVersions = flip elem [ "8.7" "8.8" "8.9" "8.10" "8.11" ]; - }; - - multinomials = {version, coqPackages}: { - buildInputs = [ which ]; - propagatedBuildInputs = with coqPackages; - [ mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; - meta = { - description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; - repo = "multinomials"; - homepage = "https://github.com/math-comp/multinomials"; - }; - passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ]; - }; - - mathcomp-analysis = {version, coqPackages}: { - propagatedBuildInputs = with coqPackages; - [ mathcomp.field mathcomp-finmap mathcomp-bigenough mathcomp-real-closed ]; - meta = { - description = "Analysis library compatible with Mathematical Components"; - homepage = "https://github.com/math-comp/analysis"; - repo = "analysis"; - license = stdenv.lib.licenses.cecill-c; - }; - passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ]; - }; - - mathcomp-real-closed = {version, coqPackages}: { - propagatedBuildInputs = with coqPackages; - [ mathcomp.field mathcomp-bigenough ]; - meta = { - description = "Mathematical Components Library on real closed fields"; - repo = "real-closed"; - homepage = "https://github.com/math-comp/real-closed"; - }; - passthru.compatibleCoqVersions = flip elem ["8.8" "8.9" "8.10" "8.11" ]; - }; - - coqeal = {version, coqPackages}: { - buildInputs = [ which ]; - propagatedBuildInputs = with coqPackages; - [ mathcomp-algebra bignums paramcoq multinomials ]; - meta = { - description = "CoqEAL - The Coq Effective Algebra Library"; - homepage = "https://github.com/coqeal/coqeal"; - license = stdenv.lib.licenses.mit; - owner = "CoqEAL"; - }; - passthru.compatibleCoqVersions = flip elem [ "8.9" "8.10" "8.11" ]; - }; - }; - - ############################### - # sha256 of released versions # - ############################### - sha256 = { - mathcomp-finmap = { - "1.5.0" = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq"; - "1.4.1" = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p"; - "1.4.0+coq-8.11" = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb"; - "1.4.0" = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd"; - "1.3.4" = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii"; - "1.3.3" = "1n844zjhv354kp4g4pfbajix0plqh7yxv6471sgyb46885298am5"; - "1.3.1" = "14rvm0rm5hd3pd0srgak3jqmddzfv6n7gdpjwhady5xcgrc7gsx7"; - "1.2.1" = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf"; - "1.2.0" = "0b6wrdr0d7rcnv86s37zm80540jl2wmiyf39ih7mw3dlwli2cyj4"; - "1.1.0" = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a"; - "1.0.0" = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa"; - }; - mathcomp-bigenough = { - "1.0.0" = "10g0gp3hk7wri7lijkrqna263346wwf6a3hbd4qr9gn8hmsx70wg"; - }; - mathcomp-analysis = { - "0.3.1" = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; - "0.3.0" = "03klwi4fja0cqb4myp3kgycfbmdv00bznmxf8yg3zzzzw997hjqc"; - "0.2.3" = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; - "0.2.2" = "1d5dwg9di2ppdzfg21zr0a691zigb5kz0lcw263jpyli1nrq7cvk"; - "0.2.0" = "1186xjxgns4ns1szyi931964bjm0mp126qzlv10mkqqgfw07nhrd"; - "0.1.0" = "0hwkr2wzy710pcyh274fcarzdx8sv8myp16pv0vq5978nmih46al"; - }; - multinomials = { - "1.5.2" = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; - "1.5.1" = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3"; - "1.5" = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw"; - "1.4" = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p"; - "1.3" = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; - "1.2" = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; - "1.1" = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; - "1.0" = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; - }; - mathcomp-real-closed = { - "1.1.1" = "0ksjscrgq1i79vys4zrmgvzy2y4ylxa8wdsf4kih63apw6v5ws6b"; - "1.1.0" = "0zgfmrlximw77bw5w6w0xg2nampp02pmrwnrzx8m1n5pqljnv8fh"; - "1.0.5" = "0q8nkxr9fba4naylr5xk7hfxsqzq2pvwlg1j0xxlhlgr3fmlavg2"; - "1.0.4" = "058v9dj973h9kfhqmvcy9a6xhhxzljr90cf99hdfcdx68fi2ha1b"; - "1.0.3" = "1xbzkzqgw5p42dx1liy6wy8lzdk39zwd6j14fwvv5735k660z7yb"; - "1.0.2" = "0097pafwlmzd0gyfs31bxpi1ih04i72nxhn99r93aj20mn7mcsgl"; - "1.0.1" = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg"; - }; - coqeal = { - "1.0.4" = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk"; - "1.0.3" = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24"; - "1.0.2" = "1brmf3gj03iky1bcl3g9vx8vknny7xfvs0y2rfr85am0296sxsfj"; - "1.0.1" = "19jhdrv2yp9ww0h8q73ihb2w1z3glz4waf2d2n45klafxckxi7bm"; - "1.0.0" = "1had6f1n85lmh9x31avbmgl3m0rsiw9f8ma95qzk5b57fjg5k1ii"; - }; - }; - - ################################ - # CONSISTENT sets of packages. # - ################################ - for-coq-and-mc = let - v6 = { - mathcomp-finmap = "1.5.0"; - mathcomp-bigenough = "1.0.0"; - mathcomp-analysis = "0.3.1"; - multinomials = "1.5.2"; - mathcomp-real-closed = "1.1.1"; - coqeal = "1.0.4"; - }; - v5 = { - mathcomp-finmap = "1.5.0"; - mathcomp-bigenough = "1.0.0"; - mathcomp-analysis = "0.3.0"; - multinomials = "1.5.1"; - mathcomp-real-closed = "1.0.5"; - coqeal = "1.0.4"; - }; - v4 = v3 // { coqeal = "1.0.3"; }; - v3 = { - mathcomp-finmap = "1.4.0"; - mathcomp-bigenough = "1.0.0"; - mathcomp-analysis = "0.2.3"; - multinomials = "1.5"; - mathcomp-real-closed = "1.0.4"; - coqeal = "1.0.0"; - }; - v2 = { - mathcomp-finmap = "1.3.4"; - mathcomp-bigenough = "1.0.0"; - mathcomp-analysis = "0.2.3"; - multinomials = "1.4"; - mathcomp-real-closed = "1.0.3"; - coqeal = "1.0.0"; - }; - v1 = { - mathcomp-finmap = "1.1.0"; - mathcomp-bigenough = "1.0.0"; - multinomials = "1.1"; - mathcomp-real-closed = "1.0.1"; - coqeal = "1.0.0"; - }; - in - { - "8.11" = { - "1.11.0" = v6; - "1.11+beta1" = v5; - "1.10.0" = v4 // {mathcomp-finmap = "1.4.0+coq-8.11";}; - }; - "8.10" = { - "1.11.0" = removeAttrs v6 ["coqeal"]; - "1.11+beta1" = removeAttrs v5 ["coqeal"]; - "1.10.0" = v4; - "1.9.0" = removeAttrs v3 ["coqeal"]; - }; - "8.9" = { - "1.11.0" = removeAttrs v6 ["mathcomp-analysis"]; - "1.11+beta1" = removeAttrs v5 ["mathcomp-analysis"]; - "1.10.0" = v4; - "1.9.0" = removeAttrs v3 ["coqeal"]; - "1.8.0" = removeAttrs v2 ["coqeal"]; - }; - "8.8" = { - "1.11.0" = removeAttrs v6 ["mathcomp-analysis"]; - "1.11+beta1" = removeAttrs v5 ["mathcomp-analysis"]; - "1.10.0" = removeAttrs v4 ["mathcomp-analysis"]; - "1.9.0" = removeAttrs v3 ["coqeal"]; - "1.8.0" = removeAttrs v2 ["coqeal"]; - "1.7.0" = removeAttrs v1 ["coqeal" "multinomials"]; - }; - "8.7" = { - "1.11.0" = removeAttrs v6 ["mathcomp-analysis"]; - "1.11+beta1" = removeAttrs v5 ["mathcomp-analysis"]; - "1.10.0" = removeAttrs v4 ["mathcomp-analysis"]; - "1.9.0" = removeAttrs v3 ["coqeal" "mathcomp-analysis"]; - "1.8.0" = removeAttrs v2 ["coqeal" "mathcomp-analysis"]; - "1.7.0" = removeAttrs v1 ["coqeal" "multinomials"]; - }; - }; - }; - - ############################## - # GENERATION, EDIT WITH CARE # - ############################## - coq = coqPackages.coq; - - default-attrs = { - version = "master"; - buildInputs = []; - propagatedBuildInputs = (with coqPackages; [ ssreflect ]); - installFlags = [ "-f" "Makefile.coq" "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - meta = { - inherit (mathcomp.meta) platforms license; - owner = "math-comp"; - maintainers = [ maintainers.vbgl maintainers.cohencyril ]; - }; - passthru.compatibleCoqVersions = (_: true); - }; - - pkgUp = recursiveUpdateUntil (path: l: r: !(isAttrs l && isAttrs r) || path == ["src"]); - - # Fixes a partial attribute set using the configuration - # in the style of the above mathcomp-extra-config.initial, - # and generates a name according to the conventional naming scheme below - fix-attrs = pkgcfg: - let attrs = pkgUp default-attrs pkgcfg; in - pkgUp attrs (rec { - name = "coq${coq.coq-version}mathcomp${mathcomp.version}-${attrs.meta.repo or attrs.meta.package or "anonymous"}-${attrs.version}"; - src = attrs.src or (fetchTarball "${meta.homepage}/archive/${attrs.version}.tar.gz"); - meta = rec { - homepage = attrs.meta.homepage or attrs.src.meta.homepage or "https://github.com/${owner}/${repo}"; - owner = attrs.meta.owner or "math-comp"; - repo = attrs.meta.repo or attrs.meta.package or "math-comp-nix"; - }; - }); - - # Gets a version out of a string, path or attribute set. - getVersion = arg: - if isFunction arg then (arg {}).version - else if arg == "" then "master" - else if isDerivation arg then arg.drvAttrs.version or "master" - else if isAttrs arg then arg.version or "master" - else if isString arg then head (reverseList (split "/" arg)) - else if isPath arg then (baseNameOf arg) - else "master"; - - # Converts a string, path or attribute set into an override function - # It tries to fill the `old` argument of the override function using - # `mathcomp-extra-config.initial` first and finishes with `fix-attrs` - rec-mathcomp-extra-override = generic: old: let - version = getVersion generic; - package = old.meta.package or "math-comp-nix"; - cfg = pkgUp ((mathcomp-extra-config.initial.${package} or (_: {})) - { inherit version coqPackages; }) old - // { inherit version; }; - fix = attrs: fix-attrs (pkgUp cfg attrs); - in - if isFunction generic then fix (generic cfg) - else if generic == null || generic == "" then fix {} - else if isDerivation generic then generic.drvAttrs - else if isAttrs generic then fix generic - else if generic == "broken" then fix { meta.broken = true; passthru.compatibleCoqVersions = _: false; } - else let fixedcfg = fix cfg; in fixedcfg // ( - if isString generic then - if (mathcomp-extra-config.sha256.${package} or {})?${generic} then { - src = fetchFromGitHub { - inherit (fixedcfg.meta) owner repo; - rev = version; - sha256 = mathcomp-extra-config.sha256.${package}.${version}; - }; - } - else let splitted = filter isString (split "/" generic); in { - src = fetchTarball - ("https://github.com/" + - (if length splitted == 1 then "${fixedcfg.meta.owner}/${fixedcfg.meta.repo}/archive/${version}.tar.gz" - else "${head splitted}/${fixedcfg.meta.repo}/archive/${concatStringsSep "/" (tail splitted)}.tar.gz")); - } - else if isPath generic then { src = generic; } - else abort "${toString generic} not a legitimate generic version/override"); - - # applies mathcomp-extra-config.for-coq-and-mc to the current mathcomp version - for-this = mathcomp-extra-config.for-coq-and-mc.${coq.coq-version}.${mathcomp.version} or {}; - - # specializes mathcomp-extra to the current mathcomp version. - rec-current-mathcomp-extra = package: mathcomp-extra package (for-this.${package} or {}); -in - { - mathcomp-extra-override = rec-mathcomp-extra-override; - mathcomp-extra-config = rec-mathcomp-extra-config; - current-mathcomp-extra = rec-current-mathcomp-extra; - mathcomp-extra = package: version: - stdenv.mkDerivation (mathcomp-extra-override version {meta = {inherit package;};}); - - mathcomp-finmap = current-mathcomp-extra "mathcomp-finmap"; - mathcomp-analysis = current-mathcomp-extra "mathcomp-analysis"; - mathcomp-bigenough = current-mathcomp-extra "mathcomp-bigenough"; - multinomials = current-mathcomp-extra "multinomials"; - mathcomp-real-closed = current-mathcomp-extra "mathcomp-real-closed"; - coqeal = current-mathcomp-extra "coqeal"; - - mathcomp-extra-fast = map current-mathcomp-extra - (attrNames (filterAttrs (pkg: config: !(config?slow && config.slow)) for-this)); - mathcomp-extra-all = map current-mathcomp-extra (attrNames for-this); - } diff --git a/pkgs/development/coq-modules/metalib/default.nix b/pkgs/development/coq-modules/metalib/default.nix index a0268a543a5..14f1bab574a 100644 --- a/pkgs/development/coq-modules/metalib/default.nix +++ b/pkgs/development/coq-modules/metalib/default.nix @@ -1,56 +1,18 @@ -{ stdenv, fetchgit, coq, haskellPackages, which, ott -}: +{ lib, mkCoqDerivation, coq, version ? null }: -stdenv.mkDerivation rec { - name = "metalib-${coq.coq-version}-${version}"; - version = "20170713"; +with lib; mkCoqDerivation { + pname = "metalib"; + owner = "plclub"; + inherit version; + defaultVersion = if versions.range "8.10" "8.13" coq.coq-version then "20200527" else null; + release."20200527".rev = "597fd7d0c93eb159274e84a39d554f10f1efccf8"; + release."20200527".sha256 = "0wbypc05d2lqfm9qaw98ynr5yc1p0ipsvyc3bh1rk9nz7zwirmjs"; - src = fetchgit { - url = "https://github.com/plclub/metalib.git"; - rev = "44e40aa082452dd333fc1ca2d2cc55311519bd52"; - sha256 = "1pra0nvx69q8d4bvpcvh9ngic1cy6z1chi03x56nisfqnc61b6y9"; - }; - - # The 'lngen' command-line utility is built from Haskell sources - lngen = with haskellPackages; mkDerivation { - pname = "lngen"; - version = "0.0.1"; - src = fetchgit { - url = "https://github.com/plclub/lngen"; - rev = "ea73ad315de33afd25f87ca738c71f358f1cd51c"; - sha256 = "1a0sj8n3lmsl1wlnqfy176k9lb9s8rl422bvg3ihl2i70ql8wisd"; - }; - isLibrary = true; - isExecutable = true; - libraryHaskellDepends = [ base containers mtl parsec syb ]; - executableHaskellDepends = [ base ]; - homepage = "https://github.com/plclub/lngen"; - description = "Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott"; - license = stdenv.lib.licenses.mit; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 which coq lngen ott findlib ]; - propagatedBuildInputs = [ coq ]; - - enableParallelBuilding = true; + sourceRoot = "source/Metalib"; + installFlags = "COQMF_COQLIB=$(out)/lib/coq/${coq.coq-version}"; - buildPhase = '' - (cd Metalib; make) - ''; - - installPhase = '' - (cd Metalib; make -f CoqSrc.mk DSTROOT=/ COQLIB=$out/lib/coq/${coq.coq-version}/ install) - ''; - - meta = with stdenv.lib; { - homepage = "https://github.com/plclub/metalib"; + meta = { license = licenses.mit; maintainers = [ maintainers.jwiegley ]; - platforms = coq.meta.platforms; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" "8.8" ]; - }; - } diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix new file mode 100644 index 00000000000..dfa6a63571f --- /dev/null +++ b/pkgs/development/coq-modules/multinomials/default.nix @@ -0,0 +1,41 @@ +{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, + lib, version ? null, useDune2 ? false }@args: +with lib; mkCoqDerivation { + + namePrefix = [ "coq" "mathcomp" ]; + pname = "multinomials"; + owner = "math-comp"; + 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.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"; } + { cases = [ (range "8.7" "8.10") (range "1.8" "1.10") ]; out = "1.4"; } + { cases = [ "8.6" (range "1.6" "1.7") ]; out = "1.1"; } + ] null; + release = { + "1.5.4".sha256 = "0s4sbh4y88l125hdxahr56325hdhxxdmqmrz7vv8524llyv3fciq"; + "1.5.3".sha256 = "1462x40y2qydjd2wcg8r6qr8cx3xv4ixzh2h8vp9h7arylkja1qd"; + "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s"; + "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3"; + "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw"; + "1.5.0".rev = "1.5"; + "1.4".sha256 = "0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p"; + "1.3".sha256 = "0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4"; + "1.2".sha256 = "1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq"; + "1.1".sha256 = "1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s"; + "1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; + }; + + useDune2ifVersion = versions.isGe "1.5.3"; + + propagatedBuildInputs = + [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ]; + + meta = { + description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; + license = licenses.cecill-c; + }; +} +// optionalAttrs (args?useDune2) { inherit useDune2; } diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix new file mode 100644 index 00000000000..adc4e3a5947 --- /dev/null +++ b/pkgs/development/coq-modules/odd-order/default.nix @@ -0,0 +1,24 @@ +{ lib, mkCoqDerivation, mathcomp, version ? null }: +with lib; + +mkCoqDerivation { + pname = "odd-order"; + owner = "math-comp"; + + 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 = pred.union (isGe "1.10.0") (isEq "dev"); out = "1.12.0"; } + ] null; + + propagatedBuildInputs = [ mathcomp.character ]; + + meta = { + description = "Formal proof of the Odd Order Theorem"; + maintainers = with maintainers; [ siraben ]; + license = licenses.cecill-b; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/paco/default.nix b/pkgs/development/coq-modules/paco/default.nix index 9d8a7a315a5..900e52f1682 100644 --- a/pkgs/development/coq-modules/paco/default.nix +++ b/pkgs/development/coq-modules/paco/default.nix @@ -1,42 +1,16 @@ -{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; - "8.10" = versions.post_8_6; - "8.11" = versions.post_8_6; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation rec { - inherit (param) version; - name = "coq${coq.coq-version}-paco-${version}"; - - src = fetchFromGitHub { - inherit (param) rev sha256; - owner = "snu-sf"; - repo = "paco"; - }; - - buildInputs = with coq.ocamlPackages; [ ocaml camlp5 unzip ]; - propagatedBuildInputs = [ coq ]; +{ lib, mkCoqDerivation, coq, version ? null }: + +with lib; mkCoqDerivation { + pname = "paco"; + 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"; } + ] null; + release."4.0.2".sha256 = "1q96bsxclqx84xn5vkid501jkwlc1p6fhb8szrlrp82zglj58b0b"; + release."1.2.8".sha256 = "05fskx5x1qgaf9qv626m38y5izichzzqc7g2rglzrkygbskrrwsb"; + releaseRev = v: "v${v}"; preBuild = "cd src"; @@ -46,15 +20,9 @@ stdenv.mkDerivation rec { cp -pR *.vo $COQLIB/user-contrib/Paco ''; - meta = with stdenv.lib; { + meta = { homepage = "http://plv.mpi-sws.org/paco/"; description = "A Coq library implementing parameterized coinduction"; maintainers = with maintainers; [ jwiegley ptival ]; - platforms = coq.meta.platforms; }; - - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.hasAttr params; - }; - } diff --git a/pkgs/development/coq-modules/paramcoq/default.nix b/pkgs/development/coq-modules/paramcoq/default.nix index 67e420b4e89..8f2ef30d37c 100644 --- a/pkgs/development/coq-modules/paramcoq/default.nix +++ b/pkgs/development/coq-modules/paramcoq/default.nix @@ -1,55 +1,23 @@ -{ stdenv, fetchFromGitHub, coq }: - -let params = - { - "8.7" = { - sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj"; - buildInputs = [ coq.ocamlPackages.camlp5 ]; - }; - "8.8" = { - sha256 = "0rc4lshqvnfdsph98gnscvpmlirs9wx91qcvffggg73xw0p1g9s0"; - buildInputs = [ coq.ocamlPackages.camlp5 ]; - }; - "8.9" = { - sha256 = "1jjzgpff09xjn9kgp7w69r096jkj0x2ksng3pawrmhmn7clwivbk"; - buildInputs = [ coq.ocamlPackages.camlp5 ]; - }; - "8.10" = { - sha256 = "1lq1mw15w4yky79qg3rm0mpzqi2ir51b6ak04ismrdr7ixky49y8"; - }; - "8.11" = { - sha256 = "09c6813988nvq4fpa45s33k70plnhxsblhm7cxxkg0i37mhvigsa"; - }; - }; - param = params.${coq.coq-version}; -in - -stdenv.mkDerivation rec { - version = "1.1.2"; - name = "coq${coq.coq-version}-paramcoq-${version}"; - src = fetchFromGitHub { - owner = "coq-community"; - repo = "paramcoq"; - rev = "v${version}+coq${coq.coq-version}"; - inherit (param) sha256; - }; - - buildInputs = [ coq ] - ++ (with coq.ocamlPackages; [ ocaml findlib ]) - ++ (param.buildInputs or []) - ; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - - passthru = { - compatibleCoqVersions = v: builtins.hasAttr v params; - }; +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; mkCoqDerivation { + pname = "paramcoq"; + inherit version; + defaultVersion = if versions.range "8.7" "8.13" coq.coq-version + then "1.1.2+coq${coq.coq-version}" else null; + displayVersion = { paramcoq = "1.1.2"; }; + release."1.1.2+coq8.13".sha256 = "02vnf8p04ynf3qk8myvjzsbga15395235mpdpj54pvxis3h5qq22"; + release."1.1.2+coq8.12".sha256 = "0qd72r45if4h7c256qdfiimv75zyrs0w0xqij3m866jxaq591v4i"; + release."1.1.2+coq8.11".sha256 = "09c6813988nvq4fpa45s33k70plnhxsblhm7cxxkg0i37mhvigsa"; + release."1.1.2+coq8.10".sha256 = "1lq1mw15w4yky79qg3rm0mpzqi2ir51b6ak04ismrdr7ixky49y8"; + release."1.1.2+coq8.9".sha256 = "1jjzgpff09xjn9kgp7w69r096jkj0x2ksng3pawrmhmn7clwivbk"; + release."1.1.2+coq8.8".sha256 = "0rc4lshqvnfdsph98gnscvpmlirs9wx91qcvffggg73xw0p1g9s0"; + release."1.1.2+coq8.7".sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj"; + releaseRev = v: "v${v}"; + mlPlugin = true; meta = { description = "Coq plugin for parametricity"; - inherit (src.meta) homepage; - license = stdenv.lib.licenses.mit; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - inherit (coq.meta) platforms; + license = licenses.mit; + maintainers = [ maintainers.vbgl ]; }; } diff --git a/pkgs/development/coq-modules/pocklington/default.nix b/pkgs/development/coq-modules/pocklington/default.nix new file mode 100644 index 00000000000..111bffeca2c --- /dev/null +++ b/pkgs/development/coq-modules/pocklington/default.nix @@ -0,0 +1,22 @@ +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; + +mkCoqDerivation { + pname = "pocklington"; + owner = "coq-community"; + + release."8.12.0".rev = "v8.12.0"; + release."8.12.0".sha256 = "sha256-0xBrw9+4g14niYdNqp0nx00fPJoSSnaDSDEaIVpPfjs="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.7"; out = "8.12.0"; } + ] null; + + meta = { + description = "Pocklington's criterion for primality in Coq"; + maintainers = with maintainers; [ siraben ]; + license = licenses.mit; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix new file mode 100644 index 00000000000..bc18108264a --- /dev/null +++ b/pkgs/development/coq-modules/reglang/default.nix @@ -0,0 +1,25 @@ +{ lib, mkCoqDerivation, coq, ssreflect, version ? null }: +with lib; + +mkCoqDerivation { + pname = "reglang"; + + releaseRev = v: "v${v}"; + + release."1.1.2".sha256 = "sha256-SEnMilLNxh6a3oiDNGLaBr8quQ/nO2T9Fwdf/1il2Yk="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.10" "8.13"; out = "1.1.2"; } + ] null; + + + propagatedBuildInputs = [ ssreflect ]; + + meta = { + description = "Regular Language Representations in Coq"; + maintainers = with maintainers; [ siraben ]; + license = licenses.cecill-b; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/relation-algebra/default.nix b/pkgs/development/coq-modules/relation-algebra/default.nix new file mode 100644 index 00000000000..da74215d537 --- /dev/null +++ b/pkgs/development/coq-modules/relation-algebra/default.nix @@ -0,0 +1,35 @@ +{ lib, mkCoqDerivation, coq, aac-tactics, mathcomp, version ? null }: +with lib; + +mkCoqDerivation { + pname = "relation-algebra"; + owner = "damien-pous"; + + releaseRev = v: "v${v}"; + + release."1.7.5".sha256 = "sha256-XdO8agoJmNXPv8Ho+KTlLCB4oRlQsb0w06aM9M16ZBU="; + release."1.7.4".sha256 = "sha256-o+v2CIAa2+9tJ/V8DneDTf4k31KMHycgMBLaQ+A4ufM="; + release."1.7.3".sha256 = "sha256-4feSNfi7h4Yhwn5L+9KP9K1S7HCPvsvaVWwoQSTFvos="; + release."1.7.2".sha256 = "sha256-f4oNjXspNMEz3AvhIeYO3avbUa1AThoC9DbcHMb5A2o="; + release."1.7.1".sha256 = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA="; + + 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"; } + ] null; + + mlPlugin = true; + + propagatedBuildInputs = [ aac-tactics mathcomp.ssreflect ]; + + meta = { + description = "Relation algebra library for Coq"; + maintainers = with maintainers; [ siraben ]; + license = licenses.gpl3Plus; + platforms = platforms.unix; + }; +} diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix new file mode 100644 index 00000000000..1fb01312e66 --- /dev/null +++ b/pkgs/development/coq-modules/semantics/default.nix @@ -0,0 +1,46 @@ +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; + +mkCoqDerivation rec { + pname = "semantics"; + owner = "coq-community"; + releaseRev = v: "v${v}"; + + release."8.13.0".sha256 = "sha256-8bDr/Ovl6s8BFaRcHeS5H33/K/pYdeKfSN+krVuKulQ="; + release."8.11.1".sha256 = "sha256-jTPgcXSNn1G2mMDC7ocFcmqs8svB7Yo1emXP15iuxiU="; + release."8.9.0".sha256 = "sha256-UBsvzlDEZsZsVkbUI0GbFEhpxnnLCiaqlqDyWVC5I6s="; + release."8.8.0".sha256 = "sha256-k2nQyNw9KT3wY7bGy8KGILF44sLxkBYqdFpzFE9fgyw="; + release."8.7.0".sha256 = "sha256-k2nQyNw9KT3wY7bGy8KGILF44sLxkBYqdFpzFE9fgyw="; + release."8.6.0".sha256 = "sha256-GltkGQ3tJqUPAbdDkqqvKLLhMOap50XvGaCkjshiNdY="; + + 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 = "8.9"; out = "8.9.0"; } + { case = "8.8"; out = "8.8.0"; } + { case = "8.7"; out = "8.7.0"; } + { case = "8.6"; out = "8.6.0"; } + ] null; + + mlPlugin = true; + extraBuildInputs = (with coq.ocamlPackages; [ num ocamlbuild ]); + + postPatch = '' + for p in Make Makefile.coq.local + do + substituteInPlace $p --replace "-libs nums" "-use-ocamlfind -package num" || true + done + ''; + + meta = { + description = "A survey of programming language semantics styles in Coq"; + longDescription = '' + A survey of semantics styles in Coq, from natural semantics through + structural operational, axiomatic, and denotational semantics, to + abstract interpretation + ''; + maintainers = with maintainers; [ siraben ]; + license = licenses.mit; + }; +} diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix index 82fa215ee9c..3631bdd54bf 100644 --- a/pkgs/development/coq-modules/simple-io/default.nix +++ b/pkgs/development/coq-modules/simple-io/default.nix @@ -1,34 +1,21 @@ -{ stdenv, fetchFromGitHub, coq, coq-ext-lib }: - -stdenv.mkDerivation rec { - version = "1.3.0"; - name = "coq${coq.coq-version}-simple-io-${version}"; - src = fetchFromGitHub { - owner = "Lysxia"; - repo = "coq-simple-io"; - rev = version; - sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax"; - }; - - buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml ocamlbuild ]); - +{ lib, mkCoqDerivation, coq, coq-ext-lib, version ? null }: + +with lib; mkCoqDerivation { + pname = "simple-io"; + owner = "Lysxia"; + repo = "coq-simple-io"; + inherit version; + defaultVersion = if versions.range "8.7" "8.13" coq.coq-version then "1.3.0" else null; + release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax"; + extraBuildInputs = (with coq.ocamlPackages; [ ocaml ocamlbuild ]); propagatedBuildInputs = [ coq-ext-lib ]; doCheck = true; checkTarget = "test"; - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; - meta = { description = "Purely functional IO for Coq"; - inherit (src.meta) homepage; - inherit (coq.meta) platforms; - license = stdenv.lib.licenses.mit; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; + license = licenses.mit; + maintainers = [ maintainers.vbgl ]; }; - } diff --git a/pkgs/development/coq-modules/stdpp/default.nix b/pkgs/development/coq-modules/stdpp/default.nix index 28917e73f29..604a3f48f87 100644 --- a/pkgs/development/coq-modules/stdpp/default.nix +++ b/pkgs/development/coq-modules/stdpp/default.nix @@ -1,32 +1,21 @@ -{ stdenv, fetchFromGitLab, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -stdenv.mkDerivation rec { - name = "coq${coq.coq-version}-stdpp-${version}"; - version = "1.4.0"; - src = fetchFromGitLab { - domain = "gitlab.mpi-sws.org"; - owner = "iris"; - repo = "stdpp"; - rev = "coq-stdpp-${version}"; - sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"; - }; - - buildInputs = [ coq ]; - - enableParallelBuilding = true; - - installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; +with lib; mkCoqDerivation rec { + pname = "stdpp"; + inherit version; + 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"; } + ] null; + release."1.5.0".sha256 = "1ym0fy620imah89p8b6rii8clx2vmnwcrbwxl3630h24k42092nf"; + release."1.4.0".sha256 = "1m6c7ibwc99jd4cv14v3r327spnfvdf3x2mnq51f9rz99rffk68r"; + releaseRev = v: "coq-stdpp-${v}"; meta = { - inherit (src.meta) homepage; description = "An extended “Standard Library” for Coq"; - inherit (coq.meta) platforms; - license = stdenv.lib.licenses.bsd3; - maintainers = [ stdenv.lib.maintainers.vbgl ]; + license = licenses.bsd3; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.8" "8.9" "8.10" "8.11" "8.12" ]; - }; - } diff --git a/pkgs/development/coq-modules/tlc/default.nix b/pkgs/development/coq-modules/tlc/default.nix index 816b2205024..1e212b44e72 100644 --- a/pkgs/development/coq-modules/tlc/default.nix +++ b/pkgs/development/coq-modules/tlc/default.nix @@ -1,41 +1,29 @@ -{ stdenv, fetchurl, fetchFromGitHub, coq }: +{ lib, mkCoqDerivation, coq, version ? null }: -let params = - if stdenv.lib.versionAtLeast coq.coq-version "8.10" - then rec { - version = "20200328"; - src = fetchFromGitHub { - owner = "charguer"; - repo = "tlc"; - rev = version; - sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx"; - }; - } else rec { - version = "20181116"; - src = fetchurl { - url = "http://tlc.gforge.inria.fr/releases/tlc-${version}.tar.gz"; - sha256 = "0iv6f6zmrv2lhq3xq57ipmw856ahsql754776ymv5wjm88ld63nm"; - }; - } -; in - -stdenv.mkDerivation { - inherit (params) version src; - pname = "coq${coq.coq-version}-tlc"; - - buildInputs = [ coq ]; - - installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ]; +with lib; (mkCoqDerivation { + pname = "tlc"; + owner = "charguer"; + inherit version; + displayVersion = { tlc = false; }; + defaultVersion = with versions; switch coq.coq-version [ + { case = range "8.12" "8.13"; out = "20210316"; } + { case = range "8.10" "8.12"; out = "20200328"; } + { case = range "8.6" "8.12"; out = "20181116"; } + ] null; + release."20210316".sha256 = "1hlavnx20lxpf2iydbbxqmim9p8wdwv4phzp9ypij93yivih0g4a"; + release."20200328".sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx"; + release."20181116".sha256 = "032lrbkxqm9d3fhf6nv1kq2z0mqd3czv3ijlbsjwnfh12xck4vpl"; meta = { homepage = "http://www.chargueraud.org/softs/tlc/"; description = "A non-constructive library for Coq"; - license = stdenv.lib.licenses.free; - maintainers = [ stdenv.lib.maintainers.vbgl ]; - inherit (coq.meta) platforms; + license = licenses.free; + maintainers = [ maintainers.vbgl ]; }; - - passthru = { - compatibleCoqVersions = stdenv.lib.flip builtins.elem [ "8.6" "8.7" "8.8" "8.9" "8.10" "8.11" "8.12" ]; - }; -} +}).overrideAttrs (x: + if versionAtLeast x.version "20210316" + then {} + else { + installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ]; + } +) diff --git a/pkgs/development/coq-modules/topology/default.nix b/pkgs/development/coq-modules/topology/default.nix new file mode 100644 index 00000000000..b4367f0a8fc --- /dev/null +++ b/pkgs/development/coq-modules/topology/default.nix @@ -0,0 +1,38 @@ +{ lib, mkCoqDerivation, coq, mathcomp, zorns-lemma, version ? null }: +with lib; + +mkCoqDerivation rec { + pname = "topology"; + + releaseRev = v: "v${v}"; + + release."8.12.0".sha256 = "sha256-ypHmHwzwZ6MQPYwuS3QyZmVOEPUCSbO2lhVaA6TypgQ="; + release."8.10.0".sha256 = "sha256-mCLF3JYIiO3AEW9yvlcLeF7zN4SjW3LG+Y5vYB0l55A="; + release."8.9.0".sha256 = "sha256-ZJh1BM34iZOQ75zqLIA+KtBjO2y33y0UpAw/ydCWQYc="; + release."8.8.0".sha256 = "sha256-Yfm3UymEP1e+BKMNPhdRFLdFhynMirtQ8E0HXnRiqHU="; + release."8.7.0".sha256 = "sha256-qcZQKvMRs5wWIAny8ciF9TrmEQfKKO9fWhwIRL+s7VA="; + release."8.6.0".sha256 = "sha256-eu/dBEFo3y6vnXlJljUD4hds6+qgAPQVvsuspyGHcj8="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.12"; out = "8.12.0"; } + { case = "8.11"; out = "8.12.0"; } + { case = "8.10"; out = "8.10.0"; } + { case = "8.9"; out = "8.9.0"; } + { case = "8.8"; out = "8.8.0"; } + { case = "8.7"; out = "8.7.0"; } + { case = "8.6"; out = "8.6.0"; } + ] null; + + propagatedBuildInputs = optional (versions.isLe "8.12" defaultVersion) zorns-lemma; + + meta = { + description = "General topology in Coq"; + longDescription = '' + This library develops some of the basic concepts and results of + general topology in Coq. + ''; + maintainers = with maintainers; [ siraben ]; + license = licenses.lgpl21Plus; + }; +} diff --git a/pkgs/development/coq-modules/zorns-lemma/default.nix b/pkgs/development/coq-modules/zorns-lemma/default.nix new file mode 100644 index 00000000000..84c3fd80519 --- /dev/null +++ b/pkgs/development/coq-modules/zorns-lemma/default.nix @@ -0,0 +1,38 @@ +{ lib, mkCoqDerivation, coq, version ? null }: +with lib; + +mkCoqDerivation { + pname = "zorns-lemma"; + + releaseRev = v: "v${v}"; + + release."8.11.0".sha256 = "sha256-2Hf7YwRcFmP/DqwFtF1p78MCNV50qUWfMVQtZbwKd0k="; + release."8.10.0".sha256 = "sha256-qLPLK2ZLJQ4SmJX2ADqFiP4kgHuQFJTeNXkBbjiFS+4="; + release."8.9.0".sha256 = "sha256-lEh978cXehglFX9D92RVltEuvN8umfPo/hvmFZm2NGo="; + release."8.8.0".sha256 = "sha256-ikXGzABu8VW7O0xNtCNvIq29c+mlDUm4k/ygVcsgDOI="; + release."8.7.0".sha256 = "sha256-jozvkkKLFBllN6K4oeYD0lNG+MdnOuKrDUPDocHUG6c="; + release."8.6.0".sha256 = "sha256-jozvkkKLFBllN6K4oeYD0lNG+MdnOuKrDUPDocHUG6c="; + release."8.5.0".sha256 = "sha256-mH/v02ObMjbVPYx2H+Jhz+Xp0XRKN67iMAdA1VNFzso="; + + inherit version; + defaultVersion = with versions; switch coq.coq-version [ + { case = isGe "8.11"; out = "8.11.0"; } + { case = "8.10"; out = "8.10.0"; } + { case = "8.9"; out = "8.9.0"; } + { case = "8.8"; out = "8.8.0"; } + { case = "8.7"; out = "8.7.0"; } + { case = "8.6"; out = "8.6.0"; } + { case = "8.5"; out = "8.5.0"; } + ] null; + + meta = { + description = "Development of basic set theory"; + longDescription = '' + This Coq library develops some basic set theory. The main + purpose the author had in writing it was as support for the + Topology library. + ''; + maintainers = with maintainers; [ siraben ]; + license = licenses.lgpl21Plus; + }; +} |