Stream: Hierarchy Builder devs & users

Topic: Hierachy Builder and coq master


view this post on Zulip Christian Doczkal (Apr 07 2021 at 16:09):

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)

view this post on Zulip Enrico Tassi (Apr 07 2021 at 17:04):

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

view this post on Zulip Enrico Tassi (Apr 07 2021 at 17:06):

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

view this post on Zulip Enrico Tassi (Apr 07 2021 at 17:07):

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

view this post on Zulip Enrico Tassi (Apr 07 2021 at 17:07):

IMO you should fix HB .dev package

view this post on Zulip Enrico Tassi (Apr 07 2021 at 17:08):

or add another one pointing to the desired branch

view this post on Zulip Enrico Tassi (Apr 07 2021 at 17:55):

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

view this post on Zulip Enrico Tassi (Apr 07 2021 at 17:55):

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

view this post on Zulip Christian Doczkal (Apr 07 2021 at 19:43):

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.

view this post on Zulip Christian Doczkal (Apr 07 2021 at 19:44):

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

view this post on Zulip Enrico Tassi (Apr 07 2021 at 20:08):

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

view this post on Zulip Enrico Tassi (Apr 07 2021 at 20:08):

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

view this post on Zulip Cyril Cohen (Apr 07 2021 at 20:41):

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

view this post on Zulip Cyril Cohen (Apr 07 2021 at 20:42):

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

view this post on Zulip Cyril Cohen (Apr 07 2021 at 20:44):

I'll try though

view this post on Zulip Christian Doczkal (Apr 07 2021 at 21:03):

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.

view this post on Zulip Christian Doczkal (Apr 08 2021 at 08:20):

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