Can somebody explain the CI error from https://github.com/coq/coq/pull/15258/checks?check_run_id=4350699723 ?
It seems that a deprecated OCaml warning is triggered, but it's explicitly deactivated via an attribute, and it only fails on plugin-tutorial.
The same line goes through happily in all other runs.
probably an issue with ocaml 4.05.0
note that the warning appears in build:base https://gitlab.com/coq/coq/-/jobs/1827779478#L506
(build:base runs dune in release profile so no warn-error)
the dune job is on 4.13.0
OK, while we're at it with the CI Q&A I can't compile quickchick locally
cppo -V COQ:8.16+alpha -V OCAML:4.07.1 -n -o plugin/coqsimpleio.mlg plugin/coqsimpleio.mlg.cppo Error: Invalid version specification: "COQ:8.16+alpha"
How come this works on the remote CI?
(I confirmed I get the warning with 4.05 and not 4.06)
@Gaëtan Gilbert about the warning, why doesn't this pop up elsewhere? We're using the very same syntax in some other places.
Or is it just because it's applied to modules?
probably because it's a module yes (can't see what else it could be)
There are many people opening that stuff when this is not needed, this is ruining the purpose of the warning
Due to the porting scheme, quite a few devs where doing
open Tacmach.Old even though it was not relevant anymore
(nobody cares about the OCaml warnings)
what's ruining what?
that if I can't mark the module deprecated, there will be people silently relying on it
(the alternative being deprecating all the entries of the module)
[@@@ocaml.warning "-3"] open Tacmach.Old [@@@ocaml.warning "-3"]
this will work?
OK, let's try
And regarding quickchick?
Last updated: Feb 05 2023 at 22:03 UTC