-
Notifications
You must be signed in to change notification settings - Fork 634
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
I'm thinking about learning myself a little Coq, but there's a glaring rock in the way: The man pages are badly formatted. Can't possibly attempt to learn as long as they stay that way. The main changes are these: Empty lines emit vertical space; replace by stylistic no-ops or actual paragraph separators. Wherever there should be a hyphen-minus in the output, use \- in the input. Tell troff where a sentence ends by following it by a newline. Ellipses look nicer with a little space between the dots; do that. The description in the NAME section shouldn't be capitalized and should be nicely readable. Let the man page titles be what the man pages are about. Don't use font-alternating macros where simple font-changing macros suffice. There's more that I'd change if I were in control of the man pages, but that's less important. If you want more rationale for the things I did do, ask me. I'm happy to talk about troff.
- Loading branch information
Lennart Jablonka
committed
May 21, 2024
1 parent
21601f5
commit 6a6dd72
Showing
11 changed files
with
613 additions
and
534 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,33 +1,35 @@ | ||
.TH COQ 1 | ||
|
||
.\" TODO: actually document this thing | ||
.TH COQ_MAKEFILE 1 | ||
. | ||
.SH NAME | ||
coq_makefile \- The Coq Proof Assistant makefile generator | ||
|
||
|
||
coq_makefile \- generate makefiles for Coq proof development | ||
. | ||
. | ||
.SH SYNOPSIS | ||
.B coq_makefile | ||
[ | ||
.B arguments | ||
.I arguments | ||
] | ||
|
||
. | ||
.SH DESCRIPTION | ||
|
||
. | ||
.B coq_makefile | ||
is a makefile generator for Coq proof developments. | ||
|
||
. | ||
.SH OPTIONS | ||
|
||
. | ||
.TP | ||
.BI \-h | ||
Will give you a description of the whole list of options of coq_makefile. | ||
|
||
.B \-h | ||
Will give you a description of the whole list of options of | ||
.BR coq_makefile . | ||
. | ||
.SH SEE ALSO | ||
|
||
. | ||
.BR coqtop (1), | ||
.BR coqtc (1), | ||
.BR coqdep (1). | ||
.br | ||
.BR coqdep (1) | ||
.PP | ||
.I | ||
The Coq Reference Manual. | ||
.I | ||
.PP | ||
The Coq web site: http://coq.inria.fr |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,64 +1,66 @@ | ||
.TH COQ 1 | ||
|
||
.TH COQC 1 | ||
. | ||
.SH NAME | ||
coqc \- The Coq Proof Assistant compiler | ||
|
||
|
||
coqc \- Coq compiler | ||
. | ||
. | ||
.SH SYNOPSIS | ||
.B coqc | ||
[ | ||
.B general \ Coq \ options | ||
general Coq options | ||
] | ||
.I file | ||
|
||
|
||
. | ||
. | ||
.SH DESCRIPTION | ||
|
||
. | ||
.B coqc | ||
is the batch compiler for the Coq Proof Assistant. | ||
The options are basically the same as coqtop(1). | ||
.IR file.v \& | ||
The options are basically the same as | ||
.BR coqtop (1). | ||
.I file.v | ||
is the vernacular file to compile. | ||
.IR file \& | ||
.I file | ||
must be formed | ||
only with the characters `a` to `Z`, `0`-`9` or `_` and must begin | ||
only with the characters `a' to `Z', `0' to `9' or `_' and must begin | ||
with a letter. | ||
The compiler produces an object file | ||
.IR file.vo \&. | ||
|
||
.PP | ||
For interactive use of Coq, see | ||
.BR coqtop(1). | ||
|
||
|
||
.BR coqtop (1). | ||
. | ||
. | ||
.SH OPTIONS | ||
|
||
. | ||
.\" TODO: Coqc is not a script. Correct this claim. | ||
.B coqc | ||
is a script that simply runs | ||
.B coqtop | ||
with option | ||
.B \-compile | ||
it accepts the same options as | ||
.B coqtop. | ||
|
||
.BR \-compile . | ||
It accepts the same options as | ||
.BR coqtop . | ||
. | ||
.TP | ||
.BI \-image \ bin | ||
use | ||
Use | ||
.I bin | ||
as underlying | ||
.B coqtop | ||
instead of the default one. | ||
|
||
. | ||
.TP | ||
.BI \-verbose | ||
print the compiled file on the standard output. | ||
|
||
.B \-verbose | ||
Print the compiled file on the standard output. | ||
. | ||
.SH SEE ALSO | ||
|
||
. | ||
.BR coqtop (1), | ||
.BR coq_makefile (1), | ||
.BR coqdep (1). | ||
.br | ||
.BR coqdep (1) | ||
.PP | ||
.I | ||
The Coq Reference Manual. | ||
.I | ||
.PP | ||
The Coq web site: http://coq.inria.fr |
Oops, something went wrong.