diff --git a/doc/api.tex b/doc/api.tex index fb75e71a363dfa744786d7a214c5818295d445c3..b603592c1b5a989d899c674f2f31da6c6c4a3a9b 100644 --- a/doc/api.tex +++ b/doc/api.tex @@ -11,14 +11,14 @@ at URL~\url{http://why3.lri.fr/api/}. We assume the reader has a fair knowledge of the OCaml language. Notice that the \why library must be installed, see Section~\ref{sec:installlib}. The OCaml code given below is available in -the source distribution as \url{examples/use_api/use_api.ml}. +the source distribution as \verb|examples/use_api/use_api.ml|. \section{Building Propositional Formulas} The first step is to know how to build propositional formulas. The module \texttt{Term} gives a few functions for building these. Here is -a piece of OCaml code for building the formula $true \lor false$. +a piece of OCaml code for building the formula $\mathit{true} \lor \mathit{false}$. \begin{ocamlcode} (* opening the Why3 library *) open Why3 @@ -55,7 +55,7 @@ Running the generated executable \texttt{f} results in the following output. formula 1 is: true \/ false \end{verbatim} -Let's now build a formula with propositional variables: $A \land B +Let us now build a formula with propositional variables:$A \land B \rightarrow A$. Propositional variables must be declared first before using them in formulas. This is done as follows. \begin{ocamlcode} @@ -87,12 +87,12 @@ when building those directly using library calls. \section{Building Tasks} -Let's see how we can call a prover to prove a formula. As said in +Let us see how we can call a prover to prove a formula. As said in previous chapters, a prover must be given a task, so we need to build tasks from our formulas. Task can be build incrementally from an empty task by adding declaration to it, using the functions -\texttt{add\_*\_decl} of module \texttt{Task}. For the formula$true \lor -false$above, this is done as follows. +\texttt{add\_*\_decl} of module \texttt{Task}. For the formula$\mathit{true} \lor +\mathit{false}$above, this is done as follows. \begin{ocamlcode} let task1 : Task.task = None (* empty task *) let goal_id1 : Decl.prsymbol = @@ -106,10 +106,9 @@ propositions in a theory or a task. Notice again that the concrete syntax of \why requires these symbols to be capitalized, but it is not mandatory when using the library. The second argument of \texttt{add\_prop\_decl} is the kind of the proposition: -\texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal} -(notice, however, that lemmas are not allowed in tasks -and can only be used in theories). - +\texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal}. +Notice that lemmas are not allowed in tasks +and can only be used in theories. Once a task is built, it can be printed. \begin{ocamlcode} @@ -164,10 +163,9 @@ let provers : Whyconf.config_prover Whyconf.Mprover.t = Whyconf.get_provers config \end{ocamlcode} The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A -provers is a record with a name, a version and an alternative description -(if someone want to compare different command line options of the same -provers for example). It's definition is in the module -\texttt{Whyconf} : +prover is a record with a name, a version, and an alternative description +(to differentiate between various configurations of a given prover). Its +definition is in the module \texttt{Whyconf}: \begin{ocamlcode} type prover = { prover_name : string; (* "Alt-Ergo" *) @@ -355,7 +353,7 @@ let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux We illustrate now how one can build theories. Building a theory must be done by a sequence of calls: \begin{itemize} -\item creating a theory under construction'', of type \verb|Theory.theory_uc| ; +\item creating a theory under construction'', of type \verb|Theory.theory_uc|; \item adding declarations, one at a time ; \item closing the theory under construction, obtaining something of type \verb|Theory.theory|. \end{itemize} @@ -366,7 +364,7 @@ let my_theory : Theory.theory_uc = Theory.create_theory (Ident.id_fresh "My_theory") \end{ocamlcode} -First let's add the formula 1 above as a goal: +First let us add the formula 1 above as a goal: \begin{ocamlcode} let decl_goal1 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1 @@ -483,7 +481,7 @@ One can run provers on those tasks exactly as we did above. \section{Proof sessions} -See the example \url{examples/use_api/create_session.ml} of the distribution for +See the example \verb|examples/use_api/create_session.ml| of the distribution for an illustration on how to manipulate proof sessions from an OCaml program. diff --git a/doc/technical.tex b/doc/technical.tex index e12ea91062ce6b48fcd603a895851f565926c644..50601f9bfd915150074592b0062b923d228a5498 100644 --- a/doc/technical.tex +++ b/doc/technical.tex @@ -98,16 +98,15 @@ name = "CoqIDE" One can use a custom configuration file. \texttt{why3config} -and other \texttt{why3} tools use priorities for which -user's configuration file to consider: -\begin{itemize} +and other \texttt{why3} tools look for it in the following order: +\begin{enumerate} \item the file specified by the \texttt{-C} or \texttt{-{}-config} options, \item the file specified by the environment variable - \texttt{WHY3CONFIG} if set. + \texttt{WHY3CONFIG} if set, \item the file \texttt{\$HOME/.why3.conf} (\texttt{\\$USERPROFILE/.why3.conf} under Windows) or, in the case of local installation, \texttt{why3.conf} in Why3 sources top directory. -\end{itemize} +\end{enumerate} If none of these files exists, a built-in default configuration is used. The configuration file is a human-readable text file, which consists @@ -121,15 +120,16 @@ the example, or it can be composed by a family name and one family argument, \texttt{prover} is one family name, \texttt{coq} and \texttt{alt-ergo} are the family argument. -Inside a section, one key can be associated with an integer (\eg{} -555), -a boolean (true, false) or a string (\eg{} "emacs"). One key can appear -only once except if its a multi-value key. The order of apparition of -the keys inside a section matter only for the multi-value key. +Sections contain associations \texttt{key=value}. A value is either +an integer (\eg{} -555), a boolean (true, false), or a string (\eg{} +"emacs"). Some specific keys can be attributed multiple values and are +thus allowed to occur several times inside a given section. In that +case, the relative order of these associations matter. \section{Drivers of External Provers} \label{sec:drivers} -The drivers of external provers are readable files, in directory +Drivers of external provers are readable files from directory \texttt{drivers}. Experimented users can modify them to change the way the external provers are called, in particular which transformations are applied to goals.