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

   1 ############################################################################
   2 # This file mainly provides the `mathcomp` derivation, which is            #
   3 # essentially a meta-package containing all core mathcomp libraries        #
   4 # (ssreflect fingroup algebra solvable field character). They can be       #
   5 # accessed individually through the passthrough attributes of mathcomp     #
   6 # bearing the same names (mathcomp.ssreflect, etc).                        #
   7 ############################################################################
   8 # Compiling a custom version of mathcomp using `mathcomp.override`.        #
   9 # This is the replacement for the former `mathcomp_ config` function.      #
  10 # See the documentation at doc/languages-frameworks/coq.section.md.        #
  11 ############################################################################
  12
  13 { lib, ncurses, graphviz, lua, fetchzip,
  14   mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false,
  15   coqPackages, coq, hierarchy-builder, version ? null }@args:
  16 with builtins // lib;
  17 let
  18   repo  = "math-comp";
  19   owner = "math-comp";
  20   withDoc = single && (args.withDoc or false);
  21   defaultVersion = with versions; lib.switch coq.coq-version [
  22       { case = range "8.19" "8.19"; out = "1.19.0"; }
  23       { case = range "8.17" "8.18"; out = "1.18.0"; }
  24       { case = range "8.15" "8.18"; out = "1.17.0"; }
  25       { case = range "8.16" "8.19"; out = "2.2.0"; }
  26       { case = range "8.16" "8.18"; out = "2.1.0"; }
  27       { case = range "8.16" "8.18"; out = "2.0.0"; }
  28       { case = range "8.13" "8.18"; out = "1.16.0"; }
  29       { case = range "8.14" "8.16"; out = "1.15.0"; }
  30       { case = range "8.11" "8.15"; out = "1.14.0"; }
  31       { case = range "8.11" "8.15"; out = "1.13.0"; }
  32       { case = range "8.10" "8.13"; out = "1.12.0"; }
  33       { case = range "8.7"  "8.12"; out = "1.11.0"; }
  34       { case = range "8.7" "8.11";  out = "1.10.0"; }
  35       { case = range "8.7" "8.11";  out = "1.9.0";  }
  36       { case = range "8.7" "8.9";   out = "1.8.0";  }
  37       { case = range "8.6" "8.9";   out = "1.7.0";  }
  38       { case = range "8.5" "8.7";   out = "1.6.4";  }
  39     ] null;
  40   release = {
  41     "2.2.0".sha256  = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
  42     "2.1.0".sha256  = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
  43     "2.0.0".sha256  = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
  44     "1.19.0".sha256 = "sha256-3kxS3qA+7WwQkXoFC/+kq3OEkv4kMEzQ/G3aXPsp1Q4=";
  45     "1.18.0".sha256 = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
  46     "1.17.0".sha256 = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
  47     "1.16.0".sha256 = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
  48     "1.15.0".sha256 = "1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
  49     "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
  50     "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
  51     "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
  52     "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
  53     "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
  54     "1.9.0".sha256  = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
  55     "1.8.0".sha256  = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
  56     "1.7.0".sha256  = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
  57     "1.6.4".sha256  = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
  58     "1.6.1".sha256  = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
  59   };
  60   releaseRev = v: "mathcomp-${v}";
  61
  62   # list of core mathcomp packages sorted by dependency order
  63   packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
  64
  65   mathcomp_ = package: let
  66       mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages)));
  67       pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
  68       pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
  69       pkgallMake = ''
  70         echo "all.v"  > Make
  71         echo "-I ." >>   Make
  72         echo "-R . mathcomp.all" >> Make
  73       '';
  74       derivation = mkCoqDerivation ({
  75         inherit version pname defaultVersion release releaseRev repo owner;
  76
  77         mlPlugin = versions.isLe "8.6" coq.coq-version;
  78         nativeBuildInputs = optionals withDoc [ graphviz lua ];
  79         buildInputs = [ ncurses ];
  80         propagatedBuildInputs = mathcomp-deps;
  81
  82         buildFlags = optional withDoc "doc";
  83
  84         preBuild = ''
  85           if [[ -f etc/utils/ssrcoqdep ]]
  86           then patchShebangs etc/utils/ssrcoqdep
  87           fi
  88           if [[ -f etc/buildlibgraph ]]
  89           then patchShebangs etc/buildlibgraph
  90           fi
  91         '' + ''
  92           cd ${pkgpath}
  93         '' + optionalString (package == "all") pkgallMake;
  94
  95         meta = {
  96           homepage    = "https://math-comp.github.io/";
  97           license     = licenses.cecill-b;
  98           maintainers = with maintainers; [ vbgl jwiegley cohencyril ];
  99         };
 100       } // optionalAttrs (package != "single")
 101         { passthru = genAttrs packages mathcomp_; }
 102         // optionalAttrs withDoc {
 103             htmldoc_template =
 104               fetchzip {
 105                 url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
 106                 sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
 107               };
 108             postBuild = ''
 109               cp -rf _build_doc/* .
 110               rm -r _build_doc
 111             '';
 112             postInstall =
 113               let tgt = "$out/share/coq/${coq.coq-version}/"; in
 114               optionalString withDoc ''
 115               mkdir -p ${tgt}
 116               cp -r htmldoc ${tgt}
 117               cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
 118             '';
 119             buildTargets = "doc";
 120             extraInstallFlags = [ "-f Makefile.coq" ];
 121           });
 122     patched-derivation1 = derivation.overrideAttrs (o:
 123       optionalAttrs (o.pname != null && o.pname == "mathcomp-all" &&
 124          o.version != null && o.version != "dev" && versions.isLt "1.7" o.version)
 125       { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; }
 126     );
 127     patched-derivation2 = patched-derivation1.overrideAttrs (o:
 128       optionalAttrs (versions.isLe "8.7" coq.coq-version ||
 129             (o.version != "dev" && versions.isLe "1.7" o.version))
 130       {
 131         installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
 132       }
 133     );
 134     patched-derivation = patched-derivation2.overrideAttrs (o:
 135       optionalAttrs (o.version != null
 136         && (o.version == "dev" || versions.isGe "2.0.0" o.version))
 137       {
 138         propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
 139       }
 140     );
 141     in patched-derivation;
 142 in
 143 mathcomp_ (if single then "single" else "all")