Documentation a la Javadocs

[ahuelsing]

It would be super helpful to ease the start for beginners if we had support for documentation a la Javadocs. This way we could a) attach a (human readable) mathematical description of a lemma statement to every EasyCrypt lemma (Plus possibly some more intuition at least for main results) b) print this description in search c) print a documentation for the whole library. There should be support for doing something like this using Markdown as formatting.

[chdoc]

IMHO, the majority of the (pure math) lemmas in the EC libraries have short and human readable statements (Ignoring things like mulrDl: left_distributive Real.(*) Real.(+), which are probably an acquired taste - one that I still haven't acquired).

Are you mainly talking about lemmas involving program logic judgments?

[strub]

Moreover, most of these human readable statements could be automatically generated (bigops, unfolding of some definitions like left_distributive, games...)

[ahuelsing]

Important point: It should be printed when using Search :-)

To answer @chdoc : Take a look at List.ec, Int.ec, DBool.ec,... actually, pick any random sample of files... please show me the comments in there.

[alleystoughton]

Something I find very helpful is to clearly mark the types and operators that are (naturally) parameters of a theory, so as to alert the user as to what could be instantiated.

[chdoc]

I'm clearly in favor of giving human-readable explanations for all the operators in a file, as is done for instance in Mathcomp: seq.v.

What I'm less sure about is the benefit of adding (automatically generated) text to the hundreds (thousands) of trivial facts about the interactions between various operators.