@Enrico Tassi I am currently preparing the Coq Platform pick for 8.17. Apparently there is no hierarchy builder version in opam which is compatible with a 8.17 compatible version of coq-elpi. Are you working on one? Should I just relax the restrictions?

@Michael Soegtrop This requires a version of coq-elpi for 8.17 (which @Enrico Tassi should release).

I did release a version of coq-elpi for 8.17, and the existing version of HB should just work

I'll look into it next week, but it should just be about relaxing a bound

Indeed, it was just a bound to relax, fixed (https://github.com/coq/opam-coq-archive/pull/2480)

@Pierre Roux @Enrico Tassi : thanks - that's what I guessed that it is just a version issue.

Btw.: I thought HB is mostly done by Enrico and Cyril, so I am a bit confused by the role of Pierre. May I ask how the responsibilities are for HB?

to list all the names: @Kazuhiko Sakaguchi was also involved in the development of the first version. @Pierre Roux did contribute some features more recently. @Thomas Portet is an Inria engineer which just started implementing some usability features / bugfixes

@Pierre Roux is also contributing to math-comp, and in particular to its port to HB.

Last updated: May 28 2023 at 18:29 UTC