Stream: Hierarchy Builder devs & users

Topic: regression in graph-theory related to HB


view this post on Zulip Karl Palmskog (Oct 02 2021 at 13:17):

@Enrico Tassi @Christian Doczkal looks like there is a problem with graph-theory (0.8 release on 8.13) that may be due to the recent release of HB:

Error: The reference Elabel.Exports.eqv' was not found in the current environment.

See the install output here

view this post on Zulip Enrico Tassi (Oct 02 2021 at 14:06):

Hum, let's see if we can chat next week @Christian Doczkal , it will be simpler.
Maybe we just changed the name of the exports module (split it into two), but that should be an implementation detail. I mean eqv' is part of the API, it's exact path not really.

view this post on Zulip Enrico Tassi (Oct 02 2021 at 14:06):

Maybe @Cyril Cohen can move this the HB stream.

view this post on Zulip Enrico Tassi (Oct 02 2021 at 14:32):

FTR, the failing is gone for good in master, so I guess we just need a tag/release from @Christian Doczkal

view this post on Zulip Notification Bot (Oct 04 2021 at 07:56):

This topic was moved here from #Coq devs & plugin devs > regression in graph-theory related to HB by Cyril Cohen

view this post on Zulip Christian Doczkal (Oct 04 2021 at 08:37):

@Karl Palmskog @Enrico Tassi : The latest release of coq-graph-theory is 0.9, is there there any problem with this release and the current stable release of HB?

view this post on Zulip Enrico Tassi (Oct 04 2021 at 08:38):

Ah, 0.8 is not the last one. Then I think it's just the constraints which are not enough strict.

view this post on Zulip Enrico Tassi (Oct 04 2021 at 08:39):

0.8 should depend on HB < 1.2 I guess

view this post on Zulip Enrico Tassi (Oct 04 2021 at 08:39):

Even if the fix seems trivial (Arguments some.private.name -> Arguments name).

view this post on Zulip Christian Doczkal (Oct 04 2021 at 08:40):

Actually, I think it rules out 1.1.0 explicitly, so it probably should depend on <= 1.0.0 or so.

view this post on Zulip Karl Palmskog (Oct 06 2021 at 08:17):

could someone submit a fix to the 0.8 opam package? It's the only version that supports Coq 8.11, so not unrealistic that someone might want to install it.

view this post on Zulip Karl Palmskog (Oct 17 2021 at 18:17):

The goal of the released Coq opam archive is that any user should be able to do opam install <package-name>.<package-version> and not have errors during the build (impossibility of installation is fine). Hence, I will remove the coq-graph-theory.0.8 package tomorrow Monday Oct 18 evening unless it's fixed by then. If removed, it can be re-added when constraints are fixed (or not, at your discretion, since a newer version of graph-theory is available).


Last updated: Mar 29 2024 at 06:39 UTC