coqPackages: add coqWithPackages/coqWithPackages' functions

doc/languages-frameworks/coq.section.md

@@ -10,6 +10,25 @@ The Coq derivation is overridable through the `coq.override overrides`, where ov
 
 The associated package set can be obtained using `mkCoqPackages coq`, where `coq` is the derivation to use.
 
+## Creating custom Coq environments with `coq.withPackages` {#coq-withPackages}
+
+The `coq.withPackages` function provides a convenient way to create a Coq environment that includes additional Coq packages. This is similar to how `python.withPackages` works for Python environments.
+
+The function takes a function that receives the Coq package set and returns a list of packages. It returns a wrapped Coq environment where all Coq binaries (`coqtop`, `coqc`, `coqdep`, `coqchk`, `coqide`, etc.) are configured with the appropriate environment variables to find the packages.
+
+### Usage {#coq-withPackages-usage}
+
+Here is an example of creating a Coq environment with specific packages.
+
+```nix
+coq.withPackages (
+  ps: with ps; [
+    mathcomp
+    bignums
+  ]
+)
+```
+
 ## Coq packages attribute sets: `coqPackages` {#coq-packages-attribute-sets-coqpackages}
 
 The recommended way of defining a derivation for a Coq library, is to use the `coqPackages.mkCoqDerivation` function, which is essentially a specialization of `mkDerivation` taking into account most of the specifics of Coq libraries. The following attributes are supported:

doc/redirects.json

@@ -20,6 +20,12 @@
   "cmake-ctest-variables": [
     "index.html#cmake-ctest-variables"
   ],
+  "coq-withPackages": [
+    "index.html#coq-withPackages"
+  ],
+  "coq-withPackages-usage": [
+    "index.html#coq-withPackages-usage"
+  ],
   "cuda": [
     "index.html#cuda"
   ],

pkgs/applications/science/logic/coq/default.nix

@@ -320,7 +320,7 @@ let
         Zimmi48
       ];
       platforms = lib.platforms.unix;
-      mainProgram = "coqide";
+      mainProgram = if buildIde then "coqide" else "coqtop";
     };
   };
 in

pkgs/applications/science/logic/coq/with-packages.nix

