diff options
Diffstat (limited to 'doc/refman/RefMan-uti.tex')
-rw-r--r-- | doc/refman/RefMan-uti.tex | 227 |
1 files changed, 0 insertions, 227 deletions
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex deleted file mode 100644 index bda4cff9..00000000 --- a/doc/refman/RefMan-uti.tex +++ /dev/null @@ -1,227 +0,0 @@ -\chapter[Utilities]{Utilities\label{Utilities}} - -The distribution provides utilities to simplify some tedious works -beside proof development, tactics writing or documentation. - -\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}} - -The native-code version of \Coq\ cannot dynamically load user tactics -using Objective Caml code. It is possible to build a toplevel of \Coq, -with Objective Caml code statically linked, with the tool {\tt - coqmktop}. - -For example, one can build a native-code \Coq\ toplevel extended with a tactic -which source is in {\tt tactic.ml} with the command -\begin{verbatim} - % coqmktop -opt -o mytop.out tactic.cmx -\end{verbatim} -where {\tt tactic.ml} has been compiled with the native-code -compiler {\tt ocamlopt}. This command generates an executable -called {\tt mytop.out}. To use this executable to compile your \Coq\ -files, use {\tt coqc -image mytop.out}. - -A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}), -which can be generated by {\tt coqmktop -opt -o coqopt.opt}. - - -\paragraph[Application: how to use the Objective Caml debugger with Coq.]{Application: how to use the Objective Caml debugger with Coq.\index{Debugger}} - -One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in -order to debug your tactics with the Objective Caml debugger. -You need to have configured and compiled \Coq\ for debugging -(see the file \texttt{INSTALL} included in the distribution). -Then, you must compile the Caml modules of your tactic with the -option \texttt{-g} (with the bytecode compiler) and build a stand-alone -bytecode toplevel with the following command: - -\begin{quotation} -\texttt{\% coqmktop -g -o coq-debug}~\emph{<your \texttt{.cmo} files>} -\end{quotation} - - -To launch the \ocaml\ debugger with the image you need to execute it in -an environment which correctly sets the \texttt{COQLIB} variable. -Moreover, you have to indicate the directories in which -\texttt{ocamldebug} should search for Caml modules. - -A possible solution is to use a wrapper around \texttt{ocamldebug} -which detects the executables containing the word \texttt{coq}. In -this case, the debugger is called with the required additional -arguments. In other cases, the debugger is simply called without additional -arguments. Such a wrapper can be found in the \texttt{dev/} -subdirectory of the sources. - -\section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies} - \index{Coqdep@{\tt coqdep}}} - -In order to compute modules dependencies (so to use {\tt make}), -\Coq\ comes with an appropriate tool, {\tt coqdep}. - -{\tt coqdep} computes inter-module dependencies for \Coq\ and -\ocaml\ 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 {\tt Require} -commands ({\tt Require}, {\tt Requi\-re Export}, {\tt Require Import}, -but also at the command {\tt Declare ML Module}. - -Dependencies of \ocaml\ modules are computed by looking at -\verb!open! commands and the dot notation {\em module.value}. However, -this is done approximatively and you are advised to use {\tt ocamldep} -instead for the \ocaml\ modules dependencies. - -See the man page of {\tt coqdep} for more details and options. - - -\section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile} -\index{Makefile@{\tt Makefile}} -\index{CoqMakefile@{\tt coq\_Makefile}}} - -When a proof development becomes large and is split into several files, -it becomes crucial to use a tool like {\tt make} to compile \Coq\ -modules. - -The writing of a generic and complete {\tt Makefile} may be a tedious work -and that's why \Coq\ provides a tool to automate its creation, -{\tt coq\_makefile}. - -Arguments are explain by \texttt{\% coq\_makefile --help}. They can be directly -written in the command line but it is recommended to write them in a file (called -for example {\tt Make}) and then call {\tt coq\_makefile -f Make -o - Makefile}. That means options are in {\tt Make} file and output is {\tt - Makefile} This way, {\tt Makefile} will be automatically regenerated if -something changes in {\tt Make}. - -The first time you use this tool, you may be happy with: -\begin{quotation} -\texttt{\% \{ echo '-R .} {\em MyFancyLib} \texttt{' ; find -name '*.v' -print \} > - Make \&\& coq\_makefile -f Make -o Makefile} -\end{quotation} - -To customize things afterwards, remember: -\begin{itemize} -\item Coq files must end in {\tt .v}, caml modules in {\tt .ml4} if they - require camlp preproccessing (and in {\tt .ml} otherwise), and caml module signatures in {\tt - .mli}. -\item If you give a directory directly as argument, it is because you provide a - Makefile for it in it. -\item {\tt -R} option is for Coq, {\tt -I} for caml. The same directory can - ``included'' by both. - Using {\tt -R} option gives a right logical path and a correct installation - emplacement to your coq files. -\item If your files depend on an external library that isn't install somewhere - looked by coqc, use {\tt OTHERFLAGS = '-R path/to/lib lib\_name'} option in your {\tt - Make} but don't do {\tt -R \dots} directly, the {\em make clean} command would - erase it! -\end{itemize} - -\Warning To compile a project containing \ocaml{} files you must keep -the sources of \Coq{} somewhere and have an environment variable named -\texttt{COQTOP} that points to that directory. - -\section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc} -\index{Coqdoc@{\sf coqdoc}}} - -\input{./coqdoc} - -\section{Exporting \Coq\ theories to XML} - -\input{./Helm} - -\section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex} - \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}} - -When writing a documentation about a proof development, one may want -to insert \Coq\ phrases inside a \LaTeX\ document, possibly together with -the corresponding answers of the system. We provide a -mechanical way to process such \Coq\ phrases embedded in \LaTeX\ files: the -{\tt coq-tex} filter. This filter extracts Coq phrases embedded in -LaTeX files, evaluates them, and insert the outcome of the evaluation -after each phrase. - -Starting with a file {\em file}{\tt.tex} containing \Coq\ phrases, -the {\tt coq-tex} filter produces a file named {\em file}{\tt.v.tex} with -the \Coq\ outcome. - -There are options to produce the \Coq\ parts in smaller font, italic, -between horizontal rules, etc. -See the man page of {\tt coq-tex} for more details. - -\medskip\noindent {\bf Remark.} This Reference Manual and the Tutorial -have been completely produced with {\tt coq-tex}. - - -\section[\Coq\ and \emacs]{\Coq\ and \emacs\label{Emacs}\index{Emacs}} - -\subsection{The \Coq\ Emacs mode} - -\Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides -syntax highlighting -and also a rudimentary indentation facility -in the style of the Caml \emacs\ mode. - -Add the following lines to your \verb!.emacs! file: - -\begin{verbatim} - (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) -\end{verbatim} - -The \Coq\ major mode is triggered by visiting a file with extension {\tt .v}, -or manually with the command \verb!M-x coq-mode!. -It gives you the correct syntax table for -the \Coq\ language, and also a rudimentary indentation facility: -\begin{itemize} - \item pressing {\sc Tab} at the beginning of a line indents the line like - the line above; - - \item extra {\sc Tab}s increase the indentation level - (by 2 spaces by default); - - \item M-{\sc Tab} decreases the indentation level. -\end{itemize} - -An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also -included in the distribution, in file \texttt{coq-inferior.el}. -Instructions to use it are contained in this file. - -\subsection[Proof General]{Proof General\index{Proof General}} - -Proof General is a generic interface for proof assistants based on -Emacs. The main idea is that the \Coq\ commands you are -editing are sent to a \Coq\ toplevel running behind Emacs and the -answers of the system automatically inserted into other Emacs buffers. -Thus you don't need to copy-paste the \Coq\ material from your files -to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some -files. - -Proof General is developped and distributed independently of the -system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!. - - -\section[Module specification]{Module specification\label{gallina}\index{Gallina@{\tt gallina}}} - -Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its -specification (inductive types declarations, definitions, type of -lemmas and theorems), removing the proofs parts of the file. The \Coq\ -file {\em file}{\tt.v} gives birth to the specification file -{\em file}{\tt.g} (where the suffix {\tt.g} stands for \gallina). - -See the man page of {\tt gallina} for more details and options. - - -\section[Man pages]{Man pages\label{ManPages}\index{Man pages}} - -There are man pages for the commands {\tt coqdep}, {\tt gallina} and -{\tt coq-tex}. Man pages are installed at installation time -(see installation instructions in file {\tt INSTALL}, step 6). - -%BEGIN LATEX -\RefManCutCommand{ENDREFMAN=\thepage} -%END LATEX - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: |