search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.86k stars 650 forks source link

Improve coqtop man pages. #10598

Open jaykru opened 5 years ago

jaykru commented 5 years ago

As of coq 8.9, coqtop's -h option includes information not available in the manpage, such as the extremely useful -Q option. Information in the manpages should at least be kept at a parity with the information available in the help option.

Zimmi48 commented 5 years ago

Hi @jaykru, thank you for your interest.

While I agree with you in theory (the manpages should be kept to parity with the documentation available elsewhere, in particular through the help option), we have currently no manpower dedicated to improving (or just maintaining) the manpages. Most of the documentation efforts have been happening on the reference manual (which also documents the options of coqtop BTW, so there are three places where this documentation can be found, with even more possible inconsistencies).

We would be really glad to receive a pull request bringing the manpages to parity with the -help command and the reference manual.

What would be even more awesome, but certainly harder and thus more long-term, would be to find a way of documenting these options only once and automatically generate the two other formats.

ejgallego commented 5 years ago

What would be even more awesome, but certainly harder and thus more long-term, would be to find a way of documenting these options only once and automatically generate the two other formats.

cmdliner [and some other cmdline parsing libs] can do that.

Zimmi48 commented 5 years ago

Related to #6920 BTW.

Zimmi48 commented 5 years ago

And to #6710. Maybe it's not worth keeping these three issues open, and just one or two would be enough...