Small refactoring in coqPackages #49456
Conversation
GrahamcOfBorg
added
10.rebuild-darwin: 0
Closes rocq-prover#8227 by solving remaining differences. Sets doNotFilter in anticipation of NixOS/nixpkgs#49456.
vbgl
force-pushed
the
coq-packages-no-filter
branch
from
f0d1ae6 to
32bf813
Compare
Closes rocq-prover#8227 by solving remaining differences. Sets doNotFilter in anticipation of NixOS/nixpkgs#49456.
Closes rocq-prover#8227 by solving remaining differences. Sets doNotFilter in anticipation of NixOS/nixpkgs#49456.
pkgs/top-level/coq-packages.nix
Outdated
| @@ -54,7 +54,8 @@ in rec { | |||
|
|
|||
| mkCoqPackages = coq: | |||
| let self = mkCoqPackages' self coq; in | |||
| filterCoqPackages coq self; | |||
| if coq.doNotFilter or false then self | |||
There was a problem hiding this comment.
| if coq.doNotFilter or false then self | |
| if coq.doNotFilter then self |
There was a problem hiding this comment.
Alright. Let me add some documentation.
There was a problem hiding this comment.
Right! It's the a.b or c syntax. I can't believe I fell for that.
Do we really need the negated name? Negated names require unnecessary extra thinking. What about "setting doFilter = false" which has a default of true?
There was a problem hiding this comment.
Maybe Théo has an opinion. Ping @Zimmi48 .
There was a problem hiding this comment.
Ah I did not know about the syntax, will use ;-)
Regarding doFilter = false vs doNotFilter = true, it seems that the implicit convention in nixpkgs (https://nixos.org/nixpkgs/manual/#sec-stdenv-phases) is that when something is off by default, it is enabled with doStuff = true but when something is on by default, it is disabled dontStuff = true. Thus, it suggests to use dontFilter here.
There was a problem hiding this comment.
Let’s go with dontFilter.
vbgl
force-pushed
the
coq-packages-no-filter
branch
2 times, most recently
from
32bf813 to
9014c5f
Compare
vbgl
force-pushed
the
coq-packages-no-filter
branch
from
ea820d0 to
33face8
Compare
Closes rocq-prover#8227 by solving remaining differences. Sets dontFilter in anticipation of NixOS/nixpkgs#49456.
Closes rocq-prover#8227 by solving remaining differences. Sets dontFilter in anticipation of NixOS/nixpkgs#49456.
Motivation for this change
Make it easier to override Coq packages.
Things done
sandboxinnix.confon non-NixOS)nix-shell -p nox --run "nox-review wip"./result/bin/)nix path-info -Sbefore and after)