Would Coq benefit from docstrings?

Hello everyone,

A bit of a light question, almost a poll.
I have been wondering for a bit as to whether Coq would benefit from docstrings, that would get returned by About, both for lemmas and definitions. In many cases the type and name already provide the necessary documentation, but there are definitely cases where a more lengthy explanation can be precious, both to parse the meaning of the statement, but even more so to specify how it is intended to be used.

Has such a thing ever been considered/discussed?
More generally, I’d be curious to hear how people feel about it.

Best,
Yannick

5 Likes

This is a very good idea idea and I think every effort into documentation is effort well spent.

That being said, I’m not sure if About would be right place to get that information, because it would pollute too much the search for lemmas. Maybe a better idea is creating a new command just for this.

2 Likes

I agree completely — the current situation that mixes docstrings and literate comments is unfortunate. This is a copy of an email I sent recently to a few people working on documentation on this topic:

As I’ve said to some of you in the past, I think it helps to distinguish two fairly separate use cases when talking about documentation tools.

  • One is attaching metadata to bits of code, in order to assemble documentation for APIs, provide code completion, in-buffer hints, etc; this is commonly done by documenting individual functions using special code comments (“docstrings”) and putting these comments together into a larger document.

  • Another one is writing manuals, tutorials, and books, possibly in literate programming style, where the focus is on interleaving code and prose.

There can be interdependencies between these systems. For example, Python folks commonly use small examples of input and output within a function’s docstring — a small form of literate programming embedded in doc comments, called doctests — and conversely Sphinx has a feature (autodoc) that will pull the docstring of a function from its file and include it in a reStructuredText document.

(In the long run, I’d like to do that with Coq’s tactics: one would put a docstring next to the definition of the tactic, and it would be possible to include that text into the manual just by referring to the tactic’s name. This would open plenty of opportunities: for example, you could display tactic docs and function docstrings in search results, even for user-defined tactics and functions).

I think it’s a feature when docstrings and literate comments are different objects, so I get uneasy when they are handled together, e.g. the way it’s done in Doxygen. OCaml gets away with it because mli files can serve as literate files: you can put signatures in any order and there’s no real code in those files, (in fact, signatures in an mli file are quite similar to autodoc commands in a Sphinx document). On the other end of the spectrum there’s the way GNU projects are documented, with a clear separation between the reference manual and the docstrings (to make this concrete, if you have a copy of Emacs at hand, compare the result of the following two commands: M-x info-lookup-symbol start-process and M-x describe-function start-process).

In Coq, CoqDoc has a hybrid role: basically we write all library documentation as literate files. This makes it hard to retrieve documentation programmatically, which means that I can’t include function docstrings in company-coq, for example. In F* things were done differently (doc comments were part of the AST), which means that F*-mode and other UIs were able to include function documentation reliably (there were issues with the implementation of the comment parsing, however, and eventually it was dropped). In contrast, OCaml’s ecosystem does have a notion of what bit of code docstrings attach to, IIUC, which is very good.

4 Likes

I would very much appreciate docstrings / a sensible way to access documentation on definitions in UIs without changing files.

Thanks a lot for the insights Clément!

Your emphasis on distinguishing docstrings from litterate comments indeed makes a lot of sense.

Indeed that would be awesome; the main TODO here is to tweak the Coq Lexer as to better handle comments; this has been in my TODO list for ages but didn’t get the time to move ahead. Any contribution here would be much appreciated.

See also https://github.com/coq/coq/issues/12413

1 Like

Ah that’s awesome, thanks Emilio!
It’s job hunting and POPL season right now, but I’d be happy to try to give a hand in August if there’s still some work to do on this front.

2 Likes