Skip to content

GitLab

why3
why3
Commit b402afbd authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

doc: version, prover detection

parent 66a33777
Hide whitespace changes
Inline Side-by-side
Showing with 214 additions and 35 deletions
Version
View file @ b402afbd
# Why version
VERSION=3.00
VERSION=0.1
doc/manpages.tex
View file @ b402afbd
......@@ -2,6 +2,7 @@
\label{chap:manpages}
\section{Compilation, Installation}
\label{sec:install}
Compilation of Why3 must start with a configuration phase which is run as
\begin{verbatim}
......@@ -29,28 +30,78 @@ liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site \url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
\item TODO Claude: sqlite3
\item The Ocaml bindings of the sqlite3 library
For debian-based Linux distributions, you can install the package
\begin{verbatim}
libsqlite3-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
\end{itemize}
\subsection{Local use, without installation}
It is not mandatory to install Why3 to use it. Local use is obtained via
\begin{verbatim}
./configure --enable-local
make
\end{verbatim}
commands are available in subdirectory \texttt{bin/}.
The Why3 executables are then available in subdirectory \texttt{bin/}.
\section{Installation of external provers}
why-config
Why3 can use a wide range of external theorem provers. These need to
be installed separately, and then Why3 needs to be configured to use
them. There is no need to install these provers before compiling and
installing Why.
ou
For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.
IDE/Detect provers
For configuring Why3 to use the provers, follow intructions given in
Section~\ref{sec:why3config}.
Provers which are auto-detected: (share/prover-detection-data)
\section{The \texttt{why3config} command-line tool}
\label{sec:why3config}.
pour chaque prouveur: lien sur page why/prover tips.
Why3 must be configured to access external provers. Typically, this is done
by running either the command line tool
\begin{verbatim}
why3config
\end{verbatim}
or using the menu
\begin{verbatim}
File/Detect provers
\end{verbatim}
of the IDE. This must be done again each time a new prover is installed.
The set of all provers which are attempted to detect is described in
the readable configuration file \texttt{provers-detection-data.conf}
of the Why3 data directory (\eg{}
\texttt{/usr/local/share/why3}). Advanced users may try to modify this
file to add support for detection of other provers. (In that case,
please consider submitting a new prover configuration on the bug
tracking system).
The result of the prover detection is stored in the user's
configuration file (\eg{} \texttt{~/.why.conf}). Again, this file is
human readable, and advanced users may modify it in order to
experiment different ways of calling provers, \eg{} different versions
of the same prover, or with different options.
The provers which are typically attemped for detection are
\begin{itemize}
\item Alt-Ergo~\cite{conchon08smt,ergo}: \url{}
\item CVC3~\cite{BarTin-CAV-07}: \url{}
\item Coq~\cite{CoqArt}: \url{}
\item Eprover~: \url{}
\item Gappa~\cite{melquiond08rnc}: \url{}
\item Simplify~\cite{simplify05}: \url{}
\item Spass~: \url{}
\item veriT~: \url{}
\item Yices~\cite{DM06}: \url{}
\item Z3~\cite{z3}: \url{}
\end{itemize}
\section{The \texttt{why3} command-line tool}
......@@ -92,11 +143,12 @@ pour chaque prouveur: lien sur page why/prover tips.
\item[File/Detect provers]
\end{description}
\subsection{Preferences}
\subsection{Structure of the database file}
TODO
[TODO]
\section{The \texttt{why.conf} configuration file}
......
doc/manual.bib
View file @ b402afbd
@comment{{This file has been generated by bib2bib 1.95}}
@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: bib2bib -c '$key="paskevich09rr" or $key="ayad10ijcar" or $key="filliatre07cav" or $key="conchon08smt" or 1=2' /home/cmarche/biblio/abbrevs.bib /home/cmarche/biblio/demons.bib /home/cmarche/biblio/demons2.bib /home/cmarche/biblio/demons3.bib /home/cmarche/biblio/team.bib /home/cmarche/biblio/crossrefs.bib /home/cmarche/biblio/crossrefs2.bib}}
@comment{{Command line: /usr/bin/bib2bib -c '$key="ayad10ijcar" or $key="CoqArt" or $key="conchon08smt" or $key="paskevich09rr" or $key="z3" or $key="ergo" or $key="simplify05" or $key="DM06" or $key="BarTin-CAV-07" or $key="melquiond08rnc" or $key="filliatre07cav" or 1=2' /home/cmarche/biblio/abbrevs.bib /home/cmarche/biblio/demons.bib /home/cmarche/biblio/demons2.bib /home/cmarche/biblio/demons3.bib /home/cmarche/biblio/team.bib /home/cmarche/biblio/crossrefs.bib /home/cmarche/biblio/crossrefs2.bib}}
@string{sv = {Springer}}
......@@ -8,6 +8,56 @@
@string{lncs = {Lecture Notes in Computer Science}}
@inproceedings{BarTin-CAV-07,
author = {Clark Barrett and Cesare Tinelli},
title = {{CVC3}},
booktitle = {Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07), Berlin, Germany},
pages = {},
year = 2007,
editor = {W.~Damm and H.~Hermanns},
volume = {},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
url = {ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarTin-CAV-07.pdf}
}
@book{CoqArt,
author = {Yves Bertot and Pierre Cast\'eran},
title = {Interactive Theorem Proving and Program Development},
subtitle = {Coq'Art: The Calculus of Inductive Constructions},
publisher = {Springer-Verlag},
serie = {Texts in Theoretical Computer Science},
year = 2004
}
@unpublished{DM06,
author = {Bruno Dutertre and Leonardo de Moura},
institution = {SRI International},
title = {The {Yices} {SMT} Solver},
year = {2006},
note = {available at \url{http://yices.csl.sri.com/tool-paper.pdf}}
}
@article{simplify05,
author = {David Detlefs and
Greg Nelson and
James B. Saxe},
title = {Simplify: a theorem prover for program checking.},
journal = {J. ACM},
volume = {52},
number = {3},
year = {2005},
pages = {365-473},
ee = {http://doi.acm.org/10.1145/1066100.1066102},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@misc{z3,
author = {Leonardo de Moura and Nikolaj Bj{\o}rner},
title = {{Z3}, An Efficient {SMT} Solver},
note = {\url{http://research.microsoft.com/projects/z3/}}
}
@inproceedings{conchon08smt,
author = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean
and St\'ephane Lescuyer},
......@@ -33,6 +83,18 @@
isbn = {978-1-60558-440-9}
}
@misc{ergo,
author = {Sylvain Conchon and \'Evelyne Contejean},
title = {The {Alt-Ergo} automatic Theorem Prover},
url = {http://alt-ergo.lri.fr/},
note = {\url{http://alt-ergo.lri.fr/}},
topics = {team,lri},
year = 2008,
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@inproceedings{filliatre07cav,
author = {Jean-Christophe Filli\^atre and Claude March\'e},
title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
......@@ -50,6 +112,26 @@
x-cle-support = {CAV}
}
@inproceedings{melquiond08rnc,
author = {Guillaume Melquiond},
title = {Floating-point arithmetic in the {C}oq system},
booktitle = {Proceedings of the 8th Conference on Real Numbers and Computers},
address = {Santiago de Compostela, Spain},
year = {2008},
pages = {93--102},
note = {\url{http://gappa.gforge.inria.fr/}},
url = {http://gappa.gforge.inria.fr/},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {RNC},
topics = {team},
x-editorial-board = {yes},
x-international-audience = {yes},
x-proceedings = {yes},
x-pdf = {http://www.msr-inria.inria.fr/~gmelquio/doc/08-rnc8-article.pdf}
}
@techreport{paskevich09rr,
author = {Andrei Paskevich},
title = {Algebraic types and pattern matching in the logical language of the {Why} verification platform},
......
doc/manual.tex
View file @ b402afbd
......@@ -15,6 +15,8 @@
\newcommand{\why}{\textsf{Why3}}
\newcommand{\eg}{\emph{e.g.}}
\input{./version.tex}
\begin{document}
\sloppy
\hbadness=1100
......@@ -23,33 +25,47 @@
\begin{center}
~
\rule\textwidth{0.8mm}
\vfill
{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
\vfill
{\Huge\bfseries Why3 manual}
\rule\textwidth{0.8mm}
\vfill
{\Large F. Bobot$^{1,2}$ \\
J.-C. Filli\^atre$^{2,1}$ \\
C. March\'e$^{3,1}$ \\
A. Paskevich$^{1,2}$}
\begin{LARGE}
Version \whyversion{}, December 2010
\end{LARGE}
\vfill
\begin{Large}
\begin{tabular}{c}
Fran\c{c}ois Bobot$^{1}$ \\
Jean-Christophe Filli\^atre$^{2}$ \\
Claude March\'e$^{3}$ \\
Andrei Paskevich$^{1}$
\end{tabular}
\end{Large}
\vfill
\begin{flushleft}
\begin{tabular}{l}
$^1$ Univ Paris-Sud, Orsay, F-91405 \\
$^2$ LRI, CNRS, Orsay, F-91405 \\
$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
\end{tabular}
\vfill
\bigskip
\begin{flushleft}
\textcopyright 2010-2010 Univ Paris-Sud, CNRS, INRIA
\textcopyright 2010 Univ Paris-Sud, CNRS, INRIA
This work has been supported by the `U3CAT' national ANR project
This work has been partly supported by the `U3CAT' national ANR project
(ANR-08-SEGI-021-08, \url{http://frama-c.cea.fr/u3cat}) and by the
Hi-Lite (\url{http://www.open-do.org/projects/hi-lite/}) FUI project of the
System@tic competitivity cluster.
......@@ -57,10 +73,6 @@ $^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
\end{flushleft}
\end{center}
\cleardoublepage
\tableofcontents
\chapter*{Foreword}
This is the manual for the Why platform version 3, or Why3 for
......@@ -72,9 +84,40 @@ which allows for the end user to easily add the support for a new
external prover if wanted. A major new feature is also the ability
to use Why programmatically, via a well-designed API.
\section*{Acknowledgements}
We gratefully thank all the people who contributed to this document:
\subsection*{Availability}
Why3 project page is \url{https://gforge.inria.fr/projects/why3}. The
last distribution is available, in source format, together with this
documentation and several examples.
Why3 is distributed as open source and freely available under the
terms of the GNU LGPL 2.1. See the file \texttt{LICENSE}.
See the file \texttt{INSTALL} for quick installation instructions, and
Section~\ref{sec:install} od this document for more detailed
instructions.
\subsection*{Contact}
There is a public mailing list for users' discussions:
\url{http://lists.gforge.inria.fr/mailman/listinfo/why3-club}.
Report any bug to the Why3 Bug Tracking System:
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.
% \section*{Acknowledgements}
% We gratefully thank all the people who contributed to this document:
% Germain Faure
% Johannes Kanig
% Simão Melo de Sousa
\cleardoublepage
\tableofcontents
\input{intro.tex}
......
examples/use_api.ml
View file @ b402afbd
......@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(*******************
This file builds some goals using the API and calls
the alt-ergo prover to check them
......
share/provers-detection-data.conf
View file @ b402afbd
......@@ -104,6 +104,7 @@ name = "Coq"
exec = "coqc"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.3"
version_ok = "8.2pl2"
version_ok = "8.2pl1"
version_ok = "8.2"
......
src/ide/gconfig.ml
View file @ b402afbd
......@@ -290,17 +290,16 @@ let show_about_window () =
let about_dialog =
GWindow.about_dialog
~name:"Why"
~authors:["Francois Bobot";
"Jean-Christophe Filliatre";
"Johannes Kanig";
"Claude Marche";
~authors:["François Bobot";
"Jean-Christophe Filliâtre";
"Claude Marché";
"Andrei Paskevich"
]
~copyright:"Copyright 2010"
~copyright:"Copyright 2010 Univ Paris-Sud, CNRS, INRIA"
~license:"Gnu Lesser General Public License"
~website:"http://why.lri.fr"
~website_label:"Click here for the web site"
~version:"3.0 alpha"
~website:"https://gforge.inria.fr/projects/why3"
~website_label:"Project web site"
~version:Config.version
()
in
let ( _ : GWindow.Buttons.about) = about_dialog#run () in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment