From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- man/coq-interface.1 | 37 +++++++++++ man/coq-tex.1 | 125 ++++++++++++++++++++++++++++++++++++ man/coq_makefile.1 | 33 ++++++++++ man/coqc.1 | 49 ++++++++++++++ man/coqdep.1 | 182 ++++++++++++++++++++++++++++++++++++++++++++++++++++ man/coqdoc.1 | 33 ++++++++++ man/coqmktop.1 | 41 ++++++++++++ man/coqtop.1 | 39 +++++++++++ man/coqtop.byte.1 | 35 ++++++++++ man/coqtop.opt.1 | 35 ++++++++++ man/coqwc.1 | 47 ++++++++++++++ man/gallina.1 | 74 +++++++++++++++++++++ man/parser.1 | 30 +++++++++ 13 files changed, 760 insertions(+) create mode 100644 man/coq-interface.1 create mode 100644 man/coq-tex.1 create mode 100644 man/coq_makefile.1 create mode 100644 man/coqc.1 create mode 100644 man/coqdep.1 create mode 100644 man/coqdoc.1 create mode 100644 man/coqmktop.1 create mode 100644 man/coqtop.1 create mode 100644 man/coqtop.byte.1 create mode 100644 man/coqtop.opt.1 create mode 100644 man/coqwc.1 create mode 100644 man/gallina.1 create mode 100644 man/parser.1 (limited to 'man') diff --git a/man/coq-interface.1 b/man/coq-interface.1 new file mode 100644 index 00000000..2ab2bf95 --- /dev/null +++ b/man/coq-interface.1 @@ -0,0 +1,37 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coq-interface \- + + +.SH SYNOPSIS +.B coq-interface +[ +.B options +] + +.SH DESCRIPTION + +.B coq-interface +is a Coq customized toplevel system for Coq containing some modules +useful for the graphical interface. This program is not for the casual +user. + +.SH OPTIONS + +.TP +.B \-h +Help. Will give you the complete list of options accepted by +coq-interface (the same as coqtop). + +.SH SEE ALSO + +.BR coqc (1), +.BR coqdep (1), +.BR coqtop (1), +.BR parser (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/man/coq-tex.1 b/man/coq-tex.1 new file mode 100644 index 00000000..737de70a --- /dev/null +++ b/man/coq-tex.1 @@ -0,0 +1,125 @@ +.TH COQ-TEX 1 "29 March 1995" + +.SH NAME +coq-tex \- Process Coq phrases embedded in LaTeX files + +.SH SYNOPSIS +.B coq-tex +[ +.BI \-o \ output-file +] +[ +.BI \-n \ line-width +] +[ +.BI \-image \ coq-image +] +[ +.B -w +] +[ +.B -v +] +[ +.B -sl +] +[ +.B -hrule +] +[ +.B -small +] +.I input-file ... + + +.SH DESCRIPTION + +The +.B coq-tex +filter extracts Coq phrases embedded in LaTeX files, evaluates +them, and insert the outcome of the evaluation after each phrase. + +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. +.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. +.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. +.PP +The resulting LaTeX code is stored in the file +.IR file \&.v.tex +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. + +The files produced by +.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. +.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. +.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 +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. +.TP +.B -v +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. +.TP +.B -hrule +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. + + +.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. +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. +(The responses ``lag behind''.) + +.SH SEE ALSO + +.B coqtop +(1). diff --git a/man/coq_makefile.1 b/man/coq_makefile.1 new file mode 100644 index 00000000..b5de6d36 --- /dev/null +++ b/man/coq_makefile.1 @@ -0,0 +1,33 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coq_makefile \- The Coq Proof Assistant makefile generator + + +.SH SYNOPSIS +.B coq_makefile +[ +.B 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. + +.SH SEE ALSO + +.BR coqtop (1), +.BR coqtc (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/man/coqc.1 b/man/coqc.1 new file mode 100644 index 00000000..741b3dcb --- /dev/null +++ b/man/coqc.1 @@ -0,0 +1,49 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coqc \- The Coq Proof Assistant compiler + + +.SH SYNOPSIS +.B coqc +[ +.B 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 \& +is the vernacular file to compile. +.IR file \& +must be formed +only with the characters `a` to `Z`, `0`-`9` or `_` and must begin +with a letter. +The compiler produces an object file +.IR file.vo \&. + +For interactive use of Coq, see +.BR coqtop(1). + + +.SH OPTIONS + +.TP +.BI \-h +Will give you a description of the whole list of options of coqc and +coqtop. + +.SH SEE ALSO + +.BR coqtop (1), +.BR coq_makefile (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/man/coqdep.1 b/man/coqdep.1 new file mode 100644 index 00000000..01d080fc --- /dev/null +++ b/man/coqdep.1 @@ -0,0 +1,182 @@ +.TH COQ 1 "28 March 1995" "Coq tools" + +.SH NAME +coqdep \- Compute inter-module dependencies for Coq and Caml programs + +.SH SYNOPSIS +.B coqdep +[ +.BI \-w +] +[ +.BI \-I \ directory +] +[ +.BI \-coqlib \ directory +] +[ +.BI \-c +] +[ +.BI \-i +] +[ +.BI \-D +] +.I filename ... +.I directory ... + +.SH DESCRIPTION + +.B coqdep +compute inter-module dependencies for Coq and Caml programs, +and prints the dependencies on the standard output in a format +readable by make. +When a directory is given as argument, it is recursively looked at. + +Dependencies of Coq modules are computed by looking at +.IR Require \& +commands (Require, Require Export, Require Import, Require Implementation), +and +.IR Declare \& +.IR ML \& +.IR Module \& +commands. Dependencies relative to modules from the Coq library are not +printed. + +Dependencies of Caml modules are computed by looking at +.IR open \& +directives and the dot notation +.IR module.value \&. + +.SH OPTIONS + +.TP +.BI \-c +Prints the dependencies of Caml modules. +(On Caml modules, the behaviour is exactly the same as cldepend, +except that nested comments and strings are correctly handled). +.TP +.BI \-w +Prints a warning if a Coq command +.IR Declare \& +.IR ML \& +.IR Module \& +is incorrect. (For instance, you wrote `Declare ML Module "A".', +but the module A contains #open "B"). The correct command is printed +(see option -D). The warning is printed on standard error. +.TP +.BI \-i +Prints also the dependencies for .vi files (Coq specification modules). +.TP +.BI \-D +This commands looks for every command +.IR Declare \& +.IR ML \& +.IR Module \& +of each Coq file given as argument and complete (if needed) +the list of Caml modules. The new command is printed on +the standard output. No dependency is computed with this option. +.TP +.BI \-I \ directory +The files .v .ml .mli of the directory +.IR directory \& +are taken into account during the calculus of dependencies, +but their own dependencies are not printed. +.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. + + +.SH SEE ALSO + +.BR ocamlc (1), +.BR coqc (1), +.BR make (1). +.br + +.SH NOTES + +Lexers (for Coq and Caml) correctly handle nested comments +and strings. + +The treatment of symbolic links is primitive. + +If two files have the same name, in two different directories, +a warning is printed on standard error. + +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.ml B.ml C.ml D.ml X.v Y.v and Z.v + +where +.TP +.BI \+ +D.ml contains the commands `#open "A"', `#open "B"' and `type t = C__t' ; +.TP +.BI \+ +Y.v contains the command `Require X' ; +.TP +.BI \+ +Z.v contains the commands `Require X' and `Declare ML Module "D"'. +.LP +To get the dependencies of the Coq files: +.IP +.B +example% coqdep -I . *.v +.RS +.sp .5 +.nf +.B Z.vo: Z.v ./X.vo ./D.zo +.B Y.vo: Y.v ./X.vo +.B X.vo: X.v +.fi +.RE +.br +.ne 7 +.LP +With a warning: +.IP +.B +example% coqdep -w -I . *.v +.RS +.sp .5 +.nf +.B Z.vo: Z.v ./X.vo ./D.zo +.B Y.vo: Y.v ./X.vo +.B X.vo: X.v +### Warning : In file Z.v, the ML modules declaration should be +### Declare ML Module "A" "B" "C" "D". +.fi +.RE +.br +.ne 7 +.LP +To get only the Caml dependencies: +.IP +.B +example% coqdep -c -I . *.ml +.RS +.sp .5 +.nf +.B D.zo: D.ml ./A.zo ./B.zo ./C.zo +.B C.zo: C.ml +.B B.zo: B.ml +.B A.zo: A.ml +.fi +.RE +.br +.ne 7 + +.SH BUGS + +Please report any bug to +.B coq-bugs@pauillac.inria.fr diff --git a/man/coqdoc.1 b/man/coqdoc.1 new file mode 100644 index 00000000..c325d221 --- /dev/null +++ b/man/coqdoc.1 @@ -0,0 +1,33 @@ +.TH coqdoc 1 "February, 2002" + +.SH NAME +coqdoc \- A documentation tool for the Coq proof assistant + + +.SH SYNOPSIS +.B coqdoc +[ +.B options +] +.B 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 + +.TP +.B \-h +Help. Will give you the complete list of options accepted by coqdoc. + + +.SH SEE ALSO + +.I +The Coq web site: http://coq.inria.fr/ diff --git a/man/coqmktop.1 b/man/coqmktop.1 new file mode 100644 index 00000000..05e73d75 --- /dev/null +++ b/man/coqmktop.1 @@ -0,0 +1,41 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coqmktop \- The Coq Proof Assistant user-tactics linker + + +.SH SYNOPSIS +.B coqmktop +[ +.I options +] +.I files + + +.SH DESCRIPTION + +.B coqmktop +builds a new Coq toplevel extended with user-tactics. +.IR files \& +are the Objective Caml object or library files (i.e. with suffix .cmo, +.cmx, .cma or .cmxa) to link with the Coq system. +The linker produces an executable Coq toplevel which can be called +directly or through coqc(1), using the -image option. + +.SH OPTIONS + +.TP +.BI \-h +Help. List the available options. + +.SH SEE ALSO + +.BR coqtop (1), +.BR ocamlmktop (1). +.BR ocamlc (1). +.BR ocamlopt (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/man/coqtop.1 b/man/coqtop.1 new file mode 100644 index 00000000..d75b283f --- /dev/null +++ b/man/coqtop.1 @@ -0,0 +1,39 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coqtop \- The Coq Proof Assistant toplevel system + + +.SH SYNOPSIS +.B coqtop +[ +.B 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). + + +.SH OPTIONS + +.TP +.B \-h +Help. Will give you the complete list of options accepted by coqtop. + +.SH SEE ALSO + +.BR coqc (1), +.BR coq-tex (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr diff --git a/man/coqtop.byte.1 b/man/coqtop.byte.1 new file mode 100644 index 00000000..ad1a358c --- /dev/null +++ b/man/coqtop.byte.1 @@ -0,0 +1,35 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coqtop.byte \- The bytecode Coq toplevel + + +.SH SYNOPSIS +.B coqtop.byte +[ +.B options +] +[ +.I file +] + +.SH DESCRIPTION + +.B coqopt.byte +is the bytecode version of Coq. It should not be called directly, but +only by +.B coqtop +and +.B coqc + +.SH SEE ALSO + +.BR coqtop (1), +.BR coqc (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr + + diff --git a/man/coqtop.opt.1 b/man/coqtop.opt.1 new file mode 100644 index 00000000..17c763da --- /dev/null +++ b/man/coqtop.opt.1 @@ -0,0 +1,35 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +coqtop.opt \- The native-code Coq toplevel + + +.SH SYNOPSIS +.B coqopt.opt +[ +.B options +] +[ +.I file +] + +.SH DESCRIPTION + +.B coqopt.opt +is the native-code version of Coq. It should not be called directly, but +only by +.B coqtop +and +.B coqc + +.SH SEE ALSO + +.BR coqtop (1), +.BR coqc (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr + + diff --git a/man/coqwc.1 b/man/coqwc.1 new file mode 100644 index 00000000..7011d148 --- /dev/null +++ b/man/coqwc.1 @@ -0,0 +1,47 @@ +.TH COQ 1 "16 March 2004" "Coq tools" + +.SH NAME +coqwc \- print the number of specification, proof and comment lines in +Coq files + +.SH SYNOPSIS +.B coqwc +[ +.BI \-p +] +[ +.BI \-s +] +[ +.BI \-r +] +[ +.BI \-e +] +.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 +.TP +.BI \-s +Print only the number of specification lines +.TP +.BI \-r +Print only the number of proof lines +.TP +.BI \-e +Do not skip headers + +.SH BUGS + +Please report any bug to +.B coq-bugs@pauillac.inria.fr diff --git a/man/gallina.1 b/man/gallina.1 new file mode 100644 index 00000000..8c607216 --- /dev/null +++ b/man/gallina.1 @@ -0,0 +1,74 @@ +.TH COQ 1 "29 March 1995" "Coq tools" + +.SH NAME +gallina \- extracts specification from Coq vernacular files + +.SH SYNOPSIS +.B gallina +[ +.BI \- +] +[ +.BI \-stdout +] +[ +.BI \-nocomments +] +.I file ... + +.SH DESCRIPTION + +.B gallina +takes Coq files as arguments and builds the corresponding +specification files. +The Coq file +.IR foo.v \& +gives bearth to the specification file +.IR foo.g. \& +The suffix '.g' stands for Gallina. + +For that purpose, gallina removes all commands that follow a +"Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it +reaches a command "Abort.", "Save.", "Qed.", "Defined." or "Proof +<...>.". It also removes every "Hint", "Syntax", +"Immediate" or "Transparent" command. + +Files without the .v suffix are ignored. + + +.SH OPTIONS + +.TP +.BI \-stdout +Prints the result on standard output. +.TP +.BI \- +Coq source is taken on standard input. The result is printed on +standard output. +.TP +.BI \-nocomments +Comments are removed in the *.g file. + +.SH NOTES + +Nested comments are correctly handled. In particular, every command +"Save." or "Abort." in a comment is not taken into account. + + +.SH BUGS + +Please report any bug to +.B coq@pauillac.inria.fr + + + + + + + + + + + + + diff --git a/man/parser.1 b/man/parser.1 new file mode 100644 index 00000000..d89465d8 --- /dev/null +++ b/man/parser.1 @@ -0,0 +1,30 @@ +.TH COQ 1 "April 25, 2001" + +.SH NAME +parser \- Coq parser + + +.SH SYNOPSIS +.B parser +[ +.B options +] + +.SH DESCRIPTION + +.B parser +is a program reading Coq proof developments and outputing them in the +structured format given in the INRIA technical report RT154. This +program is not for the casual user. + +.SH SEE ALSO + +.BR coq-interface (1), +.BR coqc (1), +.BR coqtop (1), +.BR coqdep (1). +.br +.I +The Coq Reference Manual. +.I +The Coq web site: http://coq.inria.fr -- cgit v1.2.3