Stream: Nix toolbox devs & users

Topic: `nixpkgs` PR?

Quinn (Sep 29 2023 at 04:35):

This is the only nix stream I found in zulip! what's the process for coqPackages.xyz PRs to nixos/nixpkgs? vcfloat seems right for my application https://github.com/NixOS/nixpkgs/pull/257959 --- is someone I can ping about this in here?

Théo Zimmermann (Sep 29 2023 at 07:56):

Yes, you can ping me (@Zimmi48 on GitHub) or Vincent Laporte (@vbgl on GitHub) in particular.

Quinn (Sep 29 2023 at 21:33):

thanks!

Quinn (Oct 03 2023 at 17:41):

Hi @Théo Zimmermann -- Someone tagged you in at https://github.com/NixOS/nixpkgs/pull/258096 -- let me know if you need anything from me.

Théo Zimmermann (Oct 04 2023 at 07:27):

Just need to find some time to look at it ;-)

Quinn (Nov 01 2023 at 19:51):

Hi Theo, I screwed this up the other week, the package is going to require this actually:

vcfloat-override = with pkgs.coqPackages_8_17; vcfloat.overrideAttrs (oldAttrs: {
          buildPhase = ''
            export INSTALLDIR=$out/lib/coq/${coq.coq-version}/user-contrib/vcfloat
            cd vcfloat
          '';
        });

sorry! It was my first coqPackages pr to nixpkgs, I'm learning and I'd like to become more valuable to the community. I can get a patch submitted ASAP, is there are particular stylistic preference? i.e. equations has:

}).overrideAttrs (o: {
  preBuild = "coq_makefile -f _CoqProject -o Makefile${lib.optionalString (lib.versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
})

At the bottom of the file, which would get the job done in this usecase I think.

I tested it in an emacs session this time-- I was insufficiently thorough last time that's totally on me. the Makefile lying in teh subdir (and the subdir being also the package name python style instead of theories) is slightly nonstandard these days , so I didn't know immediately how to address.

Quinn (Nov 01 2023 at 19:53):

also, a brief note: Is it valuable to use crosscompilation to test on aarch locally?

Quinn (Nov 01 2023 at 20:01):

this https://github.com/coq-community/coq-nix-toolbox/pull/167 must not've caught my error cuz there was nothing really trying to import it.

Quinn (Nov 01 2023 at 20:11):

Also, same thread: I'd like to get https://github.com/math-comp/analysis/releases caught up, do you know if cohencyril is in zulip for me to ask if he'd review a PR?

Théo Zimmermann (Nov 02 2023 at 16:02):

Quinn said:

Hi Theo, I screwed this up the other week, the package is going to require this actually:

vcfloat-override = with pkgs.coqPackages_8_17; vcfloat.overrideAttrs (oldAttrs: {
          buildPhase = ''
            export INSTALLDIR=$out/lib/coq/${coq.coq-version}/user-contrib/vcfloat
            cd vcfloat
          '';
        });

sorry! It was my first coqPackages pr to nixpkgs, I'm learning and I'd like to become more valuable to the community. I can get a patch submitted ASAP, is there are particular stylistic preference? i.e. equations has:

}).overrideAttrs (o: {
  preBuild = "coq_makefile -f _CoqProject -o Makefile${lib.optionalString (lib.versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
})

At the bottom of the file, which would get the job done in this usecase I think.

I tested it in an emacs session this time-- I was insufficiently thorough last time that's totally on me. the Makefile lying in teh subdir (and the subdir being also the package name python style instead of theories) is slightly nonstandard these days , so I didn't know immediately how to address.

Sure, the style of what you quote from Equations is good.

Théo Zimmermann (Nov 02 2023 at 16:03):

Quinn said:

also, a brief note: Is it valuable to use crosscompilation to test on aarch locally?

I have never bothered going this far...

Théo Zimmermann (Nov 02 2023 at 16:04):

Quinn said:

Also, same thread: I'd like to get https://github.com/math-comp/analysis/releases caught up, do you know if cohencyril is in zulip for me to ask if he'd review a PR?

Yes @Cyril Cohen on Zulip. Note the already open https://github.com/math-comp/analysis/pull/951. I don't know what is blocking it, but that's something to discuss directly on #math-comp analysis.

Pierre Roux (Nov 02 2023 at 16:28):

Théo Zimmermann said:

Yes Cyril Cohen on Zulip. Note the already open https://github.com/math-comp/analysis/pull/951. I don't know what is blocking it, but that's something to discuss directly on #math-comp analysis.

FWIW the performance of MC 2 when released was quite bad. It's improving and there are hopes to merge for next January or so.

Quinn (Nov 03 2023 at 16:56):

@Théo Zimmermann thanks --- your doubts make sense, and I was a little disappointed that I couldn't do it that way in the first place (I had tried a few things in the direction you were talking about). Plus, I just double checked. If anyone knows a better way https://github.com/NixOS/nixpkgs/pull/264881/files I'm happy to go that way, I just couldn't find anything reading about all the mkCoqDerivation attributes on https://ryantm.github.io/nixpkgs/languages-frameworks/coq/

Quinn (Nov 03 2023 at 17:52):

(implementing your most recent comment, figuring out how to modify commit history so that the fix remains one commit) :check:

Last updated: Nov 29 2023 at 21:01 UTC