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

   1 { lib, fetchzip,
   2   mkCoqDerivation, recurseIntoAttrs,  single ? false,
   3   coqPackages, coq, equations, version ? null }@args:
   4 with builtins // lib;
   5 let
   6   repo  = "metacoq";
   7   owner = "MetaCoq";
   8   defaultVersion = with versions; switch coq.coq-version [
   9       { case = "8.11"; out = "1.0-beta2-8.11"; }
  10       { case = "8.12"; out = "1.0-beta2-8.12"; }
  11       # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
  12       # { case = "8.13"; out = "1.0-beta2-8.13"; }
  13       { case = "8.14"; out = "1.1-8.14"; }
  14       { case = "8.15"; out = "1.1-8.15"; }
  15       { case = "8.16"; out = "1.1-8.16"; }
  16       { case = "8.17"; out = "1.3.1-8.17"; }
  17       { case = "8.18"; out = "1.3.1-8.18"; }
  18       { case = "8.19"; out = "1.3.1-8.19"; }
  19     ] null;
  20   release = {
  21     "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
  22     "1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
  23     "1.0-beta2-8.13".sha256 = "sha256-IC56/lEDaAylUbMCfG/3cqOBZniEQk8jmI053DBO5l8=";
  24     "1.0-8.14".sha256 = "sha256-iRnaNeHt22JqxMNxOGPPycrO9EoCVjusR2s0GfON1y0=";
  25     "1.0-8.15".sha256 = "sha256-8RUC5dHNfLJtJh+IZG4nPTAVC8ZKVh2BHedkzjwLf/k=";
  26     "1.0-8.16".sha256 = "sha256-7rkCAN4PNnMgsgUiiLe2TnAliknN75s2SfjzyKCib/o=";
  27     "1.1-8.14".sha256 = "sha256-6vViCNQl6BnGgOHX3P/OLfFXN4aUfv4RbDokfz2BgQI=";
  28     "1.1-8.15".sha256 = "sha256-qCD3wFW4E+8vSVk4XoZ0EU4PVya0al+JorzS9nzmR/0=";
  29     "1.1-8.16".sha256 = "sha256-cTK4ptxpPPlqxAhasZFX3RpSlsoTZwhTqs2A3BZy9sA=";
  30     "1.2.1-8.17".sha256 = "sha256-FP4upuRsG8B5Q5FIr76t+ecRirrOUX0D1QiLq0/zMyE=";
  31     "1.2.1-8.18".sha256 = "sha256-49g5db2Bv8HpltptJdxA7zrmgNFGC6arx5h2mKHhrko=";
  32     "1.3.1-8.17".sha256 = "sha256-l0/QLC7V3zSk/FsaE2eL6tXy2BzbcI5MAk/c+FESwnc=";
  33     "1.3.1-8.18".sha256 = "sha256-L6Ym4Auwqaxv5tRmJLSVC812dxCqdUU5aN8+t5HVYzY=";
  34     "1.3.1-8.19".sha256 = "sha256-fZED/Uel1jt5XF83dR6HfyhSkfBdLkET8C/ArDgsm64=";
  35   };
  36   releaseRev = v: "v${v}";
  37
  38   # list of core metacoq packages sorted by dependency order
  39   packages = if versionAtLeast coq.coq-version "8.17"
  40      then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]
  41      else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
  42
  43   template-coq = metacoq_ "template-coq";
  44
  45   metacoq_ = package: let
  46       metacoq-deps = lib.optionals (package != "single") (map metacoq_ (head (splitList (lib.pred.equal package) packages)));
  47       pkgpath = if package == "single" then "./" else "./${package}";
  48       pname = if package == "all" then "metacoq" else "metacoq-${package}";
  49       pkgallMake = ''
  50           mkdir all
  51           echo "all:" > all/Makefile
  52           echo "install:" >> all/Makefile
  53         '' ;
  54       derivation = (mkCoqDerivation ({
  55         inherit version pname defaultVersion release releaseRev repo owner;
  56
  57         mlPlugin = true;
  58         propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
  59
  60         patchPhase =  if versionAtLeast coq.coq-version "8.17" then ''
  61           patchShebangs ./configure.sh
  62           patchShebangs ./template-coq/update_plugin.sh
  63           patchShebangs ./template-coq/gen-src/to-lower.sh
  64           patchShebangs ./safechecker-plugin/clean_extraction.sh
  65           patchShebangs ./erasure-plugin/clean_extraction.sh
  66           echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
  67           sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./safechecker-plugin/clean_extraction.sh ./erasure-plugin/clean_extraction.sh
  68         '' else ''
  69           patchShebangs ./configure.sh
  70           patchShebangs ./template-coq/update_plugin.sh
  71           patchShebangs ./template-coq/gen-src/to-lower.sh
  72           patchShebangs ./pcuic/clean_extraction.sh
  73           patchShebangs ./safechecker/clean_extraction.sh
  74           patchShebangs ./erasure/clean_extraction.sh
  75           echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
  76           sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh
  77         '' ;
  78
  79         configurePhase = optionalString (package == "all") pkgallMake + ''
  80           touch ${pkgpath}/metacoq-config
  81         '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) ''
  82           echo  "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
  83         '' + optionalString (package == "single") ''
  84           ./configure.sh local
  85         '';
  86
  87         preBuild = ''
  88           cd ${pkgpath}
  89         '' ;
  90
  91         meta = {
  92           homepage    = "https://metacoq.github.io/";
  93           license     = licenses.mit;
  94           maintainers = with maintainers; [ cohencyril ];
  95         };
  96       } // optionalAttrs (package != "single")
  97         { passthru = genAttrs packages metacoq_; })
  98       ).overrideAttrs (o:
  99         let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" ||
 100                                        (o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ;
 101         in
 102           {
 103             propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
 104           });
 105   in derivation;
 106 in
 107 metacoq_ (if single then "single" else "all")