@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
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.
Maybe @Cyril Cohen can move this the HB stream.
FTR, the failing is gone for good in master, so I guess we just need a tag/release from @Christian Doczkal
This topic was moved here from #Coq devs & plugin devs > regression in graph-theory related to HB by Cyril Cohen
@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?
Ah, 0.8 is not the last one. Then I think it's just the constraints which are not enough strict.
0.8 should depend on HB < 1.2 I guess
Even if the fix seems trivial (Arguments some.private.name
-> Arguments name
).
Actually, I think it rules out 1.1.0 explicitly, so it probably should depend on <= 1.0.0 or so.
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.
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: Oct 13 2024 at 01:02 UTC