From 6a6dd72f047365e2a71cf18c22c270a14dc88f03 Mon Sep 17 00:00:00 2001 From: Lennart Jablonka Date: Tue, 21 May 2024 02:54:01 +0200 Subject: [PATCH] Fix the man pages' formatting. 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. --- man/coq-tex.1 | 102 ++++++++++---------- man/coq_makefile.1 | 36 ++++---- man/coqc.1 | 64 ++++++------- man/coqchk.1 | 122 ++++++++++++------------ man/coqdep.1 | 173 ++++++++++++++++++---------------- man/coqdoc.1 | 226 ++++++++++++++++++++++++++------------------- man/coqide.1 | 78 ++++++++-------- man/coqnative.1 | 92 +++++++++--------- man/coqtop.1 | 176 ++++++++++++++++++----------------- man/coqtop.byte.1 | 32 +++---- man/coqwc.1 | 46 ++++----- 11 files changed, 613 insertions(+), 534 deletions(-) diff --git a/man/coq-tex.1 b/man/coq-tex.1 index e4cea24c5565..351291d52613 100644 --- a/man/coq-tex.1 +++ b/man/coq-tex.1 @@ -1,10 +1,10 @@ -.TH COQ-TEX 1 - +.TH COQ\-TEX 1 +. .SH NAME -coq-tex \- Process Coq phrases embedded in LaTeX files - +coq\-tex \- process Coq phrases embedded in LaTeX files +. .SH SYNOPSIS -.B coq-tex +.B coq\-tex [ .BI \-o \ output-file ] @@ -29,33 +29,34 @@ coq-tex \- Process Coq phrases embedded in LaTeX files [ .B \-small ] -.I input-file ... - - +.I input-file .\|.\|. +. +. .SH DESCRIPTION - +. The -.B coq-tex +.B coq\-tex filter extracts Coq phrases embedded in LaTeX files, evaluates them, and insert the outcome of the evaluation after each phrase. - +.PP Three LaTeX environments are provided to include Coq code in the input files: .TP .B coq_example The phrases between \\begin{coq_example} and \\end{coq_example} are -evaluated and copied into the output file. Each phrase is followed by -the response of the toplevel loop. +evaluated and copied into the output file. +Each phrase is followed by the response of the toplevel loop. .TP .B coq_example* The phrases between \\begin{coq_example*} and \\end{coq_example*} are -evaluated and copied into the output file. The responses of the -toplevel loop are discarded. +evaluated and copied into the output file. +The responses of the toplevel loop are discarded. .TP .B coq_eval The phrases between \\begin{coq_eval} and \\end{coq_eval} are -silently evaluated. They are not copied into the output file, and the -responses of the toplevel loop are discarded. +silently evaluated. +They are not copied into the output file, and the responses of the +toplevel loop are discarded. .PP The resulting LaTeX code is stored in the file .IR file \&.v.tex @@ -63,63 +64,70 @@ if the input file has a name of the form .IR file \&.tex, otherwise the name of the output file is the name of the input file with `.v.tex' appended. - +.PP The files produced by -.B coq-tex +.B coq\-tex can be directly processed by LaTeX. Both the Coq phrases and the toplevel output are typeset in typewriter font. - +. .SH OPTIONS - +. .TP .BI \-o \ output-file -Specify the name of a file where the LaTeX output is to be stored. A -dash `\-' causes the LaTeX output to be printed on standard output. +Specify the name of a file where the LaTeX output is to be stored. +A dash `\-' causes the LaTeX output to be printed on standard output. .TP .BI \-n \ line-width -Set the line width. The default is 72 characters. The responses of the -toplevel loop are folded if they are longer than the line width. No -folding is performed on the Coq input text. +Set the line width. +The default is 72 characters. +The responses of the toplevel loop are folded if they are longer than +the line width. +No folding is performed on the Coq input text. .TP .BI \-image \ coq-image Cause the file -.IR coq-image -to be executed to evaluate the Coq phrases. By default, -this is the command -.IR coqtop +.I coq-image +to be executed to evaluate the Coq phrases. +By default, this is the command +.I coqtop without specifying any path which is used to evaluate the Coq phrases. .TP .B \-w Cause lines to be folded on a space character whenever possible, -avoiding word cuts in the output. By default, folding occurs at -the line width, regardless of word cuts. +avoiding word cuts in the output. +By default, folding occurs at the line width, regardless of word cuts. .TP .B \-v -Verbose mode. Prints the Coq answers on the standard output. +Verbose mode. +Prints the Coq answers on the standard output. Useful to detect errors in Coq phrases. .TP .B \-sl -Slanted mode. The Coq answers are written in a slanted font. +Slanted mode. +The Coq answers are written in a slanted font. .TP .B \-hrule -Horizontal lines mode. The Coq parts are written between two -horizontal lines. +Horizontal lines mode. +The Coq parts are written between two horizontal lines. .TP .B \-small -Small font mode. The Coq parts are written in a smaller font. - - +Small font mode. +The Coq parts are written in a smaller font. +. +. .SH CAVEATS -The \\begin... and \\end... phrases must sit on a line by themselves, -with no characters before the backslash or after the closing brace. +The \\begin.\|.\|. and \\end.\|.\|. phrases must sit on a line by +themselves, with no characters before the backslash or after the closing +brace. Each Coq phrase must be terminated by `.' at the end of a line. Blank space is accepted between `.' and the newline, but any other -character will cause coq-tex to ignore the end of the phrase, -resulting in an incorrect shuffling of the responses into the phrases. +character will cause +.B coq\-tex +to ignore the end of the phrase, resulting in an incorrect shuffling of +the responses into the phrases. (The responses ``lag behind''.) - +. .SH SEE ALSO - -.B coqtop -(1). +. +.BR coqtop (1) diff --git a/man/coq_makefile.1 b/man/coq_makefile.1 index 0f5912a4bbf1..04e68623ba0b 100644 --- a/man/coq_makefile.1 +++ b/man/coq_makefile.1 @@ -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 diff --git a/man/coqc.1 b/man/coqc.1 index a7be343fa030..d6188126f9ba 100644 --- a/man/coqc.1 +++ b/man/coqc.1 @@ -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 diff --git a/man/coqchk.1 b/man/coqchk.1 index 2f9e1fd84d44..4a2075dd17ef 100644 --- a/man/coqchk.1 +++ b/man/coqchk.1 @@ -1,101 +1,109 @@ -.TH COQ 1 - +.TH COQCHK 1 +. .SH NAME -coqchk \- The Coq Proof Checker compiled libraries verifier - - +coqchk \- verify compiled Coq libraries +. +. .SH SYNOPSIS .B coqchk [ -.B options +options ] .I modules - - +. +. .SH DESCRIPTION - +. .B coqchk is the standalone checker of compiled libraries (.vo files produced by -coqc) for the Coq Proof Assistant. See the Reference Manual for more -information. It returns with exit code 0 if all the requested tasks -succeeded. A non-zero return code means that something went wrong: some +.BR coqc ) +for the Coq Proof Assistant. +See the +.I Reference Manual +for more information. +It returns with exit code 0 if all the requested tasks succeeded. +A non-zero return code means that something went wrong: some library was not found, corrupted content, type-checking failure, etc. - -.IR modules \& -is a list of modules to be checked. Modules can be referred to by a -short or qualified logical name, or by their filename. - +.PP +.I modules +is a list of modules to be checked. +Modules can be referred to by a short or qualified logical name, +or by their filename. +. .SH OPTIONS - +. .TP .BI \-I \ dir, \ \-\-include \ dir -add directory +Add directory .I dir -in the include path - +to the include path. +. .TP .BI \-Q \ dir\ coqdir -map physical +Map physical .I dir to logical -.I coqdir - +.I coqdir. +. .TP .BI \-R \ dir\ coqdir -synonymous for -Q - +Synonymous to +.BR \-Q . +. .TP -.BI \-silent -makes coqchk less verbose. - +.B \-silent +Be less verbose. +. .TP .BI \-admit \ module -tag the specified module and all its dependencies as trusted, and will +Tag the specified module and all its dependencies as trusted, and will not be rechecked, unless explicitly requested by other options. - +. .TP .BI \-norec \ module -specifies that the given module shall be verified without requesting +Specifies that the given module shall be verified without requesting to check its dependencies. - +. .TP -.BI \-m,\ \-\-memory -displays a summary of the memory used by the checker. - +.BR \-m ,\ \-\-memory +Displays a summary of the memory used by the checker. +. .TP -.BI \-o,\ \-\-output\-context -displays a summary of the logical content that have been +.BR \-o ,\ \-\-output\-context +Displays a summary of the logical content that have been verified: assumptions and usage of impredicativity. - +. .TP -.BI \-impredicative\-set -allows the checker to accept libraries that have been compiled with +.B \-impredicative\-set +Allows the checker to accept libraries that have been compiled with this flag. - +. .TP -.BI \-v -print coqchk version and exit. - +.B \-v +Print +.B coqchk +version and exit. +. .TP .BI \-coqlib \ dir -overrides the default location of the standard library. - +Overrides the default location of the standard library. +. .TP -.BI \-where -print coqchk standard library location and exit. - +.B \-where +Print coqchk standard library location and exit. +. .TP -.BI \-h,\ \-\-help -print list of options - +.BR \-h ,\ \-\-help +Print list of options. +. .SH SEE ALSO - +. .BR coqtop (1), .BR coqc (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 diff --git a/man/coqdep.1 b/man/coqdep.1 index 0734ab61ae94..e409ce6b284c 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -1,8 +1,8 @@ -.TH COQ 1 - +.TH COQDEP 1 +. .SH NAME -coqdep \- Compute inter-module dependencies for Coq programs - +coqdep \- compute inter-module dependencies for Coq programs +. .SH SYNOPSIS .B coqdep [ @@ -12,66 +12,79 @@ coqdep \- Compute inter-module dependencies for Coq programs .BI \-coqlib \ directory ] [ -.BI \-i +.B \-i ] [ -.BI \-slash +.B \-slash ] -.I filename ... -.I directory ... - +.I filename .\|.\|.\& +.I directory .\|.\|. +. .SH DESCRIPTION - +. .B coqdep computes inter-module dependencies for Coq programs, and prints the dependencies on the standard output in a format -readable by make. +readable by +.BR make . When a directory is given as argument, it is recursively looked at. - +.PP Dependencies of Coq modules are computed by looking at -.IR Require \& +.I Require commands (Require, Require Export, Require Import, possibly restricted by a From clause), -.IR Declare \& -.IR ML \& -.IR Module \& +.I Declare +.I ML +.I Module commands, -.IR Add \& -.IR LoadPath \& +.I Add +.I LoadPath commands and -.IR Load \& -commands. Dependencies relative to modules from the Coq library are not +.I Load +commands. +Dependencies relative to modules from the Coq library are not printed except if -.BR \-boot \& +.B \-boot is given. - +. .SH OPTIONS - +. .TP .BI \-f \ file -Read filenames and options -I, -R and -Q from a _CoqProject FILE. +Read filenames and options +.BR \-I , +.B \-R +and +.B \-Q +from a _CoqProject +.I file. .TP -.BI \-I/\-Q/\-R \ options +.BI \-I\fR/\fB\-Q\fR/\fB\-R \ options Have the same effects on load path and modules names as for other -Coq commands (coqtop, coqc). +Coq commands (\c +.BR coqtop , +.BR coqc ). .TP .BI \-coqlib \ directory -Indicates where is the Coq library. The default value has been -determined at installation time, and therefore this option should not -be used under normal circumstances. +Indicates where is the Coq library. +The default value has been determined at installation time, and +therefore this option should not be used under normal circumstances. .TP .BI \-exclude-dir \ dir Skips subdirectory -.IR dir \ during -.BR -R/-Q \ search. +.I dir +during +.BR \-R / \-Q +search. .TP .B \-sort Output the given file name ordered by dependencies. .TP .B \-vos -Output dependencies for .vos files (this is not the default as it breaks dune's Coq mode) +Output dependencies for .vos files (this is not the default as it breaks +dune's Coq mode). .TP .B \-boot -For coq developers, prints dependencies over coq library files +For Coq developers, prints dependencies over Coq library files (omitted by default). .TP .B \-noinit @@ -80,80 +93,78 @@ Currently no effect. .B \-vos Includes dependencies about .vos files. .TP -.B \-dyndep (opt|byte|both|no|var) +.BR \-dyndep \ ( opt | byte | both | no | var ) Set how dependencies over ML modules are printed. .TP -.B \-m META -Resolve plugin names using the META file. +.BI \-m \ meta +Resolve plugin names using the +.I meta +file. .TP -.B \-w w1,...,wn -Configure display of warnings as for coqc. - +.BI \-w \ w1,\|.\|.\|.\|,\|wn +Configure display of warnings as for +.BR coqc . +. .SH EXIT STATUS -.IP "1" +.IP 1 A file given on the command line cannot be found, or some file -cannot be opened, or there is a syntax error in one of the commands recognized by coqdep. -.IP "0" -In all other cases. In particular, when a dependency cannot be -found or an invalid option is encountered, +cannot be opened, or there is a syntax error in one of the commands +recognized by +.BR coqdep . +.IP 0 +In all other cases. +In particular, when a dependency cannot be found or an invalid option is +encountered, .B coqdep -prints a warning and exits with status -.B 0\fR. - - +prints a warning and exits with status 0. +. +. .SH SEE ALSO - +. .BR ocamlc (1), .BR coqc (1), -.BR make (1). -.br - +.BR make (1) +. .SH NOTES - +. Lexers (for Coq and OCaml) correctly handle nested comments and strings. - +.PP The treatment of symbolic links is primitive. - +.PP If two files have the same name, in two different directories, a warning is printed on standard error. - +.PP There is no way to limit the scope of the recursive search for directories. - +. .SH EXAMPLES - -.LP +. Consider the files (in the same directory): - - a.mllib X.v Y.v and Z.v - +.RS +a.mllib, X.v, Y.v, and Z.v +.RE where -.TP -.BI \+ +.IP \(bu 3 a.mllib contains the module names `B' and `C'; -.TP -.BI \+ -Y.v contains the command `Require Foo.X' ; -.TP -.BI \+ +.IP \(bu +Y.v contains the command `Require Foo.X'; +.IP \(bu Z.v contains the commands `From Foo Require X' and `Declare ML Module "a"'. -.LP +.PP To get the dependencies of the Coq files: -.IP -.B -example% coqdep \-I . -Q . Foo *.v +.PP .RS -.sp .5 .nf -.B X.vo X.glob X.v.beautified X.required_vo: X.v -.B Y.vo Y.glob Y.v.beautified Y.required_vo: Y.v X.vo -.B Z.vo Z.glob Z.v.beautified Z.required_vo: Z.v X.vo ./a.cma ./a.cmxs +example% coqdep \-I . \-Q . Foo *.v + +X.vo X.glob X.v.beautified X.required_vo: X.v +Y.vo Y.glob Y.v.beautified Y.required_vo: Y.v X.vo +Z.vo Z.glob Z.v.beautified Z.required_vo: Z.v X.vo ./a.cma ./a.cmxs .fi .RE -.br - +. .SH BUGS - +. Please report any bug to -.B https://github.com/coq/coq/issues +.BR https://github.com/coq/coq/issues . diff --git a/man/coqdoc.1 b/man/coqdoc.1 index b39032961003..5fede00a017e 100644 --- a/man/coqdoc.1 +++ b/man/coqdoc.1 @@ -1,38 +1,40 @@ -.TH coqdoc 1 - +.TH COQDOC 1 +. .SH NAME -coqdoc \- A documentation tool for the Coq proof assistant - - +coqdoc \- documentation tool for the Coq proof assistant +. +. .SH SYNOPSIS .B coqdoc [ -.B options +options ] -.B files - - +.I files +. +. .SH DESCRIPTION - +. .B coqdoc is a documentation tool for the Coq proof assistant. It creates LaTeX or HTML documents from a set of Coq files. See the Coq reference manual for documentation (url below). - - +. +. .SH OPTIONS - +. .SS Overall options - +. .TP -.BI \-h -Help. Will give you the complete list of options accepted by coqdoc. +.B \-h +Help. +Will give you the complete list of options accepted by +.BR coqdoc . .TP .B \-\-html Select a HTML output. .TP .B \-\-latex -Select a LATEX output. +Select a LaTeX output. .TP .B \-\-dvi Select a DVI output. @@ -54,45 +56,53 @@ Redirect the output into the file Output files into directory .I dir instead of current directory (option -\-d does not change the filename specified with option \-o, if any). +.B \-d +does not change the filename specified with option +.BR \-o , +if any). .TP -.B \-s, \ \-\-short -Do not insert titles for the files. The default behavior is to insert -a title like ``Library Foo'' for each file. +.BR \-s , \ \-\-short +Do not insert titles for the files. +The default behavior is to insert a title like ``Library Foo'' for each +file. .TP .BI \-t \ string, \ \-\-title \ string Set the document title. .TP .B \-\-body\-only -Suppress the header and trailer of the final document. Thus, you can -insert the resulting document into a larger one. +Suppress the header and trailer of the final document. +Thus, you can insert the resulting document into a larger one. .TP .BI \-p \ string, \ \-\-preamble \ string -Insert some material in the LATEX preamble, right before \\begin{document} (meaningless with \-html). +Insert some material in the LaTeX preamble, right before +\\begin{document} (meaningless with \-html). .TP .BI \-\-vernac\-file \ file, \ \-\-tex\-file \ file -Considers the file `file' respectively as a .v (or .g) file or a .tex file. +Considers the file +.I file +respectively as a .v (or .g) file or a .tex file. .TP .BI \-\-files\-from \ file -Read file names to process in file `file' as if they were given on the -command line. Useful for program sources split in several -directories. +Read file names to process in file +.I file +as if they were given on the command line. +Useful for program sources split in several directories. .TP -.B \-q, \ \-\-quiet -Be quiet. Do not print anything except errors. +.BR \-q , \ \-\-quiet +Be quiet. +Do not print anything except errors. .TP -.B \-h, \ \-\-help +.BR \-h , \ \-\-help Give a short summary of the options and exit. .TP -.B -\-v, \ \-\-version +.BR \-v , \ \-\-version Print the version and exit. - +. .SS Index options - +. Default behavior is to build an index, for the HTML output only, into index.html. - +. .TP .B \-\-no\-index Do not output the index. @@ -100,90 +110,116 @@ Do not output the index. .B \-\-multi\-index Generate one page for each category and each letter in the index, together with a top page index.html. - +. .SS Table of contents option - -.TP -.B \-toc, \ \-\-table\-of\-contents -Insert a table of contents. For a LATEX output, it inserts a -\\tableofcontents at the beginning of the document. For a HTML output, -it builds a table of contents into toc.html. - +. +.TP +.BR \-toc , \ \-\-table\-of\-contents +Insert a table of contents. +For a LaTeX output, it inserts a \\tableofcontents at the beginning of +the document. +For a HTML output, it builds a table of contents into toc.html. +. .SS Hyperlinks options - +. .TP -.B \-\-glob\-from \ file -Make references using Coq globalizations from file file. (Such -globalizations are obtained with Coq option \-dump\-glob). - +.BI \-\-glob\-from \ file +Make references using Coq globalizations from file file. +(Such globalizations are obtained with Coq option +.BR \-dump\-glob ). +. .TP .B \-\-no\-externals Do not insert links to the Coq standard library. - +. .TP -.BI \-\-external \ url \ libroot -Set base URL for the external library whose root prefix is libroot. - +.BI \-\-external \ url\ libroot +Set base URL for the external library whose root prefix is +.I libroot. +. .TP .BI \-\-coqlib_url \ url -Set base URL for the Coq standard library (default is http://coq.inria.fr/library/). - +Set base URL for the Coq standard library (default is +http://coq.inria.fr/library/). +. .TP .BI \-\-coqlib \ dir -Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css. - +Set the base path where the Coq files are installed, especially style +files coqdoc.sty and coqdoc.css. +. .TP -.BI \-R \ dir \ coqdir +.BI \-R \ dir\ coqdir Map physical directory dir to Coq logical directory coqdir (similarly -to Coq option \-R). +to Coq option +.BR \-R ). .B Note: -option \-R only has effect on the files following it on the command +option +.B \-R +only has effect on the files following it on the command line, so you will probably need to put this option first. - +. .SS Contents options - +. .TP -.B \-g, \ \-\-gallina +.BR \-g , \ \-\-gallina Do not print proofs. - -.TP -.B \-l, \ \-\-light -Light mode. Suppress proofs (as with \-g) and the following commands: - - * [Recursive] Tactic Definition - * Hint / Hints - * Require - * Transparent / Opaque - * Implicit Argument / Implicits - * Section / Variable / Hypothesis / End - -The behavior of options \-g and \-l can be locally overridden using the (* begin show *) ... (* end show *) environment (see above). - +. +.TP +.BR \-l , \ \-\-light +Light mode. Suppress proofs (as with +.BR \-g ) +and the following commands: +.RS +.IP \(bu 3 +[Recursive] Tactic Definition +.IP \(bu +Hint / Hints +.IP \(bu +Require +.IP \(bu +Transparent / Opaque +.IP \(bu +Implicit Argument / Implicits +.IP \(bu +Section / Variable / Hypothesis / End +.PP +The behavior of options +.B \-g +and +.B \-l +can be locally overridden using the +(*\ begin show\ *) .\|.\|. (*\ end show\ *) environment (see above). +.RE +. .SS Language options - +. Default behavior is to assume ASCII 7 bits input files. - -.TP -.B \-latin1, \ \-\-latin1 -Select ISO-8859-1 input files. It is equivalent to \-\-inputenc latin1 -\-\-charset iso\-8859\-1. - -.TP -.B \-utf8, \ \-\-utf8 -Select UTF-8 (Unicode) input files. It is equivalent to \-\-inputenc -utf8 \-\-charset utf\-8. LATEX UTF-8 support can be found at +. +.TP +.BR \-latin1 , \ \-\-latin1 +Select ISO-8859-1 input files. +It is equivalent to +.BR "\-\-inputenc\ latin1 \-\-charset\ iso\-8859\-1" . +. +.TP +.BR \-utf8 , \ \-\-utf8 +Select UTF-8 (Unicode) input files. +It is equivalent to +.BR "\-\-inputenc\ utf8 \-\-charset\ utf\-8" . +LaTeX UTF-8 support can be found at http://www.ctan.org/tex\-archive/macros/latex/contrib/supported/unicode/. - +. .TP .BI \-\-inputenc \ string -Give a LATEX input encoding, as an option to LATEX package inputenc. - +Give a LaTeX input encoding, as an option to LaTeX package inputenc. +. .TP .BI \-\-charset \ string Specify the HTML character set, to be inserted in the HTML header. - - +. +. .SH SEE ALSO - +. .I -The Coq Reference Manual from http://coq.inria.fr/ +The Coq Reference Manual +from http://coq.inria.fr/ diff --git a/man/coqide.1 b/man/coqide.1 index 267f8a8d4b75..504b52c254dc 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -1,41 +1,43 @@ .TH COQIDE 1 - +. .SH NAME -coqide \- The Coq Proof Assistant graphical interface - - +coqide \- graphical interface for the Coq proof assistant +. +. .SH SYNOPSIS .B coqide [ -.B options +options ] - +. .SH DESCRIPTION - +. .B coqide is a gtk graphical interface for the Coq proof assistant. - +.PP For command-line-oriented use of Coq, see -.BR coqtop (1) -; for batch-oriented use of Coq, see +.BR coqtop (1); +for batch-oriented use of Coq, see .BR coqc (1). - - +. +. .SH OPTIONS - +. .TP .B \-h Show the complete list of options accepted by .BR coqide . .TP -.BI \-I\ dir ,\ \-include\ dir -Add directory dir in the include path. +.BI \-I\ dir, \ \-include\ dir +Add directory +.I dir +in the include path. .TP .BI \-R\ dir\ coqdir Recursively map physical .I dir to logical -.IR coqdir . +.I coqdir. .TP .B \-src Add source directories in the include path. @@ -45,35 +47,35 @@ Start with an empty state. .TP .BI \-load\-ml\-object\ f Load ML object file -.IR f . +.I f. .TP .BI \-load\-ml\-source\ f Load ML file -.IR f . +.I f. .TP -.BI \-l\ f ,\ \-load\-vernac\-source\ f +.BI \-l\ f, \ \-load\-vernac\-source\ f Load Coq file .IR f .v (Load -.IR f .). +.IR f. ). .TP -.BI \-lv\ f ,\ \-load\-vernac\-source\-verbose\ f +.BI \-lv\ f, \ \-load\-vernac\-source\-verbose\ f Load Coq file .IR f .v (Load Verbose -.IR f .). +.IR f. ). .TP .BI \-load\-vernac\-object\ path Load Coq library -.IR path +.I path (Require -.IR path .). +.IR path. ). .TP .BI \-require-import\ path Load Coq library -.IR path +.I path and import it (Require Import -.IR path .). +.IR path. ). .TP .BI \-compile\ f Compile Coq file @@ -98,7 +100,7 @@ Skip loading of rcfile. .TP .BI \-init\-file\ f Set the rcfile to -.IR f . +.I f. .TP .B \-emacs Tells Coq it is executed under Emacs. @@ -114,21 +116,21 @@ Set sort Set impredicative. .TP .B \-dont\-load\-proofs Don't load opaque proofs in memory. - +. .SH SEE ALSO - +. .BR coqc (1), .BR coqtop (1), -.BR coq-tex (1), -.BR coqdep (1). -.br -.I -The Coq Reference Manual, -.I -The Coq web site: http://coq.inria.fr, +.BR coq\-tex (1), +.BR coqdep (1) +.PP .I -/usr/share/doc/coqide/FAQ. - +The Coq Reference Manual +.PP +The Coq web site: http://coq.inria.fr +.PP +/usr/share/doc/coqide/FAQ +. .SH AUTHOR This manual page was written by Samuel Mimram , for the Debian project (but may be used by others). diff --git a/man/coqnative.1 b/man/coqnative.1 index ca8c128bfc03..6ffa039d2e4b 100644 --- a/man/coqnative.1 +++ b/man/coqnative.1 @@ -1,80 +1,84 @@ -.TH COQ 1 - +.TH COQNATIVE 1 +. .SH NAME -coqnative \- The Coq native compiler - - +coqnative \- native Coq compiler +. +. .SH SYNOPSIS .B coqnative [ -.B options +options ] .I filename - - +. +. .SH DESCRIPTION - +. .B coqnative compiles vo files to binary files used by the native compute mechanism -of the Coq Proof Assistant. See the Reference Manual for more -information. It returns with exit code 0 if all the requested tasks -succeeded. A non-zero return code means that something went wrong. - -.IR filename \& +of the Coq Proof Assistant. +See the +.I "Reference Manual" +for more information. +It returns with exit code 0 if all the requested tasks succeeded. +A non-zero return code means that something went wrong. +.PP +.I filename is a Coq object file (a .vo) to compile to a native binary. - +. .SH OPTIONS - +. .TP .BI \-Q \ dir\ coqdir -map physical +Map physical .I dir to logical -.I coqdir - +.I coqdir. +. .TP .BI \-R \ dir\ coqdir -synonymous for -Q - +Synonymous to +.BR \-Q . +. .TP .BI \-I \ dir -ignored, for compatibility - +Ignored, for compatibility. +. .TP -.BI \-noinit -ignored, for compatibility - +.B \-noinit +Ignored, for compatibility. +. .TP -.BI \-boot -boot mode - +.B \-boot +Boot mode. +. .TP .BI \-coqlib \ dir -override the default location of the standard library - +Override the default location of the standard library. +. .TP .BI \-nI \ dir -add +Add .I dir -to the set of paths for the native files of the dependencies - +to the set of paths for the native files of the dependencies. +. .TP .BI \-native-output-dir \ dir -output the generated files to -.I dir - +Output the generated files to +.I dir. +. .TP -.BI \-h,\ \-\-help -print list of options - +.BR \-h , \ \-\-help +Print list of options. +. .SH SEE ALSO - +. .BR coqtop (1), .BR coqc (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 diff --git a/man/coqtop.1 b/man/coqtop.1 index 06af4547b7a8..d7972f41e959 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -1,164 +1,170 @@ -.TH COQ 1 - +.TH COQTOP 1 +. .SH NAME -coqtop \- The Coq Proof Assistant toplevel system - - +coqtop \- toplevel Coq system +. +. .SH SYNOPSIS .B coqtop [ -.B options +options ] - +. .SH DESCRIPTION - +. .B coqtop is the toplevel system of Coq, for interactive use. It reads phrases on the standard input, and prints results on the standard output. - +. For batch-oriented use of Coq, see -.BR coqc(1). - - +.BR coqc (1). +. +. .SH OPTIONS - +. .TP -.B \-h, \-\-help -Help. Will give you the complete list of options accepted by coqtop. - +.BR \-h , \ \-\-help +Help. +Will give you the complete list of options accepted by coqtop. +. .TP .BI \-I \ dir, \ \-\-include \ dir -add directory +Add directory .I dir -in the include path - +in the include path. +. .TP .BI \-R \ dir\ coqdir -recursively map physical +Recursively map physical .I dir to logical -.I coqdir - +.I coqdir. +. .TP .BI \-top \ coqdir -set the toplevel name to be +Set the toplevel name to be .I coqdir -instead of Top - +instead of Top. +. .TP .B \-nois -start with an empty initial state - +Start with an empty initial state. +. .TP .BI \-load\-ml\-source \ filename -load ML file -.I filename - +Load ML file +.I filename. +. .TP .BI \-load\-ml\-object \ filename -load ML object file -.I filenname - +Load ML object file +.I filenname. +. .TP .BI \-load\-vernac\-source \ filename, \ \-l \ filename -load Coq file -.I filename.v +Load Coq file +.I filename.v. (Load filename.) - +. .TP .BI \-load\-vernac\-source\-verbose \ filename, \ \-lv \ filename -load verbosely Coq file -.I filename.v +Load verbosely Coq file +.I filename.v. (Load Verbose filename.) - +. .TP .BI \-require \ lib -load Coq library -.I lib +Load Coq library +.I lib. (Require lib.) - +. .TP .BI \-require-import \ lib, \ \-ri \ lib -load Coq library +Load Coq library .I lib -and import it (Require Import lib.) - +and import it. +(Require Import lib.) +. .TP .BI \-require-export \ lib, \ \-re \ lib -load Coq library +Load Coq library .I lib -and transitively import it (Require Export lib.) - +and transitively import it. +(Require Export lib.) +. .TP .BI \-require-from \ root\ lib, \ \-rfrom \ root\ lib -load Coq library -.I lib +Load Coq library +.I lib. (From root Require lib.) - +. .TP .BI \-require-import-from \ root\ lib, \ \-rifrom \ root\ lib -load Coq library +Load Coq library .I lib -and import it (From root Require Import lib.) - +and import it. +(From root Require Import lib.) +. .TP .BI \-require-export-from \ root\ lib, \ \-refrom \ root\ lib -load Coq library +Load Coq library .I lib -and transitively import it (From root Require Export lib.) - +and transitively import it. +(From root Require Export lib.) +. .TP .BI \-load\-vernac\-object \ lib -obsolete synonym of -.BI \-require \ lib - +Obsolete synonym of +.BR \-require . +. .TP .B \-where -print Coq's standard library location and exit - +Print Coq's standard library location and exit. +. .TP .B \-v -print Coq version and exit - +Print Coq version and exit. +. .TP .B \-q -skip loading of rcfile (resource file) if any - +Skip loading of rcfile (resource file) if any. +. .TP .BI \-init\-file \ filename -set the rcfile to -.I filename - +Set the rcfile to +.I filename. +. .TP .B \-batch -batch mode (exits just after arguments parsing) - +Batch mode (exits just after arguments parsing). +. .TP .B \-emacs -tells Coq it is executed under Emacs - +Tells Coq it is executed under Emacs. +. .TP .BI \-dump\-glob \ filename -dump globalizations in file f (to be used by -.B coqdoc(1) -) - +Dump globalizations in file +.I filename +(to be used by +.BR coqdoc (1)). +. .TP .B \-impredicative\-set -set sort Set impredicative - +Set sort Set impredicative. +. .TP .B \-dont\-load\-proofs -don't load opaque proofs in memory - +Don't load opaque proofs in memory. +. .SH SEE ALSO - +. .BR coqc (1), .BR coq-tex (1), -.BR coqdep (1). -.br +.BR coqdep (1) +.PP .I The Coq Reference Manual. -.I +.PP The Coq web site: http://coq.inria.fr diff --git a/man/coqtop.byte.1 b/man/coqtop.byte.1 index 4ef317749da1..8338b5c7971d 100644 --- a/man/coqtop.byte.1 +++ b/man/coqtop.byte.1 @@ -1,33 +1,33 @@ -.TH COQ 1 - +.TH COQTOP.BYTE 1 +. .SH NAME -coqtop.byte \- The bytecode Coq toplevel - - +coqtop.byte \- bytecode toplevel Coq system +. +. .SH SYNOPSIS .B coqtop.byte [ -.B options +options ] [ .I file ] - +. .SH DESCRIPTION - +. .B coqopt.byte -is the bytecode version of Coq. It should not be called directly, but -only by +is the bytecode version of Coq. +It should not be called directly, but only by .B coqtop and -.B coqc - +.BR coqc . +. .SH SEE ALSO - +. .BR coqtop (1), -.BR coqc (1). -.br +.BR coqc (1) +.PP .I The Coq Reference Manual. -.I +.PP The Coq web site: http://coq.inria.fr diff --git a/man/coqwc.1 b/man/coqwc.1 index 344b1fecc5c6..208b121d4adf 100644 --- a/man/coqwc.1 +++ b/man/coqwc.1 @@ -1,47 +1,47 @@ -.TH COQ 1 - +.TH COQWC 1 +. .SH NAME coqwc \- print the number of specification, proof and comment lines in Coq files - +. .SH SYNOPSIS .B coqwc [ -.BI \-p +.B \-p ] [ -.BI \-s +.B \-s ] [ -.BI \-r +.B \-r ] [ -.BI \-e +.B \-e ] -.I files ... - +.I files .\|.\|. +. .SH DESCRIPTION - +. .B coqwc computes the number of specification lines, proof lines and comment lines in Coq files. - +. .SH OPTIONS - +. .TP -.BI \-p -Print the percentage of comments +.B \-p +Print the percentage of comments. .TP -.BI \-s -Print only the number of specification lines +.B \-s +Print only the number of specification lines. .TP -.BI \-r -Print only the number of proof lines +.B \-r +Print only the number of proof lines. .TP -.BI \-e -Do not skip headers - +.B \-e +Do not skip headers. +. .SH BUGS - +. Please report any bug to -.B https://github.com/coq/coq/issues +.BR https://github.com/coq/coq/issues .