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]
that's probably the thing where ltac does the intern phase twice
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.
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.
Yeah it is so annoying we didn't manage to fix this.
Last updated: Dec 06 2023 at 14:01 UTC