Stream: Coq users

Topic: Backwards compatibility w.r.t. Div0 without warnings


view this post on Zulip Robbert Krebbers (Apr 25 2023 at 10:21):

std++ and Iris aim to support the last 3 released Coq versions, and have them compile without warnings. Since Coq 8.17 has just been released, we want to support it, but are having issues due to the recent Div0 changes in https://github.com/coq/coq/pull/16203

We get the following warnings:

Warning: Notation Nat.add_mod_idemp_l is deprecated since 8.17.
Use Div0.add_mod_idemp_l instead.
[deprecated-syntactic-definition,deprecated]
File "./stdpp/numbers.v", line 1472, characters 28-47:

We are wondering what is the proper way to fix or to suppress these warnings? The suggestion of using Div0. or Module Nat := Nat.Div0 (from the Coq changelog) does not work with Coq 8.16 or 8.15, so that violates our policy to support the last 3 Coq versions.

We could suppress deprecated-syntactic-definition entirely, but then we do not get notified about other deprecation warnings that we could fix.

Does any of you have an idea how we could suppress or fix just the Div0 warnings? Thank you.

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 10:57):

here's an ugly starting point — this defines an alias that you could use internally without warnings — in coqtop or coqc, AFAICT:

#[local] Set Warnings "-deprecated-syntactic-definition".
#[local] Notation Nat_add_mod_idemp_l := Nat.add_mod_idemp_l.
#[local] Set Warnings "deprecated-syntactic-definition".

(* test *)
Check Nat.add_mod_idemp_l. (* still warns, do not use *)
Check Nat_add_mod_idemp_l. (* does not warn*)

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 10:59):

while ugly, this only suppresses warnings about this deprecation.

view this post on Zulip Gaëtan Gilbert (Apr 25 2023 at 11:00):

https://github.com/coq/coq/pull/17489 was recently merged and should help with these types of problems
until then you have to disable the whole warning or use a workaround like Paolo provided

view this post on Zulip Pierre Roux (Apr 25 2023 at 12:09):

Also note that Coq deprecation policy is to enable easy support of 2 consecutive versions (maybe even only one, I'm not sure). You might be able to easily support 3 but that's pure luck.

view this post on Zulip Robbert Krebbers (Apr 25 2023 at 13:14):

@Paolo Giarrusso Thanks, let me try that.

@Gaëtan Gilbert Good to know about since. It still would be nicer if there were categories for the notation deprecation warnings, so that you can disable them on a more fine-grained level. Has anyone thought about that?

@Pierre Roux We have been able to support even more than 3 released versions of Coq for std++ and Iris over the years without many problems. So there is constructive evidence of this being possible for sizeable developments :)

view this post on Zulip Pierre Roux (Apr 25 2023 at 13:17):

Sure, this often works, I'm only pointing that this is not guaranteed.

view this post on Zulip Ralf Jung (Apr 25 2023 at 13:49):

Pierre Roux said:

Also note that Coq deprecation policy is to enable easy support of 2 consecutive versions (maybe even only one, I'm not sure). You might be able to easily support 3 but that's pure luck.

where can I learn more about this policy? This is the first time I hear about this.

view this post on Zulip Ralf Jung (Apr 25 2023 at 13:50):

Supporting only 2 versions seems a bit too aggressive to me for widely used foundational libraries such as std++.

view this post on Zulip Ralf Jung (Apr 25 2023 at 13:50):

(of course if coq_makefile supported some form of version-dependent compilation we could fairly easily do this without coq itself having to remain compatible)

view this post on Zulip Pierre Roux (Apr 25 2023 at 14:03):

I never remember where this deprecation policy is written. @Théo Zimmermann probably knows better.

view this post on Zulip Pierre Roux (Apr 25 2023 at 14:04):

(version-dependent compilation is done with autoconf in Flocq, I wouldn't call that extremely convenient though)

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 14:30):

I've seen part of the core team is against conditional compilation support in Coq

view this post on Zulip Paolo Giarrusso (Apr 25 2023 at 14:30):

(IIRC at least Emilio?)

view this post on Zulip Théo Zimmermann (Apr 25 2023 at 15:09):

Ralf Jung said:

Pierre Roux said:

Also note that Coq deprecation policy is to enable easy support of 2 consecutive versions (maybe even only one, I'm not sure). You might be able to easily support 3 but that's pure luck.

where can I learn more about this policy? This is the first time I hear about this.

I think the only place where this was really written down was my PhD thesis: https://theses.hal.science/tel-02451322 (section 3.6.3.1).

view this post on Zulip Théo Zimmermann (Apr 25 2023 at 15:10):

In practice, we often take longer than two versions to remove a feature. However, we do have a systematic process to remove old -compat options.

view this post on Zulip Théo Zimmermann (Apr 25 2023 at 15:13):

It really depends on how much used a feature is in the end. If it is not very much used, we might deprecate it and remove it soon after. If it used in high profile projects and that the replacement has not been available for a long time, it will take longer just to prepare the overlays and get them approved :stuck_out_tongue:

view this post on Zulip Pierre Roux (Apr 26 2023 at 15:01):

Théo Zimmermann said:

I think the only place where this was really written down was my PhD thesis: https://theses.hal.science/tel-02451322 (section 3.6.3.1).

Thanks, maybe we should link that in the refman: https://github.com/coq/coq/pull/17532

view this post on Zulip Pierre Roux (Apr 26 2023 at 15:03):

@Ralf Jung I understand you are requesting the deprecation policy to be changed from "at least 2 consecutive versions" to "at least 3". You should probably put the point to the agenda of some Coq weekly call so that is is discussed.

view this post on Zulip Karl Palmskog (Apr 26 2023 at 17:36):

we also documented the compatibility policy in the Platform paper (p. 3): https://arxiv.org/pdf/2203.09835.pdf

view this post on Zulip Ralf Jung (Apr 28 2023 at 15:30):

Pierre Roux said:

Ralf Jung I understand you are requesting the deprecation policy to be changed from "at least 2 consecutive versions" to "at least 3". You should probably put the point to the agenda of some Coq weekly call so that is is discussed.

the policy came as a surprise to me, though for my own projects I could probably live with it. but it means we should probably change our std++ policy to also only cover two coq versions. I will raise this question with our community.


Last updated: Jun 15 2024 at 08:01 UTC