Robbert Krebbers (Apr 25 2023 at 10:21): 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.
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*)
while ugly, this only suppresses warnings about this deprecation.
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
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.
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 :)
Pierre Roux (Apr 25 2023 at 13:17):Sure, this often works, I'm only pointing that this is not guaranteed.
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.
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++.
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)
Pierre Roux (Apr 25 2023 at 14:03):I never remember where this deprecation policy is written. @Théo Zimmermann probably knows better.
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)
Paolo Giarrusso (Apr 25 2023 at 14:30):I've seen part of the core team is against conditional compilation support in Coq
Paolo Giarrusso (Apr 25 2023 at 14:30):(IIRC at least Emilio?)
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).
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.
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:
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
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.
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
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: Oct 13 2024 at 01:02 UTC