Stream: Coq devs & plugin devs

Topic: Weird CI error w.r.t. warnings


view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:05):

Can somebody explain the CI error from https://github.com/coq/coq/pull/15258/checks?check_run_id=4350699723 ?

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:06):

It seems that a deprecated OCaml warning is triggered, but it's explicitly deactivated via an attribute, and it only fails on plugin-tutorial.

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:06):

The same line goes through happily in all other runs.

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 13:30):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:33):

OK, while we're at it with the CI Q&A I can't compile quickchick locally

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:33):

I get

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"

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:33):

How come this works on the remote CI?

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 13:34):

(I confirmed I get the warning with 4.05 and not 4.06)

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:35):

@Gaëtan Gilbert about the warning, why doesn't this pop up elsewhere? We're using the very same syntax in some other places.

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:35):

Or is it just because it's applied to modules?

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 13:36):

probably because it's a module yes (can't see what else it could be)

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:36):

Gah.

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:37):

There are many people opening that stuff when this is not needed, this is ruining the purpose of the warning

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 13:38):

??

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:38):

Due to the porting scheme, quite a few devs where doing open Tacmach.Old even though it was not relevant anymore

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:38):

(nobody cares about the OCaml warnings)

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 13:39):

what's ruining what?

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:39):

that if I can't mark the module deprecated, there will be people silently relying on it

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:39):

(the alternative being deprecating all the entries of the module)

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 13:40):

just do

[@@@ocaml.warning "-3"]
open Tacmach.Old
[@@@ocaml.warning "-3"]

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:40):

?

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:40):

this will work?

view this post on Zulip Gaëtan Gilbert (Nov 29 2021 at 13:40):

y

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:41):

OK, let's try

view this post on Zulip Pierre-Marie Pédrot (Nov 29 2021 at 13:41):

And regarding quickchick?


Last updated: Dec 05 2023 at 05:01 UTC