deps bug (`coq-serapi` incompatible with newest `cmdliner`, making some Docker-Coq builds fail) + question

[erikmd]

Hi @ejgallego,

FYI after the bump of opam to 2.1.2 in coqorg/base (coq-community/docker-base#17), I rebuilt all coqorg/coq images (pipeline) but some jobs failed:

https://gitlab.com/coq-community/docker-coq/-/jobs/2284076471 https://gitlab.com/coq-community/docker-coq/-/jobs/2284076472

with the same error:

#=== ERROR while compiling coq-serapi.8.8.0+0.5.6 =============================#
# context              2.1.2 | linux/x86_64 | ocaml-variants.4.08.1+flambda | [https://opam.ocaml.org#cd8a40f4](https://opam.ocaml.org/#cd8a40f4)
# path                 ~/.opam/4.08.1+flambda/.opam-switch/build/coq-serapi.8.8.0+0.5.6
# command              /usr/bin/make -j2 TARGET=native
# exit-code            2
# env-file             ~/.opam/log/coq-serapi-180-78ccae.env
# output-file          ~/.opam/log/coq-serapi-180-78ccae.out
### output ###
# [...]
# File "sertop/sertop.ml", line 74, characters 2-11:
# 74 |   Term.info "sertop" ~version:sertop_version ~doc ~man
#        ^^^^^^^^^
# Error (alert deprecated): Cmdliner.Term.info
# Use Cmd.info instead.
# File "sertop/sertop.ml", line 77, characters 8-17:
# 77 |   match Term.eval sertop_cmd with
#              ^^^^^^^^^
# Error (alert deprecated): Cmdliner.Term.eval
# Use Cmd.v and one of Cmd.eval* instead.
# Command exited with code 2.
# make: *** [Makefile:34: sertop] Error 10

Given cmdliner's release notes, this non-backward-compatible change dates back to 1.1.0, so it seems it should suffice to add the constraint

  "cmdliner" {< "1.1.0"}

in opam-repository/packages/coq-serapi/coq-serapi.8.8.0+0.5.6/opam, and likewise in all coq-serapi opam releases.

I plan to open one such PR in opam-repository this Sunday, let me know if you object (or think my fix above is not the best fix?)

[erikmd]

BTW, apart from the issue for old releases I was talking about, the dev version of coq-serapi is also impacted, cf. e.g. this line: https://github.com/ejgallego/coq-serapi/blob/380586b0021c08c6e0dddb02e4210d7c0ec6789b/sertop/sertop_bin.ml#L84

[ejgallego]

Hi @erikmd , sorry for the lag with this. Indeed it seems to me that the right solution is to add the upper bound. I'll update the branches here when I get a minute. Thanks for the report.

[erikmd]

@ejgallego

I'll update the branches here when I get a minute.

BTW to ease this coq-serapi refactoring, feel free to draw some inspiration from the diff of PR https://github.com/ocaml-sf/learn-ocaml/pull/480, where @hernoufM contributed a similar cmdliner bump for learn-ocaml.

[erikmd]

Closing the issue which is solved now.

[ejgallego]

I reopen as I need to update the opam files here, thanks a lot @erikmd

[erikmd]

Ah indeed I see what you mean, sorry @ejgallego

So just to sum up, it seems there's some choice between:

1. either require "cmdliner" {>= "1.1.0"} (and replace the deprecated functions) as we'll do in learn-ocaml, to completely avoid the deprecation warnings and benefit from the new release features;
2. or adding an upper-bound "cmdliner {< "1.1.0"} in coq-serapi's main branch .opam (as we had to do for prev. releases)
3. or doing nothing for now… because it seems the deprecation warning is not fatal with in every context (see e.g. this log line 7148, albeit I didn't fully understood why they were not fatal?)

So… maybe solution 1. would be better(?)

[ejgallego]

That was fixed in 8.16, thanks and sorry for the trouble (better opam repos testing should prevent this in the future)