Skip to content

{coq,rocq}Packages.mk{Coq,Rocq}Derivation: move env variables into env for structuredAttrs #492142

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
philiptaron merged 2 commits into from
Jul 6, 2026
Merged

{coq,rocq}Packages.mk{Coq,Rocq}Derivation: move env variables into env for structuredAttrs #492142

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8ad58c0
coqPackages.mkCoqDerivation: move env variables into env for structur…
SFrijters Feb 19, 2026
0f83565
rocqPackages.mkRocqDerivation: move env variables into env
SFrijters Mar 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 12 additions & 4 deletions pkgs/build-support/coq/default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,7 @@ let
"dropAttrs"
"dropDerivationAttrs"
"keepAttrs"
"env"

@MattSturgeon MattSturgeon May 25, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Off-topic:

It's unfortunate that // (removeAttrs args args-to-remove) is on the RHS of the update, so we need to explicitly "remove" args that'd shadow explicit overrides below. I assume there are other things that we'd want args to shadow the "default values" below?

These coq & rcoq builders would benefit from being refactored to use extendMkDerivation.

]
++ dropAttrs
) keepAttrs;
Expand Down Expand Up @@ -162,8 +163,8 @@ let
"COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
];
docdir-flags = [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib";
in

stdenv.mkDerivation (
removeAttrs (
{
Expand All @@ -187,6 +188,15 @@ stdenv.mkDerivation (
args.overrideBuildInputs or ([ coq ] ++ (args.buildInputs or [ ]) ++ extraBuildInputs);
inherit enableParallelBuilding;

env =
optionalAttrs setCOQBIN {
COQBIN = "${coq}/bin/";
}
// optionalAttrs (args ? useMelquiondRemake) {
inherit COQUSERCONTRIB;
}
// (args.env or { });

@SFrijters SFrijters Mar 18, 2026

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should the args.env be at the end (making the variables above overridable), or at the top?

@MattSturgeon MattSturgeon May 25, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that's open to interpretation.

It depends on who should have the final say for COQBIN and COQUSERCONTRIB's values; args.COQBIN or setCOQBIN; args.COQUSERCONTRIB or useMelquiondRemake?

Or should we we warning/throwing when there is a conflict? We don't usually do that in nixpkgs, but it would be more explicit if you think this is prone to user error.


meta =
(
{
Expand All @@ -208,7 +218,6 @@ stdenv.mkDerivation (
// (args.meta or { });

}
// (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; })
// (optionalAttrs (!args ? installPhase && !args ? useMelquiondRemake) {
installFlags = coqlib-flags ++ docdir-flags ++ extraInstallFlags;
})
Expand All @@ -226,8 +235,7 @@ stdenv.mkDerivation (
runHook postInstall
'';
})
// (optionalAttrs (args ? useMelquiondRemake) rec {
COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib";
// (optionalAttrs (args ? useMelquiondRemake) {
preConfigurePhases = [ "autoconf" ];
configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ];
buildPhase = "./remake -j$NIX_BUILD_CORES";
Expand Down
15 changes: 12 additions & 3 deletions pkgs/build-support/rocq/default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,7 @@ let
"dropAttrs"
"dropDerivationAttrs"
"keepAttrs"
"env"
]
++ dropAttrs
) keepAttrs;
Expand Down Expand Up @@ -162,6 +163,7 @@ let
"COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
];
docdir-flags = [ "COQDOCINSTALL=$(out)/share/coq/${rocq-core.rocq-version}/user-contrib" ];
COQUSERCONTRIB = "$out/lib/coq/${rocq-core.rocq-version}/user-contrib";
in

stdenv.mkDerivation (
Expand All @@ -187,6 +189,15 @@ stdenv.mkDerivation (
args.overrideBuildInputs or ([ rocq-core ] ++ (args.buildInputs or [ ]) ++ extraBuildInputs);
inherit enableParallelBuilding;

env =
optionalAttrs setROCQBIN {
ROCQBIN = "${rocq-core}/bin/";
}
// optionalAttrs (args ? useMelquiondRemake) {
inherit COQUSERCONTRIB;
}
// (args.env or { });

meta =
(
{
Expand All @@ -208,7 +219,6 @@ stdenv.mkDerivation (
// (args.meta or { });

}
// (optionalAttrs setROCQBIN { ROCQBIN = "${rocq-core}/bin/"; })
// (optionalAttrs (!args ? installPhase && !args ? useMelquiondRemake) {
installFlags = rocqlib-flags ++ docdir-flags ++ extraInstallFlags;
})
Expand All @@ -226,8 +236,7 @@ stdenv.mkDerivation (
runHook postInstall
'';
})
// (optionalAttrs (args ? useMelquiondRemake) rec {
COQUSERCONTRIB = "$out/lib/coq/${rocq-core.rocq-version}/user-contrib";
// (optionalAttrs (args ? useMelquiondRemake) {
preConfigurePhases = [ "autoconf" ];
configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ];
buildPhase = "./remake -j$NIX_BUILD_CORES";
Expand Down
Loading