Théo Zimmermann (Jun 30 2022 at 15:30): 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)?
Vincent Laporte (Jun 30 2022 at 15:34):Yes! and yes again!
Move CoqIDE into its separate package if it’s working now.
Cyril Cohen (Jun 30 2022 at 15:40):Sure! But I do not have the time to do so... :-/
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.
Emilio Jesús Gallego Arias (Jul 06 2022 at 17:52):@Théo Zimmermann don't hesitate to ping me for help
Emilio Jesús Gallego Arias (Jul 06 2022 at 17:52):I'd be happy to hear about the bugs
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.
Théo Zimmermann (Jul 06 2022 at 17:55):I'll try again checking if the problem comes from lablgtk.
Emilio Jesús Gallego Arias (Jul 06 2022 at 17:57):You mean in the Nix bug tracker? I see nothing on Coq's
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 ;-)
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:09):I got worried by the "many bugs" statement
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.
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
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:23):let's submit a PR
Théo Zimmermann (Jul 06 2022 at 18:25):Anyway, thanks to you I finally managed to make the split package work.
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)
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:26):you can't pass COQLIB?
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:27):actually there is this file you can use to override that
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:27):I'm confused tho
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?
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:28):or can it also use some file in /etc
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:28):?
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.
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:38):Ok
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:38):Yeah coqide and coqide server have been regular dune packages for a while
Emilio Jesús Gallego Arias (Jul 06 2022 at 18:38):and split in the opam repos
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?
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)
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: Jun 10 2023 at 23:01 UTC