Meeting room: https://rendez-vous.renater.fr/coq-docstring

We will discuss the following:

• the design of a potential new feature of Coq to attach some information (like docstring) to definitions, lemmas, etc.,
  • such a feature has been discussed before, e.g., in a Coq call, in a pull request to Coq, and as a Coq CEP.
• a database of results in libraries of formalized mathematics (which some people started during the Dagstuhl Seminar 23401), and
• tool support for the first item, e.g., new coqdoc, GUI support, and a new tool to auto-generate the database (the second item) from Coq files.

Agenda

• Presenting each work in the form of a demo and discussing issues
  • The header documentation in MathComp
  • The knowledge graph stuff from the Dagstuhl Seminar
  • The docstring feature of Hierarchy Builder
  • A prototype of a document engine by Emilio?
• Roadmap
  • The first checkpoint would be discussing what kind of data we want to attach and opening a CEP (or contributing to CEP #65)
  • How to continue: next meeting, and potential physical meeting as a part of the Hausdorff Trimester?

Minutes

coq-lsp demo

• coq-lsp has a table of contents with all the definitions and kind for the project
• this TOC is maintained incrementality
• demo: use the TOC to show the user the comment attached to the definition
• implementation: a hover plugin ~20 lines of code, mostly for parsing the comment

coq-lsp prototype

One possibility is to extend the previous coq-lsp plugin to prototype the following:

• have a tag entry in the document Table of Contents
• the data is filled from the comments / or attributes attached to a definition
• have coq-lsp show the user a link to the tag data if present
• have coq-lsp propose to fill this data if not present
• more complex: query HB for relationships (requires tweaking the Coq plugin API)