fixup #775

[gares]

that was clearly incomplete

[gares]

@rtetley we need a CI job with warn-as-errors, in elpi I do have:

https://github.com/LPCIC/elpi/blob/702576e6521a6a5b5ed2dfa5886d0de704552af4/dune#L12-L13

and then a job

https://github.com/LPCIC/elpi/blob/702576e6521a6a5b5ed2dfa5886d0de704552af4/.github/workflows/main.yml#L24-L27

and a run line that calls dune with --profile ${{ matrix.profile }}. Ideally it should use a very recent ocaml version, since new warnings are constantly added.

[gares]

Such a ci job would have detected the author of the PR did introduce warnings (that happened to be errors)

[rtetley]

I agree, I'll take care of it. They merged the PR without the CI working anyways so... Should we go back to having a coq-master branch ?

[rtetley]

Something like #782 ?

[gares]

I agree, I'll take care of it. They merged the PR without the CI working anyways so... Should we go back to having a coq-master branch ?

I think we should make sure that the coq ci job does not break the other supported versions. My guess is that if we put the sources in a directory together with the stable version of Coq and we run dune build check we can do that quite fast (like 1 minute). Then we should detect this error and print "Use optcomp: put the change in a [%%if] block".

@SkySkimmer WDYT?

[SkySkimmer]

IDK

[gares]

with this it works: ocaml/dune#10631 in less than 1 minute
until it is merged, we cannot do much better than the status quo