@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)?
Yes! and yes again!
Move CoqIDE into its separate package if it’s working now.
Sure! But I do not have the time to do so... :-/
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.
@Théo Zimmermann don't hesitate to ping me for help
I'd be happy to hear about the bugs
Yes. So far, I've reported all of them in either Zulip or the bug tracker.
I'll try again checking if the problem comes from lablgtk.
You mean in the Nix bug tracker? I see nothing on Coq's
No, I was talking of the bug I reported on Monday and that you already fixed ;-)
I got worried by the "many bugs" statement
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.
yes it is annoying, but that's opam fault, I'm happy to remove it from Coq
let's submit a PR
Anyway, thanks to you I finally managed to make the split package work.
(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)
you can't pass COQLIB?
actually there is this file you can use to override that
I'm confused tho
the only mean for coq-stdlib to tell coq where to look is an env var?
or can it also use some file in /etc
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.
Yeah coqide and coqide server have been regular dune packages for a while
and split in the opam repos
@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?
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)
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