summary refs log tree commit diff
path: root/pkgs/development/coq-modules/equations
diff options
context:
space:
mode:
authorCyril Cohen <cohen@crans.org>2020-08-28 23:05:46 +0200
committerVincent Laporte <vbgl@users.noreply.github.com>2021-01-09 11:56:17 +0100
commit9ffd16b3850536094ca36bc31520bb15a6d5a9ef (patch)
treea837e242f85684e721a9d5fa65d1de869a559e11 /pkgs/development/coq-modules/equations
parent04065a73547d3c93a25225531ee1e9d9642ff761 (diff)
downloadnixpkgs-9ffd16b3850536094ca36bc31520bb15a6d5a9ef.tar
nixpkgs-9ffd16b3850536094ca36bc31520bb15a6d5a9ef.tar.gz
nixpkgs-9ffd16b3850536094ca36bc31520bb15a6d5a9ef.tar.bz2
nixpkgs-9ffd16b3850536094ca36bc31520bb15a6d5a9ef.tar.lz
nixpkgs-9ffd16b3850536094ca36bc31520bb15a6d5a9ef.tar.xz
nixpkgs-9ffd16b3850536094ca36bc31520bb15a6d5a9ef.tar.zst
nixpkgs-9ffd16b3850536094ca36bc31520bb15a6d5a9ef.zip
coqPackages: refactor
Diffstat (limited to 'pkgs/development/coq-modules/equations')
-rw-r--r--pkgs/development/coq-modules/equations/default.nix113
1 files changed, 41 insertions, 72 deletions
diff --git a/pkgs/development/coq-modules/equations/default.nix b/pkgs/development/coq-modules/equations/default.nix
index 5a07d537536..352222e8aa6 100644
--- a/pkgs/development/coq-modules/equations/default.nix
+++ b/pkgs/development/coq-modules/equations/default.nix
@@ -1,79 +1,48 @@
-{ stdenv, fetchFromGitHub, coq }:
-
-let
-  params = {
-    "8.6" = {
-      version = "1.0";
-      rev = "v1.0";
-      sha256 = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj";
-    };
-
-    "8.7" = {
-      version = "1.0";
-      rev = "v1.0-8.7";
-      sha256 = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h";
-    };
-
-    "8.8" = {
-      version = "1.2";
-      rev = "v1.2-8.8";
-      sha256 = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx";
-    };
-
-    "8.9" = {
-      version = "1.2.1";
-      rev = "v1.2.1-8.9";
-      sha256 = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij";
-    };
-
-    "8.10" = {
-      version = "1.2.1";
-      rev = "v1.2.1-8.10-2";
-      sha256 = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68";
-    };
-
-    "8.11" = {
-      version = "1.2.3";
-      rev = "v1.2.3-8.11";
-      sha256 = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf";
-    };
-
-    "8.12" = {
-      version = "1.2.3";
-      rev = "v1.2.3-8.12";
-      sha256 = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643";
-    };
-  };
-  param = params.${coq.coq-version};
-in
-
-stdenv.mkDerivation rec {
-
-  name = "coq${coq.coq-version}-equations-${version}";
-  version = param.version;
-
-  src = fetchFromGitHub {
-    owner = "mattam82";
-    repo = "Coq-Equations";
-    rev = param.rev;
-    sha256 = param.sha256;
-  };
-
-  buildInputs = with coq.ocamlPackages; [ ocaml camlp5 findlib coq ];
-
+{ lib, mkCoqDerivation, coq, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "equations";
+  owner = "mattam82";
+  repo = "Coq-Equations";
+  inherit version;
+  defaultVersion = switch coq.coq-version [
+    { case = "8.12"; out = "1.2.3+coq8.12"; }
+    { case = "8.11"; out = "1.2.3+coq8.11"; }
+    { case = "8.10"; out = "1.2.1+coq8.10-2"; }
+    { case = "8.9";  out = "1.2.1+coq8.9"; }
+    { case = "8.8";  out = "1.2+coq8.8"; }
+    { case = "8.7";  out = "1.0+coq8.7"; }
+    { case = "8.6";  out = "1.0+coq8.6"; }
+  ] null;
+
+    release."1.0+coq8.6".version      = "1.0";
+    release."1.0+coq8.6".rev          = "v1.0";
+    release."1.0+coq8.6".sha256       = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj";
+    release."1.0+coq8.7".version      = "1.0";
+    release."1.0+coq8.7".rev          = "v1.0-8.7";
+    release."1.0+coq8.7".sha256       = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h";
+    release."1.2+coq8.8".version      = "1.2";
+    release."1.2+coq8.8".rev          = "v1.2-8.8";
+    release."1.2+coq8.8".sha256       = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx";
+    release."1.2.1+coq8.9".version    = "1.2.1";
+    release."1.2.1+coq8.9".rev        = "v1.2.1-8.9";
+    release."1.2.1+coq8.9".sha256     = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij";
+    release."1.2.1+coq8.10-2".version = "1.2.1";
+    release."1.2.1+coq8.10-2".rev     = "v1.2.1-8.10-2";
+    release."1.2.1+coq8.10-2".sha256  = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68";
+    release."1.2.3+coq8.11".version   = "1.2.3";
+    release."1.2.3+coq8.11".rev       = "v1.2.3-8.11";
+    release."1.2.3+coq8.11".sha256    = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf";
+    release."1.2.3+coq8.12".version   = "1.2.3";
+    release."1.2.3+coq8.12".rev       = "v1.2.3-8.12";
+    release."1.2.3+coq8.12".sha256    = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643";
+
+  mlPlugin = true;
   preBuild = "coq_makefile -f _CoqProject -o Makefile";
 
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-
-  meta = with stdenv.lib; {
+  meta = {
     homepage = "https://mattam82.github.io/Coq-Equations/";
     description = "A plugin for Coq to add dependent pattern-matching";
     maintainers = with maintainers; [ jwiegley ];
-    platforms = coq.meta.platforms;
-  };
-
-  passthru = {
-    compatibleCoqVersions = v: builtins.hasAttr v params;
   };
-
 }