Version 0.86

CHANGES

 
 * marks an incompatible change
 
+version 0.86, May 11th, 2015
+============================
+
 core
   o steps limit for reliable replay of proofs, available for Alt-Ergo
     and CVC4
@@ -32,6 +35,8 @@ IDE:
     is saved on disk for future sessions if, and only if, preferences
     window is exited by hitting the "Save&Close" button
   o right part of main window organized in tabs.
+  o better explanations and task highlighting
+    (contributed by Mikhail Mandrykin)
 
 bug fixes:
   o bug in interpreter in presence of nested mutable fields

ROADMAP

@@ -236,15 +236,7 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
   (check that manual in HTML is also generated, doc/html/index.html)
 * do "make dist"
 * test distrib/why3-0.86.tar.gz
-* put on the web page why3-0.86.tar.gz:
-  cp distrib/why3-0.86.tar.gz /users/www-perso/projets/why3/download
-* inform Jerry James <loganjerry@gmail.com> so that he can test the
-  Fedora package
-* install web page for why2 which includes an updated page for the
-  quick migration guide. (sources are in CVS repository
-  ~filliatr/ARCHIVE/www/why).
 * move distrib from Why3 site to Inria forge:
-** remove /users/www-perso/projets/why3/download/why3-0.86.tar.gz
 ** upload distrib/why3-0.86.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
 * put on the web page
  - the manual in PDF
@@ -259,35 +251,20 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
  - standard library online, using why3doc, to http://why3.lri.fr/stdlib/
    make stdlibdoc
    cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.86
-   rm /users/www-perso/projets/why3/stdlib
-   ln -s /users/www-perso/projets/why3/stdlib-0.86 \
+   ln -s -n -f /users/www-perso/projets/why3/stdlib-0.86 \
             /users/www-perso/projets/why3/stdlib
  - API doc, produced using ocamldoc, to http://why3.lri.fr/api/
     make apidoc
     cp -r doc/apidoc /users/www-perso/projets/why3/api-0.86
-    rm /users/www-perso/projets/why3/api
-    ln -s /users/www-perso/projets/why3/api-0.86 \
+    ln -s -n -f /users/www-perso/projets/why3/api-0.86 \
       /users/www-perso/projets/why3/api
 
  - update the main HTML page (sources are in repository why3-www)
-   edit index.html
+   edit index.html, change at least all occurrences of 0.85 by 0.86, and
+     update the url for download
    make (to check validity)
    make export
 
- - add links to extra resources like
-   http://why3.lri.fr/jfla-2012/, http://www.lri.fr/~marche/MPRI-2-36-1/,
-   page du cours de l'X (in french ? using Krakatoa/why3 bridge)
-
- - make everything writeable for the group
-   chmod -R g+w /users/www-perso/projets/why3
-
-* prepare for the OPAM package
-
-. update opam/url: url and checksum of why-0.86.tar.gz
-   (use "md5sum distrib/why3-0.86.tar.gz")
-. update opam/descr if necessary
-. update opam/opam with correct dependencies and such
-
 * make a last commit:
  - git commit -am "release 0.86"
  - add tag 0.86 to the git repository, using
@@ -300,6 +277,13 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
   https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
 
 
+* prepare the OPAM package
+
+. update opam/url: url and checksum of why-0.86.tar.gz
+   (use "md5sum distrib/why3-0.86.tar.gz")
+. update opam/descr if necessary
+. update opam/opam with correct dependencies and such
+
 * test the OPAM package
 
   . with opam 1.2:
@@ -342,11 +326,16 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
   git push
   sur github: creer un pull request
 
+* inform Jerry James <loganjerry@gmail.com> so that he can produce the
+  Fedora package
+
 * produce the Why3 part of Toccata gallery
   -> add also a tar.gz and a ZIP file of it (this is done by doing
   "make gallery-files" in the sources of the Toccata web pages)
+
 * Announce the distrib
  - What to put in the announcement: see New Features above
+
 * The next commit : add +git to the version in file Version
 
 

Version

 # Why version
-VERSION=0.85+git
-
+VERSION=0.86

doc/manual.tex

@@ -108,7 +108,7 @@
 %BEGIN LATEX
 \begin{LARGE}
 %END LATEX
-  Version \whyversion{}, September 2014
+  Version \whyversion{}, May 2015
 %BEGIN LATEX
 \end{LARGE}
 %END LATEX
@@ -141,20 +141,20 @@ $^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120
 \bigskip
 %END LATEX
 
-  \textcopyright 2010-2014 University Paris-Sud, CNRS, Inria
+  \textcopyright 2010-2015 University Paris-Sud, CNRS, Inria
 
 \urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
 \urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
 \urldef{\urlbware}{\url}{http://bware.lri.fr/}
+\urldef{\urlproofinuse}{\url}{http://www.spark-2014.org/proofinuse}
 
 This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
 national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
-  \urlutcat\end{latexonly}), the `\ahref{\urlhilite}{Hi-Lite}'
+  \urlutcat\end{latexonly}) ; the `\ahref{\urlhilite}{Hi-Lite}'
 \begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
-System@tic competitivity cluster, and the `\ahref{\urlbware}{BWare}'
+System@tic competitivity cluster ; the `\ahref{\urlbware}{BWare}'
 ANR project (ANR-12-INSE-0010\begin{latexonly},
-  \urlbware\end{latexonly}).
-
+  \urlbware\end{latexonly}) ; and the \ahref{\urlproofinuse}{Joint Laboratory ProofInUse} (ANR-13-LAB3-0007\begin{latexonly}, \urlproofinuse\end{latexonly})
 \end{flushleft}
 \end{center}
 
@@ -265,7 +265,7 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
 
 \section{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
 
-The syntax of \whyml programs changed in release 0.80. 
+The syntax of \whyml programs changed in release 0.80.
 The table in Figure~\ref{fig:syntax080} summarizes the changes.
 
 \begin{figure}[thbp]

share/why3session.dtd

@@ -45,7 +45,7 @@
 <!ATTLIST proof archived CDATA #IMPLIED>
 
 <!ELEMENT result EMPTY>
-<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|failure|highfailure) #REQUIRED>
+<!ATTLIST result status (valid|invalid|unknown|timeout|outofmemory|stepslimitexceeded|failure|highfailure) #REQUIRED>
 <!ATTLIST result time CDATA #IMPLIED>
 <!ATTLIST result steps CDATA #IMPLIED>
 

src/core/term.mli

@@ -309,8 +309,8 @@ val t_pred_app_l : term -> term list -> term  (* prop-typed application *)
 (** {2 Lambda-term manipulation} *)
 
 val t_lambda : vsymbol list -> trigger -> term -> term
-(** [t_lambda vl tr e] produces a term [eps f. (forall vl [tr]. f@vl = e)]
-    or [eps f. (forall vl [tr]. f@vl = True <-> e] if [e] is prop-typed.
+(** [t_lambda vl tr e] produces a term [eps f. (forall vl [tr]. f\@vl = e)]
+    or [eps f. (forall vl [tr]. f\@vl = True <-> e] if [e] is prop-typed.
     If [vl] is empty, [t_lambda] returns [e] or [if e then True else False],
     if [e] is prop-typed. *)
 

src/ide/gconfig.ml

@@ -533,6 +533,7 @@ let show_about_window () =
                 "David Hauzar";
                 "Daisuke Ishii";
                 "Johannes Kanig";
+                "Mikhail Mandrykin";
                 "David Mentré";
                 "Benjamin Monate";
                 "Thi-Minh-Tuyen Nguyen";