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: Oct 13 2024 at 01:02 UTC