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.

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*)
```

while ugly, this only suppresses warnings about this deprecation.

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

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.

@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 :)

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

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.

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

(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)

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

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

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

(IIRC at least Emilio?)

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

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.

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:

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

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

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

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