Stream: Coq devs & plugin devs

Topic: Coq Interval master does not build with Coq 8.16+rc1


view this post on Zulip Michael Soegtrop (Jun 13 2022 at 12:19):

@Guillaume Melquiond : I am currently preparing a Coq Platform pick for Coq 8.16+rc1 intended for package maintainers. One issue is that Coq Interval master does not build with 8.16 cause of the renaming/restructuring of the Int63 module. I guess you are aware of this and wonder if you already have a date for an update.

view this post on Zulip Ali Caglayan (Jun 13 2022 at 12:36):

Flocq has some compatibility files for Int63: https://gitlab.inria.fr/flocq/flocq/-/tree/master/src/IEEE754 Perhaps you need to use those?

view this post on Zulip Guillaume Melquiond (Jun 13 2022 at 13:26):

No, I was not aware of the issue. Presumably, the same configure machinery as in Flocq will have to be used in CoqInterval.

view this post on Zulip Guillaume Melquiond (Jun 13 2022 at 13:27):

I might have some time at the end of next week.

view this post on Zulip Michael Soegtrop (Jun 13 2022 at 17:00):

No, I was not aware of the issue.

Should I add coq-interval to Coq CI?

I might have some time at the end of next week.

I see if I can handle it then.

view this post on Zulip Théo Zimmermann (Jun 13 2022 at 17:09):

Interval used to be part of Coq CI but was removed at the request of Guillaume: https://github.com/coq/coq/pull/14437

view this post on Zulip Théo Zimmermann (Jun 13 2022 at 17:09):

The same recently happened to Gappa BTW: https://github.com/coq/coq/pull/16102

view this post on Zulip Michael Soegtrop (Jun 14 2022 at 09:02):

I see - well every package maintainer must decide what is most convenient. It is only a small amount of extra work to report it for the RC1 as part of the Coq Platform releases.

Coq Interval would be interesting to have in Coq CI though, because it already found two (afair) regressions in native integer arithmetic which lead to proofs of False.

view this post on Zulip Michael Soegtrop (Jun 14 2022 at 09:32):

@Guillaume Melquiond : since the majority of packages need adjustments for 8.16+rc1 I will wait until end of June with a Coq Platform dev-preview release. So I won't look into coq-interval until then.

view this post on Zulip Michael Soegtrop (Jul 06 2022 at 16:30):

@Guillaume Melquiond : just wanted to sync on this. Did you have time to work on this?

From a quick look at the logs it seems to be a plugin name issue.

view this post on Zulip Guillaume Melquiond (Jul 06 2022 at 17:28):

The plugin name is the easy part. There are a lot more issues. Those are hopefully fixed on the coq-8.16 branch. But anyway, due to a bug in Coq, Interval is not usable with Coq 8.16+rc1.

view this post on Zulip Michael Soegtrop (Aug 08 2022 at 09:19):

@Guillaume Melquiond : I just wanted to ask what the status of this is.
@Pierre-Marie Pédrot : what is the status of the Coq issue Guillaume mentioned above?

view this post on Zulip Pierre-Marie Pédrot (Aug 08 2022 at 10:05):

I think this was https://github.com/coq/coq/issues/16284 and it's fixed as of 8.16.0.


Last updated: Feb 06 2023 at 18:03 UTC