diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md index f758d89d3269..0eab34d044e4 100644 --- a/doc/languages-frameworks/coq.section.md +++ b/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: diff --git a/doc/redirects.json b/doc/redirects.json index d52ae8a8f047..8f28dc5dc4bb 100644 --- a/doc/redirects.json +++ b/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" ], diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 590c2d6a2d12..1884ef85fe57 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/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 diff --git a/pkgs/applications/science/logic/coq/with-packages.nix b/pkgs/applications/science/logic/coq/with-packages.nix new file mode 100644 index 000000000000..62a95c927f84 --- /dev/null +++ b/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; +} diff --git a/pkgs/development/coq-modules/stdlib/default.nix b/pkgs/development/coq-modules/stdlib/default.nix index ebbe95b7fa64..eb1091ea642a 100644 --- a/pkgs/development/coq-modules/stdlib/default.nix +++ b/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 = { diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix index 8a35e3a59feb..6e2e29b41ea8 100644 --- a/pkgs/top-level/coq-packages.nix +++ b/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;