pkgs/development/coq-modules/mathcomp-abel/default.nix

   1 {
   2   coq,
   3   mkCoqDerivation,
   4   mathcomp,
   5   mathcomp-real-closed,
   6   lib,
   7   version ? null,
   8 }:
   9
  10 mkCoqDerivation {
  11
  12   namePrefix = [
  13     "coq"
  14     "mathcomp"
  15   ];
  16   pname = "abel";
  17   owner = "math-comp";
  18
  19   inherit version;
  20   defaultVersion =
  21     lib.switch
  22       [ coq.version mathcomp.version ]
  23       [
  24         {
  25           cases = [
  26             (lib.versions.range "8.10" "8.16")
  27             (lib.versions.range "1.12.0" "1.15.0")
  28           ];
  29           out = "1.2.1";
  30         }
  31         {
  32           cases = [
  33             (lib.versions.range "8.10" "8.15")
  34             (lib.versions.range "1.12.0" "1.14.0")
  35           ];
  36           out = "1.2.0";
  37         }
  38         {
  39           cases = [
  40             (lib.versions.range "8.10" "8.14")
  41             (lib.versions.range "1.11.0" "1.12.0")
  42           ];
  43           out = "1.1.2";
  44         }
  45       ]
  46       null;
  47
  48   release."1.2.1".sha256 = "sha256-M1q6WIPBsayHde2hwlTxylH169hcTs3OuFsEkM0e3yc=";
  49   release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
  50   release."1.1.2".sha256 = "0565w713z1cwxvvdlqws2z5lgdys8lddf0vpwfdj7bpd7pq9hwxg";
  51   release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
  52
  53   propagatedBuildInputs = [
  54     mathcomp.field
  55     mathcomp-real-closed
  56   ];
  57
  58   meta = with lib; {
  59     description = "Abel - Galois and Abel - Ruffini Theorems";
  60     license = licenses.cecill-b;
  61     maintainers = [ maintainers.cohencyril ];
  62   };
  63 }