{coq,rocq}Packages.mk{Coq,Rocq}Derivation: move env variables into env for structuredAttrs by SFrijters · Pull Request #492142 · NixOS/nixpkgs

SFrijters · 2026-02-19T16:03:23Z

This probably needs some careful review because of the conditional variables.

Things done

SFrijters · 2026-02-19T16:15:21Z

`nixpkgs-review` result

Generated using nixpkgs-review.

Command: nixpkgs-review pr 492142
Commit: cb9287924a2ae9f6218bcdcddcaf8b661d97311c

SFrijters · 2026-03-18T19:54:20Z

+        // optionalAttrs (args ? useMelquiondRemake) {
+          inherit COQUSERCONTRIB;
+        }
+        // (args.env or { });


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

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.

SFrijters · 2026-03-23T10:55:07Z

Added the same change for rocqPackages, the question of ordering of env still applies.

SFrijters · 2026-04-07T13:10:50Z

@philiptaron Gentle poke for review?

vbgl · 2026-04-07T13:18:24Z

Could you help debugging the following error:

error: The `env` attribute set cannot contain any attributes passed to derivation. The following attributes are overlapping:
- COQBIN: in `env`: "/nix/store/…-coq-9.0.1/bin/"; in derivation arguments: ""

SFrijters · 2026-04-07T13:31:51Z

What exactly are you doing to cause that error?

And does this new commit fix the issue? It may not be the right way to go, but at least it would help me understand what is happening. The rocq variant will need a similar fix, whatever it might end up being.

vbgl · 2026-04-07T14:28:39Z

I’m trying to use the coq-nix-toolbox to review this PR. Running genNixActions produces the reported error. Your latest commit did not help (no observable change).

SFrijters · 2026-04-07T14:49:42Z

Almost certainly related to https://github.com/rocq-community/coq-nix-toolbox/blob/77b185941e037f5afd21dee4713b8d1be1d67aa9/default.nix#L106

My "fix" doesn't work because that repo seems to override whatever comes out of nixpkgs, not the other way around?

I'm not sure that line makes sense anyway? Using optionalString (condition) "" is just always "", no?
I assume it's meant to leave the variable alone if do-nothing? Then optionalAttrs would be better instead.

For forward compatibility it should blank either COQBIN or env.COQBIN, whichever exists.

philiptaron

Change LGTM from the Nixpkgs POV, I don't know the coq part of the ecosystem super-well though.

SFrijters · 2026-05-01T14:55:01Z

@vbgl Do you have any plans for making the toolbox more compatible with env?

vbgl · 2026-05-04T07:24:23Z

No plans on my side.

With structuredAttrs enabled, environment variables should live inside the `env` attrset. In the case of this project, this affects COQBIN, as per NixOS/nixpkgs#492142 , which moves it into env. Setting `COQBIN = "";` in `default.nix` while `env.COQBIN` exists causes an evaluation error: Error: The `env` attribute set cannot contain any attributes passed to derivation. To fix this, remove the attr instead if it exists, in either place.

SFrijters · 2026-05-04T09:58:35Z

Rebased on top of the pinned nixpkgs commit in coq-nix-toolbox for easier testing. @vbgl Could you take a look at rocq-community/coq-nix-toolbox#460 ?

SFrijters · 2026-05-16T21:20:05Z

This is pretty much the only package set in nixpkgs that still has env variables outside of env so I would like to move ahead on this at some point - I have provided a likely solution for downstream and I don't like this issue lingering any more than necessary.

@proux01 Any thoughts on this and/or the PR I opened on the toolbox?

MattSturgeon

Change LGTM from the Nixpkgs POV, I don't know the coq part of the ecosystem super-well though.

Same here

MattSturgeon · 2026-05-25T14:49:18Z

      "dropDerivationAttrs"
      "keepAttrs"
      "enableParallelBuilding"
+      "env"


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.

MattSturgeon · 2026-05-25T14:52:49Z

+        // optionalAttrs (args ? useMelquiondRemake) {
+          inherit COQUSERCONTRIB;
+        }
+        // (args.env or { });


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.

SFrijters · 2026-05-26T10:38:28Z

