pkgs/development/coq-modules/autosubst/default.nix

   1 {
   2   lib,
   3   mkCoqDerivation,
   4   coq,
   5   mathcomp-ssreflect,
   6   version ? null,
   7 }:
   8
   9 mkCoqDerivation {
  10   pname = "autosubst";
  11
  12   releaseRev = v: "v${v}";
  13
  14   release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI=";
  15   release."1.8".sha256 = "sha256-n0lD8D+tjqkDDjFiE4CggxczOPS5TkEnxpB3zEwWZ2I=";
  16   release."1.9".sha256 = "sha256-XiLZjMc+1iwRGOstfLm/WQRF6FTdX6oJr5urn3wmLlA=";
  17
  18   inherit version;
  19   defaultVersion =
  20     with lib.versions;
  21     lib.switch coq.coq-version [
  22       {
  23         case = range "8.14" "8.20";
  24         out = "1.9";
  25       }
  26       {
  27         case = range "8.14" "8.18";
  28         out = "1.8";
  29       }
  30       {
  31         case = range "8.10" "8.13";
  32         out = "1.7";
  33       }
  34     ] null;
  35
  36   propagatedBuildInputs = [ mathcomp-ssreflect ];
  37
  38   meta = with lib; {
  39     homepage = "https://www.ps.uni-saarland.de/autosubst/";
  40     description = "Automation for de Bruijn syntax and substitution in Coq";
  41     maintainers = with maintainers; [
  42       siraben
  43       jwiegley
  44     ];
  45     license = licenses.mit;
  46   };
  47 }