Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Coqtop and coqc: cleaning description of options in RefMan and manpages.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14934 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit df9ef93cd565a7a45589dd77ba8aa1a2ab81dcec 1 parent fa5d9b8
@pirbo pirbo authored
View
147 doc/refman/RefMan-com.tex
@@ -59,8 +59,7 @@ \section{Batch compilation ({\tt coqc})}
number (e.g. 8.3). If this file is not found, then the file
\verb:$XDG_CONFIG_HOME/coqrc: is searched. You can also specify an
arbitrary name for the resource file (see option \verb:-init-file:
-below), or the name of another user to load the resource file of someone
-else (see option \verb:-user:).
+below).
This file may contain, for instance, \verb:Add LoadPath: commands to add
@@ -74,7 +73,7 @@ \section{Batch compilation ({\tt coqc})}
There are four environment variables used by the \Coq\ system.
\verb:$COQBIN: for the directory where the binaries are,
\verb:$COQLIB: for the directory where the standard library is,
-\verb:$COQPATH: for a list of directories seperated by \verb|:|
+\verb:$COQPATH: for a list of directories separated by \verb|:|
(\verb|;| on windows) to add to the load path, and
\verb:$COQTOP: for the directory of the sources. The latter is useful
only for developers that are writing their own tactics and are using
@@ -96,86 +95,52 @@ \section{Batch compilation ({\tt coqc})}
coqc} and {\tt coqtop}, unless stated otherwise:
\begin{description}
-\item[{\tt -byte}]\
+\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}[ {\tt -as} {\em dirpath}]]\
- Run the byte-code version of \Coq{}.
-
-\item[{\tt -opt}]\
-
- Run the native-code version of \Coq{}.
-
-\item[{\tt -I} {\em directory}, {\tt -include} {\em directory}]\
-
- Add physical path {\em directory} to the list of directories where to
- look for a file and bind it to the empty logical directory. The
- subdirectory structure of {\em directory} is recursively available
- from {\Coq} using absolute names (see Section~\ref{LongNames}).
-
-\item[{\tt -I} {\em directory} {\tt -as} {\em dirpath}]\
-
- Add physical path {\em directory} to the list of directories where to
- look for a file and bind it to the logical directory {\dirpath}. The
- subdirectory structure of {\em directory} is recursively available
- from {\Coq} using absolute names extending the {\dirpath} prefix.
+Add physical path {\em directory} to the list of directories where to look for a
+file and bind it to the empty logical directory/the logical directory {\em
+ dirpath}. The sub-directory structure of {\em directory} is recursively available
+from {\Coq} using absolute names (extending the {\dirpath} prefix) (see
+Section~\ref{LongNames}).
\SeeAlso {\tt Add LoadPath} in Section~\ref{AddLoadPath} and logical
paths in Section~\ref{Libraries}.
-\item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} {\tt -as} {\dirpath}]\
+\item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} [{\tt -as} {\dirpath}]]\
Do as {\tt -I} {\em directory} {\tt -as} {\dirpath} but make the
- subdirectory structure of {\em directory} recursively visible so
+ sub-directory structure of {\em directory} recursively visible so
that the recursive contents of physical {\em directory} is available
from {\Coq} using short or partially qualified names.
\SeeAlso {\tt Add Rec LoadPath} in Section~\ref{AddRecLoadPath} and logical
paths in Section~\ref{Libraries}.
-\item[{\tt -top} {\dirpath}]\
-
- This sets the toplevel module name to {\dirpath} instead of {\tt
- Top}. Not valid for {\tt coqc}.
+\item[{\tt -top} {\dirpath}, {\tt -notop}]\
-\item[{\tt -notop} {\dirpath}]\
-
- This sets the toplevel module name to the empty logical dirpath. Not
- valid for {\tt coqc}.
+ This sets the toplevel module name to {\dirpath}/the empty logical path instead
+ of {\tt Top}. Not valid for {\tt coqc}.
\item[{\tt -exclude-dir} {\em subdirectory}]\
- This tells to exclude any subdirectory named {\em subdirectory}
+ This tells to exclude any sub-directory named {\em subdirectory}
while processing option {\tt -R}. Without this option only the
- conventional version control management subdirectories named {\tt
+ conventional version control management sub-directories named {\tt
CVS} and {\tt \_darcs} are excluded.
-\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}]\
-
- Cause \Coq~to use the state put in the file {\em file} as its input
- state. The default state is {\em initial.coq}.
- Mainly useful to build the standard input state.
+\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}, {\tt -outputstate} {\em file}]\
-\item[{\tt -outputstate} {\em file}]\
+ Load at the beginning/Dump at the end a \Coq{} state from the file {\em file}.
- Cause \Coq~to dump its state to file {\em file}.coq just after finishing
- parsing and evaluating all the arguments from the command line.
+ Incompatible with some not purely functional aspect of the code
\item[{\tt -nois}]\
- Cause \Coq~to begin with an empty state. Mainly useful to build the
- standard input state.
-
-%Obsolete?
-%
-%\item[{\tt -notactics}]\
-%
-% Forbid the dynamic loading of tactics in the bytecode version of {\Coq}.
-
-\item[{\tt -init-file} {\em file}]\
-
- Take {\em file} as the resource file.
+ Cause \Coq~to begin with an empty state.
-\item[{\tt -q}]\
+\item[{\tt -init-file} {\em file}, {\tt -q}]\
+ Take {\em file} as the resource file. /
Cause \Coq~not to load the resource file.
\item[{\tt -load-ml-source} {\em file}]\
@@ -186,51 +151,34 @@ \section{Batch compilation ({\tt coqc})}
Load the Caml object file {\em file}.
-\item[{\tt -l} {\em file}, {\tt -load-vernac-source} {\em file}]\
+\item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\
- Load \Coq~file {\em file}{\tt .v}
-
-\item[{\tt -lv} {\em file}, {\tt -load-vernac-source-verbose} {\em file}]\
-
- Load \Coq~file {\em file}{\tt .v} with
- a copy of the contents of the file on standard input.
+ Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
+ standard input.
\item[{\tt -load-vernac-object} {\em file}]\
Load \Coq~compiled file {\em file}{\tt .vo}
-%\item[{\tt -preload} {\em file}]\ \\
-%Add {\em file}{\tt .vo} to the files to be loaded and opened
-%before making the initial state.
-%
\item[{\tt -require} {\em file}]\
Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
Require} {\em file}).
-\item[{\tt -compile} {\em file}]\
-
- This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo}.
- This option implies options {\tt -batch} and {\tt -silent}. It is
- only available for {\tt coqtop}.
+\item[{\tt -compile} {\em file},{\tt -compile-verbose} {\em file}, {\tt -batch}]\
-\item[{\tt -compile-verbose} {\em file}]\
+ {\tt coqtop} options only used internally by {\tt coqc}.
- This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} with
- a copy of the contents of the file on standard input.
- This option implies options {\tt -batch} and {\tt -silent}. It is
- only available for {\tt coqtop}.
+ This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} without/with a
+ copy of the contents of the file on standard input. This option implies options
+ {\tt -batch} (exit just after arguments parsing). It is only
+ available for {\tt coqtop}.
\item[{\tt -verbose}]\
This option is only for {\tt coqc}. It tells to compile the file with
a copy of its contents on standard input.
-\item[{\tt -batch}]\
-
- Batch mode : exit just after arguments parsing. This option is only
- used by {\tt coqc}.
-
%Mostly unused in the code
%\item[{\tt -debug}]\
%
@@ -241,13 +189,23 @@ \section{Batch compilation ({\tt coqc})}
This option is for use with {\tt coqc}. It tells \Coq\ to export on
the standard output the content of the compiled file into XML format.
+\item[{\tt -with-geoproof} (yes|no)]\
+
+ Activate or not special functions for Geoproof within Coqide (default is yes).
+
+\item[{\tt -beautify}]\
+
+ While compiling {\em file}, pretty prints each command just after having parsing
+ it in {\em file}{\tt .beautified} in order to get old-fashion
+ syntax/definitions/notations.
+
\item[{\tt -quality}]
Improve the legibility of the proof terms produced by some tactics.
-\item[{\tt -emacs}]\
+\item[{\tt -emacs}, {\tt -ide-slave}]\
- Tells \Coq\ it is executed under Emacs.
+ Start a special main loop to communicate with ide.
\item[{\tt -impredicative-set}]\
@@ -256,11 +214,16 @@ \section{Batch compilation ({\tt coqc})}
some standard axioms of classical mathematics such as the functional
axiom of choice or the principle of description
-\item[{\tt -dump-glob} {\em file}]\
+\item[{\tt -compat} {\em version}] \null
+
+ Attempt to maintain some of the incompatible changes in their {\em version}
+ behavior.
+
+\item[{\tt -dump-glob} {\em file}]\
This dumps references for global names in file {\em file}
(to be used by coqdoc, see~\ref{coqdoc})
-
+
\item[{\tt -dont-load-proofs}]\
Warning: this is an unsafe mode.
@@ -283,6 +246,8 @@ \section{Batch compilation ({\tt coqc})}
Proofs of opaque theorems are loaded in memory as soon as the
corresponding {\tt Require} is done. This used to be Coq's default behavior.
+\item[{\tt -no-hash-consing}] \null
+
\item[{\tt -vm}]\
This activates the use of the bytecode-based conversion algorithm
@@ -290,18 +255,20 @@ \section{Batch compilation ({\tt coqc})}
\item[{\tt -image} {\em file}]\
- This option sets the binary image to be used to be {\em file}
+ This option sets the binary image to be used by {\tt coqc} to be {\em file}
instead of the standard one. Not of general use.
\item[{\tt -bindir} {\em directory}]\
Set for {\tt coqc} the directory containing \Coq\ binaries.
It is equivalent to do \texttt{export COQBIN=}{\em directory}
- before lauching {\tt coqc}.
+ before launching {\tt coqc}.
-\item[{\tt -where}]\
+\item[{\tt -where}, {\tt -config}, {\tt -filteropts}]\
- Print the \Coq's standard library location and exit.
+ Print the \Coq's standard library location or \Coq's binaries, dependencies,
+ libraries locations or the list of command line arguments that {\tt coqtop} has
+ recognize as options and exit.
\item[{\tt -v}]\
View
12 man/coqc.1
@@ -40,6 +40,18 @@ with option
it accepts the same options as
.B coqtop.
+.TP
+.BI \-image \ bin
+use
+.I bin
+as underlying
+.B coqtop
+instead of the default one.
+
+.TP
+.BI \-verbose
+print the compiled file on the standard output.
+
.SH SEE ALSO
.BR coqtop (1),
View
6 man/coqtop.1
@@ -135,12 +135,6 @@ set the rcfile to
.I filename
.TP
-.BI \-user \ uid
-use the rcfile of user
-.I uid
-
-
-.TP
.B \-batch
batch mode (exits just after arguments parsing)
View
23 scripts/coqc.ml
@@ -28,8 +28,6 @@ let image = ref ""
(* coqc options *)
-let specification = ref false
-let keep = ref false
let verbose = ref false
(* Verifies that a string starts by a letter and do not contain
@@ -104,28 +102,21 @@ let parse_args () =
let rec parse (cfiles,args) = function
| [] ->
List.rev cfiles, List.rev args
- | "-i" :: rem ->
- specification := true ; parse (cfiles,args) rem
- | "-t" :: rem ->
- keep := true ; parse (cfiles,args) rem
| ("-verbose" | "--verbose") :: rem ->
verbose := true ; parse (cfiles,args) rem
- | "-boot" :: rem ->
- Flags.boot := true;
- parse (cfiles, "-boot"::args) rem
- | "-byte" :: rem ->
- binary := "coqtop.byte"; parse (cfiles,args) rem
- | "-opt" :: rem ->
- binary := "coqtop.opt"; parse (cfiles,args) rem
| "-image" :: f :: rem ->
image := f; parse (cfiles,args) rem
| "-image" :: [] ->
usage ()
+ | "-byte" :: rem ->
+ binary := "coqtop.byte"; parse (cfiles,args) rem
+ | "-opt" :: rem ->
+ binary := "coqtop.opt"; parse (cfiles,args) rem
| "-libdir" :: _ :: rem ->
- print_string "Warning: option -libdir deprecated\n"; flush stdout;
+ print_string "Warning: option -libdir deprecated and ignored\n"; flush stdout;
parse (cfiles,args) rem
| ("-db"|"-debugger") :: rem ->
- print_string "Warning: option -db/-debugger deprecated\n";flush stdout;
+ print_string "Warning: option -db/-debugger deprecated and ignored\n";flush stdout;
parse (cfiles,args) rem
| ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
@@ -150,7 +141,7 @@ let parse_args () =
| "-R" :: s :: "-as" :: [] -> usage ()
| "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
- | ("-notactics"|"-debug"|"-nolib"
+ | ("-notactics"|"-debug"|"-nolib"|"-boot"
|"-batch"|"-nois"|"-noglob"|"-no-glob"
|"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
|"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
Please sign in to comment.
Something went wrong with that request. Please try again.