mails d'annonce dans ROADMAP

ROADMAP

@@ -5,7 +5,7 @@
 
 1 Introduction (done: suppressed)
 2 getting started (Claude: done, to be read by others)
-3 Syntax, tutorial (TODO: Andrei)
+3 Syntax, tutorial (done: Andrei)
 4 tutorial for API:
 ** build a task (Claude: done, to be read by others)
 ** call a prover (Claude: done, to be read by others)
@@ -67,6 +67,97 @@
 * META for ocamlfind (done)
 * headers (done)
 
+== Mails announcement ==
+
+----------------------- Why-discuss list ---------------------------
+
+We are happy to announce the first public release of Why3, also known
+as the Why platform next generation. It is a new project, independent
+from Why.
+
+The home web page of Why3 is http://why3.gforge.inria.fr/, where you
+can find the source distribution and the manual. See the manual for 
+installation instructions and contact information.
+
+The main new features with respect to Why are the following.
+
+1) Completely redesigned input syntax for logic declarations
+
+* new syntax for terms and formulas
+* definitions of algebraic data types, definitions by pattern-matching
+* recursive definitions of logic functions and predicate, which are
+  checked terminating
+* inductive definitions of predicates
+* declarations are structured in components called theories. 
+
+2) More generic handling of goals and lemmas to prove
+
+* concept of proof task
+* generic concept of task transformation
+* generic approach for communicating with external provers
+
+3) Source code organized as a library with a documented API, to allow
+   access to Why3 features programmatically by linking.
+
+4) GUI with new features w.r.t. the former GWhy
+
+* session save and restore
+* prover calls in parallel
+* splitting, and more generally applying task transformations, on demand
+* ability to edit proofs for interactive provers (Coq only for the moment) 
+  on any subtask
+
+5) Extensible architecture via plugins
+
+* users can define new transformations
+* users can add connections to additional provers
+
+
+Beware that some Why features are not available in Why3:
+
+* There is a VC generator distributed in Why3 in an experimental stage
+  and intentionally undocumented (the input syntax for programs may
+  change a lot in the future).  
+
+* There is no front-end for other languages like C or Java. However,
+  the last release Why 2.28 is able to use Why3 as a back-end
+
+
+
+
+--------------------- Frama-C list ----------------------------
+
+
+The first release of Why3, also known as the Why platform next
+generation, is publicly available. Why3 is a new project, independent
+from Why. The detailed annoucement is attached below.
+
+The Jessie plugin of the Why release 2.28 has the ability to use Why3
+as back-end. You must install both Why 2.28 and Why3 for this to work.
+
+Using the Why3 GUI on a C file is done as follows
+  frama-c -jessie -jessie-atp why3ide <file>.c
+(You can also run it in batch mode using
+  frama-c -jessie -jessie-atp why3 <file>.c
+and process the generated Why3 file "<file>.jessie/why/<file>_why3.why" 
+with Why3 batch tools).
+
+The main new features of interest in the GUI are
+
+* new provers available
+* calling provers in parallel
+* splitting on demand
+* ability to call Coq on a given VC a provide a proof script. Incidentally,
+  this feature can be used to analyse the VC to understand why it is
+  not proved automatically.  
+* proof session saved and restored at startup
+
+Any question, remark or bug report concerning only Why3 should be done
+using the Why3 public discussion list and bug tracker.
+
+
+
+
 
 
 
@@ -78,7 +169,7 @@
 * proof replay 
 ** in IDE
 ** in whybench
-** add replay of existing proof in make bench to detect regression
+** add replay of existing proofs in "make bench" to detect regression
 
 = Roadmap for 2011 =