I just noticed that `coq-hierarchy-builder.dev`

does not build against `coq.dev`

and `coq-elpi.dev`

, breaking the "dev" CI for coq-graph-theory, which is based on the `mathcomp-dev:coq-dev`

docker image. Looking at the CI setup of HB, I don't even see HB master testing against Coq master. Should I just abandon testing against `coq.dev`

for the time being?

(cf. https://github.com/coq-community/graph-theory/pull/15/checks?check_run_id=2288891748)

does coq-hierarchy-builder.dev point to the coq-master branch? (same for coq-elpi.dev)?

This one seems wrong [coq-hierarchy-builder.dev] synchronised from git+https://github.com/math-comp/hierarchy-builder.git#master

indeed a while back coq-elpi/coq-master got an update which was breaking hb, and I think I did fix it, but not in master, which is for coq.8.13, but in coq-master, which is for 8.14

IMO you should fix HB .dev package

or add another one pointing to the desired branch

https://github.com/coq/opam-coq-archive/pull/1680

it would be nice if you could actually test that this solves your problem

Ah, I hadn't realized that there was a `coq-master`

branch. That explains a lot. Indeed, this compiles and works, thanks!

And the good news is, that coq-master does not run against the "regression" in 1.1.0 that makes this mixin declaration throw a type error involving phantom types.

I guess it's your choice whether HB.dev points to master or coq-master, but for CI reasons coq-master seems preferable. :shrug:

I summon @Cyril Cohen to add yor graph library to our CI

In theory, 1.1.0 got much better at type inference of mixins, so the regressions is not expected.

Our CI does not test agains coq dev + coq-elpi dev... should it?

I'm a tiny bit afraid to mess up with the CI in the middle of the porting week though :-/

I'll try though

Don't worry, I need to fix a few things before my library will work again with coq-master. So you can wait until after the porting week.

Cyril Cohen said:

Our CI does not test agains coq dev + coq-elpi dev... should it?

Well, there is the `mathcomp-dev/coq-dev`

OPAM docker image that I have been using for CI, where opam tries to install a version of HB that builds against coq.dev. Presumably, this only works using coq-elpi.dev. So I advocate for the CI of HB testing this combination.

Last updated: Jan 29 2023 at 16:02 UTC