pkgs/development/coq-modules/aac-tactics/default.nix

   1 {
   2   lib,
   3   mkCoqDerivation,
   4   coq,
   5   stdlib,
   6   version ? null,
   7 }:
   8
   9 mkCoqDerivation {
  10   pname = "aac-tactics";
  11
  12   releaseRev = v: "v${v}";
  13
  14   release."8.20.0".sha256 = "sha256-VQzeINIZAfP3Qyh29uPqcNVlNJfIzzRLtN0Cm4EuGCk=";
  15   release."8.19.1".sha256 = "sha256-W/V57h+rjb3m0ktCG83PquMHfXiv6H1Nhvw9sVEPLqM=";
  16   release."8.19.0".sha256 = "sha256-IeCBd8gcu4bAXH5I/XIT7neQIILi+EWR6qqAA4GzQD0=";
  17   release."8.18.0".sha256 = "sha256-Vpe79qCyFLOdOtFFvLKR0N+MMpGD661Q01yx4gxRhZo=";
  18   release."8.17.0".sha256 = "sha256-c8DtD21QFDZEVyCQc7ScPZEMTmolxlT3+Db3gStofF8=";
  19   release."8.16.0".sha256 = "sha256-sE1w8q/60adNF9yMJQO70CEk3D8QUopvgiszdHt5Wsw=";
  20   release."8.15.1".sha256 = "sha256:0k2sl3ns897a5ll11bazgpv4ppgi1vmx4n89v2dnxabm5dglyglp";
  21   release."8.14.1".sha256 = "sha256:1w99jgm7mxwdxnalxhralmhmpwwbd52pbbifq0mx13ixkv6iqm1a";
  22   release."8.14.0".sha256 = "04x47ngb95m1h4jw2gl0v79s5im7qimcw7pafc34gkkf51pyhakp";
  23   release."8.13.2".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTa=";
  24   release."8.13.0".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTY=";
  25   release."8.12.0".sha256 = "sha256-dPNA19kZo/2t3rbyX/R5yfGcaEfMhbm9bo71Uo4ZwoM=";
  26   release."8.11.0".sha256 = "sha256-CKKMiJLltIb38u+ZKwfQh/NlxYawkafp+okY34cGCYU=";
  27   release."8.10.0".sha256 = "sha256-Ny3AgfLAzrz3FnoUqejXLApW+krlkHBmYlo3gAG0JsM=";
  28   release."8.9.0".sha256 = "sha256-6Pp0dgYEnVaSnkJR/2Cawt5qaxWDpBI4m0WAbQboeWY=";
  29   release."8.8.0".sha256 = "sha256-mwIKp3kf/6i9IN3cyIWjoRtW8Yf8cc3MV744zzFM3u4=";
  30   release."8.6.1".sha256 = "sha256-PfovQ9xJnzr0eh/tO66yJ3Yp7A5E1SQG46jLIrrbZFg=";
  31   release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
  32
  33   inherit version;
  34   defaultVersion =
  35     with lib.versions;
  36     lib.switch coq.coq-version [
  37       {
  38         case = "8.20";
  39         out = "8.20.0";
  40       }
  41       {
  42         case = "8.19";
  43         out = "8.19.1";
  44       }
  45       {
  46         case = "8.18";
  47         out = "8.18.0";
  48       }
  49       {
  50         case = "8.17";
  51         out = "8.17.0";
  52       }
  53       {
  54         case = "8.16";
  55         out = "8.16.0";
  56       }
  57       {
  58         case = "8.15";
  59         out = "8.15.1";
  60       }
  61       {
  62         case = "8.14";
  63         out = "8.14.1";
  64       }
  65       {
  66         case = "8.13";
  67         out = "8.13.2";
  68       }
  69       {
  70         case = "8.12";
  71         out = "8.12.0";
  72       }
  73       {
  74         case = "8.11";
  75         out = "8.11.0";
  76       }
  77       {
  78         case = "8.10";
  79         out = "8.10.0";
  80       }
  81       {
  82         case = "8.9";
  83         out = "8.9.0";
  84       }
  85       {
  86         case = "8.8";
  87         out = "8.8.0";
  88       }
  89       {
  90         case = "8.6";
  91         out = "8.6.1";
  92       }
  93       {
  94         case = "8.5";
  95         out = "8.5.0";
  96       }
  97     ] null;
  98
  99   mlPlugin = true;
 100
 101   propagatedBuildInputs = [ stdlib ];
 102
 103   meta = with lib; {
 104     description = "Coq plugin providing tactics for rewriting universally quantified equations";
 105     longDescription = ''
 106       This Coq plugin provides tactics for rewriting universally quantified
 107       equations, modulo associativity and commutativity of some operator.
 108       The tactics can be applied for custom operators by registering the
 109       operators and their properties as type class instances. Many common
 110       operator instances, such as for Z binary arithmetic and booleans, are
 111       provided with the plugin.
 112     '';
 113     maintainers = with maintainers; [ siraben ];
 114     license = licenses.gpl3Plus;
 115     platforms = platforms.unix;
 116   };
 117 }