Michael Soegtrop (Jun 13 2022 at 12:19): 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.
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?
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.
Guillaume Melquiond (Jun 13 2022 at 13:27):I might have some time at the end of next week.
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.
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
Théo Zimmermann (Jun 13 2022 at 17:09):The same recently happened to Gappa BTW: https://github.com/coq/coq/pull/16102
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.
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.
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.
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.
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?
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: Jun 09 2023 at 07:01 UTC