Michael Soegtrop (Feb 24 2023 at 15:46): Michael Soegtrop (Feb 24 2023 at 15:46):@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?
Pierre Roux (Feb 24 2023 at 16:40):@Michael Soegtrop This requires a version of coq-elpi for 8.17 (which @Enrico Tassi should release).
Enrico Tassi (Feb 24 2023 at 17:04):I did release a version of coq-elpi for 8.17, and the existing version of HB should just work
Enrico Tassi (Feb 24 2023 at 17:05):I'll look into it next week, but it should just be about relaxing a bound
Pierre Roux (Feb 24 2023 at 21:02):Indeed, it was just a bound to relax, fixed (https://github.com/coq/opam-coq-archive/pull/2480)
Michael Soegtrop (Feb 27 2023 at 12:46):@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?
Enrico Tassi (Feb 27 2023 at 12:52):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: Apr 19 2024 at 14:02 UTC