I'd like to move forward on this so it's off my PR list (and because we're getting really close to eliminating these free-ranging env variables overall), but I don't have much bandwidth at the moment to deal with any potential fallout if there are any unexpected issues, so I'd prefer if someone who actually uses Coq/Rocq could weigh in before I push a merge button.

…edAttrs

SFrijters · 2026-07-06T12:57:42Z

Rebased to resolved merge conflicts.

With structuredAttrs enabled, environment variables should live inside the `env` attrset. In the case of this project, this affects COQBIN, as per NixOS/nixpkgs#492142 , which moves it into env. Setting `COQBIN = "";` in `default.nix` while `env.COQBIN` exists causes an evaluation error: Error: The `env` attribute set cannot contain any attributes passed to derivation. To fix this, remove the attr instead if it exists, in either place. Update after NixOS/nixpkgs#492142

SFrijters changed the title ~~coqPackages.mkCoqDerivation: move env variables into env for structur…~~ coqPackages.mkCoqDerivation: move env variables into env for structuredAttrs Feb 19, 2026

SFrijters force-pushed the coq-env branch from a95b697 to cb92879 Compare February 19, 2026 16:04

nixpkgs-ci Bot added 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin. 10.rebuild-linux: 0 This PR does not cause any packages to rebuild on Linux. labels Feb 19, 2026

SFrijters marked this pull request as ready for review February 19, 2026 16:15

nixpkgs-ci Bot requested a review from philiptaron February 19, 2026 16:27

SFrijters mentioned this pull request Feb 20, 2026

[Tracking Issue] __structuredAttrs TODOs and FIXMEs #205690

Open

3 tasks

SFrijters requested review from qweered and vbgl March 18, 2026 19:52

SFrijters commented Mar 18, 2026

View reviewed changes

SFrijters force-pushed the coq-env branch 2 times, most recently from 7d33727 to 0a7e0a1 Compare March 23, 2026 10:53

SFrijters changed the title ~~coqPackages.mkCoqDerivation: move env variables into env for structuredAttrs~~ {coq,rocq}Packages.mk{Coq,Rocq}Derivation: move env variables into env for structuredAttrs Mar 23, 2026

SFrijters requested a review from proux01 March 23, 2026 13:09

SFrijters force-pushed the coq-env branch from faeda45 to 0a7e0a1 Compare April 7, 2026 15:14

philiptaron approved these changes Apr 7, 2026

View reviewed changes

nixpkgs-ci Bot added the 12.approvals: 1 This PR was reviewed and approved by one person. label Apr 7, 2026

SFrijters force-pushed the coq-env branch from 0a7e0a1 to bd62d98 Compare May 4, 2026 09:45

SFrijters mentioned this pull request May 4, 2026

Add support for structuredAttrs being enabled in nixpkgs rocq-community/coq-nix-toolbox#460

Open

MattSturgeon approved these changes May 25, 2026

View reviewed changes

nixpkgs-ci Bot added 12.approvals: 2 This PR was reviewed and approved by two persons. and removed 12.approvals: 1 This PR was reviewed and approved by one person. labels May 25, 2026

This was referenced May 26, 2026

rocq: move env variable into env for structuredAttrs #524038

Closed

coqPackages: move env variable into env for structuredAttrs #524037

Closed

SFrijters added 2 commits July 6, 2026 14:55

coqPackages.mkCoqDerivation: move env variables into env for structur…

8ad58c0

…edAttrs

rocqPackages.mkRocqDerivation: move env variables into env

0f83565

SFrijters force-pushed the coq-env branch from bd62d98 to 0f83565 Compare July 6, 2026 12:57

SFrijters requested a review from Zimmi48 July 6, 2026 12:58

philiptaron added this pull request to the merge queue Jul 6, 2026

Merged via the queue into NixOS:master with commit 9195f26 Jul 6, 2026
26 checks passed

SFrijters deleted the coq-env branch July 7, 2026 09:37

Uh oh!

Uh oh!

Conversation

SFrijters commented Feb 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Things done

Uh oh!

SFrijters commented Feb 19, 2026

nixpkgs-review result

Uh oh!

SFrijters Mar 18, 2026

Choose a reason for hiding this comment

Uh oh!

MattSturgeon May 25, 2026

Choose a reason for hiding this comment

Uh oh!

SFrijters commented Mar 23, 2026

Uh oh!

SFrijters commented Apr 7, 2026

Uh oh!

vbgl commented Apr 7, 2026

Uh oh!

SFrijters commented Apr 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

vbgl commented Apr 7, 2026

Uh oh!

SFrijters commented Apr 7, 2026

Uh oh!

philiptaron left a comment

Choose a reason for hiding this comment

Uh oh!

SFrijters commented May 1, 2026

Uh oh!

vbgl commented May 4, 2026

Uh oh!

SFrijters commented May 4, 2026

Uh oh!

SFrijters commented May 16, 2026

Uh oh!

MattSturgeon left a comment

Choose a reason for hiding this comment

Uh oh!

MattSturgeon May 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MattSturgeon May 25, 2026

Choose a reason for hiding this comment

Uh oh!

SFrijters commented May 26, 2026

Uh oh!

SFrijters commented Jul 6, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

SFrijters commented Feb 19, 2026 •

edited

Loading

`nixpkgs-review` result

SFrijters commented Apr 7, 2026 •

edited

Loading

MattSturgeon May 25, 2026 •

edited

Loading