Stream: CUDW 2020

Topic: WG: Nix setup

Cyril Cohen (Nov 30 2020 at 09:46):

In order to understand what to do, I would have to understand better the needs of future user, in terms of feature and accessibility

Cyril Cohen (Nov 30 2020 at 09:47):

I would also like to know what the current Coq setup does because I have had a hard time untangling it...

Théo Zimmermann (Nov 30 2020 at 10:01):

@Cyril Cohen Do you want to discuss this now? I don't think I'm really useful in the Windows installer breakout room.

Cyril Cohen (Nov 30 2020 at 10:01):

Right now I am in the uint room, I believe it will be over soon

Cyril Cohen (Nov 30 2020 at 10:02):

Can we meet in approx 30'?

Théo Zimmermann (Nov 30 2020 at 10:02):

Sure, ping me when it's a good time for you.

Cyril Cohen (Nov 30 2020 at 10:14):

@Théo Zimmermann we can start now, if you like

Théo Zimmermann (Nov 30 2020 at 10:14):

OK

Michael Soegtrop (Nov 30 2020 at 10:38):

Some time this week I would like to discuss Coq platform and Nix with the experts.

Théo Zimmermann (Nov 30 2020 at 12:26):

Sure!

Théo Zimmermann (Nov 30 2020 at 12:26):

@Cyril Cohen I'm back.

Cyril Cohen (Nov 30 2020 at 12:34):

I'm sorry, I'm a bit late, would you mind meeting at 2pm?

Théo Zimmermann (Nov 30 2020 at 12:38):

No pb, it'll give me time to catch up on Zulip and maybe also write down some notes about what we discussed so far.

Karl Palmskog (Nov 30 2020 at 12:47):

what's the link to list all Coq packages in Nix? this one is dead nowadays: https://nixos.org/nixos/packages.html?channel=nixpkgs-unstable&query=coqPackages

Théo Zimmermann (Nov 30 2020 at 12:48):

Here's an updated one: https://search.nixos.org/packages?channel=unstable&query=coqPackages

Cyril Cohen (Nov 30 2020 at 12:55):

:-/ it does not seem up to date to me

Cyril Cohen (Nov 30 2020 at 12:55):

mathcomp 1.11 is supposed to be available...

Cyril Cohen (Nov 30 2020 at 12:55):

I'm a bit worried

Cyril Cohen (Nov 30 2020 at 12:55):

ah no I understand

Cyril Cohen (Nov 30 2020 at 12:56):

I never promoted mathcomp 1.11 to priority 1 :(

Théo Zimmermann (Nov 30 2020 at 12:58):

"priority 1"? What is that?

Cyril Cohen (Nov 30 2020 at 13:00):

at the time of mathcomp 1.11+beta1 I invented a priority system to make sure people would not accidentally en up trying mathcomp 1.11+beta instead of the stable 1.10

Cyril Cohen (Nov 30 2020 at 13:00):

And I forgot to reorder when 1.11 went out

Cyril Cohen (Nov 30 2020 at 13:01):

cf https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/mathcomp/default.nix#L99

Cyril Cohen (Nov 30 2020 at 13:01):

I'm back

Théo Zimmermann (Nov 30 2020 at 13:02):

OK, let's go to room 1

Cyril Cohen (Nov 30 2020 at 13:04):

room 5

Cyril Cohen (Dec 02 2020 at 15:45):

@Théo Zimmermann

Théo Zimmermann (Dec 02 2020 at 15:45):

Huh?

Cyril Cohen (Dec 02 2020 at 15:45):

Can you remind me where is the post about naming paths?

Théo Zimmermann (Dec 02 2020 at 15:45):

Yep, let me find it again.

Cyril Cohen (Dec 02 2020 at 15:45):

thanks!

Théo Zimmermann (Dec 02 2020 at 15:45):

Here: https://discourse.nixos.org/t/the-papercut-thread-post-your-small-annoyances-confusions-here/3100/77

Cyril Cohen (Dec 02 2020 at 15:46):

thanks!

Théo Zimmermann (Dec 04 2020 at 13:01):

@Vincent Laporte and @Cyril Cohen : shall we go to a breakout room? E.g., breakout room 5?

Cyril Cohen (Dec 04 2020 at 13:06):

I am there

Cyril Cohen (Dec 04 2020 at 13:09):

https://github.com/NixOS/nixpkgs/pull/105877

Cyril Cohen (Dec 04 2020 at 15:19):

@Théo Zimmermann Indeed you were right
let f = {x ? null}@args: [x args (args.x or 42)]; in f {}
returns [ null {} 42 ] so you can always document optional fields by putting ? whatever and use args.x or stuff to avoid doing the longer if !isNull x then x else stuff.

Cyril Cohen (Dec 08 2020 at 11:10):

Cyril Cohen said:

https://github.com/NixOS/nixpkgs/pull/105877

FTR, I migrated the entire coqPackages to mkCoqDerivation based on an improved meta-fetcher to take into account every single current use-case...

Cyril Cohen (Dec 08 2020 at 11:12):

• I am begining to write the new package repository root default.nix toolbox, to catchup with my current use cases.
• Next step will be to extend it to a CI infrastructure
• And finally turn this CI infrastructure into a template...

Cyril Cohen (Dec 08 2020 at 11:12):

cc @Théo Zimmermann

Cyril Cohen (Dec 10 2020 at 13:30):

@Théo Zimmermann and @Vincent Laporte we should be meeting now... do you have a preference about the videoconferencing system to use?

Théo Zimmermann (Dec 10 2020 at 13:31):

No preference.

Cyril Cohen (Dec 10 2020 at 13:33):

email sent

Cyril Cohen (Dec 10 2020 at 13:33):

(visio.inria.fr) $\longrightarrow$ Zoom

Last updated: Jun 11 2023 at 00:30 UTC