Stream: Coq Platform devs & users

Topic: Package picking 8.13~2021.09


view this post on Zulip Michael Soegtrop (Sep 24 2021 at 10:34):

@Enrico Tassi : according to opam, the latest version of hierarchy builder (1.1.0) is not compatible with the latest few versions of coq-elpi (1.11.X or 1.10.X). Is the opam file accurate?

It says: depends: [ "coq-elpi" {= "1.6.2~8.11" | = "1.8.2~8.12" | (>= "1.9.5" & < "1.10~")} ]

view this post on Zulip Enrico Tassi (Sep 24 2021 at 10:34):

I'm working on it, please be patient ;-)

view this post on Zulip Michael Soegtrop (Sep 24 2021 at 10:36):

Note: this is not for 8.14, but for an updated pick for 8.13.

view this post on Zulip Enrico Tassi (Sep 24 2021 at 10:41):

I'll make a release of HB which works with both 8.13 and 8.14 (with the corresponding coq-elpi versions)

view this post on Zulip Enrico Tassi (Sep 24 2021 at 10:41):

would that work?

view this post on Zulip Michael Soegtrop (Sep 24 2021 at 10:46):

Yes sure, but if you want it for the 8.13 updated pick, it should be quick. For 8.14 the schedule is fairly relaxed. I wanted to publish 2021.09 with the updated 8.13 pick and an 8.14 preview pick early next week.

view this post on Zulip Michael Soegtrop (Sep 24 2021 at 10:47):

I don't see a good reason for putting yourself under too much pressure - I think the latest working version is quite an improvement over 2021.02. Namely coq-elpi.1.9.7 elpi.1.13.7 coq-hierarchy-builder.1.1.0 vs coq-elpi.1.8.1 elpi.1.12.0 coq-hierarchy-builder.1.0.0

view this post on Zulip Michael Soegtrop (Sep 24 2021 at 10:48):

The 8.14 pick can use different versions.

view this post on Zulip Enrico Tassi (Sep 24 2021 at 10:57):

I agree the pick up there is much better than before. But lets see what I can do...

view this post on Zulip Michael Soegtrop (Sep 24 2021 at 10:58):

Sure. I will use the above pick for the time being. Deadline is Monday or so.

view this post on Zulip Enrico Tassi (Sep 24 2021 at 20:19):

So, HB 1.2.0 should be the pick for 8.13 and 8.14 (https://github.com/coq/opam-coq-archive/pull/1827).
Unfortunately the coq-opam-archive CI will not test the combination coq.8.14+rc1 + coq-elpi.1.11.2 + coq-hierarchy-builder.1.2.0 since the latter is not in extra-dev, but rather in released (since it also works with coq.8.13.2 + coq-elpi.1.11.1). I guess the platform CI will tell us if my testing was good or not...

view this post on Zulip Michael Soegtrop (Sep 26 2021 at 13:00):

@Enrico Tassi : thanks, works fine. Btw.: the previous HB version had build issues on Windows - I didn't investigate what it was. 1.2 works fine.


Last updated: Jan 30 2023 at 10:03 UTC