Stream: Hierarchy Builder devs & users

Topic: Version for Coq 8.17


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Feb 24 2023 at 17:05):

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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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 21 2024 at 01:02 UTC