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

treewide: remove global with lib; statements in pkgs/coq-modules

Browse Source
This commit is contained in:
Shawn8901 2023-01-21 23:19:48 +01:00
parent 11da253ac9
commit 4dcb03a5c3
77 changed files with 209 additions and 242 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, StructTact, version ? null }: { lib, mkCoqDerivation, coq, StructTact, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "cheerios"; pname = "cheerios";
owner = "uwplse"; owner = "uwplse";
inherit version; inherit version;
defaultVersion = if versions.range "8.6" "8.16" coq.version then "20200201" else null; defaultVersion = if lib.versions.range "8.6" "8.16" coq.version then "20200201" else null;
release."20200201".rev = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d"; release."20200201".rev = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d";
release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1"; release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1";

6
pkgs/development/coq-modules/CoLoR/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, bignums, version ? null }: { lib, mkCoqDerivation, coq, bignums, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "color"; pname = "color";
owner = "fblanqui"; owner = "fblanqui";
inherit version; inherit version;
defaultVersion = with versions; switch coq.version [ defaultVersion = with lib.versions; lib.switch coq.version [
{case = range "8.12" "8.16"; out = "1.8.2"; } {case = range "8.12" "8.16"; out = "1.8.2"; }
{case = range "8.10" "8.11"; out = "1.7.0"; } {case = range "8.10" "8.11"; out = "1.7.0"; }
{case = range "8.8" "8.9"; out = "1.6.0"; } {case = range "8.8" "8.9"; out = "1.6.0"; }
@ -26,6 +26,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
homepage = "https://github.com/fblanqui/color"; homepage = "https://github.com/fblanqui/color";
description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant."; 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 ]; maintainers = with lib.maintainers; [ jpas jwiegley ];
}; };
} }

6
pkgs/development/coq-modules/HoTT/default.nix
View File

@ -1,11 +1,11 @@
{ lib, mkCoqDerivation, autoconf, automake, coq, version ? null }: { lib, mkCoqDerivation, autoconf, automake, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "HoTT"; pname = "HoTT";
repo = "Coq-HoTT"; repo = "Coq-HoTT";
owner = "HoTT"; owner = "HoTT";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.14" "8.16"; out = coq.coq-version; } { case = range "8.14" "8.16"; out = coq.coq-version; }
] null; ] null;
releaseRev = v: "V${v}"; releaseRev = v: "V${v}";
@ -20,6 +20,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
homepage = "http://homotopytypetheory.org/"; homepage = "http://homotopytypetheory.org/";
description = "Homotopy type theory"; description = "Homotopy type theory";
maintainers = with maintainers; [ siddharthist ]; maintainers = with lib.maintainers; [ siddharthist ];
}; };
} }

6
pkgs/development/coq-modules/ITree/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }: { lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "InteractionTrees"; pname = "InteractionTrees";
owner = "DeepSpec"; owner = "DeepSpec";
inherit version; inherit version;
defaultVersion = with versions; switch coq.version [ defaultVersion = with lib.versions; lib.switch coq.version [
{ case = range "8.10" "8.16"; out = "4.0.0"; } { case = range "8.10" "8.16"; out = "4.0.0"; }
] null; ] null;
release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm"; release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm";
@ -12,6 +12,6 @@ with lib; mkCoqDerivation rec {
propagatedBuildInputs = [ coq-ext-lib paco ]; propagatedBuildInputs = [ coq-ext-lib paco ];
meta = { meta = {
description = "A Library for Representing Recursive and Impure Programs in Coq"; description = "A Library for Representing Recursive and Impure Programs in Coq";
maintainers = with maintainers; [ larsr ]; maintainers = with lib.maintainers; [ larsr ];
}; };
} }

5
pkgs/development/coq-modules/LibHyps/default.nix
View File

@ -1,11 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "LibHyps"; pname = "LibHyps";
owner = "Matafou"; owner = "Matafou";
inherit version; inherit version;
defaultVersion = if (versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null; defaultVersion = if (lib.versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;
release = { release = {
"2.0.4.1".sha256 = "09p89701zhrfdmqlpxw3mziw8yylj1w1skb4b0xpbdwd1vsn4k3h"; "2.0.4.1".sha256 = "09p89701zhrfdmqlpxw3mziw8yylj1w1skb4b0xpbdwd1vsn4k3h";
}; };
@ -16,6 +15,6 @@ mkCoqDerivation {
meta = { meta = {
description = "Hypotheses manipulation library"; description = "Hypotheses manipulation library";
license = licenses.mit; license = lib.licenses.mit;
}; };
} }

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

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "StructTact"; pname = "StructTact";
owner = "uwplse"; owner = "uwplse";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.6" "8.16"; out = "20210328"; } { case = range "8.6" "8.16"; out = "20210328"; }
{ case = range "8.5" "8.13"; out = "20181102"; } { case = range "8.5" "8.13"; out = "20181102"; }
] null; ] null;

6
pkgs/development/coq-modules/VST/default.nix
View File

