Support for deprecating a file

[herbelin]

This is an experimental support for associating comments or warnings to global names.
This provides support for associating warnings or deprecation to a library file.

As an example, two commands Library Comment string. and Library Warning string. are
A command Library Attributes #[...] is provided, with the idea that it could be used to warn about the status of some files (as e.g. for #18032, w/o requiring the indirection of an abbreviation, nor to rely on the deprecation system).

The supported attributes are deprecated(...) and information="...".

Fixes: #8032

• Added changelog.
• Added / updated documentation.

[Villetaneuse]

Thank you!

If I may, some first (probably very naive, really at user level) impressions:

• you could also mention How to deprecate a library? #8032 which asks about how to deprecate a whole file
• it's not clear to me what a "library" is, (maybe it will be when/if there are namespaces?) It seems what you target instead are files (or modules?) so maybe change it to something else like "File Comment" and "File Warning" or the same with a module?
• if one of the use cases is indeed to deprecate a whole file (which is much needed), I think it should be closer to what we can do with other objects: have a "deprecated" attribute, with "since" and "note" keys, then it should be decided if the objects defined in that file inherit this deprecated attribute or not
• a "Module comment" of "file comment" should possibly be a very long string, with maybe some formatting (coqdoc, mathcomp file comments), and a way to output it for the user, some discussions with UI designers (coq-lsp, vscoq2) could help.
• docstrings should be provided for every defined object, not just files or modules, again with user interfaces in mind

Again, these are really first impressions from a non-specialist. Feel free to ignore them.

[Villetaneuse]

Other things that come in mind:

• multilingual support: Not everyone understands English, this could be important, especially for teaching
• what parts are actually in Coq, what parts are left to external tools (user interfaces, documentation generators, ...): for instance, there is no concept of docstring for the C language, but some IDEs recognize /** ... */ as documentation and display it.

[herbelin]

it's not clear to me what a "library" is, (maybe it will be when/if there are namespaces?) It seems what you target instead are files (or modules?) so maybe change it to something else like "File Comment" and "File Warning" or the same with a module?

This ambiguity should indeed be resolved. In commands such as Print Loaded Libraries, a library is a file, but often, in standard language, a library is a repository of files forming a whole. Here, I used the library=file terminology.

I agree with your other comments.

[proux01]

* docstrings should be provided for every defined object, not just files or modules, again with user interfaces in mind

Agree, but that's a somewhat orthogonal feature. I'd propose the following course of actions in order to make quick and effective progress on those long stalled points:

• consolidate and merge this PR for deprecating files (user facing syntax, test-suite, changelog and merge if there is no opposition, hope this can be done in a couple of weeks, less than a month)
• in a separate PR: docstrings, this seems more midterm as it requires more discussion, hope this can land in 8.19 but less obvious

[SkySkimmer]

Why is this hybrid? main_w looks unused.
Also what's the point of having nested categories info and info-warning?
You should just do let info_cat = CWarnings.create_category ~name:"info" () at toplevel and then let w = CWarnings.create ~category:info_cat ~name:("info-" ^ name) pp (when not in the table)

[herbelin]

With your change, it gives the warnings info-MyRoot.MyFile,info,default which seems ok.

I'm not familiar with the design of the warning and deprecation system. What should it be for deprecation? Should it be deprecated-libraries-since-8.XX,deprecated-since-8.XX,deprecated-libraries,deprecated,default (on the model of what is done for abbreviations)? Something different?

[herbelin]

I pushed a new version that includes deprecation. As of now, it works as follows:

• in file foo.v:

  Library Warning "This implements foo arithmetic".
  Library Deprecation since "8.18" "Please use bar arithmetic".
  

• output at require time:

  Toplevel input, characters 0-12:
  > Require Foo.
  > ^^^^^^^^^^^^
  Warning: Library Foo is deprecated since 8.4.
  Please use bar arithmetic
  [deprecated-libraries-since-8.4,deprecated-since-8.4,deprecated-libraries,deprecated,default]
  Toplevel input, characters 0-12:
  > Require Foo.
  > ^^^^^^^^^^^^^
  Warning: This implements foo arithmetic [info-Foo,info,default]
  

PS: To be clear, I'm not attached to any syntax, nor to any particular solution. My motivation is primarily that this is needed for other PRs.

[ejgallego]

in a separate PR: docstrings, this seems more midterm as it requires more discussion, hope this can land in 8.19 but less obvious

Indeed I agree with @proux01 . While I'm not against with the implementation the PR provides for docstrings, there are a few questions around them, related to the libobject CEP , and some questions about usability, etc... I have thought about this problem for a while.

IMHO it would be great to collaborate on a design with all the knowlegde we have, once we converge, we can go ahead and implement it. How does it sound folks to meet one day over Zoom to discuss?

[herbelin]

IMHO it would be great to collaborate on a design with all the knowlegde we have, once we converge, we can go ahead and implement it. How does it sound folks to meet one day over Zoom to discuss?

