Jerome Hugues (Mar 16 2022 at 17:59): Jerome Hugues (Mar 16 2022 at 17:59):Hi,
I have setup a github action to build my project that relies on coq-json. It compiles fine with coq 8.14 and coq 8.15.
There is a compilation error with coq-dev docker container that appeared after the last successful build on March 3 and March 11 when I first spotted this issue. I am curious to know how to diagnose it to report it properly, if that is even relevant.
The build error is when I try to install coq-json using opam . I omitted some details, the full log is available here: https://github.com/Oqarina/oqarina/runs/5570892211?check_suite_focus=true
+ (script @ line 11) $ opam install -y -j 2 coq-oqarina --deps-only
[..]
#=== ERROR while compiling coq-json.dev =======================================#
# context 2.0.9 | linux/x86_64 | ocaml-variants.4.11.2+flambda | https://coq.inria.fr/opam/extra-dev#2022-03-16 12:00
# path ~/.opam/4.11.2+flambda/.opam-switch/build/coq-json.dev
[..]
# File "./Operator.v", line 20, characters 0-160:
# Error:
# This command does not support this attribute: deprecated (use a notation and deprecate that instead).
# [unsupported-attributes,parsing]
./Operator.v line 20 is
#[deprecated(since="8.14", note="Use Ascii.compare instead.")]
Definition ascii_compare (a b : ascii) : comparison :=
N.compare (N_of_ascii a) (N_of_ascii b).
From https://coq.inria.fr/refman/using/libraries/writing.html?highlight=deprecated#coq:attr.deprecated and the release notes, it does not seem there has been any change in this syntax. I am curious to know what could be the source of this. As far as I can tell, ascii_compare is not used in any notation in coq-json.
I am installing coq-json using + (script @ line 11) $ opam install -y -j 2 coq-oqarina --deps-only
and here is the relevant part in my opam file (I just noted a stupid issue on the dune version requirement)
depends: [
"dune" {>= "2.8" & > "2.5"}
"coq" {dev & >= "8.13"}
"coq-ext-lib" {dev}
"coq-simple-io" {>= "1.6.0"}
"coq-json" {dev}
"odoc" {with-doc}
]
It might also be the case that this could be ignored since the -dev branch should not be considered as stable in my case. I tried this to evaluate any impact in forthcoming version of Coq, nothing more.
Thanks
Ali Caglayan (Mar 16 2022 at 18:06):There has been a change. Definition was erroneously accepting the deprecated attribute which did nothing. It now rejects it properly.
Ali Caglayan (Mar 16 2022 at 18:07):The point of the warning is that you should define a notation for ascii_compare and deprecate that notation instead.
Jerome Hugues (Mar 16 2022 at 18:07):Oh, I see. I read too quickly the definition of the deprecated attribute. It applies to Ltac2 definition, not to Gallina (?) ones.
Ali Caglayan (Mar 16 2022 at 18:09):No, deprecated only works for regular Notation. When we deprecate things in the stdlib for example, we define a notation that has the old name and deprecate that.
Ali Caglayan (Mar 16 2022 at 18:10):Deprecation warnings for definitions (lemmas etc) haven't actually been implemented, so the previous behaviour was just doing nothing.
Ali Caglayan (Mar 16 2022 at 18:13):I've submitted an issue to coq-json https://github.com/liyishuai/coq-json/issues/3
Théo Zimmermann (Mar 16 2022 at 18:14):Actually, Jérôme is right Ltac2 also accept the deprecated attribute. At the moment, that's the only command besides notation commands that does. Ltac also does.
Notification Bot (Mar 16 2022 at 18:25):12 messages were moved from this topic to #Coq devs & plugin devs > deprecation for definitions by Ali Caglayan.
Jerome Hugues (Mar 16 2022 at 18:31):Thanks for the quick feedback!
Notification Bot (Mar 16 2022 at 18:31):Jerome Hugues has marked this topic as resolved.
Ali Caglayan (Mar 18 2022 at 09:05):The fix has been merged upstream https://github.com/liyishuai/coq-json/pull/4
Last updated: Oct 03 2023 at 04:02 UTC