@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.

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

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

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

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.

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

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

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.

@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.

@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.

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.

@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?

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

Last updated: Oct 13 2024 at 01:02 UTC