@@ -0,0 +1,63 @@
+{
+  buildEnv,
+  coq,
+  lib,
+  makeBinaryWrapper,
+  runCommand,
+}:
+
+packages:
+
+let
+  # At version 9.0, Coq underwent a name change to Rocq.
+  # A couple paths and environment variables need to change at this point.
+  isRocq = lib.versionAtLeast coq.coq-version "9.0";
+
+  collectPropagated =
+    pkg:
+    [ pkg ]
+    ++ (pkg.propagatedBuildInputs or [ ])
+    ++ (lib.concatMap collectPropagated (pkg.propagatedBuildInputs or [ ]));
+
+  allPackages = lib.unique (lib.concatMap collectPropagated packages);
+
+  coqPath = lib.makeSearchPath "/lib/coq/${coq.coq-version}/user-contrib" allPackages;
+
+  ocamlPath = lib.makeSearchPath "/lib/ocaml/${coq.ocaml.version}/site-lib" (
+    [ coq.ocamlPackages.findlib ] ++ allPackages
+  );
+
+  pathEnvVar = if isRocq then "ROCQPATH" else "COQPATH";
+in
+
+buildEnv {
+  name = "${coq.pname}-with-packages-${coq.version}";
+
+  paths = [ coq ] ++ allPackages;
+
+  nativeBuildInputs = [ makeBinaryWrapper ];
+
+  postBuild = ''
+    mkdir -p $out/bin
+
+    # If coq is the only path that has a bin dir, buildEnv may decide to
+    # symlink $out/bin directly to that. So we do this step to make sure we get a
+    # writable bin dir
+    mv $out/bin $out/bin-orig
+
+    for binary in $out/bin-orig/*; do
+      if [ -f "$binary" ] && [ -x "$binary" ]; then
+        makeWrapper "$binary" "$out/bin/$(basename "$binary")" \
+          --prefix ${pathEnvVar} : "${coqPath}" \
+          --prefix OCAMLPATH : "${ocamlPath}"
+      fi
+    done
+  '';
+
+  passthru = coq.passthru // {
+    unwrapped = coq;
+    packages = allPackages;
+  };
+
+  meta = coq.meta;
+}

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

@@ -35,7 +35,8 @@ let
     '';
     installPhase = ''
       echo installing nothing
-      touch $out
+      # Make an output directory rather than a file, so this is more friendly to buildEnv
+      mkdir $out
     '';
 
     meta = {

pkgs/top-level/coq-packages.nix

@@ -24,12 +24,12 @@ let
     self: coq:
     let
       callPackage = self.callPackage;
-    in
-    {
-      inherit coq lib;
       coqPackages = self // {
         recurseForDerivations = false;
       };
+    in
+    {
+      inherit coqPackages lib;
 
       metaFetch = import ../build-support/coq/meta-fetch/default.nix {
         inherit
@@ -41,6 +41,17 @@ let
       };
       mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq { });
 
+      coq = coq.overrideAttrs (oldAttrs: {
+        passthru = (oldAttrs.passthru or { }) // {
+          withPackages =
+            f:
+            (callPackage ../applications/science/logic/coq/with-packages.nix {
+              inherit coq;
+            })
+              (f self);
+        };
+      });
+
       contribs = lib.recurseIntoAttrs (callPackage ../development/coq-modules/contribs { });
 
       aac-tactics = callPackage ../development/coq-modules/aac-tactics { };
@@ -302,39 +313,39 @@ rec {
     in
     self.filterPackages (!coq.dontFilter or false);
 
-  coq_8_7 = mkCoq "8.7" { };
-  coq_8_8 = mkCoq "8.8" { };
-  coq_8_9 = mkCoq "8.9" { };
-  coq_8_10 = mkCoq "8.10" { };
-  coq_8_11 = mkCoq "8.11" { };
-  coq_8_12 = mkCoq "8.12" { };
-  coq_8_13 = mkCoq "8.13" { };
-  coq_8_14 = mkCoq "8.14" { };
-  coq_8_15 = mkCoq "8.15" { };
-  coq_8_16 = mkCoq "8.16" { };
-  coq_8_17 = mkCoq "8.17" { };
-  coq_8_18 = mkCoq "8.18" { };
-  coq_8_19 = mkCoq "8.19" { };
-  coq_8_20 = mkCoq "8.20" { };
-  coq_9_0 = mkCoq "9.0" rocqPackages_9_0;
-  coq_9_1 = mkCoq "9.1" rocqPackages_9_1;
+  coqPackages_8_7 = mkCoqPackages (mkCoq "8.7" { });
+  coqPackages_8_8 = mkCoqPackages (mkCoq "8.8" { });
+  coqPackages_8_9 = mkCoqPackages (mkCoq "8.9" { });
+  coqPackages_8_10 = mkCoqPackages (mkCoq "8.10" { });
+  coqPackages_8_11 = mkCoqPackages (mkCoq "8.11" { });
+  coqPackages_8_12 = mkCoqPackages (mkCoq "8.12" { });
+  coqPackages_8_13 = mkCoqPackages (mkCoq "8.13" { });
+  coqPackages_8_14 = mkCoqPackages (mkCoq "8.14" { });
+  coqPackages_8_15 = mkCoqPackages (mkCoq "8.15" { });
+  coqPackages_8_16 = mkCoqPackages (mkCoq "8.16" { });
+  coqPackages_8_17 = mkCoqPackages (mkCoq "8.17" { });
+  coqPackages_8_18 = mkCoqPackages (mkCoq "8.18" { });
+  coqPackages_8_19 = mkCoqPackages (mkCoq "8.19" { });
+  coqPackages_8_20 = mkCoqPackages (mkCoq "8.20" { });
+  coqPackages_9_0 = mkCoqPackages (mkCoq "9.0" rocqPackages_9_0);
+  coqPackages_9_1 = mkCoqPackages (mkCoq "9.1" rocqPackages_9_1);
 
-  coqPackages_8_7 = mkCoqPackages coq_8_7;
-  coqPackages_8_8 = mkCoqPackages coq_8_8;
-  coqPackages_8_9 = mkCoqPackages coq_8_9;
-  coqPackages_8_10 = mkCoqPackages coq_8_10;
-  coqPackages_8_11 = mkCoqPackages coq_8_11;
-  coqPackages_8_12 = mkCoqPackages coq_8_12;
-  coqPackages_8_13 = mkCoqPackages coq_8_13;
-  coqPackages_8_14 = mkCoqPackages coq_8_14;
-  coqPackages_8_15 = mkCoqPackages coq_8_15;
-  coqPackages_8_16 = mkCoqPackages coq_8_16;
-  coqPackages_8_17 = mkCoqPackages coq_8_17;
-  coqPackages_8_18 = mkCoqPackages coq_8_18;
-  coqPackages_8_19 = mkCoqPackages coq_8_19;
-  coqPackages_8_20 = mkCoqPackages coq_8_20;
-  coqPackages_9_0 = mkCoqPackages coq_9_0;
-  coqPackages_9_1 = mkCoqPackages coq_9_1;
+  coq_8_7 = coqPackages_8_7.coq;
+  coq_8_8 = coqPackages_8_8.coq;
+  coq_8_9 = coqPackages_8_9.coq;
+  coq_8_10 = coqPackages_8_10.coq;
+  coq_8_11 = coqPackages_8_11.coq;
+  coq_8_12 = coqPackages_8_12.coq;
+  coq_8_13 = coqPackages_8_13.coq;
+  coq_8_14 = coqPackages_8_14.coq;
+  coq_8_15 = coqPackages_8_15.coq;
+  coq_8_16 = coqPackages_8_16.coq;
+  coq_8_17 = coqPackages_8_17.coq;
+  coq_8_18 = coqPackages_8_18.coq;
+  coq_8_19 = coqPackages_8_19.coq;
+  coq_8_20 = coqPackages_8_20.coq;
+  coq_9_0 = coqPackages_9_0.coq;
+  coq_9_1 = coqPackages_9_1.coq;
 
   coqPackages = lib.recurseIntoAttrs coqPackages_9_0;
   coq = coqPackages.coq;