diff --git a/maintainers/maintainer-list.nix b/maintainers/maintainer-list.nix index 3ed31c9ce919..22f9b78a650a 100644 --- a/maintainers/maintainer-list.nix +++ b/maintainers/maintainer-list.nix @@ -3498,6 +3498,12 @@ github = "jorsn"; githubId = 4646725; }; + jpas = { + name = "Jarrod Pas"; + email = "jarrod@jarrodpas.com"; + github = "jpas"; + githubId = 5689724; + }; jpdoyle = { email = "joethedoyle@gmail.com"; github = "jpdoyle"; diff --git a/pkgs/development/coq-modules/CoLoR/default.nix b/pkgs/development/coq-modules/CoLoR/default.nix index 82c6e58a7b03..d145586af43b 100644 --- a/pkgs/development/coq-modules/CoLoR/default.nix +++ b/pkgs/development/coq-modules/CoLoR/default.nix @@ -1,11 +1,40 @@ -{ stdenv, fetchurl, coq, bignums }: +{ stdenv, fetchFromGitHub, coq, bignums }: + +let + coqVersions = { + "8.6" = "1.4.0"; + "8.7" = "1.4.0"; + "8.8" = "1.6.0"; + "8.9" = "1.6.0"; + "8.10" = "1.7.0"; + }; + params = { + "1.4.0" = { + version = "1.4.0"; + rev = "168c6b86c7d3f87ee51791f795a8828b1521589a"; + sha256 = "1d2whsgs3kcg5wgampd6yaqagcpmzhgb6a0hp6qn4lbimck5dfmm"; + }; + "1.6.0" = { + version = "1.6.0"; + rev = "328aa06270584b578edc0d2925e773cced4f14c8"; + sha256 = "07sy9kw1qlynsqy251adgi8b3hghrc9xxl2rid6c82mxfsp329sd"; + }; + "1.7.0" = { + version = "1.7.0"; + rev = "08b5481ed6ea1a5d2c4c068b62156f5be6d82b40"; + sha256 = "1w7fmcpf0691gcwq00lm788k4ijlwz3667zj40j5jjc8j8hj7cq3"; + }; + }; + param = params.${coqVersions.${coq.coq-version}}; +in stdenv.mkDerivation { - name = "coq${coq.coq-version}-CoLoR-1.4.0"; + name = "coq${coq.coq-version}-CoLoR-${param.version}"; - src = fetchurl { - url = https://gforge.inria.fr/frs/download.php/file/37205/color.1.4.0.tar.gz; - sha256 = "1jsp9adsh7w59y41ihbwchryjhjpajgs9bhf8rnb4b3hzccqxgag"; + src = fetchFromGitHub { + owner = "fblanqui"; + repo = "color"; + inherit (param) rev sha256; }; buildInputs = [ coq bignums ]; @@ -18,11 +47,11 @@ stdenv.mkDerivation { meta = with stdenv.lib; { homepage = http://color.inria.fr/; description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant."; - maintainers = with maintainers; [ jwiegley ]; + maintainers = with maintainers; [ jpas jwiegley ]; platforms = coq.meta.platforms; }; passthru = { - compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ]; + compatibleCoqVersions = v: builtins.hasAttr v coqVersions; }; }