Hugo Herbelin (Nov 01 2023 at 19:56): Hugo Herbelin (Nov 01 2023 at 19:56):Hi, to add an "information" attribute (as discussed in Coq call) besides the "deprecation" attribute, what would be the best way to do? To avoid a proliferation of arguments to various functions and API, I guess the best way would be to keep the deprecation field present here and there and to change its type from Deprecation.t option to say Information.t option with Information.t typically defined by:
type t = Deprecation of Deprecation.t | Information of string option
Does this sound right?
Or would we like to possibly support both a deprecation and an information? Or to support several informations?
Gaëtan Gilbert (Nov 01 2023 at 20:07):what does Information None mean?
Hugo Herbelin (Nov 01 2023 at 20:09):Oups, sorry, I meant here without the option... going to edit.
Hugo Herbelin (Nov 01 2023 at 21:16):In the same vein, would it make sense to unify Declare.Info.t and DefAttributes.t (poly, inline, kind, scope, cleabody, deprecation, typing_flags, to which probably adding "using", "reversible" and "program"?)? I'm probably pushing open doors, but just to know how much it is in the air.
Pierre Roux (Nov 02 2023 at 10:06):Hugo Herbelin said:
type t = Deprecation of Deprecation.t | Information of string
IIRC the expected syntax from the Call discussion was more an attribute like #[alert(note="bla", categories="a,b,c")]. And although multiple deprecations probably don't make sense, I guess multiple alerts could do, or even both alerts and deprecation (which is just a particular case of alert anyway).
Hugo Herbelin (Nov 02 2023 at 11:22):About "alert", it was told it is the name used in OCaml, but it has a "danger" connotation. If we provide "alert", we should also provide neutral terms such as "info" (or "note", "comment", ...) and why not also positive ones such as "tip" (or "recommendation", ...).
#[alert(note="bla", categories="a,b,c")]
So, something like:
type info_kind =
| Deprecation of { since : string option }
| Comment of { categories : category list }
type info = { note : string option ; kind : info_kind }
type infos = info list
??
Gaëtan Gilbert (Nov 02 2023 at 11:40):About "alert", it was told it is the name used in OCaml, but it has a "danger" connotation
Wasn't the plan to print the message as a warning? That already has that connotation
Pierre Roux (Nov 02 2023 at 13:12):Either that or modify the warning mechanisms to add some kind of "Infos" in addition to "Warning" and "Error" but that's even more modifications.
Hugo Herbelin (Nov 02 2023 at 14:22):In #18193, I made that each warning on a global Foo.bar generate a specific warning name info-Foo.bar allowing to deactivate the warning only on the given declaration. Is it worth to be maintained? Or would it eventually be too many warnings?
Pierre Roux (Nov 02 2023 at 14:32):I guess it would be more flexible to let the user give its own categories, allowing her to have one warning per declaration (as you offer) or shared between many, depending on the use case.
Hugo Herbelin (Nov 02 2023 at 16:42):I have a prototype here: https://github.com/herbelin/github-coq/pull/new/master+extend-deprecation-support-with-warnings
Example:
#[information="foo bar"] Definition a := 0.
Check a.
Toplevel input, characters 6-7:
> Check a.
> ^
Warning: Reference a, information: foo bar [comment-reference,default]
or, combining with a deprecation:
#[information="foo bar", deprecated(note="use b")] Definition a := 0.
Check a.
Toplevel input, characters 6-7:
> Check a.
> ^
Warning: Reference a, information: foo bar [comment-reference,default]
Toplevel input, characters 6-7:
> Check a.
> ^
Warning: Reference a is deprecated. use b
[deprecated-reference,deprecated,default]
Some choices are arbitrary, especially the rudimentary input syntax, but that's to give a first flavor of what is possible.
Pierre Roux (Nov 02 2023 at 17:13):Hugo Herbelin said:
I have a prototype here: https://github.com/herbelin/github-coq/pull/new/master+extend-deprecation-support-with-warnings
Sounds a good start for a PR, could you open it (the PR)?
Hugo Herbelin (Nov 02 2023 at 17:51):OK, I added support for a command Library Attributes and I opened a new PR.
Pierre Roux (Nov 03 2023 at 08:22):I still think we have two orthogonal features here:
These should be two separate PR, whichever is not merged first can then be easily rebased on top of the other. The curent PR is already pretty large and mixing different things into it makes the review process uselessly difficult. So ideally:
Hugo Herbelin (Nov 03 2023 at 10:15):We can do that. The common intersection is:
information attribute (here with syntax information="...")In any case, I retained from the Coq call that we don't want to have a liboject of docstrings anyway, so I think noone will object if I override #18193 with the version that stores instead the information in the header of the vo file. And then we can choose which version to merge first (knowing that the user-facing syntax will anyway evolved at the same time as it becomes clearer which "metadata" we want to support).
Hugo Herbelin (Nov 03 2023 at 13:33):The curent PR is already pretty large
Note that what makes it large is the generalization of Deprecation.t into Information.t which disseminates at many places but without much contents other than renaming Deprecation into Information or to embed Deprecation.t into Information.Deprecation.t.
Last updated: Oct 13 2024 at 01:02 UTC