Karl Palmskog (Feb 05 2023 at 11:55): 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]
that's probably the thing where ltac does the intern phase twice
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.
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.
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