Broken in Coq CI

[SkySkimmer]

eg https://gitlab.inria.fr/coq/coq/-/jobs/4793860

File "./classical/classical_orders.v", line 364, characters 26-30:
Error:
In environment
d : order.Order.disp_t
K : nat -> finOrderType d
n : Order.NatOrder.Datatypes_nat__canonical__Order_POrder
x : big_lexi_order (fun x : nat => K x)
x0 : ?T
n0 : nat
The term "\bot%O" has type "Order.BPOrder.sort ?s"
while it is expected to have type "Equality.sort (K n0)".

PRs merged in coq since the last success do not seem to be related, this may be due to a change in mathcomp's main repo or a change in mathcomp analysis.

[affeldt-aist]

Thanks for letting us know! @proux01 @zstone1

[zstone1]

@SkySkimmer I've got #1335 which should fix it by just removing that lemma. I don't need it right now, so it's fine. But I'm a bit curious why it didn't break anything (new) on our side. I'm hoping to see if there's an easy way to prevent us breaking it again. Can you share a little more about the configuration of the CI runner that failed, like what version of Coq, mathcomp, and HB was it using?

[SkySkimmer]

It uses master for everything.

[proux01]

Yes, this should be tested in CI here. I guess someone accidentaly merged a PR with a red CI.

[zstone1]

Ah, I see what's going on. When I merged b685927 the broken CI was clearly HB issues, and not related to analysis

make -f Makefile.coq install
make[1]: Entering directory '/build/source'
structures.vo does not exist
structures.v does not exist
structures.glob does not exist

But that prevented the master CI pipeline from running at all. which is why this \bot thing made it through

[proux01]

@SkySkimmer should be fixed, sorry we should be more careful about not breaking master