[ci] [nix] Build for stable branches fails

[ejgallego]

Build for the 8.17 branch fails with:

       last 10 log lines:
       > File "lang/dune", line 4, characters 16-32:
       > 4 |  (libraries uri coq-core.library))
       >                     ^^^^^^^^^^^^^^^^
       > Error: Library "coq-core.library" not found.
       > -> required by library "coq-lsp.lang" in _build/default/lang
       > -> required by _build/default/META.coq-lsp
       > -> required by _build/install/default/lib/coq-lsp/META
       > -> required by _build/default/coq-lsp.install
       > -> required by alias install
       >
       For full logs, run 'nix log /nix/store/6q4rf52h9kyk53nnwfr5ahhba20c7ban-ocaml4.14.1-coq-lsp-20230705222339+8.17-rc1.drv'.

[kylechui]

This seems to happen for me as well when building on NixOS using Coq 8.15 with the 8.15 branch.

[ejgallego]

Hi @kylechui , sorry to hear that. The problem is that for some reason ocamlfind cannot locate the libraries for coq-core.

@Alizter @Zimmi48 , is there a problem with Coq's Nix package for 8.15 so that findlib libraries are not properly registered?

This could likely happen due to Coq 8.15 in Nix being built with the makefile (not dune) and somehow the makefile not interacting well with Nix findlib setup.

[ejgallego]

By the way @kylechui , the 8.15 branch is quite lagging behind main; our idea is to have 8.17 as the baseline, but we are happy to keep supporting older Coq versions.

Do you have a particular use case that needs 8.15?

[kylechui]

Hey @ejgallego, thanks for the fast response! I'm currently working in a group that relies on QuantumLib, which has only been thoroughly tested for Coq versions 8.12 through 8.15. As a result, the rest of my team and myself have all been using Coq 8.15, rather than any newer versions.

[Alizter]

I think this is because the flake we include is really just a development flake, only exposing devShell for nix develop. I'll try to take a look at some point and see how we can fix nix build. The same issue occurs on main when doing

nix build github:ejgallego/coq-lsp

[Zimmi48]

@kylechui Perhaps you would be better served by extending the nixpkgs expression of coq-lsp to include support for Coq 8.15: https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/coq-lsp/default.nix

[kylechui]

@Zimmi48 Yeah I would definitely be open to trying to submit a PR to nixpkgs! Right now I have coq-lsp manually packaged using pkgs.coq_8_15 in my flake's devShell and things seem to be... mostly working. I'll take a look at some of the contribution materials; I imagine testing could be done by adding my fork as an input to my NixOS's configuration flake? Any advice would be much appreciated.

@ejgallego Notably, my friend patched coq-lsp with a few changes in order to have it run at all with pkgs.coq_8_15 from nixpkgs; here's his fork. I suspect that perhaps Coq 8.15's version of serlib does not yet support some functions that you call in your code, and my friend regressed those changes. However, I'm still getting these warnings when I open any file importing modules from QuantumLib.

Thanks to both of you!

[ejgallego]

Hi @kylechui , sorry indeed for the late reply (due to holidays in my area), and thanks for the patch!

Indeed, while coq-8.15 is supported, there is some more work to do to make it fully usable, in particular:

• coq-serapi needs a new release with backports from 8.16
• coq itself needs some important patches backported from 8.19, fixing critical bugs with async interruptions and grammar, note that a branch already exists with these backports for 8.16.

That's not too hard to do, but on the other hand, it may be worth it to jump to 8.16 (note that for sure you want to use the patched Coq)

Indeed it seems to me that having a fully working version for 8.15 could be worth it, so I'll try.

But note that unless we get some help, I'll have to drop support for Coq < 8.17 in the 0.2.0 series, it is just more work than what I can handle.

[kylechui]

No worries! The main reason I'm looking at 8.15 is because the library I'm depending on hasn't really been tested extensively on 8.16 and beyond. It may be true that things will "just work", but I'd rather not test it at the moment (as there will be friction convincing others to also switch to 8.16). It's perfectly understandable that you drop support for < Coq 8.17 in the future; I really appreciate all your work on this project! For the time being, I'll just continue using my friend's fork; if I have extra bandwidth I'll try to figure out where these extra serlib warnings are coming from on my end.