From b002b817ce305be3ba753dc1634a01b008b243bd Mon Sep 17 00:00:00 2001 From: courant Date: Wed, 25 Apr 2001 07:35:06 +0000 Subject: - Ajout pages de man pour coqc, coqtop, coqtop.opt et coqtop.byte - Deplacement pages de tools/ vers man/ - Modif distrib/Makefile pour Debian - Modif mode emacs pour Debian git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1710 85f007b7-540e-0410-9357-904b9bb8a0f7 --- man/coq-tex.1 | 125 +++++++++++++++++++++++++++++++++++++ man/coqc.1 | 48 ++++++++++++++ man/coqdep.1 | 182 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ man/coqtop.1 | 38 ++++++++++++ man/coqtop.byte.1 | 35 +++++++++++ man/coqtop.opt.1 | 35 +++++++++++ man/gallina.1 | 74 ++++++++++++++++++++++ 7 files changed, 537 insertions(+) create mode 100644 man/coq-tex.1 create mode 100644 man/coqc.1 create mode 100644 man/coqdep.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/gallina.1 (limited to 'man') diff --git a/man/coq-tex.1 b/man/coq-tex.1 new file mode 100644 index 000000000..737de70a9 --- /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/coqc.1 b/man/coqc.1 new file mode 100644 index 000000000..96fbcc2ae --- /dev/null +++ b/man/coqc.1 @@ -0,0 +1,48 @@ +.TH COQ 1 "April 24, 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 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 000000000..01d080fc2 --- /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/coqtop.1 b/man/coqtop.1 new file mode 100644 index 000000000..5662a3dc4 --- /dev/null +++ b/man/coqtop.1 @@ -0,0 +1,38 @@ +.TH COQ 1 "April 24, 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 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 000000000..4248c9e3d --- /dev/null +++ b/man/coqtop.byte.1 @@ -0,0 +1,35 @@ +.TH COQ 1 "April 24, 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 000000000..8b6b362a1 --- /dev/null +++ b/man/coqtop.opt.1 @@ -0,0 +1,35 @@ +.TH COQ 1 "April 24, 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/gallina.1 b/man/gallina.1 new file mode 100644 index 000000000..8c607216e --- /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 + + + + + + + + + + + + + -- cgit v1.2.3