Merge pull request #134413 from Zimmi48/package-hydra-battles

doc/languages-frameworks/coq.section.md

@@ -33,6 +33,7 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
 * `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `extraBuildInputs` to depend on the same package set Coq was built against.
 * `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2if = versions.isGe "1.1"`  will use dune if the version of the package is greater or equal to `"1.1"`,
 * `useDune2` (optional, defaults to `false`) uses Dune2 to build the package if set to true, the presence of this attribute overrides the behavior of the previous one.
+* `opam-name` (optional, defaults to `coq-` followed by the value of `pname`), name of the Dune package to build.
 * `enableParallelBuilding` (optional, defaults to `true`), since it is activated by default, we provide a way to disable it.
 * `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variable `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation.
 * `setCOQBIN` (optional, defaults to `true`), by default, the environment variable `$COQBIN` is set to the current Coq's binary, but one can disable this behavior by setting it to `false`,

pkgs/build-support/coq/default.nix

@@ -27,6 +27,7 @@ in
   dropDerivationAttrs ? [],
   useDune2ifVersion ? (x: false),
   useDune2 ? false,
+  opam-name ? "coq-${pname}",
   ...
 }@args:
 let
@@ -34,7 +35,7 @@ let
     "version" "fetcher" "repo" "owner" "domain" "releaseRev"
     "displayVersion" "defaultVersion" "useMelquiondRemake"
     "release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix"
-    "meta" "useDune2ifVersion" "useDune2"
+    "meta" "useDune2ifVersion" "useDune2" "opam-name"
     "extraInstallFlags" "setCOQBIN" "mlPlugin"
     "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
   fetch = import ../coq/meta-fetch/default.nix
@@ -90,9 +91,14 @@ stdenv.mkDerivation (removeAttrs ({
     extraInstallFlags;
 })
 // (optionalAttrs useDune2 {
+  buildPhase = ''
+    runHook preBuild
+    dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
+    runHook postBuild
+  '';
   installPhase = ''
     runHook preInstall
-    dune install --prefix=$out
+    dune install ${opam-name} --prefix=$out
     mv $out/lib/coq $out/lib/TEMPORARY
     mkdir $out/lib/coq/
     mv $out/lib/TEMPORARY $out/lib/coq/${coq.coq-version}

pkgs/development/coq-modules/addition-chains/default.nix

@@ -0,0 +1,33 @@
+{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, paramcoq
+, version ? null }:
+with lib;
+
+mkCoqDerivation {
+  pname = "addition-chains";
+  repo = "hydra-battles";
+
+  release."0.4".sha256 = "sha256:1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch coq.coq-version [
+    { case = isGe "8.11"; out = "0.4"; }
+  ] null;
+
+  propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-algebra paramcoq ];
+
+  useDune2 = true;
+
+  meta = {
+    description = "Exponentiation algorithms following addition chains";
+    longDescription = ''
+      Addition chains are algorithms for computations of the p-th
+      power of some x, with the least number of multiplication as
+      possible. We present a few implementations of addition chains,
+      with proofs of their correctness.
+    '';
+    maintainers = with maintainers; [ Zimmi48 ];
+    license = licenses.mit;
+    platforms = platforms.unix;
+  };
+}

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

@@ -0,0 +1,24 @@
+{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
+
+with lib; mkCoqDerivation {
+  pname = "gaia";
+
+  release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5";
+  release."1.12".sha256 = "sha256:0c6cim4x6f9944g8v0cp0lxs244lrhb04ms4y2s6y1wh321zj5mi";
+  releaseRev = (v: "v${v}");
+
+  inherit version;
+  defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
+    { cases = [ (range "8.10" "8.13") "1.12.0" ]; out = "1.12"; }
+    { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; }
+  ] null;
+
+  propagatedBuildInputs =
+    [ mathcomp.ssreflect mathcomp.algebra ];
+
+  meta = {
+    description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq";
+    maintainers = with maintainers; [ Zimmi48 ];
+    license = licenses.mit;
+  };
+}

pkgs/development/coq-modules/hydra-battles/default.nix

@@ -1,28 +1,32 @@
-{ lib, mkCoqDerivation, coq, mathcomp, equations, paramcoq, version ? null }:
+{ lib, mkCoqDerivation, coq, equations, version ? null }:
 with lib;
 
 mkCoqDerivation {
   pname = "hydra-battles";
   owner = "coq-community";
 
-  release."0.3".rev    = "v0.3";
-  release."0.3".sha256 = "sha256-rXP/vJqVEg2tN/I9LWV13YQ1+C7M6lzGu3oI+7pSZzg=";
+  release."0.4".sha256 = "sha256:1f7pc4w3kir4c9p0fjx5l77401bx12y72nmqxrqs3qqd3iynvqlp";
+  releaseRev = (v: "v${v}");
 
   inherit version;
   defaultVersion = with versions; switch coq.coq-version [
-    { case = isGe "8.11"; out = "0.3"; }
+    { case = isGe "8.11"; out = "0.4"; }
   ] null;
 
-  propagatedBuildInputs = [ mathcomp equations paramcoq ];
+  propagatedBuildInputs = [ equations ];
+
+  useDune2 = true;
 
   meta = {
-    description = "Variations on Kirby & Paris' hydra battles and other entertaining math in Coq";
+    description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
     longDescription = ''
-       Variations on Kirby & Paris' hydra battles and other
-       entertaining math in Coq (collaborative, documented, includes
-       exercises)
+      An exploration of some properties of Kirby and Paris' hydra
+      battles, with the help of the Coq Proof assistant. This
+      development includes the study of several representations of
+      ordinal numbers, and a part of the so-called Ketonen and Solovay
+      machinery (combinatorial properties of epsilon0).
     '';
-    maintainers = with maintainers; [ siraben ];
+    maintainers = with maintainers; [ siraben Zimmi48 ];
     license = licenses.mit;
     platforms = platforms.unix;
   };

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

@@ -4,7 +4,10 @@ with lib; mkCoqDerivation {
 
   namePrefix = [ "coq" "mathcomp" ];
   pname = "multinomials";
+  opam-name = "coq-mathcomp-multinomials";
+
   owner = "math-comp";
+
   inherit version;
   defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
       { cases = [ (range "8.10" "8.13") "1.12.0" ];             out = "1.5.4"; }

pkgs/top-level/coq-packages.nix

@@ -14,6 +14,7 @@ let
         (callPackage ../development/coq-modules/contribs {});
 
       aac-tactics = callPackage ../development/coq-modules/aac-tactics {};
+      addition-chains = callPackage ../development/coq-modules/addition-chains {};
       autosubst = callPackage ../development/coq-modules/autosubst {};
       bignums = if lib.versionAtLeast coq.coq-version "8.6"
         then callPackage ../development/coq-modules/bignums {}
@@ -40,6 +41,7 @@ let
       fiat_HEAD = callPackage ../development/coq-modules/fiat/HEAD.nix {};
       flocq = callPackage ../development/coq-modules/flocq {};
       fourcolor = callPackage ../development/coq-modules/fourcolor {};
+      gaia = callPackage ../development/coq-modules/gaia {};
       gappalib = callPackage ../development/coq-modules/gappalib {};
       goedel = callPackage ../development/coq-modules/goedel {};
       graph-theory = callPackage ../development/coq-modules/graph-theory {};