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

   1 { lib, mkCoqDerivation, coq, version ? null }:
   2
   3 mkCoqDerivation {
   4   pname = "aac-tactics";
   5
   6   releaseRev = v: "v${v}";
   7
   8   release."8.18.0".sha256 = "sha256-Vpe79qCyFLOdOtFFvLKR0N+MMpGD661Q01yx4gxRhZo=";
   9   release."8.17.0".sha256 = "sha256-c8DtD21QFDZEVyCQc7ScPZEMTmolxlT3+Db3gStofF8=";
  10   release."8.16.0".sha256 = "sha256-sE1w8q/60adNF9yMJQO70CEk3D8QUopvgiszdHt5Wsw=";
  11   release."8.15.1".sha256 = "sha256:0k2sl3ns897a5ll11bazgpv4ppgi1vmx4n89v2dnxabm5dglyglp";
  12   release."8.14.1".sha256 = "sha256:1w99jgm7mxwdxnalxhralmhmpwwbd52pbbifq0mx13ixkv6iqm1a";
  13   release."8.14.0".sha256 = "04x47ngb95m1h4jw2gl0v79s5im7qimcw7pafc34gkkf51pyhakp";
  14   release."8.13.2".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTa=";
  15   release."8.13.0".sha256 = "sha256-MAnMc4KzC551JInrRcfKED4nz04FO0GyyyuDVRmnYTY=";
  16   release."8.12.0".sha256 = "sha256-dPNA19kZo/2t3rbyX/R5yfGcaEfMhbm9bo71Uo4ZwoM=";
  17   release."8.11.0".sha256 = "sha256-CKKMiJLltIb38u+ZKwfQh/NlxYawkafp+okY34cGCYU=";
  18   release."8.10.0".sha256 = "sha256-Ny3AgfLAzrz3FnoUqejXLApW+krlkHBmYlo3gAG0JsM=";
  19   release."8.9.0".sha256 = "sha256-6Pp0dgYEnVaSnkJR/2Cawt5qaxWDpBI4m0WAbQboeWY=";
  20   release."8.8.0".sha256 = "sha256-mwIKp3kf/6i9IN3cyIWjoRtW8Yf8cc3MV744zzFM3u4=";
  21   release."8.6.1".sha256 = "sha256-PfovQ9xJnzr0eh/tO66yJ3Yp7A5E1SQG46jLIrrbZFg=";
  22   release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
  23
  24   inherit version;
  25   defaultVersion = with lib.versions; lib.switch coq.coq-version [
  26     { case = "8.18"; out = "8.18.0"; }
  27     { case = "8.17"; out = "8.17.0"; }
  28     { case = "8.16"; out = "8.16.0"; }
  29     { case = "8.15"; out = "8.15.1"; }
  30     { case = "8.14"; out = "8.14.1"; }
  31     { case = "8.13"; out = "8.13.2"; }
  32     { case = "8.12"; out = "8.12.0"; }
  33     { case = "8.11"; out = "8.11.0"; }
  34     { case = "8.10"; out = "8.10.0"; }
  35     { case = "8.9"; out = "8.9.0"; }
  36     { case = "8.8"; out = "8.8.0"; }
  37     { case = "8.6"; out = "8.6.1"; }
  38     { case = "8.5"; out = "8.5.0"; }
  39   ] null;
  40
  41   mlPlugin = true;
  42
  43   meta = with lib; {
  44     description = "Coq plugin providing tactics for rewriting universally quantified equations";
  45     longDescription = ''
  46       This Coq plugin provides tactics for rewriting universally quantified
  47       equations, modulo associativity and commutativity of some operator.
  48       The tactics can be applied for custom operators by registering the
  49       operators and their properties as type class instances. Many common
  50       operator instances, such as for Z binary arithmetic and booleans, are
  51       provided with the plugin.
  52     '';
  53     maintainers = with maintainers; [ siraben ];
  54     license = licenses.gpl3Plus;
  55     platforms = platforms.unix;
  56   };
  57 }