Adapt to coq/coq#19346 (ComInductive flags)

[SkySkimmer]

No description provided.

[SkySkimmer]

I let you add the optcomp stuff because I really don't want to deal with it.

[gares]

on it

[ppedrot]

Please merge now. (For some reason I still don't have write rights to coq-elpi.)

[gares]

Damn, we should look into that.

[erikmd]

Hi @gares,
Given this overlay is not present in the latest release of coq-elpi, 2.2.1:
the mathcomp/mathcomp:2.2.0-coq-dev and mathcomp/mathcomp-dev:coq-dev FTBFS.

would it make sense to release a coq-elpi.2.2.1 compatible with coq-dev ?

otherwise, no worries, but I'll need to remove the mathcomp/*:coq-dev images from Docker Hub.

[gares]

I can do another release, but a released version can only work on coq dev up to the day it was released, I'm not so sure I understand your request. For coq master you should track coq-elpi master

[erikmd]

Hi, thanks for your reply, to better explain my request:

1. mathcomp/mathcomp provides images of stable releases of mathcomp + coq-dev,
2. mathcomp/mathcomp-dev provides images of mathcomp master + coq-dev

it happens 1. and 2. don't compile anymore because in both cases, opam installs coq-hierarchy-builder.dev, which subsequently installs coq-elpi.2.2.1, which fails.

See the two logs:

• https://gitlab.inria.fr/math-comp/docker-mathcomp/-/jobs/4561637
• https://gitlab.inria.fr/math-comp/math-comp/-/jobs/4561638

I don't know what's the best solution, but note that this issue may occur again later on, given coq-elpi is a main dependency of mathcomp.

[SkySkimmer]

The solution is probably coq/opam#3102

[erikmd]

Maybe, the opam constraints could induce that coq-hierarchy-builder.dev installs coq-elpi.dev, so that the merge of overlay could straightforwardly solve the issue in the docker-mathcomp builds? @gares, WDYT?

[gares]

Maybe, the opam constraints could induce that coq-hierarchy-builder.dev installs coq-elpi.dev, so that the merge of overlay could straightforwardly solve the issue in the docker-mathcomp builds? @gares, WDYT?

I don't know how to do that, but if you do, then go ahead, it seems the right fix

[SkySkimmer]

There shouldn't be a need to change HB, only make the coq-elpi released version package stop claiming to be compatible with arbitrarily high coq versions when it's only compatible with coq versions that were already released when the coq-elpi was released.

[erikmd]

I agree with you, this should be enough.

(I restarted the mathcomp+coq-dev builds, hopefully the build/deployment will be OK now.)