@ -1,7 +1,5 @@
{ lib, mkCoqDerivation, coq, compcert, ITree, version ? null }: { lib, mkCoqDerivation, coq, compcert, ITree, version ? null }:
with lib;
# A few modules that are not built and installed by default # A few modules that are not built and installed by default
# but that may be useful to some users. # but that may be useful to some users.
# They depend on ITree. # They depend on ITree.
@ -11,7 +9,7 @@ let extra_floyd_files = [
"powerlater.v" "powerlater.v"
] ]
# floyd/printf.v is broken in VST 2.9 # floyd/printf.v is broken in VST 2.9
++ optional (!versions.isGe "8.13" coq.coq-version) "printf.v" ++ lib.optional (!lib.versions.isGe "8.13" coq.coq-version) "printf.v"
++ [ ++ [
"quickprogram.v" "quickprogram.v"
]; ];
@ -24,7 +22,7 @@ mkCoqDerivation {
owner = "PrincetonUniversity"; owner = "PrincetonUniversity";
repo = "VST"; repo = "VST";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.15" "8.16"; out = "2.11.1"; } { case = range "8.15" "8.16"; out = "2.11.1"; }
{ case = range "8.14" "8.16"; out = "2.10"; } { case = range "8.14" "8.16"; out = "2.10"; }
{ case = range "8.13" "8.15"; out = "2.9"; } { case = range "8.13" "8.15"; out = "2.9"; }

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

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "Velisarios"; pname = "Velisarios";
owner = "vrahli"; owner = "vrahli";
inherit version; inherit version;
defaultVersion = if versions.range "8.6" "8.8" coq.coq-version then "20180221" else null; defaultVersion = if lib.versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
release."20180221".rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b"; release."20180221".rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2"; release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";

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

@ -1,11 +1,11 @@
{ lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }: { lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "verdi"; pname = "verdi";
owner = "uwplse"; owner = "uwplse";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.7" "8.16"; out = "20211026"; } { case = range "8.7" "8.16"; out = "20211026"; }
{ case = range "8.7" "8.14"; out = "20210524"; } { case = range "8.7" "8.14"; out = "20210524"; }
{ case = range "8.7" "8.13"; out = "20200131"; } { case = range "8.7" "8.13"; out = "20200131"; }

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

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "aac-tactics"; pname = "aac-tactics";
@ -21,7 +20,7 @@ mkCoqDerivation {
release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4="; release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = "8.16"; out = "8.16.0"; } { case = "8.16"; out = "8.16.0"; }
{ case = "8.15"; out = "8.15.1"; } { case = "8.15"; out = "8.15.1"; }
{ case = "8.14"; out = "8.14.1"; } { case = "8.14"; out = "8.14.1"; }
@ -37,7 +36,7 @@ mkCoqDerivation {
mlPlugin = true; mlPlugin = true;
meta = { meta = with lib; {
description = "Coq plugin providing tactics for rewriting universally quantified equations"; description = "Coq plugin providing tactics for rewriting universally quantified equations";
longDescription = '' longDescription = ''
This Coq plugin provides tactics for rewriting universally quantified This Coq plugin provides tactics for rewriting universally quantified

5
pkgs/development/coq-modules/addition-chains/default.nix
View File

@ -1,6 +1,5 @@
{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, mathcomp-fingroup, paramcoq { lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, mathcomp-fingroup, paramcoq
, version ? null }: , version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "addition-chains"; pname = "addition-chains";
@ -12,7 +11,7 @@ mkCoqDerivation {
releaseRev = (v: "v${v}"); releaseRev = (v: "v${v}");
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.13" "8.16"; out = "0.6"; } { case = range "8.13" "8.16"; out = "0.6"; }
{ case = range "8.11" "8.12"; out = "0.4"; } { case = range "8.11" "8.12"; out = "0.4"; }
] null; ] null;
@ -21,7 +20,7 @@ mkCoqDerivation {
useDune = true; useDune = true;
meta = { meta = with lib; {
description = "Exponentiation algorithms following addition chains"; description = "Exponentiation algorithms following addition chains";
longDescription = '' longDescription = ''
Addition chains are algorithms for computations of the p-th Addition chains are algorithms for computations of the p-th

5
pkgs/development/coq-modules/autosubst/default.nix
View File

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }: { lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "autosubst"; pname = "autosubst";
@ -8,13 +7,13 @@ mkCoqDerivation {
release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI="; release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.10" "8.16"; out = "1.7"; } { case = range "8.10" "8.16"; out = "1.7"; }
] null; ] null;
propagatedBuildInputs = [ mathcomp-ssreflect ]; propagatedBuildInputs = [ mathcomp-ssreflect ];
meta = { meta = with lib; {
homepage = "https://www.ps.uni-saarland.de/autosubst/"; homepage = "https://www.ps.uni-saarland.de/autosubst/";
description = "Automation for de Bruijn syntax and substitution in Coq"; description = "Automation for de Bruijn syntax and substitution in Coq";
maintainers = with maintainers; [ siraben jwiegley ]; maintainers = with maintainers; [ siraben jwiegley ];

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

@ -1,11 +1,11 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "bignums"; pname = "bignums";
owner = "coq"; owner = "coq";
displayVersion = { bignums = ""; }; displayVersion = { bignums = ""; };
inherit version; inherit version;
defaultVersion = if versions.isGe "8.6" coq.coq-version defaultVersion = if lib.versions.isGe "8.6" coq.coq-version
then "${coq.coq-version}.0" else null; then "${coq.coq-version}.0" else null;
release."8.17.0".sha256 = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw="; release."8.17.0".sha256 = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
@ -25,5 +25,5 @@ with lib; mkCoqDerivation {
mlPlugin = true; mlPlugin = true;
meta = { license = licenses.lgpl2; }; meta = { license = lib.licenses.lgpl2; };
} }

6
pkgs/development/coq-modules/category-theory/default.nix
View File

@ -1,6 +1,6 @@
{ lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }: { lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "category-theory"; pname = "category-theory";
owner = "jwiegley"; owner = "jwiegley";
@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs"; release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.14" "8.16"; out = "1.0.0"; } { case = range "8.14" "8.16"; out = "1.0.0"; }
{ case = range "8.10" "8.15"; out = "20211213"; } { case = range "8.10" "8.15"; out = "20211213"; }
{ case = range "8.8" "8.9"; out = "20190414"; } { case = range "8.8" "8.9"; out = "20190414"; }
@ -28,6 +28,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
description = "A formalization of category theory in Coq for personal study and practical work"; description = "A formalization of category theory in Coq for personal study and practical work";
maintainers = with maintainers; [ jwiegley ]; maintainers = with lib.maintainers; [ jwiegley ];
}; };
} }

5
pkgs/development/coq-modules/ceres/default.nix
View File

@ -1,6 +1,5 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "ceres"; pname = "ceres";
@ -8,10 +7,10 @@ mkCoqDerivation {
owner = "Lysxia"; owner = "Lysxia";
inherit version; inherit version;
defaultVersion = if versions.range "8.8" "8.16" coq.version then "0.4.0" else null; defaultVersion = if lib.versions.range "8.8" "8.16" coq.version then "0.4.0" else null;
release."0.4.0".sha256 = "sha256:0zwp3pn6fdj0qdig734zdczrls886al06mxqhhabms0jvvqijmbi"; release."0.4.0".sha256 = "sha256:0zwp3pn6fdj0qdig734zdczrls886al06mxqhhabms0jvvqijmbi";
meta = { meta = with lib; {
description = "Library for serialization to S-expressions"; description = "Library for serialization to S-expressions";
license = licenses.mit; license = licenses.mit;
maintainers = with maintainers; [ Zimmi48 ]; maintainers = with maintainers; [ Zimmi48 ];

6
pkgs/development/coq-modules/compcert/default.nix
View File

@ -5,8 +5,6 @@
, version ? null , version ? null
}: }:
with lib;
let compcert = mkCoqDerivation rec { let compcert = mkCoqDerivation rec {
pname = "compcert"; pname = "compcert";
@ -15,7 +13,7 @@ let compcert = mkCoqDerivation rec {
inherit version; inherit version;
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
defaultVersion = with versions; switch coq.version [ defaultVersion = with lib.versions; lib.switch coq.version [
{ case = range "8.14" "8.16"; out = "3.11"; } { case = range "8.14" "8.16"; out = "3.11"; }
{ case = isEq "8.13" ; out = "3.10"; } { case = isEq "8.13" ; out = "3.10"; }
{ case = isEq "8.12" ; out = "3.9"; } { case = isEq "8.12" ; out = "3.9"; }
@ -84,7 +82,7 @@ let compcert = mkCoqDerivation rec {
}; in }; in
compcert.overrideAttrs (o: compcert.overrideAttrs (o:
{ {
patches = with versions; switch [ coq.version o.version ] [ patches = with lib.versions; lib.switch [ coq.version o.version ] [
{ cases = [ (range "8.12.2" "8.13.2") "3.8" ]; { cases = [ (range "8.12.2" "8.13.2") "3.8" ];
out = [ out = [
# Support for Coq 8.12.2 # Support for Coq 8.12.2

6
pkgs/development/coq-modules/contribs/default.nix
View File

@ -1,16 +1,16 @@
{ lib, mkCoqDerivation, coq, callPackage }: { lib, mkCoqDerivation, coq, callPackage }:
with lib; let mkContrib = pname: coqs: param: let mkContrib = pname: coqs: param:
let contribVersion = {version ? null}: mkCoqDerivation ({ let contribVersion = {version ? null}: mkCoqDerivation ({
inherit pname version; inherit pname version;
owner = "coq-contribs"; owner = "coq-contribs";
mlPlugin = true; mlPlugin = true;
} // optionalAttrs (builtins.elem coq.coq-version coqs) ({ } // lib.optionalAttrs (builtins.elem coq.coq-version coqs) ({
defaultVersion = param.version; defaultVersion = param.version;
release = { "${param.version}" = { inherit (param) rev sha256; }; }; release = { "${param.version}" = { inherit (param) rev sha256; }; };
} // (removeAttrs param [ "version" "rev" "sha256" ])) } // (removeAttrs param [ "version" "rev" "sha256" ]))
); in ); in
makeOverridable contribVersion {} ; in lib.makeOverridable contribVersion {} ; in
{ {
aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] { aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] {
"8.7" = { "8.7" = {

6
pkgs/development/coq-modules/coq-bits/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }: { lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "coq-bits"; pname = "coq-bits";
repo = "bits"; repo = "bits";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.10" "8.16"; out = "1.1.0"; } { case = range "8.10" "8.16"; out = "1.1.0"; }
{ case = range "8.7" "8.15"; out = "1.0.0"; } { case = range "8.7" "8.15"; out = "1.0.0"; }
] null; ] null;
@ -14,7 +14,7 @@ with lib; mkCoqDerivation {
propagatedBuildInputs = [ mathcomp-algebra ]; propagatedBuildInputs = [ mathcomp-algebra ];
meta = { meta = with lib; {
description = "A formalization of bitset operations in Coq"; description = "A formalization of bitset operations in Coq";
license = licenses.asl20; license = licenses.asl20;
maintainers = with maintainers; [ ptival ]; maintainers = with maintainers; [ ptival ];

6
pkgs/development/coq-modules/coq-ext-lib/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "coq-ext-lib"; pname = "coq-ext-lib";
owner = "coq-ext-lib"; owner = "coq-ext-lib";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.11" "8.16"; out = "0.11.7"; } { case = range "8.11" "8.16"; out = "0.11.7"; }
{ case = range "8.8" "8.16"; out = "0.11.6"; } { case = range "8.8" "8.16"; out = "0.11.6"; }
{ case = range "8.8" "8.14"; out = "0.11.4"; } { case = range "8.8" "8.14"; out = "0.11.4"; }
@ -30,6 +30,6 @@ with lib; mkCoqDerivation rec {
meta = { meta = {
description = "A collection of theories and plugins that may be useful in other Coq developments"; description = "A collection of theories and plugins that may be useful in other Coq developments";
maintainers = with maintainers; [ jwiegley ptival ]; maintainers = with lib.maintainers; [ jwiegley ptival ];
}; };
} }

6
pkgs/development/coq-modules/coq-haskell/default.nix
View File

@ -1,11 +1,11 @@
{ lib, mkCoqDerivation, coq, ssreflect, version ? null }: { lib, mkCoqDerivation, coq, ssreflect, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "coq-haskell"; pname = "coq-haskell";
owner = "jwiegley"; owner = "jwiegley";
inherit version; inherit version;
defaultVersion = if versions.range "8.5" "8.8" coq.coq-version then "20171215" else null; defaultVersion = if lib.versions.range "8.5" "8.8" coq.coq-version then "20171215" else null;
release."20171215".rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968"; release."20171215".rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
release."20171215".sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv"; release."20171215".sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
@ -16,6 +16,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
description = "A library for formalizing Haskell types and functions in Coq"; description = "A library for formalizing Haskell types and functions in Coq";
maintainers = with maintainers; [ jwiegley ]; maintainers = with lib.maintainers; [ jwiegley ];
}; };
} }

6
pkgs/development/coq-modules/coq-record-update/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "coq-record-update"; pname = "coq-record-update";
owner = "tchajed"; owner = "tchajed";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.10" "8.16"; out = "0.3.1"; } { case = range "8.10" "8.16"; out = "0.3.1"; }
] null; ] null;
release."0.3.1".sha256 = "sha256-DyGxO2tqmYZZluXN6Oy5Tw6fuLMyuyxonj8CCToWKkk="; release."0.3.1".sha256 = "sha256-DyGxO2tqmYZZluXN6Oy5Tw6fuLMyuyxonj8CCToWKkk=";
@ -13,6 +13,6 @@ with lib; mkCoqDerivation rec {
buildFlags = [ "NO_TEST=1" ]; buildFlags = [ "NO_TEST=1" ];
meta = { meta = {
description = "Library to create Coq record update functions"; description = "Library to create Coq record update functions";
maintainers = with maintainers; [ ineol ]; maintainers = with lib.maintainers; [ ineol ];
}; };
} }

8
pkgs/development/coq-modules/coqeal/default.nix
View File

@ -2,14 +2,12 @@
mathcomp-real-closed, mathcomp-real-closed,
lib, version ? null }: lib, version ? null }:
with lib;
(mkCoqDerivation { (mkCoqDerivation {
pname = "CoqEAL"; pname = "CoqEAL";
inherit version; inherit version;
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (range "8.13" "8.16") (isGe "1.13.0") ]; out = "1.1.1"; } { cases = [ (range "8.13" "8.16") (isGe "1.13.0") ]; out = "1.1.1"; }
{ cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.1.0"; } { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.1.0"; }
{ cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; } { cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; }
@ -28,9 +26,9 @@ with lib;
meta = { meta = {
description = "CoqEAL - The Coq Effective Algebra Library"; description = "CoqEAL - The Coq Effective Algebra Library";
license = licenses.mit; license = lib.licenses.mit;
}; };
}).overrideAttrs (o: { }).overrideAttrs (o: {
propagatedBuildInputs = o.propagatedBuildInputs propagatedBuildInputs = o.propagatedBuildInputs
++ optional (versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed; ++ lib.optional (lib.versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
}) })

6
pkgs/development/coq-modules/coqhammer/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
inherit version; inherit version;
pname = "coqhammer"; pname = "coqhammer";
owner = "lukaszcz"; owner = "lukaszcz";
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = "8.15"; out = "1.3.2-coq8.15"; } { case = "8.15"; out = "1.3.2-coq8.15"; }
{ case = "8.14"; out = "1.3.2-coq8.14"; } { case = "8.14"; out = "1.3.2-coq8.14"; }
{ case = "8.13"; out = "1.3.2-coq8.13"; } { case = "8.13"; out = "1.3.2-coq8.13"; }
@ -57,7 +57,7 @@ with lib; mkCoqDerivation {
mlPlugin = true; mlPlugin = true;
meta = { meta = with lib; {
homepage = "http://cl-informatik.uibk.ac.at/cek/coqhammer/"; homepage = "http://cl-informatik.uibk.ac.at/cek/coqhammer/";
description = "Automation for Dependent Type Theory"; description = "Automation for Dependent Type Theory";
license = licenses.lgpl21; license = licenses.lgpl21;

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

@ -8,14 +8,14 @@
, coq , coq
, version ? null }: , version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "coqide"; pname = "coqide";
inherit version; inherit version;
inherit (coq) src; inherit (coq) src;
release."${coq.version}" = {}; release."${coq.version}" = {};
defaultVersion = if versions.isGe "8.14" coq.version then coq.version else null; defaultVersion = if lib.versions.isGe "8.14" coq.version then coq.version else null;
preConfigure = '' preConfigure = ''
patchShebangs dev/tools/ patchShebangs dev/tools/

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

@ -1,11 +1,11 @@
{ which, lib, mkCoqDerivation, coq, bignums, version ? null }: { which, lib, mkCoqDerivation, coq, bignums, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "coqprime"; pname = "coqprime";
owner = "thery"; owner = "thery";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.12" "8.16"; out = "8.15"; } { case = range "8.12" "8.16"; out = "8.15"; }
{ case = range "8.10" "8.11"; out = "8.10"; } { case = range "8.10" "8.11"; out = "8.10"; }
{ case = range "8.8" "8.9"; out = "8.8"; } { case = range "8.8" "8.9"; out = "8.8"; }

6
pkgs/development/coq-modules/coqtail-math/default.nix
View File

@ -1,12 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "coqtail-math"; pname = "coqtail-math";
owner = "coq-community"; owner = "coq-community";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.11" "8.15"; out = "8.14"; } { case = range "8.11" "8.15"; out = "8.14"; }
{ case = range "8.11" "8.13"; out = "20201124"; } { case = range "8.11" "8.13"; out = "20201124"; }
] null; ] null;
@ -15,7 +13,7 @@ mkCoqDerivation {
release."20201124".rev = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e"; release."20201124".rev = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e";
release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ="; release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ=";
mlPlugin = true; mlPlugin = true;
meta = { meta = with lib; {
license = licenses.lgpl3Only; license = licenses.lgpl3Only;
maintainers = [ maintainers.siraben ]; maintainers = [ maintainers.siraben ];
}; };

6
pkgs/development/coq-modules/coquelicot/default.nix
View File

@ -1,12 +1,12 @@
{ lib, mkCoqDerivation, autoconf, { lib, mkCoqDerivation, autoconf,
coq, ssreflect, version ? null }: coq, ssreflect, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "coquelicot"; pname = "coquelicot";
owner = "coquelicot"; owner = "coquelicot";
domain = "gitlab.inria.fr"; domain = "gitlab.inria.fr";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.8" "8.16"; out = "3.2.0"; } { case = range "8.8" "8.16"; out = "3.2.0"; }
{ case = range "8.8" "8.13"; out = "3.1.0"; } { case = range "8.8" "8.13"; out = "3.1.0"; }
{ case = range "8.5" "8.9"; out = "3.0.2"; } { case = range "8.5" "8.9"; out = "3.0.2"; }
@ -20,7 +20,7 @@ with lib; mkCoqDerivation {
propagatedBuildInputs = [ ssreflect ]; propagatedBuildInputs = [ ssreflect ];
useMelquiondRemake.logpath = "Coquelicot"; useMelquiondRemake.logpath = "Coquelicot";
meta = { meta = with lib; {
homepage = "http://coquelicot.saclay.inria.fr/"; homepage = "http://coquelicot.saclay.inria.fr/";
description = "A Coq library for Reals"; description = "A Coq library for Reals";
license = licenses.lgpl3; license = licenses.lgpl3;

6
pkgs/development/coq-modules/corn/default.nix
View File

@ -1,9 +1,9 @@
{ lib, mkCoqDerivation, coq, bignums, math-classes, version ? null }: { lib, mkCoqDerivation, coq, bignums, math-classes, version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "corn"; pname = "corn";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = "8.6"; out = "8.8.1"; } { case = "8.6"; out = "8.8.1"; }
{ case = (range "8.11" "8.16"); out = "8.16.0"; } { case = (range "8.11" "8.16"); out = "8.16.0"; }
{ case = (range "8.7" "8.15"); out = "8.13.0"; } { case = (range "8.7" "8.15"); out = "8.13.0"; }
@ -21,7 +21,7 @@ with lib; mkCoqDerivation rec {
propagatedBuildInputs = [ bignums math-classes ]; propagatedBuildInputs = [ bignums math-classes ];
meta = { meta = with lib; {
homepage = "http://c-corn.github.io/"; homepage = "http://c-corn.github.io/";
license = licenses.gpl2; license = licenses.gpl2;
description = "A Coq library for constructive analysis"; description = "A Coq library for constructive analysis";

5
pkgs/development/coq-modules/deriving/default.nix
View File

@ -1,14 +1,13 @@
{ lib, mkCoqDerivation, coq, version ? null { lib, mkCoqDerivation, coq, version ? null
, ssreflect , ssreflect
}: }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "deriving"; pname = "deriving";
owner = "arthuraa"; owner = "arthuraa";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.11" "8.16"; out = "0.1.0"; } { case = range "8.11" "8.16"; out = "0.1.0"; }
] null; ] null;
@ -20,7 +19,7 @@ mkCoqDerivation {
mlPlugin = true; mlPlugin = true;
meta = { meta = with lib; {
description = "Generic instances of MathComp classes"; description = "Generic instances of MathComp classes";
license = licenses.mit; license = licenses.mit;
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];

11
pkgs/development/coq-modules/dpdgraph/default.nix
View File

@ -1,14 +1,13 @@
{ lib, mkCoqDerivation, autoreconfHook, coq, version ? null }: { lib, mkCoqDerivation, autoreconfHook, coq, version ? null }:
with lib; let hasWarning = lib.versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
let hasWarning = versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
mkCoqDerivation { mkCoqDerivation {
pname = "dpdgraph"; pname = "dpdgraph";
owner = "Karmaki"; owner = "Karmaki";
repo = "coq-dpdgraph"; repo = "coq-dpdgraph";
inherit version; inherit version;
defaultVersion = switch coq.coq-version [ defaultVersion = lib.switch coq.coq-version [
{ case = "8.16"; out = "1.0+8.16"; } { case = "8.16"; out = "1.0+8.16"; }
{ case = "8.15"; out = "1.0+8.15"; } { case = "8.15"; out = "1.0+8.15"; }
{ case = "8.14"; out = "1.0+8.14"; } { case = "8.14"; out = "1.0+8.14"; }
@ -47,11 +46,11 @@ mkCoqDerivation {
# dpd_compute.ml uses deprecated Pervasives.compare # dpd_compute.ml uses deprecated Pervasives.compare
# Versions prior to 0.6.5 do not have the WARN_ERR build flag # Versions prior to 0.6.5 do not have the WARN_ERR build flag
preConfigure = optionalString hasWarning '' preConfigure = lib.optionalString hasWarning ''
substituteInPlace Makefile.in --replace "-warn-error +a " "" substituteInPlace Makefile.in --replace "-warn-error +a " ""
''; '';
buildFlags = optional hasWarning "WARN_ERR="; buildFlags = lib.optional hasWarning "WARN_ERR=";
preInstall = '' preInstall = ''
mkdir -p $out/bin mkdir -p $out/bin
@ -59,7 +58,7 @@ mkCoqDerivation {
extraInstallFlags = [ "BINDIR=$(out)/bin" ]; extraInstallFlags = [ "BINDIR=$(out)/bin" ];
meta = { meta = with lib; {
description = "Build dependency graphs between Coq objects"; description = "Build dependency graphs between Coq objects";
license = licenses.lgpl21; license = licenses.lgpl21;
maintainers = with maintainers; [ vbgl ]; maintainers = with maintainers; [ vbgl ];

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

@ -1,11 +1,11 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; (mkCoqDerivation { (mkCoqDerivation {
pname = "equations"; pname = "equations";
owner = "mattam82"; owner = "mattam82";
repo = "Coq-Equations"; repo = "Coq-Equations";
inherit version; inherit version;
defaultVersion = switch coq.coq-version [ defaultVersion = lib.switch coq.coq-version [
{ case = "8.16"; out = "1.3+8.16"; } { case = "8.16"; out = "1.3+8.16"; }
{ case = "8.15"; out = "1.3+8.15"; } { case = "8.15"; out = "1.3+8.15"; }
{ case = "8.14"; out = "1.3+8.14"; } { case = "8.14"; out = "1.3+8.14"; }
@ -57,11 +57,11 @@ with lib; (mkCoqDerivation {
mlPlugin = true; mlPlugin = true;
meta = { meta = with lib; {
homepage = "https://mattam82.github.io/Coq-Equations/"; homepage = "https://mattam82.github.io/Coq-Equations/";
description = "A plugin for Coq to add dependent pattern-matching"; description = "A plugin for Coq to add dependent pattern-matching";
maintainers = with maintainers; [ jwiegley ]; maintainers = with maintainers; [ jwiegley ];
}; };
}).overrideAttrs (o: { }).overrideAttrs (o: {
preBuild = "coq_makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}"; preBuild = "coq_makefile -f _CoqProject -o Makefile${lib.optionalString (lib.versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
}) })

7
pkgs/development/coq-modules/extructures/default.nix
View File

@ -2,14 +2,13 @@
, ssreflect , ssreflect
, deriving , deriving
}: }:
with lib;
(mkCoqDerivation { (mkCoqDerivation {
pname = "extructures"; pname = "extructures";
owner = "arthuraa"; owner = "arthuraa";
inherit version; inherit version;
defaultVersion = with versions; switch [coq.coq-version ssreflect.version] [ defaultVersion = with lib.versions; lib.switch [coq.coq-version ssreflect.version] [
{ cases = [(range "8.11" "8.16") (isGe "1.12.0") ]; out = "0.3.1"; } { cases = [(range "8.11" "8.16") (isGe "1.12.0") ]; out = "0.3.1"; }
{ cases = [(range "8.11" "8.14") (isLe "1.12.0") ]; out = "0.3.0"; } { cases = [(range "8.11" "8.14") (isLe "1.12.0") ]; out = "0.3.0"; }
{ cases = [(range "8.10" "8.12") (isLe "1.12.0") ]; out = "0.2.2"; } { cases = [(range "8.10" "8.12") (isLe "1.12.0") ]; out = "0.2.2"; }
@ -23,7 +22,7 @@ with lib;
propagatedBuildInputs = [ ssreflect ]; propagatedBuildInputs = [ ssreflect ];
meta = { meta = with lib; {
description = "Finite data structures with extensional reasoning"; description = "Finite data structures with extensional reasoning";
license = licenses.mit; license = licenses.mit;
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];
@ -31,5 +30,5 @@ with lib;
}).overrideAttrs (o: { }).overrideAttrs (o: {
propagatedBuildInputs = o.propagatedBuildInputs propagatedBuildInputs = o.propagatedBuildInputs
++ optional (versionAtLeast o.version "0.3.0") deriving; ++ lib.optional (lib.versionAtLeast o.version "0.3.0") deriving;
}) })

4
pkgs/development/coq-modules/fiat/HEAD.nix
View File

@ -1,6 +1,6 @@
{lib, mkCoqDerivation, coq, python27, version ? null }: {lib, mkCoqDerivation, coq, python27, version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "fiat"; pname = "fiat";
owner = "mit-plv"; owner = "mit-plv";
repo = "fiat"; repo = "fiat";
@ -29,6 +29,6 @@ with lib; mkCoqDerivation rec {
meta = { meta = {
homepage = "http://plv.csail.mit.edu/fiat/"; 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"; description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
maintainers = with maintainers; [ jwiegley ]; maintainers = with lib.maintainers; [ jwiegley ];
}; };
} }

6
pkgs/development/coq-modules/flocq/default.nix
View File

@ -1,12 +1,12 @@
{ lib, bash, autoconf, automake, { lib, bash, autoconf, automake,
mkCoqDerivation, coq, version ? null }: mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "flocq"; pname = "flocq";
owner = "flocq"; owner = "flocq";
domain = "gitlab.inria.fr"; domain = "gitlab.inria.fr";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.14" "8.16"; out = "4.1.0"; } { case = range "8.14" "8.16"; out = "4.1.0"; }
{ case = range "8.7" "8.15"; out = "3.4.3"; } { case = range "8.7" "8.15"; out = "3.4.3"; }
{ case = range "8.5" "8.8"; out = "2.6.1"; } { case = range "8.5" "8.8"; out = "2.6.1"; }
@ -22,7 +22,7 @@ with lib; mkCoqDerivation {
mlPlugin = true; mlPlugin = true;
useMelquiondRemake.logpath = "Flocq"; useMelquiondRemake.logpath = "Flocq";
meta = { meta = with lib; {
description = "A floating-point formalization for the Coq system"; description = "A floating-point formalization for the Coq system";
license = licenses.lgpl3; license = licenses.lgpl3;
maintainers = with maintainers; [ jwiegley ]; maintainers = with maintainers; [ jwiegley ];

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

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: { lib, mkCoqDerivation, coq, mathcomp, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "fourcolor"; pname = "fourcolor";
@ -12,15 +11,15 @@ mkCoqDerivation {
release."1.2.5".sha256 = "sha256-3qOPNCRjGK2UdHGMSqElpIXhAPVCklpeQgZwf9AFals="; release."1.2.5".sha256 = "sha256-3qOPNCRjGK2UdHGMSqElpIXhAPVCklpeQgZwf9AFals=";
inherit version; inherit version;
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (isGe "8.11") (isGe "1.12") ]; out = "1.2.5"; } { cases = [ (isGe "8.11") (isGe "1.12") ]; out = "1.2.5"; }
{ cases = [ (isGe "8.11") (range "1.11" "1.14") ]; out = "1.2.4"; } { cases = [ (isGe "8.11") (range "1.11" "1.14") ]; out = "1.2.4"; }
{ cases = [ (isLe "8.13") (pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; } { cases = [ (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
] null; ] null;
propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ]; propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
meta = { meta = with lib; {
description = "Formal proof of the Four Color Theorem "; description = "Formal proof of the Four Color Theorem ";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.cecill-b; license = licenses.cecill-b;

6
pkgs/development/coq-modules/gaia-hydras/default.nix
View File

@ -1,7 +1,7 @@
{ lib, mkCoqDerivation, coq, hydra-battles, gaia, { lib, mkCoqDerivation, coq, hydra-battles, gaia,
mathcomp-zify, mathcomp, version ? null }: mathcomp-zify, mathcomp, version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "gaia-hydras"; pname = "gaia-hydras";
repo = "hydra-battles"; repo = "hydra-battles";
@ -10,7 +10,7 @@ with lib; mkCoqDerivation rec {
releaseRev = (v: "v${v}"); releaseRev = (v: "v${v}");
inherit version; inherit version;
defaultVersion = with versions; switch [coq.coq-version mathcomp.version] [ defaultVersion = with lib.versions; lib.switch [coq.coq-version mathcomp.version] [
{ cases = [ (range "8.14" "8.16") (isGe "1.12.0") ]; out = "0.6"; } { cases = [ (range "8.14" "8.16") (isGe "1.12.0") ]; out = "0.6"; }
{ cases = [ (range "8.13" "8.14") (isGe "1.12.0") ]; out = "0.5"; } { cases = [ (range "8.13" "8.14") (isGe "1.12.0") ]; out = "0.5"; }
] null; ] null;
@ -23,7 +23,7 @@ with lib; mkCoqDerivation rec {
useDune = true; useDune = true;
meta = { meta = with lib; {
description = "Comparison between ordinals in Gaia and Hydra battles"; description = "Comparison between ordinals in Gaia and Hydra battles";
longDescription = '' longDescription = ''
The Gaia and Hydra battles projects develop different notions of ordinals. The Gaia and Hydra battles projects develop different notions of ordinals.

6
pkgs/development/coq-modules/gaia/default.nix
View File

@ -1,6 +1,6 @@
{ lib, mkCoqDerivation, coq, mathcomp, version ? null }: { lib, mkCoqDerivation, coq, mathcomp, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "gaia"; pname = "gaia";
release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5"; release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5";
@ -11,7 +11,7 @@ with lib; mkCoqDerivation {
releaseRev = (v: "v${v}"); releaseRev = (v: "v${v}");
inherit version; inherit version;
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (range "8.10" "8.16") (isGe "1.12.0") ]; out = "1.15"; } { cases = [ (range "8.10" "8.16") (isGe "1.12.0") ]; out = "1.15"; }
{ cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; } { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; }
] null; ] null;
@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
propagatedBuildInputs = propagatedBuildInputs =
[ mathcomp.ssreflect mathcomp.algebra mathcomp.fingroup ]; [ mathcomp.ssreflect mathcomp.algebra mathcomp.fingroup ];
meta = { meta = with lib; {
description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq"; description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq";
maintainers = with maintainers; [ Zimmi48 ]; maintainers = with maintainers; [ Zimmi48 ];
license = licenses.mit; license = licenses.mit;

6
pkgs/development/coq-modules/gappalib/default.nix
View File

@ -1,12 +1,12 @@
{ which, lib, mkCoqDerivation, autoconf, coq, flocq, version ? null }: { which, lib, mkCoqDerivation, autoconf, coq, flocq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "gappalib"; pname = "gappalib";
repo = "coq"; repo = "coq";
owner = "gappa"; owner = "gappa";
domain = "gitlab.inria.fr"; domain = "gitlab.inria.fr";
inherit version; inherit version;
defaultVersion = if versions.range "8.8" "8.16" coq.coq-version then "1.5.2" else null; defaultVersion = if lib.versions.range "8.8" "8.16" coq.coq-version then "1.5.2" else null;
release."1.5.2".sha256 = "sha256-A021Bhqz5r2CZBayfjIiWrCIfUlejcQAfbTmOaf6QTM="; release."1.5.2".sha256 = "sha256-A021Bhqz5r2CZBayfjIiWrCIfUlejcQAfbTmOaf6QTM=";
release."1.5.1".sha256 = "1806bq1z6q5rq2ma7d5kfbqfyfr755hjg0dq7b2llry8fx9cxjsg"; release."1.5.1".sha256 = "1806bq1z6q5rq2ma7d5kfbqfyfr755hjg0dq7b2llry8fx9cxjsg";
release."1.5.0".sha256 = "1i1c0gakffxqqqqw064cbvc243yl325hxd50jmczr6mk18igk41n"; release."1.5.0".sha256 = "1i1c0gakffxqqqqw064cbvc243yl325hxd50jmczr6mk18igk41n";
@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
propagatedBuildInputs = [ flocq ]; propagatedBuildInputs = [ flocq ];
useMelquiondRemake.logpath = "Gappa"; useMelquiondRemake.logpath = "Gappa";
meta = { meta = with lib; {
description = "Coq support library for Gappa"; description = "Coq support library for Gappa";
license = licenses.lgpl21; license = licenses.lgpl21;
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];

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

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, hydra-battles, pocklington, version ? null }: { lib, mkCoqDerivation, coq, hydra-battles, pocklington, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "goedel"; pname = "goedel";
@ -11,13 +10,13 @@ mkCoqDerivation {
release."8.13.0".sha256 = "0sqqkmj6wsk4xmhrnqkhcsbsrqjzn2gnk67nqzgrmjpw5danz8y5"; release."8.13.0".sha256 = "0sqqkmj6wsk4xmhrnqkhcsbsrqjzn2gnk67nqzgrmjpw5danz8y5";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.11" "8.16"; out = "8.13.0"; } { case = range "8.11" "8.16"; out = "8.13.0"; }
] null; ] null;
propagatedBuildInputs = [ hydra-battles pocklington ]; propagatedBuildInputs = [ hydra-battles pocklington ];
meta = { meta = with lib; {
description = "The Gödel-Rosser 1st incompleteness theorem in Coq"; description = "The Gödel-Rosser 1st incompleteness theorem in Coq";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.mit; license = licenses.mit;

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

@ -1,8 +1,6 @@
{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup { lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup
, hierarchy-builder, version ? null }: , hierarchy-builder, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "graph-theory"; pname = "graph-theory";
@ -11,13 +9,13 @@ mkCoqDerivation {
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.13" "8.16"; out = "0.9"; } { case = range "8.13" "8.16"; out = "0.9"; }
] null; ] null;
propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup hierarchy-builder ]; propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup hierarchy-builder ];
meta = { meta = with lib; {
description = "Library of formalized graph theory results in Coq"; description = "Library of formalized graph theory results in Coq";
longDescription = '' longDescription = ''
A library of formalized graph theory results, including various A library of formalized graph theory results, including various

6
pkgs/development/coq-modules/heq/default.nix
View File

@ -5,13 +5,13 @@ let fetcher = {rev, repo, owner, sha256, domain, ...}:
url = "https://${domain}/${owner}/${repo}/download/${repo}-${rev}.zip"; url = "https://${domain}/${owner}/${repo}/download/${repo}-${rev}.zip";
inherit sha256; inherit sha256;
}; in }; in
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "heq"; pname = "heq";
repo = "Heq"; repo = "Heq";
owner = "gil.hur"; owner = "gil.hur";
domain = "sf.snu.ac.kr"; domain = "sf.snu.ac.kr";
inherit version fetcher; inherit version fetcher;
defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null; defaultVersion = if lib.versions.isLt "8.8" coq.coq-version then "0.92" else null;
release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74"; release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74";
mlPlugin = true; mlPlugin = true;
@ -22,6 +22,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/"; homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/";
description = "Heq : a Coq library for Heterogeneous Equality"; description = "Heq : a Coq library for Heterogeneous Equality";
maintainers = with maintainers; [ jwiegley ]; maintainers = with lib.maintainers; [ jwiegley ];
}; };
} }

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

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, coq-elpi, version ? null }: { lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
with lib; let hb = mkCoqDerivation { let hb = mkCoqDerivation {
pname = "hierarchy-builder"; pname = "hierarchy-builder";
owner = "math-comp"; owner = "math-comp";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.15" "8.16"; out = "1.4.0"; } { case = range "8.15" "8.16"; out = "1.4.0"; }
{ case = range "8.13" "8.14"; out = "1.2.0"; } { case = range "8.13" "8.14"; out = "1.2.0"; }
{ case = range "8.12" "8.13"; out = "1.1.0"; } { case = range "8.12" "8.13"; out = "1.1.0"; }
@ -25,16 +25,16 @@ with lib; let hb = mkCoqDerivation {
extraInstallFlags = [ "VFILES=structures.v" ]; extraInstallFlags = [ "VFILES=structures.v" ];
meta = { meta = with lib; {
description = "High level commands to declare a hierarchy based on packed classes"; description = "High level commands to declare a hierarchy based on packed classes";
maintainers = with maintainers; [ cohencyril siraben ]; maintainers = with maintainers; [ cohencyril siraben ];
license = licenses.mit; license = licenses.mit;
}; };
}; in }; in
hb.overrideAttrs (o: hb.overrideAttrs (o:
optionalAttrs (versions.isGe "1.2.0" o.version || o.version == "dev") lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev")
{ buildPhase = "make build"; } { buildPhase = "make build"; }
// //
optionalAttrs (versions.isGe "1.1.0" o.version || o.version == "dev") lib.optionalAttrs (lib.versions.isGe "1.1.0" o.version || o.version == "dev")
{ installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; } { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
) )

7
pkgs/development/coq-modules/hydra-battles/default.nix
View File

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, equations, LibHyps, version ? null }: { lib, mkCoqDerivation, coq, equations, LibHyps, version ? null }:
with lib;
(mkCoqDerivation { (mkCoqDerivation {
pname = "hydra-battles"; pname = "hydra-battles";
@ -11,14 +10,14 @@ with lib;
releaseRev = (v: "v${v}"); releaseRev = (v: "v${v}");
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.13" "8.16"; out = "0.6"; } { case = range "8.13" "8.16"; out = "0.6"; }
{ case = range "8.11" "8.12"; out = "0.4"; } { case = range "8.11" "8.12"; out = "0.4"; }
] null; ] null;
useDune = true; useDune = true;
meta = { meta = with lib; {
description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq"; description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
longDescription = '' longDescription = ''
An exploration of some properties of Kirby and Paris' hydra An exploration of some properties of Kirby and Paris' hydra
@ -33,5 +32,5 @@ with lib;
}; };
}).overrideAttrs(o: }).overrideAttrs(o:
let inherit (o) version; in { let inherit (o) version; in {
propagatedBuildInputs = [ equations ] ++ optional (versions.isGe "0.6" version || version == "dev") LibHyps; propagatedBuildInputs = [ equations ] ++ lib.optional (lib.versions.isGe "0.6" version || version == "dev") LibHyps;
}) })

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

@ -1,11 +1,11 @@
{ lib, mkCoqDerivation, coq, stdpp, version ? null }: { lib, mkCoqDerivation, coq, stdpp, version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "iris"; pname = "iris";
domain = "gitlab.mpi-sws.org"; domain = "gitlab.mpi-sws.org";
owner = "iris"; owner = "iris";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.13" "8.16"; out = "4.0.0"; } { case = range "8.13" "8.16"; out = "4.0.0"; }
{ case = range "8.12" "8.14"; out = "3.5.0"; } { case = range "8.12" "8.14"; out = "3.5.0"; }
{ case = range "8.11" "8.13"; out = "3.4.0"; } { case = range "8.11" "8.13"; out = "3.4.0"; }
@ -26,7 +26,7 @@ with lib; mkCoqDerivation rec {
fi fi
''; '';
meta = { meta = with lib; {
description = "The Coq development of the Iris Project"; description = "The Coq development of the Iris Project";
license = licenses.bsd3; license = licenses.bsd3;
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];

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

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation rec { mkCoqDerivation rec {
pname = "itauto"; pname = "itauto";
@ -11,7 +10,7 @@ mkCoqDerivation rec {
release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9"; release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9";
release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A="; release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = isEq "8.16"; out = "8.16.0"; } { case = isEq "8.16"; out = "8.16.0"; }
{ case = isEq "8.15"; out = "8.15.0"; } { case = isEq "8.15"; out = "8.15.0"; }
{ case = isEq "8.14"; out = "8.14.0"; } { case = isEq "8.14"; out = "8.14.0"; }
@ -22,7 +21,7 @@ mkCoqDerivation rec {
nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]); nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
enableParallelBuilding = false; enableParallelBuilding = false;
meta = { meta = with lib; {
description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support"; description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.gpl3Plus; license = licenses.gpl3Plus;

6
pkgs/development/coq-modules/ltac2/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, which, coq, version ? null }: { lib, mkCoqDerivation, which, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "ltac2"; pname = "ltac2";
owner = "coq"; owner = "coq";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = "8.10"; out = "0.3"; } { case = "8.10"; out = "0.3"; }
{ case = "8.9"; out = "0.2"; } { case = "8.9"; out = "0.2"; }
{ case = "8.8"; out = "0.1"; } { case = "8.8"; out = "0.1"; }
@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
mlPlugin = true; mlPlugin = true;
meta = { meta = with lib; {
description = "A robust and expressive tactic language for Coq"; description = "A robust and expressive tactic language for Coq";
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];
license = licenses.lgpl21; license = licenses.lgpl21;

6
pkgs/development/coq-modules/math-classes/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, bignums, version ? null }: { lib, mkCoqDerivation, coq, bignums, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "math-classes"; pname = "math-classes";
inherit version; inherit version;
defaultVersion = if versions.range "8.6" "8.16" coq.coq-version then "8.15.0" else null; defaultVersion = if lib.versions.range "8.6" "8.16" coq.coq-version then "8.15.0" else null;
release."8.12.0".sha256 = "14nd6a08zncrl5yg2gzk0xf4iinwq4hxnsgm4fyv07ydbkxfb425"; release."8.12.0".sha256 = "14nd6a08zncrl5yg2gzk0xf4iinwq4hxnsgm4fyv07ydbkxfb425";
release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby"; release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby";
release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw"; release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw";
@ -14,6 +14,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
homepage = "https://math-classes.github.io"; homepage = "https://math-classes.github.io";
description = "A library of abstract interfaces for mathematical structures in Coq."; description = "A library of abstract interfaces for mathematical structures in Coq.";
maintainers = with maintainers; [ siddharthist jwiegley ]; maintainers = with lib.maintainers; [ siddharthist jwiegley ];
}; };
} }

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

@ -7,7 +7,7 @@ mkCoqDerivation {
owner = "math-comp"; owner = "math-comp";
inherit version; inherit version;
defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with lib; with versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (range "8.10" "8.16") (range "1.12.0" "1.15.0") ]; out = "1.2.1"; } { cases = [ (range "8.10" "8.16") (range "1.12.0" "1.15.0") ]; out = "1.2.1"; }
{ cases = [ (range "8.10" "8.15") (range "1.12.0" "1.14.0") ]; out = "1.2.0"; } { cases = [ (range "8.10" "8.15") (range "1.12.0" "1.14.0") ]; out = "1.2.0"; }
{ cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; } { cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; }

8
pkgs/development/coq-modules/mathcomp-algebra-tactics/default.nix
View File

@ -1,14 +1,14 @@
{ lib, mkCoqDerivation, coq, mathcomp-algebra, { lib, mkCoqDerivation, coq, mathcomp-algebra,
coq-elpi, mathcomp-zify, version ? null }: coq-elpi, mathcomp-zify, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "algebra-tactics"; pname = "algebra-tactics";
owner = "math-comp"; owner = "math-comp";
inherit version; inherit version;
defaultVersion = with versions; defaultVersion = with lib.versions;
switch [ coq.coq-version mathcomp-algebra.version ] [ lib.switch [ coq.coq-version mathcomp-algebra.version ] [
{ cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.0.0"; } { cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.0.0"; }
] null; ] null;
@ -18,6 +18,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
description = "Ring and field tactics for Mathematical Components"; description = "Ring and field tactics for Mathematical Components";
maintainers = with maintainers; [ cohencyril ]; maintainers = with lib.maintainers; [ cohencyril ];
}; };
} }

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

@ -21,7 +21,7 @@ let
release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8"; release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966"; release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (isGe "8.14") (isGe "1.13.0") ]; out = "0.5.3"; } { cases = [ (isGe "8.14") (isGe "1.13.0") ]; out = "0.5.3"; }
{ cases = [ (isGe "8.14") (range "1.13" "1.15") ]; out = "0.5.2"; } { cases = [ (isGe "8.14") (range "1.13" "1.15") ]; out = "0.5.2"; }
{ cases = [ (isGe "8.13") (range "1.13" "1.14") ]; out = "0.5.1"; } { cases = [ (isGe "8.13") (range "1.13" "1.14") ]; out = "0.5.1"; }
@ -40,7 +40,7 @@ let
classical-deps = [ mathcomp.algebra mathcomp-finmap hierarchy-builder ]; classical-deps = [ mathcomp.algebra mathcomp-finmap hierarchy-builder ];
analysis-deps = [ mathcomp.field mathcomp-bigenough ]; analysis-deps = [ mathcomp.field mathcomp-bigenough ];
intra-deps = if package == "single" then [] intra-deps = if package == "single" then []
else map mathcomp_ (head (splitList (pred.equal package) packages)); else map mathcomp_ (head (splitList (lib.pred.equal package) packages));
pkgpath = if package == "single" then "." pkgpath = if package == "single" then "."
else if package == "analysis" then "theories" else "${package}"; else if package == "analysis" then "theories" else "${package}";
pname = if package == "single" then "mathcomp-analysis-single" pname = if package == "single" then "mathcomp-analysis-single"

6
pkgs/development/coq-modules/mathcomp-bigenough/default.nix
View File

@ -1,6 +1,6 @@
{ coq, mkCoqDerivation, mathcomp, lib, version ? null }: { coq, mkCoqDerivation, mathcomp, lib, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "bigenough"; pname = "bigenough";
@ -11,7 +11,7 @@ with lib; mkCoqDerivation {
"1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw"; "1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
}; };
inherit version; inherit version;
defaultVersion = with versions; switch coq.version [ defaultVersion = with lib.versions; lib.switch coq.version [
{ case = range "8.10" "8.16"; out = "1.0.1"; } { case = range "8.10" "8.16"; out = "1.0.1"; }
{ case = range "8.5" "8.14"; out = "1.0.0"; } { case = range "8.5" "8.14"; out = "1.0.0"; }
] null; ] null;
@ -20,6 +20,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
description = "A small library to do epsilon - N reasonning"; description = "A small library to do epsilon - N reasonning";
license = licenses.cecill-b; license = lib.licenses.cecill-b;
}; };
} }

6
pkgs/development/coq-modules/mathcomp-finmap/default.nix
View File

@ -1,12 +1,12 @@
{ coq, mkCoqDerivation, mathcomp, lib, version ? null }: { coq, mkCoqDerivation, mathcomp, lib, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "finmap"; pname = "finmap";
owner = "math-comp"; owner = "math-comp";
inherit version; inherit version;
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.5.2"; } { cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.5.2"; }
{ cases = [ (isGe "8.10") (isGe "1.11") ]; out = "1.5.1"; } { cases = [ (isGe "8.10") (isGe "1.11") ]; out = "1.5.1"; }
{ cases = [ (range "8.7" "8.11") "1.11.0" ]; out = "1.5.0"; } { cases = [ (range "8.7" "8.11") "1.11.0" ]; out = "1.5.0"; }
@ -33,6 +33,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
description = "A finset and finmap library"; description = "A finset and finmap library";
license = licenses.cecill-b; license = lib.licenses.cecill-b;
}; };
} }

6
pkgs/development/coq-modules/mathcomp-real-closed/default.nix
View File

@ -1,7 +1,7 @@
{ coq, mkCoqDerivation, mathcomp, mathcomp-bigenough, { coq, mkCoqDerivation, mathcomp, mathcomp-bigenough,
lib, version ? null }: lib, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "real-closed"; pname = "real-closed";
@ -17,7 +17,7 @@ with lib; mkCoqDerivation {
"1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg"; "1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
}; };
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (isGe "8.13") (isGe "1.12.0") ]; out = "1.1.3"; } { cases = [ (isGe "8.13") (isGe "1.12.0") ]; out = "1.1.3"; }
{ cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.1.2"; } { cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.1.2"; }
{ cases = [ (isGe "8.7") "1.11.0" ]; out = "1.1.1"; } { cases = [ (isGe "8.7") "1.11.0" ]; out = "1.1.1"; }
@ -37,6 +37,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
description = "Mathematical Components Library on real closed fields"; description = "Mathematical Components Library on real closed fields";
license = licenses.cecill-c; license = lib.licenses.cecill-c;
}; };
} }

9
pkgs/development/coq-modules/mathcomp-tarjan/default.nix
View File

@ -1,14 +1,15 @@
{ coq, mkCoqDerivation, mathcomp-ssreflect, mathcomp-fingroup, { coq, mkCoqDerivation, mathcomp-ssreflect, mathcomp-fingroup,
lib, version ? null }@args: lib, version ? null }@args:
with lib; mkCoqDerivation {
mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "tarjan"; pname = "tarjan";
owner = "math-comp"; owner = "math-comp";
inherit version; inherit version;
defaultVersion = with versions; defaultVersion = with lib.versions;
switch [ coq.version mathcomp-ssreflect.version ] [{ lib.switch [ coq.version mathcomp-ssreflect.version ] [{
cases = [ (range "8.10" "8.16") (isGe "1.12.0") ]; out = "1.0.0"; cases = [ (range "8.10" "8.16") (isGe "1.12.0") ]; out = "1.0.0";
}] null; }] null;
release."1.0.0".sha256 = "sha256:0r459r0makshzwlygw6kd4lpvdjc43b3x5y9aa8x77f2z5gymjq1"; release."1.0.0".sha256 = "sha256:0r459r0makshzwlygw6kd4lpvdjc43b3x5y9aa8x77f2z5gymjq1";
@ -17,6 +18,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
description = "Proofs of Tarjan and Kosaraju connected components algorithms"; description = "Proofs of Tarjan and Kosaraju connected components algorithms";
license = licenses.cecill-b; license = lib.licenses.cecill-b;
}; };
} }

5
pkgs/development/coq-modules/mathcomp-word/default.nix
View File

@ -1,6 +1,5 @@
{ coq, mkCoqDerivation, mathcomp, lib, version ? null }: { coq, mkCoqDerivation, mathcomp, lib, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "word"; pname = "word";
@ -15,13 +14,13 @@ mkCoqDerivation {
release."1.0".sha256 = "sha256:0703m97rnivcbc7vvbd9rl2dxs6l8n52cbykynw61c6w9rhxspcg"; release."1.0".sha256 = "sha256:0703m97rnivcbc7vvbd9rl2dxs6l8n52cbykynw61c6w9rhxspcg";
inherit version; inherit version;
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (range "8.12" "8.16") (isGe "1.12") ]; out = "2.0"; } { cases = [ (range "8.12" "8.16") (isGe "1.12") ]; out = "2.0"; }
] null; ] null;
propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ]; propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
meta = { meta = with lib; {
description = "Yet Another Coq Library on Machine Words"; description = "Yet Another Coq Library on Machine Words";
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];
license = licenses.mit; license = licenses.mit;

8
pkgs/development/coq-modules/mathcomp-zify/default.nix
View File

@ -1,14 +1,14 @@
{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-ssreflect, mathcomp-fingroup, version ? null }: { lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-ssreflect, mathcomp-fingroup, version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "zify"; pname = "zify";
repo = "mczify"; repo = "mczify";
owner = "math-comp"; owner = "math-comp";
inherit version; inherit version;
defaultVersion = with versions; defaultVersion = with lib.versions;
switch [ coq.coq-version mathcomp-algebra.version ] [ lib.switch [ coq.coq-version mathcomp-algebra.version ] [
{ cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; } { cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; }
] null; ] null;
@ -19,6 +19,6 @@ with lib; mkCoqDerivation rec {
meta = { meta = {
description = "Micromega tactics for Mathematical Components"; description = "Micromega tactics for Mathematical Components";
maintainers = with maintainers; [ cohencyril ]; maintainers = with lib.maintainers; [ cohencyril ];
}; };
} }

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

@ -18,7 +18,7 @@ let
repo = "math-comp"; repo = "math-comp";
owner = "math-comp"; owner = "math-comp";
withDoc = single && (args.withDoc or false); withDoc = single && (args.withDoc or false);
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with versions; lib.switch coq.coq-version [
{ case = range "8.14" "8.16"; out = "1.15.0"; } { case = range "8.14" "8.16"; out = "1.15.0"; }
{ case = range "8.11" "8.15"; out = "1.14.0"; } { case = range "8.11" "8.15"; out = "1.14.0"; }
{ case = range "8.11" "8.15"; out = "1.13.0"; } { case = range "8.11" "8.15"; out = "1.13.0"; }
@ -50,7 +50,7 @@ let
mathcomp_ = package: let mathcomp_ = package: let
mathcomp-deps = if package == "single" then [] mathcomp-deps = if package == "single" then []
else map mathcomp_ (head (splitList (pred.equal package) packages)); else map mathcomp_ (head (splitList (lib.pred.equal package) packages));
pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
pname = if package == "single" then "mathcomp" else "mathcomp-${package}"; pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
pkgallMake = '' pkgallMake = ''

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

@ -5,7 +5,7 @@ with builtins // lib;
let let
repo = "metacoq"; repo = "metacoq";
owner = "MetaCoq"; owner = "MetaCoq";
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with versions; lib.switch coq.coq-version [
{ case = "8.11"; out = "1.0-beta2-8.11"; } { case = "8.11"; out = "1.0-beta2-8.11"; }
{ case = "8.12"; out = "1.0-beta2-8.12"; } { case = "8.12"; out = "1.0-beta2-8.12"; }
# Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3) # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
@ -34,7 +34,7 @@ let
metacoq_ = package: let metacoq_ = package: let
metacoq-deps = if package == "single" then [] metacoq-deps = if package == "single" then []
else map metacoq_ (head (splitList (pred.equal package) packages)); else map metacoq_ (head (splitList (lib.pred.equal package) packages));
pkgpath = if package == "single" then "./" else "./${package}"; pkgpath = if package == "single" then "./" else "./${package}";
pname = if package == "all" then "metacoq" else "metacoq-${package}"; pname = if package == "all" then "metacoq" else "metacoq-${package}";
pkgallMake = '' pkgallMake = ''

6
pkgs/development/coq-modules/metalib/default.nix
View File

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "metalib"; pname = "metalib";
owner = "plclub"; owner = "plclub";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.14" "8.16"; out = "8.15"; } { case = range "8.14" "8.16"; out = "8.15"; }
{ case = range "8.10" "8.13"; out = "8.10"; } { case = range "8.10" "8.13"; out = "8.10"; }
] null; ] null;
@ -14,7 +14,7 @@ with lib; mkCoqDerivation {
sourceRoot = "source/Metalib"; sourceRoot = "source/Metalib";
meta = { meta = with lib; {
license = licenses.mit; license = licenses.mit;
maintainers = [ maintainers.jwiegley ]; maintainers = [ maintainers.jwiegley ];
}; };

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

@ -1,6 +1,6 @@
{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, { coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
lib, version ? null, useDune ? false }@args: lib, version ? null, useDune ? false }@args:
with lib; mkCoqDerivation { mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "multinomials"; pname = "multinomials";
@ -8,7 +8,7 @@ with lib; mkCoqDerivation {
owner = "math-comp"; owner = "math-comp";
inherit version; inherit version;
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
{ cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.5.5"; } { cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.5.5"; }
{ cases = [ (range "8.10" "8.12") "1.12.0" ]; out = "1.5.3"; } { cases = [ (range "8.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.12") "1.11.0" ]; out = "1.5.2"; }
@ -31,7 +31,7 @@ with lib; mkCoqDerivation {
"1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; "1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
}; };
useDuneifVersion = v: versions.isGe "1.5.3" v || v == "dev"; useDuneifVersion = v: lib.versions.isGe "1.5.3" v || v == "dev";
preConfigure = '' preConfigure = ''
patchShebangs configure || true patchShebangs configure || true
@ -42,7 +42,7 @@ with lib; mkCoqDerivation {
meta = { meta = {
description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials"; description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
license = licenses.cecill-c; license = lib.licenses.cecill-c;
}; };
} }
// optionalAttrs (args?useDune) { inherit useDune; } // lib.optionalAttrs (args?useDune) { inherit useDune; }

5
pkgs/development/coq-modules/odd-order/default.nix
View File

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, mathcomp, version ? null }: { lib, mkCoqDerivation, mathcomp, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "odd-order"; pname = "odd-order";
@ -11,7 +10,7 @@ mkCoqDerivation {
releaseRev = v: "mathcomp-odd-order.${v}"; releaseRev = v: "mathcomp-odd-order.${v}";
inherit version; inherit version;
defaultVersion = with versions; switch mathcomp.character.version [ defaultVersion = with lib.versions; lib.switch mathcomp.character.version [
{ case = (range "1.13.0" "1.15.0"); out = "1.14.0"; } { case = (range "1.13.0" "1.15.0"); out = "1.14.0"; }
{ case = (range "1.12.0" "1.14.0"); out = "1.13.0"; } { case = (range "1.12.0" "1.14.0"); out = "1.13.0"; }
{ case = (range "1.10.0" "1.12.0"); out = "1.12.0"; } { case = (range "1.10.0" "1.12.0"); out = "1.12.0"; }
@ -27,7 +26,7 @@ mkCoqDerivation {
mathcomp.all mathcomp.all
]; ];
meta = { meta = with lib; {
description = "Formal proof of the Odd Order Theorem"; description = "Formal proof of the Odd Order Theorem";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.cecill-b; license = licenses.cecill-b;

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

@ -1,10 +1,10 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "paco"; pname = "paco";
owner = "snu-sf"; owner = "snu-sf";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.12" "8.16"; out = "4.1.2"; } { case = range "8.12" "8.16"; out = "4.1.2"; }
{ case = range "8.9" "8.13"; out = "4.1.1"; } { case = range "8.9" "8.13"; out = "4.1.1"; }
{ case = range "8.6" "8.13"; out = "4.0.2"; } { case = range "8.6" "8.13"; out = "4.0.2"; }
@ -27,6 +27,6 @@ with lib; mkCoqDerivation {
meta = { meta = {
homepage = "http://plv.mpi-sws.org/paco/"; homepage = "http://plv.mpi-sws.org/paco/";
description = "A Coq library implementing parameterized coinduction"; description = "A Coq library implementing parameterized coinduction";
maintainers = with maintainers; [ jwiegley ptival ]; maintainers = with lib.maintainers; [ jwiegley ptival ];
}; };
} }

6
pkgs/development/coq-modules/paramcoq/default.nix
View File

@ -1,9 +1,9 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "paramcoq"; pname = "paramcoq";
inherit version; inherit version;
defaultVersion = with versions; switch coq.version [ defaultVersion = with lib.versions; lib.switch coq.version [
{ case = range "8.10" "8.16"; out = "1.1.3+coq${coq.coq-version}"; } { case = range "8.10" "8.16"; out = "1.1.3+coq${coq.coq-version}"; }
{ case = range "8.7" "8.13"; out = "1.1.2+coq${coq.coq-version}"; } { case = range "8.7" "8.13"; out = "1.1.2+coq${coq.coq-version}"; }
] null; ] null;
@ -24,7 +24,7 @@ with lib; mkCoqDerivation {
release."1.1.2+coq8.7".sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj"; release."1.1.2+coq8.7".sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj";
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
mlPlugin = true; mlPlugin = true;
meta = { meta = with lib; {
description = "Coq plugin for parametricity"; description = "Coq plugin for parametricity";
license = licenses.mit; license = licenses.mit;
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];

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

@ -1,6 +1,5 @@
{ lib, mkCoqDerivation, coq, ceres, coq-ext-lib, version ? null }: { lib, mkCoqDerivation, coq, ceres, coq-ext-lib, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "parsec"; pname = "parsec";
@ -11,14 +10,14 @@ mkCoqDerivation {
releaseRev = (v: "v${v}"); releaseRev = (v: "v${v}");
inherit version; inherit version;
defaultVersion = with versions; switch coq.version [ defaultVersion = with lib.versions; lib.switch coq.version [
{ case = range "8.12" "8.16"; out = "0.1.1"; } { case = range "8.12" "8.16"; out = "0.1.1"; }
{ case = range "8.12" "8.13"; out = "0.1.0"; } { case = range "8.12" "8.13"; out = "0.1.0"; }
] null; ] null;
release."0.1.1".sha256 = "sha256:1c0l18s68pzd4c8i3jimh2yz0pqm4g38pca4bm7fr18r8xmqf189"; release."0.1.1".sha256 = "sha256:1c0l18s68pzd4c8i3jimh2yz0pqm4g38pca4bm7fr18r8xmqf189";
release."0.1.0".sha256 = "sha256:01avfcqirz2b9wjzi9iywbhz9szybpnnj3672dgkfsimyg9jgnsr"; release."0.1.0".sha256 = "sha256:01avfcqirz2b9wjzi9iywbhz9szybpnnj3672dgkfsimyg9jgnsr";
meta = { meta = with lib; {
description = "Library for serialization to S-expressions"; description = "Library for serialization to S-expressions";
license = licenses.bsd3; license = licenses.bsd3;
maintainers = with maintainers; [ Zimmi48 ]; maintainers = with maintainers; [ Zimmi48 ];

5
pkgs/development/coq-modules/pocklington/default.nix
View File

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "pocklington"; pname = "pocklington";
@ -9,11 +8,11 @@ mkCoqDerivation {
release."8.12.0".sha256 = "sha256-0xBrw9+4g14niYdNqp0nx00fPJoSSnaDSDEaIVpPfjs="; release."8.12.0".sha256 = "sha256-0xBrw9+4g14niYdNqp0nx00fPJoSSnaDSDEaIVpPfjs=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = isGe "8.7"; out = "8.12.0"; } { case = isGe "8.7"; out = "8.12.0"; }
] null; ] null;
meta = { meta = with lib; {
description = "Pocklington's criterion for primality in Coq"; description = "Pocklington's criterion for primality in Coq";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.mit; license = licenses.mit;

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

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, ssreflect, version ? null }: { lib, mkCoqDerivation, coq, ssreflect, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "reglang"; pname = "reglang";
@ -9,14 +8,14 @@ mkCoqDerivation {
release."1.1.2".sha256 = "sha256-SEnMilLNxh6a3oiDNGLaBr8quQ/nO2T9Fwdf/1il2Yk="; release."1.1.2".sha256 = "sha256-SEnMilLNxh6a3oiDNGLaBr8quQ/nO2T9Fwdf/1il2Yk=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.10" "8.16"; out = "1.1.2"; } { case = range "8.10" "8.16"; out = "1.1.2"; }
] null; ] null;
propagatedBuildInputs = [ ssreflect ]; propagatedBuildInputs = [ ssreflect ];
meta = { meta = with lib; {
description = "Regular Language Representations in Coq"; description = "Regular Language Representations in Coq";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.cecill-b; license = licenses.cecill-b;

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

@ -1,12 +1,11 @@
{ lib, mkCoqDerivation, coq, aac-tactics, mathcomp, version ? null }: { lib, mkCoqDerivation, coq, aac-tactics, mathcomp, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "relation-algebra"; pname = "relation-algebra";
owner = "damien-pous"; owner = "damien-pous";
releaseRev = v: releaseRev = v:
if versions.isGe "1.7.6" v if lib.versions.isGe "1.7.6" v
then "v.${v}" then "v.${v}"
else "v${v}"; else "v${v}";
@ -20,7 +19,7 @@ mkCoqDerivation {
release."1.7.1".sha256 = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA="; release."1.7.1".sha256 = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = isEq "8.16"; out = "1.7.8"; } { case = isEq "8.16"; out = "1.7.8"; }
{ case = isEq "8.15"; out = "1.7.7"; } { case = isEq "8.15"; out = "1.7.7"; }
{ case = isEq "8.14"; out = "1.7.6"; } { case = isEq "8.14"; out = "1.7.6"; }
@ -35,7 +34,7 @@ mkCoqDerivation {
propagatedBuildInputs = [ aac-tactics mathcomp.ssreflect ]; propagatedBuildInputs = [ aac-tactics mathcomp.ssreflect ];
meta = { meta = with lib; {
description = "Relation algebra library for Coq"; description = "Relation algebra library for Coq";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.gpl3Plus; license = licenses.gpl3Plus;

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

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation rec { mkCoqDerivation rec {
pname = "semantics"; pname = "semantics";
@ -15,7 +14,7 @@ mkCoqDerivation rec {
release."8.6.0".sha256 = "sha256-GltkGQ3tJqUPAbdDkqqvKLLhMOap50XvGaCkjshiNdY="; release."8.6.0".sha256 = "sha256-GltkGQ3tJqUPAbdDkqqvKLLhMOap50XvGaCkjshiNdY=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.10" "8.16"; out = "8.14.0"; } { case = range "8.10" "8.16"; out = "8.14.0"; }
{ case = "8.9"; out = "8.9.0"; } { case = "8.9"; out = "8.9.0"; }
{ case = "8.8"; out = "8.8.0"; } { case = "8.8"; out = "8.8.0"; }
@ -34,7 +33,7 @@ mkCoqDerivation rec {
done done
''; '';
meta = { meta = with lib; {
description = "A survey of programming language semantics styles in Coq"; description = "A survey of programming language semantics styles in Coq";
longDescription = '' longDescription = ''
A survey of semantics styles in Coq, from natural semantics through A survey of semantics styles in Coq, from natural semantics through

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

@ -17,7 +17,7 @@ in
inherit version release; inherit version release;
defaultVersion = with versions; defaultVersion = with versions;
switch coq.version [ lib.switch coq.version [
{ case = isEq "8.16"; out = "8.16.0+0.16.0"; } { case = isEq "8.16"; out = "8.16.0+0.16.0"; }
{ case = isEq "8.15"; out = "8.15.0+0.15.0"; } { case = isEq "8.15"; out = "8.15.0+0.15.0"; }
{ case = isEq "8.14"; out = "8.14.0+0.14.0"; } { case = isEq "8.14"; out = "8.14.0+0.14.0"; }

6
pkgs/development/coq-modules/simple-io/default.nix
View File

@ -1,11 +1,11 @@
{ lib, callPackage, mkCoqDerivation, coq, coq-ext-lib, version ? null }: { lib, callPackage, mkCoqDerivation, coq, coq-ext-lib, version ? null }:
with lib; mkCoqDerivation { mkCoqDerivation {
pname = "simple-io"; pname = "simple-io";
owner = "Lysxia"; owner = "Lysxia";
repo = "coq-simple-io"; repo = "coq-simple-io";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.11" "8.16"; out = "1.7.0"; } { case = range "8.11" "8.16"; out = "1.7.0"; }
{ case = range "8.7" "8.13"; out = "1.3.0"; } { case = range "8.7" "8.13"; out = "1.3.0"; }
] null; ] null;
@ -21,7 +21,7 @@ with lib; mkCoqDerivation {
passthru.tests.HelloWorld = callPackage ./test.nix {}; passthru.tests.HelloWorld = callPackage ./test.nix {};
meta = { meta = with lib; {
description = "Purely functional IO for Coq"; description = "Purely functional IO for Coq";
license = licenses.mit; license = licenses.mit;
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];

5
pkgs/development/coq-modules/smpl/default.nix
View File

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "smpl"; pname = "smpl";
@ -13,7 +12,7 @@ mkCoqDerivation {
releaseRev = v: "v${v}"; releaseRev = v: "v${v}";
inherit version; inherit version;
defaultVersion = with versions; switch coq.version [ defaultVersion = with lib.versions; lib.switch coq.version [
{ case = isEq "8.15"; out = "8.15"; } { case = isEq "8.15"; out = "8.15"; }
{ case = isEq "8.14"; out = "8.14"; } { case = isEq "8.14"; out = "8.14"; }
{ case = "8.13.2"; out = "8.13"; } { case = "8.13.2"; out = "8.13"; }
@ -23,7 +22,7 @@ mkCoqDerivation {
mlPlugin = true; mlPlugin = true;
meta = { meta = with lib; {
description = "A Coq plugin providing an extensible tactic similar to first"; description = "A Coq plugin providing an extensible tactic similar to first";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.mit; license = licenses.mit;

5
pkgs/development/coq-modules/smtcoq/default.nix
View File

@ -1,5 +1,4 @@
{ lib, stdenv, gcc10StdenvCompat, pkgs, mkCoqDerivation, coq, trakt, veriT, zchaff, fetchurl, version ? null }: { lib, stdenv, gcc10StdenvCompat, pkgs, mkCoqDerivation, coq, trakt, veriT, zchaff, fetchurl, version ? null }:
with lib;
let let
# version of veriT that works with SMTCoq # version of veriT that works with SMTCoq
@ -23,7 +22,7 @@ mkCoqDerivation {
release."2021-09-17".sha256 = "sha256-bF7ES+tXraaAJwVEwAMx3CUESpNlAUerQjr4d2eaGJQ="; release."2021-09-17".sha256 = "sha256-bF7ES+tXraaAJwVEwAMx3CUESpNlAUerQjr4d2eaGJQ=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.version [ defaultVersion = with lib.versions; lib.switch coq.version [
{ case = isEq "8.13"; out = "2021-09-17"; } { case = isEq "8.13"; out = "2021-09-17"; }
] null; ] null;
@ -34,7 +33,7 @@ mkCoqDerivation {
# This is meant to ease future troubleshooting of cvc4 build failures # This is meant to ease future troubleshooting of cvc4 build failures
passthru = { inherit cvc4; }; passthru = { inherit cvc4; };
meta = { meta = with lib; {
description = "Communication between Coq and SAT/SMT solvers "; description = "Communication between Coq and SAT/SMT solvers ";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.cecill-b; license = licenses.cecill-b;

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

@ -1,11 +1,11 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; mkCoqDerivation rec { mkCoqDerivation rec {
pname = "stdpp"; pname = "stdpp";
inherit version; inherit version;
domain = "gitlab.mpi-sws.org"; domain = "gitlab.mpi-sws.org";
owner = "iris"; owner = "iris";
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.13" "8.16"; out = "1.8.0"; } { case = range "8.13" "8.16"; out = "1.8.0"; }
{ case = range "8.12" "8.14"; out = "1.6.0"; } { case = range "8.12" "8.14"; out = "1.6.0"; }
{ case = range "8.11" "8.13"; out = "1.5.0"; } { case = range "8.11" "8.13"; out = "1.5.0"; }
@ -24,7 +24,7 @@ with lib; mkCoqDerivation rec {
fi fi
''; '';
meta = { meta = with lib; {
description = "An extended “Standard Library” for Coq"; description = "An extended “Standard Library” for Coq";
license = licenses.bsd3; license = licenses.bsd3;
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];

8
pkgs/development/coq-modules/tlc/default.nix
View File

@ -1,11 +1,11 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib; (mkCoqDerivation { (mkCoqDerivation {
pname = "tlc"; pname = "tlc";
owner = "charguer"; owner = "charguer";
inherit version; inherit version;
displayVersion = { tlc = false; }; displayVersion = { tlc = false; };
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.13" "8.16"; out = "20211215"; } { case = range "8.13" "8.16"; out = "20211215"; }
{ case = range "8.12" "8.13"; out = "20210316"; } { case = range "8.12" "8.13"; out = "20210316"; }
{ case = range "8.10" "8.12"; out = "20200328"; } { case = range "8.10" "8.12"; out = "20200328"; }
@ -16,14 +16,14 @@ with lib; (mkCoqDerivation {
release."20200328".sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx"; release."20200328".sha256 = "16vzild9gni8zhgb3qhmka47f8zagdh03k6nssif7drpim8233lx";
release."20181116".sha256 = "032lrbkxqm9d3fhf6nv1kq2z0mqd3czv3ijlbsjwnfh12xck4vpl"; release."20181116".sha256 = "032lrbkxqm9d3fhf6nv1kq2z0mqd3czv3ijlbsjwnfh12xck4vpl";
meta = { meta = with lib; {
homepage = "http://www.chargueraud.org/softs/tlc/"; homepage = "http://www.chargueraud.org/softs/tlc/";
description = "A non-constructive library for Coq"; description = "A non-constructive library for Coq";
license = licenses.free; license = licenses.free;
maintainers = [ maintainers.vbgl ]; maintainers = [ maintainers.vbgl ];
}; };
}).overrideAttrs (x: }).overrideAttrs (x:
if versionAtLeast x.version "20210316" if lib.versionAtLeast x.version "20210316"
then {} then {}
else { else {
installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ]; installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ];

7
pkgs/development/coq-modules/topology/default.nix
View File

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, mathcomp, zorns-lemma, version ? null }: { lib, mkCoqDerivation, coq, mathcomp, zorns-lemma, version ? null }:
with lib;
mkCoqDerivation rec { mkCoqDerivation rec {
pname = "topology"; pname = "topology";
@ -15,7 +14,7 @@ mkCoqDerivation rec {
release."8.6.0".sha256 = "sha256-eu/dBEFo3y6vnXlJljUD4hds6+qgAPQVvsuspyGHcj8="; release."8.6.0".sha256 = "sha256-eu/dBEFo3y6vnXlJljUD4hds6+qgAPQVvsuspyGHcj8=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.10" "8.16"; out = "9.0.0"; } { case = range "8.10" "8.16"; out = "9.0.0"; }
{ case = "8.9"; out = "8.9.0"; } { case = "8.9"; out = "8.9.0"; }
{ case = "8.8"; out = "8.8.0"; } { case = "8.8"; out = "8.8.0"; }
@ -25,9 +24,9 @@ mkCoqDerivation rec {
propagatedBuildInputs = [ zorns-lemma ]; propagatedBuildInputs = [ zorns-lemma ];
useDuneifVersion = versions.isGe "9.0"; useDuneifVersion = lib.versions.isGe "9.0";
meta = { meta = with lib; {
description = "General topology in Coq"; description = "General topology in Coq";
longDescription = '' longDescription = ''
This library develops some of the basic concepts and results of This library develops some of the basic concepts and results of

5
pkgs/development/coq-modules/trakt/default.nix
View File

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, coq-elpi, version ? null }: { lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
with lib;
mkCoqDerivation { mkCoqDerivation {
pname = "trakt"; pname = "trakt";
@ -9,13 +8,13 @@ mkCoqDerivation {
release."1.0".sha256 = "sha256-Qhw5fWFYxUFO2kIWWz/og+4fuy9aYG27szfNk3IglhY="; release."1.0".sha256 = "sha256-Qhw5fWFYxUFO2kIWWz/og+4fuy9aYG27szfNk3IglhY=";
inherit version; inherit version;
defaultVersion = with versions; switch [ coq.version ] [ defaultVersion = with lib.versions; lib.switch [ coq.version ] [
{ cases = [ (range "8.13" "8.16") ]; out = "1.0"; } { cases = [ (range "8.13" "8.16") ]; out = "1.0"; }
] null; ] null;
propagatedBuildInputs = [ coq-elpi ]; propagatedBuildInputs = [ coq-elpi ];
meta = { meta = with lib; {
description = "A generic goal preprocessing tool for proof automation tactics in Coq"; description = "A generic goal preprocessing tool for proof automation tactics in Coq";
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.cecill-b; license = licenses.cecill-b;

9
pkgs/development/coq-modules/zorns-lemma/default.nix
View File

@ -1,5 +1,4 @@
{ lib, mkCoqDerivation, coq, version ? null }: { lib, mkCoqDerivation, coq, version ? null }:
with lib;
(mkCoqDerivation { (mkCoqDerivation {
pname = "zorns-lemma"; pname = "zorns-lemma";
@ -16,7 +15,7 @@ with lib;
release."8.5.0".sha256 = "sha256-mH/v02ObMjbVPYx2H+Jhz+Xp0XRKN67iMAdA1VNFzso="; release."8.5.0".sha256 = "sha256-mH/v02ObMjbVPYx2H+Jhz+Xp0XRKN67iMAdA1VNFzso=";
inherit version; inherit version;
defaultVersion = with versions; switch coq.coq-version [ defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.10" "8.16"; out = "9.0.0"; } { case = range "8.10" "8.16"; out = "9.0.0"; }
{ case = "8.9"; out = "8.9.0"; } { case = "8.9"; out = "8.9.0"; }
{ case = "8.8"; out = "8.8.0"; } { case = "8.8"; out = "8.8.0"; }
@ -25,9 +24,9 @@ with lib;
{ case = "8.5"; out = "8.5.0"; } { case = "8.5"; out = "8.5.0"; }
] null; ] null;
useDuneifVersion = versions.isGe "9.0"; useDuneifVersion = lib.versions.isGe "9.0";
meta = { meta = with lib; {
description = "Development of basic set theory"; description = "Development of basic set theory";
longDescription = '' longDescription = ''
This Coq library develops some basic set theory. The main This Coq library develops some basic set theory. The main
@ -37,4 +36,4 @@ with lib;
maintainers = with maintainers; [ siraben ]; maintainers = with maintainers; [ siraben ];
license = licenses.lgpl21Plus; license = licenses.lgpl21Plus;
}; };
}).overrideAttrs({version, ...}: if versions.isGe "9.0" version then { repo = "topology"; } else {}) }).overrideAttrs({version, ...}: if lib.versions.isGe "9.0" version then { repo = "topology"; } else {})