Stream: Coq devs & plugin devs

Topic: Warnings in compat theories


view this post on Zulip Pierre-Marie Pédrot (Dec 15 2022 at 11:19):

Since recently I'm getting annoying warnings in the compilation version compatibility files

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2022 at 11:19):

e.g.

File "./Coq816.v", line 13, characters 0-33:
Warning: Trying to mask the absolute name "Coq.Lists.ListSet"!
[masking-absolute-name,deprecated]

view this post on Zulip Pierre-Marie Pédrot (Dec 15 2022 at 11:20):

any idea of the root cause?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2022 at 11:23):

I don't get these

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2022 at 11:25):

Oh wait I just got them

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2022 at 11:26):

Most likely candidate is #16945

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2022 at 11:27):

or #16926

view this post on Zulip Emilio Jesús Gallego Arias (Dec 15 2022 at 11:30):

tho indeed we don't seem to compile the stdlib with -warn-error

view this post on Zulip Gaëtan Gilbert (Dec 15 2022 at 12:17):

Emilio Jesús Gallego Arias said:

tho indeed we don't seem to compile the stdlib with -warn-error

we do AFAICT at least in dev mode
I used a deprecated thing in Datatypes.v and got

        coqc theories/Init/Datatypes.{glob,vo,vos} (exit 1)
File "./Datatypes.v", line 516, characters 18-29:
Error: Notation prodT_curry is deprecated since 8.13. Use uncurry instead.
[deprecated-syntactic-definition,deprecated]

view this post on Zulip Gaëtan Gilbert (Dec 15 2022 at 12:18):

problem is coq817.v restores the warnings by doing Global Set Warnings "masking-absolute-name".

view this post on Zulip Gaëtan Gilbert (Dec 15 2022 at 12:24):

https://github.com/coq/coq/pull/17000


Last updated: May 28 2023 at 16:30 UTC