Stream: CUDW 2020

Topic: WG: Nix setup


view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Nov 30 2020 at 10:01):

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

view this post on Zulip Cyril Cohen (Nov 30 2020 at 10:02):

Can we meet in approx 30'?

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 10:02):

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

view this post on Zulip Cyril Cohen (Nov 30 2020 at 10:14):

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

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 10:14):

OK

view this post on Zulip Michael Soegtrop (Nov 30 2020 at 10:38):

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

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 12:26):

Sure!

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 12:26):

@Cyril Cohen I'm back.

view this post on Zulip Cyril Cohen (Nov 30 2020 at 12:34):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 12:48):

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

view this post on Zulip Cyril Cohen (Nov 30 2020 at 12:55):

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

view this post on Zulip Cyril Cohen (Nov 30 2020 at 12:55):

mathcomp 1.11 is supposed to be available...

view this post on Zulip Cyril Cohen (Nov 30 2020 at 12:55):

I'm a bit worried

view this post on Zulip Cyril Cohen (Nov 30 2020 at 12:55):

ah no I understand

view this post on Zulip Cyril Cohen (Nov 30 2020 at 12:56):

I never promoted mathcomp 1.11 to priority 1 :(

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 12:58):

"priority 1"? What is that?

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Nov 30 2020 at 13:00):

And I forgot to reorder when 1.11 went out

view this post on Zulip Cyril Cohen (Nov 30 2020 at 13:01):

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

view this post on Zulip Cyril Cohen (Nov 30 2020 at 13:01):

I'm back

view this post on Zulip Théo Zimmermann (Nov 30 2020 at 13:02):

OK, let's go to room 1

view this post on Zulip Cyril Cohen (Nov 30 2020 at 13:04):

room 5

view this post on Zulip Cyril Cohen (Dec 02 2020 at 15:45):

@Théo Zimmermann

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 15:45):

Huh?

view this post on Zulip Cyril Cohen (Dec 02 2020 at 15:45):

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

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 15:45):

Yep, let me find it again.

view this post on Zulip Cyril Cohen (Dec 02 2020 at 15:45):

thanks!

view this post on Zulip 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

view this post on Zulip Cyril Cohen (Dec 02 2020 at 15:46):

thanks!

view this post on Zulip 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?

view this post on Zulip Cyril Cohen (Dec 04 2020 at 13:06):

I am there

view this post on Zulip Cyril Cohen (Dec 04 2020 at 13:09):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Cyril Cohen (Dec 08 2020 at 11:12):

view this post on Zulip Cyril Cohen (Dec 08 2020 at 11:12):

cc @Théo Zimmermann

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Dec 10 2020 at 13:31):

No preference.

view this post on Zulip Cyril Cohen (Dec 10 2020 at 13:33):

email sent

view this post on Zulip Cyril Cohen (Dec 10 2020 at 13:33):

(visio.inria.fr) \longrightarrow Zoom


Last updated: Oct 16 2021 at 09:07 UTC