Stream: math-comp analysis

Topic: ✔ broken opam package for 0.3.X


view this post on Zulip Karl Palmskog (Nov 24 2021 at 13:52):

As can be seen here the coq-mathcomp-analysis 0.3.10 package is broken since the dependency on coq-mathcomp-bigenough is no longer guaranteed to be installed. Previously, bigenough was installed as a dependency of finmap. But finmap 1.5.1 recently had its bigenough dependency removed.

cc: @Reynald Affeldt @Guillaume Claret

view this post on Zulip Reynald Affeldt (Nov 24 2021 at 14:05):

(thank you for the ping)

view this post on Zulip Karl Palmskog (Nov 24 2021 at 14:09):

sorry, I didn't want to cause a race for the PR.

view this post on Zulip Reynald Affeldt (Nov 24 2021 at 14:15):

anyway, mine seems wrong... :-/

view this post on Zulip Karl Palmskog (Nov 24 2021 at 14:25):

it seems to be some elpi issue, not with the change itself

view this post on Zulip Notification Bot (Nov 24 2021 at 15:51):

Karl Palmskog has marked this topic as resolved.

view this post on Zulip Notification Bot (Nov 25 2021 at 08:51):

Karl Palmskog has marked this topic as unresolved.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 08:52):

it looks like, unfortunately, more packages before 0.3.10 are affected by this, for example, 0.3.9 is marked as compatible with finmap 1.5.1.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 15:32):

now I think we can say this is resolved.

view this post on Zulip Notification Bot (Nov 25 2021 at 15:32):

Karl Palmskog has marked this topic as resolved.


Last updated: Aug 11 2022 at 01:03 UTC