Stream: Nix toolbox devs & users

Topic: Update for Coq 8.17+alpha


view this post on Zulip Théo Zimmermann (Jun 30 2022 at 15:30):

@Vincent Laporte @Cyril Cohen Since the big Dune PR, the Coq derivation in nixpkgs cannot build Coq master (again). Recommendations on how to package Coq can be found here and here. One thing that I wonder about is: should we use the opportunity to finally split CoqIDE into its own package? And if yes, should we start afresh (separate Nix file)?

view this post on Zulip Vincent Laporte (Jun 30 2022 at 15:34):

Yes! and yes again!
Move CoqIDE into its separate package if it’s working now.

view this post on Zulip Cyril Cohen (Jun 30 2022 at 15:40):

Sure! But I do not have the time to do so... :-/

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 16:39):

Unfortunately, I have encountered many bugs of the new build infrastructure, so I will reduce the scope of my goals for now to just fixing Nix CI.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:52):

@Théo Zimmermann don't hesitate to ping me for help

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:52):

I'd be happy to hear about the bugs

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 17:55):

Yes. So far, I've reported all of them in either Zulip or the bug tracker.

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 17:55):

I'll try again checking if the problem comes from lablgtk.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:57):

You mean in the Nix bug tracker? I see nothing on Coq's

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 18:04):

No, I was talking of the bug I reported on Monday and that you already fixed ;-)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:09):

I got worried by the "many bugs" statement

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 18:12):

So it turns out that one of them was indeed my fault and not Coq's fault. But this (optional) field is indeed an annoyance that does not help figure out what's going on.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:23):

yes it is annoying, but that's opam fault, I'm happy to remove it from Coq

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:23):

let's submit a PR

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 18:25):

Anyway, thanks to you I finally managed to make the split package work.

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 18:26):

(split between coq and coqide, splitting coq into coq-core and coq-stdlib will continue being difficult as long as the Coq binaries need to know where the stdlib is located)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:26):

you can't pass COQLIB?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:27):

actually there is this file you can use to override that

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:27):

I'm confused tho

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:28):

the only mean for coq-stdlib to tell coq where to look is an env var?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:28):

or can it also use some file in /etc

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:28):

?

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 18:32):

I dunno, but to be honest I'm not sufficiently interested to investigate more. I'm already happy to have managed to split CoqIDE out.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:38):

Ok

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:38):

Yeah coqide and coqide server have been regular dune packages for a while

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 18:38):

and split in the opam repos

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 19:51):

@Cyril Cohen and @Vincent Laporte: so in the end, I have one PR updating Coq for compatibility with the new build infrastructure on the one hand (https://github.com/NixOS/nixpkgs/pull/180370), and on the other hand I'm ready to open a PR splitting CoqIDE into its own package, and the two are orthogonal. The split works all the way back to Coq 8.14, so I was wondering whether I should do the split only starting in Coq 8.16 (new release in preparation) or as soon as it is possible. Do you have an opinion?

view this post on Zulip Paolo Giarrusso (Jul 06 2022 at 20:48):

Sorry to butt in, but split = users can install/uninstall coqide without rebuilding Coq? Not a Nix user, but FWIW that seems like a strict improvement (no idea about any costs)

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 21:23):

Indeed. Until now, CoqIDE was part of the Coq derivation by default, but if you did not want it, you had to rebuild Coq.


Last updated: Jan 29 2023 at 14:02 UTC