coqPackages: Enable override with dev branches (#329356)

Useful for CI applications.

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

@@ -1,6 +1,6 @@
 { lib, mkCoqDerivation, coq, ssreflect, coq-ext-lib, simple-io, version ? null }:
 
-let recent = lib.versions.isGe "8.7" coq.coq-version; in
+let recent = lib.versions.isGe "8.7" coq.coq-version || coq.coq-version == "dev"; in
 (mkCoqDerivation {
   pname = "QuickChick";
   owner = "QuickChick";
@@ -40,6 +40,9 @@ let recent = lib.versions.isGe "8.7" coq.coq-version; in
   preConfigure = lib.optionalString recent
     "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
 
+  useDuneifVersion = v: lib.versions.isGe "2.1" v || v == "dev";
+  opam-name = "coq-quickchick";
+
   mlPlugin = true;
   nativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
   propagatedBuildInputs = [ ssreflect ]
@@ -54,9 +57,11 @@ let recent = lib.versions.isGe "8.7" coq.coq-version; in
   };
 }).overrideAttrs (o:
   let after_1_6 = lib.versions.isGe "1.6" o.version || o.version == "dev";
+      after_2_1 = lib.versions.isGe "2.1" o.version || o.version == "dev";
   in {
     nativeBuildInputs = o.nativeBuildInputs
-    ++ lib.optional after_1_6 coq.ocamlPackages.cppo;
+    ++ lib.optional after_1_6 coq.ocamlPackages.cppo
+    ++ lib.optional after_2_1 coq.ocamlPackages.menhir;
     propagatedBuildInputs = o.propagatedBuildInputs
     ++ lib.optionals after_1_6 (with coq.ocamlPackages; [ findlib zarith ]);
 })

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

@@ -66,8 +66,8 @@ compcert = mkCoqDerivation {
     -coqdevdir $lib/lib/coq/${coq.coq-version}/user-contrib/compcert/ \
     -toolprefix ${tools}/bin/ \
     -use-external-Flocq \
-    ${target}
-  '';
+    ${target} \
+  '';  # don't remove the \ above, the command gets appended in override below
 
   installTargets = "documentation install";
   installFlags = []; # trust ./configure
@@ -100,8 +100,8 @@ compcert = mkCoqDerivation {
     platforms   = builtins.attrNames targets;
     maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ];
   };
-}; in
-compcert.overrideAttrs (o:
+};
+patched_compcert = compcert.overrideAttrs (o:
   {
     patches = with lib.versions; lib.switch [ coq.version o.version ] [
       { cases = [ (range "8.12.2" "8.13.2") "3.8" ];
@@ -210,5 +210,8 @@ compcert.overrideAttrs (o:
         ];
       }
     ] [];
-  }
+  }); in
+patched_compcert.overrideAttrs (o:
+  lib.optionalAttrs (coq.version != null && coq.version == "dev")
+  { configurePhase = "${o.configurePhase} -ignore-ocaml-version -ignore-coq-version"; }
 )

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

@@ -1,6 +1,6 @@
 { lib, mkCoqDerivation, coq, serapi, makeWrapper, version ? null }:
 
