diff options
Diffstat (limited to 'doc/faq/FAQ.tex')
| -rw-r--r-- | doc/faq/FAQ.tex | 172 |
1 files changed, 124 insertions, 48 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index bd6f7dbf..c0f8c087 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -22,7 +22,6 @@ \usepackage[dvips]{graphicx} \fi -\input{../common/version.tex} %\input{../macros.tex} % Making hevea happy @@ -134,7 +133,7 @@ %%%%%%% Coq pour les nuls %%%%%%% -\title{Coq Version {\coqversion} for the Clueless\\ +\title{Coq Version 8.3 for the Clueless\\ \large(\protect\ref{lastquestion} \ Hints) } @@ -166,7 +165,7 @@ proofs in \Coq. Since we are singularly short-minded, we wrote the answers we found on bits of papers to have them at hand whenever the situation occurs again. This is pretty much the result of that: a collection of tips one can refer to when proofs become intricate. Yes, -this means we won't take the blame for the shortcomings of this +it means we won't take the blame for the shortcomings of this FAQ. But if you want to contribute and send in your own question and answers, feel free to write to us\ldots @@ -372,7 +371,7 @@ downloadable postscripts. \Question{Where can I find this FAQ on the web?} -This FAQ is available online at \ahref{http://coq.inria.fr/faq}{\url{http://coq.inria.fr/faq}}. +This FAQ is available online at \ahref{http://coq.inria.fr/doc/faq.html}{\url{http://coq.inria.fr/doc/faq.html}}. \Question{How can I submit suggestions / improvements / additions for this FAQ?} @@ -380,20 +379,20 @@ This FAQ is unfinished (in the sense that there are some obvious sections that are missing). Please send contributions to Coq-Club. \Question{Is there any mailing list about {\Coq}?} -The main {\Coq} mailing list is \url{coq-club@inria.fr}, which +The main {\Coq} mailing list is \url{coq-club@pauillac.inria.fr}, which broadcasts questions and suggestions about the implementation, the logical formalism or proof developments. See -\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{https://sympa-roc.inria.fr/wws/info/coq-club}} for +\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://pauillac.inria.fr/mailman/listinfo/coq-club}} for subscription. For bugs reports see question \ref{coqbug}. \Question{Where can I find an archive of the list?} The archives of the {\Coq} mailing list are available at -\ahref{http://pauillac.inria.fr/pipermail/coq-club}{\url{https://sympa-roc.inria.fr/wws/arc/coq-club}}. +\ahref{http://pauillac.inria.fr/pipermail/coq-club}{\url{http://coq.inria.fr/pipermail/coq-club}}. \Question{How can I be kept informed of new releases of {\Coq}?} -New versions of {\Coq} are announced on the coq-club mailing list. +New versions of {\Coq} are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to {\Coq} on \ahref{http://freshmeat.net/projects/coq/}{\url{http://freshmeat.net/projects/coq/}}. \Question{Is there any book about {\Coq}?} @@ -417,7 +416,7 @@ You can also find large developments using \Question{How can I report a bug?}\label{coqbug} -You can use the web interface accessible at \ahref{http://coq.inria.fr/bugs}{\url{http://coq.inria.fr/bugs}}. +You can use the web interface accessible at \ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link ``contacts''. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -432,7 +431,7 @@ You can use the web interface accessible at \ahref{http://coq.inria.fr/bugs}{\ur The sources of {\Coq} can be found online in the tar.gz'ed packages (\ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link ``download''). Development sources can be accessed at -\ahref{https://gforge.inria.fr/scm/?group_id=269}{\url{https://gforge.inria.fr/scm/?group_id=269}} +\ahref{http://coq.gforge.inria.fr/}{\url{http://coq.gforge.inria.fr/}} \Question{On which platform is {\Coq} available?} Compiled binaries are available for Linux, MacOS X, and Windows. The @@ -666,9 +665,10 @@ where both excluded-middle and the axiom of description are valid (see file \vfile{\LogicClassicalDescription}{ClassicalDescription} for a proof that excluded-middle and description implies the double negation of excluded-middle in {\Set} and file {\tt Hurkens\_Set.v} from the -user contribution {\tt Rocq/PARADOXES} for a proof that -impredicativity of {\Set} implies the simple negation of -excluded-middle in {\Set}). +user contribution {\tt Paradoxes} at +\ahref{http://coq.inria.fr/contribs}{\url{http://coq.inria.fr/contribs}} +for a proof that impredicativity of {\Set} implies the simple negation +of excluded-middle in {\Set}). \Question{Is {\Type} impredicative?} @@ -1509,7 +1509,7 @@ apply the elimination scheme using the \verb=using= option of The short answer : You should use {\texttt le\_lt\_dec n p} instead.\\ -That's right, you can't. +The long answer: That's right, you can't. If you type for instance the following ``definition'': \begin{coq_eval} Reset Initial. @@ -1627,7 +1627,7 @@ certified programs which need to compare natural numbers, and is not designed to compare quickly two numbers. Nevertheless, the \emph{extraction} of \texttt{le\_lt\_dec} towards -\emph{Ocaml} or \emph{Haskell}, is a reasonable program for comparing two +\emph{OCaml} or \emph{Haskell}, is a reasonable program for comparing two natural numbers in Peano form in linear time. It is also possible to keep your boolean function as a decision procedure, @@ -1700,7 +1700,7 @@ Lemma Rwf : well_founded R. \item Define the step function (which needs proofs that recursive calls are on smaller arguments). -\begin{coq_example*} +\begin{verbatim} Definition split (l : list nat) : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l} := (* ... *) . @@ -1710,7 +1710,7 @@ Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) let (l1,H1) := lH1 in let (l2,H2) := lH2 in concat (f l1 H1) (f l2 H2). -\end{coq_example*} +\end{verbatim} \item Define the recursive function by fixpoint on the step function. @@ -1890,13 +1890,15 @@ because ``$^2$'' is an iso-latin character. If you really want this kind of nota \Question{Why ``no associativity'' and ``left associativity'' at the same level does not work?} -Because we relie on camlp4 for syntactical analysis and camlp4 does not really implement no associativity. By default, non associative operators are defined as right associative. +Because we relie on Camlp4 for syntactical analysis and Camlp4 does not really +implement no associativity. By default, non associative operators are defined +as right associative. \Question{How can I know the associativity associated with a level?} -You can do ``Print Grammar constr'', and decode the output from camlp4, good luck ! +You can do ``Print Grammar constr'', and decode the output from Camlp4, good luck ! \section{Modules} @@ -1991,13 +1993,81 @@ todo \Question{How can I define static and dynamic code?} \fi -\section{Tactics written in Ocaml} +\section{Tactics written in OCaml} \Question{Can you show me an example of a tactic written in OCaml?} -You have some examples of tactics written in Ocaml in the ``plugins'' directory of {\Coq} sources. - - +Have a look at the skeleton ``Hello World'' tactic from the next question. +You also have some examples of tactics written in OCaml in the ``plugins'' directory of {\Coq} sources. + +\Question{Is there a skeleton of OCaml tactic I can reuse somewhere?} + +The following steps describe how to write a simplistic ``Hello world'' OCaml +tactic. This takes the form of a dynamically loadable OCaml module, which will +be invoked from the Coq toplevel. +\begin{enumerate} +\item In the \verb+plugins+ directory of the Coq source location, create a +directory \verb+hello+. Proceed to create a grammar and OCaml file, respectively +\verb+plugins/hello/g_hello.ml4+ and \verb+plugins/hello/coq_hello.ml+, +containing: + \begin{itemize} + \item in \verb+g_hello.ml4+: +\begin{verbatim} +(*i camlp4deps: "parsing/grammar.cma" i*) +TACTIC EXTEND Hello +| [ "hello" ] -> [ Coq_hello.printHello ] +END +\end{verbatim} + \item in \verb+coq_hello.ml+: +\begin{verbatim} +let printHello gl = +Tacticals.tclIDTAC_MESSAGE (Pp.str "Hello world") gl + \end{verbatim} + \end{itemize} +\item Create a file \verb+plugins/hello/hello_plugin.mllib+, containing the +names of the OCaml modules bundled in the dynamic library: +\begin{verbatim} +Coq_hello +G_hello +\end{verbatim} +\item Append the following lines in \verb+plugins/plugins{byte,opt}.itarget+: +\begin{itemize} + \item in \verb+pluginsopt.itarget+: +\begin{verbatim} +hello/hello_plugin.cmxa +\end{verbatim} + \item in \verb+pluginsbyte.itarget+: +\begin{verbatim} +hello/hello_plugin.cma +\end{verbatim} +\end{itemize} +\item In the root directory of the Coq source location, modify the file +\verb+Makefile.common+: + \begin{itemize} + \item add \verb+hello+ to the \verb+SRCDIR+ definition (second argument of the + \verb+addprefix+ function); + \item in the section ``Object and Source files'', add \verb+HELLOCMA:=plugins/hello/hello_plugin.cma+; + \item add \verb+$(HELLOCMA)+ to the \verb+PLUGINSCMA+ definition. + \end{itemize} +\item Modify the file \verb+Makefile.build+, adding in section ``3) plugins'' the +line: +\begin{verbatim} +hello: $(HELLOCMA) +\end{verbatim} +\item From the command line, run \verb+make hello+, then \verb+make plugins/hello/hello_plugin.cmxs+. +\end{enumerate} +The call to the tactic \verb+hello+ from a Coq script has to be preceded by +\verb+Declare ML Module "hello_plugin"+, which will load the dynamic object +\verb+hello_plugin.cmxs+. For instance: +\begin{verbatim} +Declare ML Module "hello_plugin". +Variable A:Prop. +Goal A-> A. +Proof. +hello. +auto. +Qed. +\end{verbatim} \section{Case studies} @@ -2238,7 +2308,8 @@ You can use this bibtex entry: @Manual{Coq:manual, title = {The Coq proof assistant reference manual}, author = {\mbox{The Coq development team}}, - note = {Version 8.3}, + organization = {LogiCal Project}, + note = {Version 8.2}, year = {2009}, url = "http://coq.inria.fr" } @@ -2276,8 +2347,8 @@ Depending on your configuration, use either one of these two methods \begin{itemize} \item Insert \texttt{gtk-key-theme-name = "Emacs"} - in your \texttt{.coqide-gtk2rc} file. It may be in the current dir - or in \verb#$HOME# dir. This is done by default. + in your \texttt{coqide-gtk2rc} file. It should be in + \verb#$XDG_CONFIG_DIRS/coq# dir. This is done by default. \item If in Gnome, run the gnome configuration editor (\texttt{gconf-editor}) and set key \texttt{gtk-key-theme} to \texttt{Emacs} in the category @@ -2323,21 +2394,32 @@ pretty simple notations. 2200 is the hexadecimal code for forall in unicode charts and is encoded as in UTF-8. 2203 is for exists. See \ahref{http://www.unicode.org}{\url{http://www.unicode.org}} for more codes. -\item Second solution: rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. - Under X11, you need to use something like +\item Second solution: rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. + + Under X11, one can add those lines in the file ~/.xmodmaprc : + \begin{verbatim} - xmodmap -e "keycode 24 = a A F13 F13" - xmodmap -e "keycode 26 = e E F14 F14" +! forall +keycode 24 = a A a A U2200 NoSymbol U2200 NoSymbol +! exists +keycode 26 = e E e E U2203 NoSymbol U2203 NoSymbol \end{verbatim} - and then to add +and then run xmodmap ~/.xmodmaprc. + + Alternatively, if your version of \verb=xmodmap= does not support unicode, you need to use something like \begin{verbatim} - bind "F13" {"insert-at-cursor" ("")} - bind "F14" {"insert-at-cursor" ("")} +xmodmap -e "keycode 24 = a A F13 F13" +xmodmap -e "keycode 26 = e E F14 F14" \end{verbatim} - to your "binding "text"" section in \verb#.coqiderc-gtk2rc.# - The strange ("") argument is the UTF-8 encoding for - 0x2200. - You can compute these encodings using the lablgtk2 toplevel with + and then to add + +\verb=bind "F13" {"insert-at-cursor" ("=$\forall$\verb=")}=\\ +\verb=bind "F14" {"insert-at-cursor" ("=$\exists$\verb=")}= + + to your "binding "text"" section in \verb#coqiderc-gtk2rc#. + The last arguments to {\tt bind} between "" are + the UTF-8 encodings for 0x2200 and 0x2203. + You can compute these encodings using the lablgtk2 toplevel with \begin{verbatim} Glib.Utf8.from_unichar 0x2200;; \end{verbatim} @@ -2345,17 +2427,11 @@ Glib.Utf8.from_unichar 0x2200;; do not need . \end{itemize} -\Question{How to build a custom {\CoqIde} with user ml code?} - Use - coqmktop -ide -byte m1.cmo...mi.cmo - or - coqmktop -ide -opt m1.cmx...mi.cmx - \Question{How to customize the shortcuts for menus?} Two solutions are offered: \begin{itemize} -\item Edit \$HOME/.coqide.keys by hand or -\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then +\item Edit \verb+$XDG_CONFIG_HOME/coq/coqide.keys+ (which is usually \verb+$HOME/.config/coq/coqide.keys+) by hand or +\item Add "gtk-can-change-accels = 1" in your coqide-gtk2rc file. Then from \CoqIde, you may select a menu entry and press the desired shortcut. \end{itemize} @@ -2375,9 +2451,9 @@ Glib.Utf8.from_unichar 0x2200;; Some users may experiment problems with unwanted automatic templates while using Coqide. This is due to a change in the modifiers keys available through GTK. The straightest way to get -rid of the problem is to edit by hand your .coqiderc (either -\verb|/home/<user>/.coqiderc| under Linux, or \\ -\verb|C:\Documents and Settings\<user>\.coqiderc| under Windows) +rid of the problem is to edit by hand your coqiderc (either +\verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\ +\verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) and replace any occurence of \texttt{MOD4} by \texttt{MOD1}. |