Commit afc727a3 authored by MARCHE Claude's avatar MARCHE Claude

Prepare for 0.82: authors

parent ac1ef3c2
......@@ -8,7 +8,9 @@ The Why3 Verification Platform is developed by
with contributions of
Stefan Berghofer
Sylvie Boldo
Martin Clochard
Simon Cruanes
Leon Gondelman
Johannes Kanig
......@@ -16,5 +18,6 @@ with contributions of
Benjamin Monate
Thi-Minh-Tuyen Nguyen
Simão Melo de Sousa
Asma Tafat-Bouzid
Asma Tafat
Piotr Trojanek
......@@ -158,16 +158,17 @@ Scheduled for 9 december 2013
* input language
** lemma functions
** polymorphic recursion permitted
** types "opaques" ???
** types "opaques" TODO ???
* new provers:
** veriT 201310
** Metitarski 2.2
** Metitarski 2.2 (contribution by Piotr Trojanek)
** Metis 2.3
** Beagle 0.4.1
** Princess 2013-05-13
** Yices2 2.0.4
** Isabelle 2013-2 (contribution by Stefan Berghofer)
* new versions of provers:
** Alt-Ergo 0.95.2
......
# Why version
VERSION=0.81+git
VERSION=0.82
......
\subsection{Isabelle/HOL}
When using Isabelle, files generated from Why3 theories are stored in
a dedicated XML format. Those files should not be edited. Instead,
realizations must be designed in some \texttt{.thy} as follows. See
directory \url{lib/isabelle} for examples.
The realization file corresponding to some Why3 file \url{f.why}
should have the following form.
\begin{verbatim}
theory Why3_f
imports Why3_Setup
begin
section {* realization of theory T *}
why3_open "f/T.xml"
why3_vc <some lemma>
<proof>
why3_vc <some other lemma> by proof
[...]
why3_end
\end{verbatim}
......@@ -104,7 +104,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, March 2013
Version \whyversion{}, December 2013
%BEGIN LATEX
\end{LARGE}
%END LATEX
......@@ -201,8 +201,11 @@ Report any bug to the \why Bug Tracking System:
\subsection*{Acknowledgements}
We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Simon Cruanes, Leon Gondelman, Johannes Kanig,
St\'ephane Lescuyer, Sim\~ao Melo de Sousa, Benjamin Monate, Asma Tafat.
indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
Clochard, Simon Cruanes, Leon Gondelman, Johannes Kanig, St\'ephane
Lescuyer, David Mentr\'e, Sim\~ao Melo de Sousa, Benjamin Monate,
Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
\cleardoublepage
......
......@@ -101,6 +101,8 @@ comment.
\input{./pvs.tex}
\input{./isabelle.tex}
\section{Shipping libraries of realizations}
While modifying an existing driver file might be sufficient for local
......
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
valid "Finished Why3 theory"
fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
......
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
printer "isabelle-realize"
filename "%t.xml"
......
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
printer "isabelle"
filename "%f_%t_%g.xml"
......
(* Why driver for MetiTarski *)
(* main author: Piotr Trojanek <piotr.trojanek@gmail.com> *)
(* TODO:
* real.FromInt
......
......@@ -7,6 +7,8 @@
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
(* *)
(********************************************************************)
(** Isabelle printer *)
......
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