Sure. I can today any time, and otherwise from Thursday afternoon. (Is there some literature to read already?)

[proux01]

IMHO it would be great to collaborate on a design with all the knowlegde we have, once we converge, we can go ahead and implement it. How does it sound folks to meet one day over Zoom to discuss?

What about discussing it shortly during the call tomorrow (it's been added to the roadmap anyway) and plan a specific meeting with anyone interested, to have more in depth discussions?

[ejgallego]

Sure. I can today any time, and otherwise from Thursday afternoon. (Is there some literature to read already?)

Would it work for you Hugo if we ask in Zulip , we can do a framadate?

I'm happy to explain what I know about docstrings in 5 minutes in the meeting, but indeed, off the top of my head, the liberabaci proposal included quite a few ideas, Hiearchy Builder has a docstring system, and the libobject PR has some discussion about this too.

Some issues to consider:

• as of today, we store two copies of an object for many objects, for each phase, which one to attach the doc to?
• IMHO a docstring system should not require the file to be Required in order to access the docstrings
• document engines actually can actually read the comments directly from the sources without having to invoke anything, I have a little prototype ready if you are curious (happy to demo it too!)

[ejgallego]

IMHO it would be great to collaborate on a design with all the knowlegde we have, once we converge, we can go ahead and implement it. How does it sound folks to meet one day over Zoom to discuss?

What about discussing it shortly during the call tomorrow (it's been added to the roadmap anyway) and plan a specific meeting with anyone interested, to have more in depth discussions?

That also works for me!

[herbelin]

document engines actually can actually read the comments directly from the sources without having to invoke anything, I have a little prototype ready if you are curious (happy to demo it too!)

That's a question I had. If the GUI does the job (e.g. by linking directly to the source), would docstring be really necessary???

[proux01]

We have use cases in hierarchy-builder (current HB.about to know what structures are instantiated on a type) where the GUI couldn't do the job as we need to build the docstring programatically.

[herbelin]

We have use cases in hierarchy-builder (current HB.about to know what structures are instantiated on a type) where the GUI couldn't do the job as we need to build the docstring programatically.

Is there something to read about it? And what are the docstring plans regarding HB?

[CohenCyril]

ping @pi8027

[pi8027]

During the Dagstuhl Seminar 23401, some people worked on a mapping from definitions in MathComp to their informal description and corresponding Wikidata tags (like Q534381). A feature of Coq to attach some metadata to definitions would have several use cases, e.g., generate nicer documentation (like mathlib), generate relational data similar to one done in the Dagstuhl Seminar, and look up the description of the definition through the About command.

So, I think we first have to discuss the design of the docstring feature we need and eventually open a CEP. We will have a meeting to discuss it (mainly between MathComp dev and some participants of the Dagstuhl Seminar) this Thursday at 16:00 Paris Time. Let me know if you want to participate in it.

[herbelin]

some people worked on a mapping from definitions in MathComp to their informal description and corresponding Wikidata tags

Very nice!

Let me know if you want to participate in it.

If things are already moving on your side, my presence is probably not necessary. In any case, this is great news.

[herbelin]

Regarding the PR, considering that warning/deprecation is not the kind of data mentioned by @pi8027, considering the related question of GUI support, and considering @proux01's suggestion of consolidate and merging the PR for deprecating files, I'm going to stop here with the implementation (up to an agreement on the user facing syntax).

[pi8027]

@herbelin (also @ejgallego) It seems that discussions about docstring-like features are happening in several groups of people. I first want to make sure that we understand the needs of each other. So I would appreciate your presence.

[ejgallego]

Thanks @pi8027 , I was not aware this was happening, happy to be there!

[herbelin]

So I would appreciate your presence.

Thanks! Note however that it is not clear yet whether I will be able to attend, but I'll try.

Note also that I don't have precise ideas about docstring. I was seduced by the projects of Florian R. at some time (but without time to work on it myself), and by the Logipedia projects too. I consider that Coq documents should be more structured, connected to ontologies, supporting classifications, and machine learning would probably benefit of it. Somehow, this should also be integrated with coqdoc (and with GUI).

[proux01]

@herbelin during yesterday's call there was an agreement on Attributes (alone), I updated the PR, if it's ok for you I merge (once CI is green).

[herbelin]

It is ok. Thanks!

[proux01]

@coqbot merge now

[coqbot-app]

@proux01: You can't merge the PR because it hasn't been approved yet.

[proux01]

@coqbot merge now

[proux01]

I'm just discovering that this is transitive, making it hardly usable:

A.v

Attributes deprecated(note="A deprecated").

B.v

Require Import A.
(* warning as expected *)

C.v

Require Import B.
(* also a warning *)

[herbelin]

To have it only if textually mentioned in a Require line, the line with Library_info.warn_library_info in library.ml needs to be moved to rec_intern_library (and lsd or lsd.md_info be propagated), iinm.

[proux01]

Thanks, that's indeed what I have in a patch, I'm opening a PR.