summaryrefslogtreecommitdiff
path: root/doc/faq
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /doc/faq
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'doc/faq')
-rw-r--r--doc/faq/FAQ.tex172
-rw-r--r--doc/faq/fk.bib7
2 files changed, 128 insertions, 51 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}.
diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
index 976b36b0..d41ab7f0 100644
--- a/doc/faq/fk.bib
+++ b/doc/faq/fk.bib
@@ -1117,9 +1117,10 @@ cedures.},
@Manual{Coq:manual,
title = {The Coq proof assistant reference manual},
author = {\mbox{The Coq development team}},
- note = {Version 8.3},
- year = {2010},
- url = "http://coq.inria.fr/doc"
+ organization = {LogiCal Project},
+ note = {Version 8.0},
+ year = {2004},
+ url = "http://coq.inria.fr"
}
@string{jfp = "Journal of Functional Programming"}