Pierre-Marie Pédrot (Nov 29 2021 at 13:05): 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 ?
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.
Pierre-Marie Pédrot (Nov 29 2021 at 13:06):The same line goes through happily in all other runs.
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
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
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"
How come this works on the remote CI?
Gaëtan Gilbert (Nov 29 2021 at 13:34):(I confirmed I get the warning with 4.05 and not 4.06)
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.
Pierre-Marie Pédrot (Nov 29 2021 at 13:35):Or is it just because it's applied to modules?
Gaëtan Gilbert (Nov 29 2021 at 13:36):probably because it's a module yes (can't see what else it could be)
Pierre-Marie Pédrot (Nov 29 2021 at 13:36):Gah.
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
Gaëtan Gilbert (Nov 29 2021 at 13:38):??
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
Pierre-Marie Pédrot (Nov 29 2021 at 13:38):(nobody cares about the OCaml warnings)
Gaëtan Gilbert (Nov 29 2021 at 13:39):what's ruining what?
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
Pierre-Marie Pédrot (Nov 29 2021 at 13:39):(the alternative being deprecating all the entries of the module)
Gaëtan Gilbert (Nov 29 2021 at 13:40):just do
[@@@ocaml.warning "-3"]
open Tacmach.Old
[@@@ocaml.warning "-3"]
?
Pierre-Marie Pédrot (Nov 29 2021 at 13:40):this will work?
Gaëtan Gilbert (Nov 29 2021 at 13:40):y
Pierre-Marie Pédrot (Nov 29 2021 at 13:41):OK, let's try
Pierre-Marie Pédrot (Nov 29 2021 at 13:41):And regarding quickchick?
Last updated: Dec 05 2023 at 05:01 UTC