-mkCoqDerivation rec {
+(mkCoqDerivation rec {
   pname = "coq-lsp";
   owner = "ejgallego";
   namePrefix = [ ];
@@ -24,13 +24,13 @@ mkCoqDerivation rec {
 
   installPhase = ''
     runHook preInstall
-    dune install ${pname} --prefix=$out
+    dune install -p ${pname} --prefix=$out --libdir $OCAMLFIND_DESTDIR
     wrapProgram $out/bin/coq-lsp --prefix OCAMLPATH : $OCAMLPATH
     runHook postInstall
   '';
 
-  propagatedBuildInputs = [ serapi ]
-    ++ (with coq.ocamlPackages; [ camlp-streams dune-build-info menhir uri yojson ]);
+  propagatedBuildInputs =
+    with coq.ocamlPackages; [ dune-build-info menhir uri yojson ];
 
   meta = with lib; {
     description = "Language Server Protocol and VS Code Extension for Coq";
@@ -39,4 +39,12 @@ mkCoqDerivation rec {
     maintainers = with maintainers; [ alizter ];
     license = licenses.lgpl21Only;
   };
-}
+}).overrideAttrs (o:
+  with coq.ocamlPackages;
+  { propagatedBuildInputs = o.propagatedBuildInputs ++
+    (if o.version != null && lib.versions.isLe "0.1.9+8.19" o.version && o.version != "dev" then
+     [ camlp-streams serapi ]
+    else
+     [ cmdliner ppx_deriving ppx_deriving_yojson ppx_import ppx_sexp_conv
+       ppx_compare ppx_hash sexplib ]);
+})

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

@@ -3,9 +3,12 @@
 let
   namePrefix = [ "coq" "mathcomp" ];
   pname = "word";
-  fetcher = { domain, owner, repo, rev, sha256, ...}:
+  fetcher = { domain, owner, repo, rev, sha256 ? null, ...}:
+    let prefix = "https://${domain}/${owner}/${repo}/"; in
+    if sha256 == null then
+      fetchTarball { url = "${prefix}archive/refs/heads/${rev}.tar.gz"; } else
   fetchurl {
-    url = "https://${domain}/${owner}/${repo}/releases/download/${rev}/${lib.concatStringsSep "-" (namePrefix ++ [ pname ])}-${rev}.tbz";
+    url = "${prefix}releases/download/${rev}/${lib.concatStringsSep "-" (namePrefix ++ [ pname ])}-${rev}.tbz";
     inherit sha256;
   };
 in

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

@@ -36,7 +36,7 @@ let
   releaseRev = v: "v${v}";
 
   # list of core metacoq packages sorted by dependency order
-  packages = if lib.versionAtLeast coq.coq-version "8.17"
+  packages = if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev"
      then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]
      else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
 
@@ -57,7 +57,7 @@ let
         mlPlugin = true;
         propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
 
-        patchPhase =  if lib.versionAtLeast coq.coq-version "8.17" then ''
+        patchPhase = if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev" then ''
           patchShebangs ./configure.sh
           patchShebangs ./template-coq/update_plugin.sh
           patchShebangs ./template-coq/gen-src/to-lower.sh

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

@@ -1,4 +1,4 @@
-{ lib, fetchzip, mkCoqDerivation, coq, version ? null }:
+{ lib, fetchzip, mkCoqDerivation, coq, coq-lsp, version ? null }:
 
 let
   release = {
@@ -17,6 +17,7 @@ in
 
 (with lib; mkCoqDerivation {
   pname = "serapi";
+  repo = "coq-serapi";
   inherit version release;
 
   defaultVersion =  with versions;
@@ -35,20 +36,15 @@ in
 
   useDune = true;
 
-  patches = [ ./janestreet-0.15.patch ];
-
   propagatedBuildInputs =
     with coq.ocamlPackages; [
       cmdliner
       findlib # run time dependency of SerAPI
       ppx_deriving
-      ppx_deriving_yojson
       ppx_import
       ppx_sexp_conv
       ppx_hash
       sexplib
-      yojson
-      zarith # needed because of Coq
     ];
 
   installPhase = ''
@@ -64,6 +60,7 @@ in
     maintainers = with maintainers; [ alizter Zimmi48 ];
   };
 }).overrideAttrs(o:
+if lib.versions.isLe "8.19.0+0.19.3" o.version && o.version != "dev" then
   let inherit (o) version; in {
   src = fetchzip {
     url =
@@ -98,8 +95,9 @@ in
     else [
     ];
 
-    propagatedBuildInputs = o.propagatedBuildInputs ++
-      lib.optional (version == "8.16.0+0.16.3" || version == "dev") coq.ocamlPackages.ppx_hash
-    ;
-
-})
+    propagatedBuildInputs = o.propagatedBuildInputs
+      ++ (with coq.ocamlPackages; [ ppx_deriving_yojson yojson zarith ])  # zarith needed because of Coq
+    ; }
+else
+  { propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq-lsp ]; }
+)

pkgs/development/coq-modules/simple-io/default.nix

@@ -20,6 +20,10 @@
   doCheck = true;
   checkTarget = "test";
 
+  useDuneifVersion = v:
+    (lib.versionAtLeast v "1.8.0" || v == "dev")
+    && (lib.versionAtLeast coq.version "8.20" || coq.version == "dev");
+
   passthru.tests.HelloWorld = callPackage ./test.nix {};
 
   meta = with lib; {
@@ -29,5 +33,4 @@
   };
 }).overrideAttrs (o: lib.optionalAttrs (lib.versionAtLeast o.version "1.8.0" || o.version == "dev") {
   doCheck = false;
-  useDune = true;
 })

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

@@ -23,7 +23,7 @@
     maintainers = [ maintainers.vbgl ];
   };
 }).overrideAttrs (x:
-  lib.optionalAttrs (lib.versionOlder x.version "20210316") {
+  lib.optionalAttrs (lib.versionOlder x.version "20210316" && x.version != "dev") {
     installFlags = [ "CONTRIB=$(out)/lib/coq/${coq.coq-version}/user-contrib" ];
   }
 )