Stream: Coq devs & plugin devs

Topic: Repeated deprecation warnings


view this post on Zulip Karl Palmskog (Feb 05 2023 at 11:55):

I don't know if this should be considered an issue (I can report it if so), but is there any obvious reason why deprecation warnings are always repeated 2 or 3 times when running coqc on them? For example:

File "./coq/Algorithms/KVSAlg1.v", line 2287, characters 14-27:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./coq/Algorithms/KVSAlg1.v", line 2287, characters 14-27:
Warning: Notation lt_n_Sm_le is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]

view this post on Zulip Gaëtan Gilbert (Feb 05 2023 at 11:59):

that's probably the thing where ltac does the intern phase twice

view this post on Zulip Karl Palmskog (Feb 05 2023 at 12:03):

ah, I think I found it: https://github.com/coq/coq/issues/7861

I will at least make a comment to flag up this is a hassle when fixing deprecations.

view this post on Zulip Karl Palmskog (Feb 05 2023 at 12:10):

and for the record, I would strongly prefer a central workaround, rather than that all of: coq_makefile, coq-lsp, ProofGeneral, etc., do their own workaround.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 05 2023 at 12:20):

Yeah it is so annoying we didn't manage to fix this.


Last updated: Dec 06 2023 at 14:01 UTC