The Coq mailing list

[andré hirschowitz <ah AT unice.fr>]

Hello,

I do not know if there is an agreement on this question, but I have a very modest idea, and here it is. My point of view aims to help the reader who  wants to understand what is going on in the development, rather than to help the user who wants to execute the (certified) code.

It is the responsability of the developer to extract from the code the (minimal?) part which he considers sufficient for the reader who wants to check that what is stated formally reflects correctly what is claimed informally. This (minimal?) part is in general not unique. Typically, a definition may be justified by its body or by a (sufficiently?) characteristic statement.

It would thus be nice if the system could provide an edition tool  allowing such an (incremental...) extraction, from a graph of .v-files, of the corresponding graph of, say, .spec-files. That's it.

ah

2017-09-27 19:11 GMT+02:00 Benjamin C. Pierce <bcpierce AT cis.upenn.edu>:

We have a largeish Coq development (https://github.com/QuickChick/QuickChick) that is gaining users and deserves to be better documented.

In the OCaml world, we’d do this by making a small number of .mli files containing just type declarations and signatures of all the externally useful functions.  Function bodies, auxiliary definitions, etc. are all hidden in .ml files that users of the library never look at.

On the other hand, in Coq, this seems not to be the default style, even for the standard library and thoughtfully packaged libraries like ExtLib; instead, library writers just sprinkle coqdoc comments near the main definitions in their .v files and nothing more — no separate interface files collecting just the user-facing bits.

Is there agreement in the community about how a library should best be structured so that its API is easy for users to grok, search, etc.?  Are there examples illustrating best practices?

Thanks!

    - Benjamin (and Leo and Zoe)