Commit 88004948 authored by MARCHE Claude's avatar MARCHE Claude

release 0.85

parent eb7bb11c
* marks an incompatible change * marks an incompatible change
version 0.85, September 17, 2014
================================
langage langage
* fix a soundness bug in the detection of aliases when calling a * fix a soundness bug in the detection of aliases when calling a
WhyML function: some alias could have been forgotten when a type WhyML function: some alias could have been forgotten when a type
variable was substituted with a mutable types variable was substituted with a mutable type
sessions sessions
o use the full path of identifiers when the user introduces namespaces o use the full path of identifiers when the user introduces namespaces
......
...@@ -147,6 +147,144 @@ and no epsilon ...@@ -147,6 +147,144 @@ and no epsilon
chaque instance necessaires. plutot qu'un seul symbole _match chaque instance necessaires. plutot qu'un seul symbole _match
polymorphe. polymorphe.
==================== Roadmap for release 0.85 ========================
Release Notes:
Mainly a bug-fix release, in particular to fix two soundness bugs
See CHANGES
== Final preparation ==
* faire une passe sur le BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate-local" is OK
(see below : copy the dtd on the web)
* put 0.85 in file Version, and then run ./config.status
* check/update the content of the About dialog in src/ide/gconfig.ml
around lines 550-600
* check headers
* check the file CHANGES, add the release date
* manual in PDF:
** update the date in doc/manual.tex (near \whyversion{})
** check that macro \todo is commented out in doc/macros.tex
** and then "make doc"
(check that manual in HTML is also generated, doc/html/index.html)
* do "make dist"
* test distrib/why3-0.85.tar.gz
* put on the web page why3-0.85.tar.gz:
cp distrib/why3-0.85.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.85.tar.gz
** upload distrib/why3-0.85.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
* put on the web page
- the manual in PDF
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.85.pdf
- the HTML version of the manual (content of doc/html)
cp -r doc/html /users/www-perso/projets/why3/doc-0.85
- why3session.dtd
cp -f share/why3session.dtd /users/www-perso/projets/why3/
- standard library online, using why3doc, to http://why3.lri.fr/stdlib/
make stdlibdoc
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.85
rm /users/www-perso/projets/why3/stdlib
ln -s /users/www-perso/projets/why3/stdlib-0.85 \
/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.85
rm /users/www-perso/projets/why3/api
ln -s /users/www-perso/projets/why3/api-0.85 \
/users/www-perso/projets/why3/api
- update the main HTML page (sources are in repository why3-www)
edit index.html
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.85.tar.gz
(use "md5sum distrib/why3-0.85.tar.gz")
. update opam/descr if necessary
. update opam/opam with correct dependencies and such
* make a last commit:
- git commit -am "release 0.85"
- add tag 0.85 to the git repository, using
git tag 0.85
- do not forget to push it using
git push
git push --tags
* add a new version to the bugtracker:
https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
* test the OPAM package
. with opam 1.2:
opam pin add why3 --kind=git <...>/why3/.git
(it runs "opam install why3")
. with opam < 1.2:
- first step: have a local copy of opam-repository if not done yet, e.g.:
git clone git@github.com:claudemarche/opam-repository.git
cd opam-repository/
git remote add opam https://github.com/ocaml/opam-repository.git
or, if you already have one, make sure it is up-to-date:
git pull --ff-only opam master
- second step: copy why3 opam files into it :
cd packages/why3
cp -r <source why3>/opam why3.0.85
- second step:
opam repository add local <...>/opam-repository
opam install why3
(* test it, e.g.
cp example/quicksort.mlw ~/tmp
why3 ide ~/tmp/quicksort.mlw *)
opam remove why3
opam repository remove local
* make a pull request on OPAM
git add why3.0.85
commit et push
sur github: creer un pull request
* 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
==================== Roadmap for release 0.84 ======================== ==================== Roadmap for release 0.84 ========================
== TODOs == == TODOs ==
......
# Why version # Why version
VERSION=0.84+git VERSION=0.85
...@@ -204,37 +204,40 @@ goal G : ...@@ -204,37 +204,40 @@ goal G :
end end
\end{whycode} \end{whycode}
When induction can be applied to several variables, the transformation When induction can be applied to several variables, the transformation
picks one heuristically. A label \verb|induction| can be used to picks one heuristically. A label \verb|"induction"| can be used to
force induction over one particular variable, \emph{e.g.}, force induction over one particular variable, \eg with
\begin{whycode} \begin{whycode}
goal G: forall l1 "induction" l2 l3: list 'a. goal G: forall l1 "induction" l2 l3: list 'a.
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3 l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
\end{whycode} \end{whycode}
If such a label is used on several variables, a lexicographic induction will be applied on \verb|l1|. If this label is attached on
induction is performed on these variables, from left to right. several variables, a lexicographic induction is performed on these
variables, from left to right.
\item[] Induction on inductive predicates. %\item[] Induction on inductive predicates.
[TO BE COMPLETED] %[TO BE COMPLETED]
% TODO: implement also induction on int !
\end{description} \end{description}
\subsection{Simplification by Computation} \subsection{Simplification by Computation}
These transformations simplify the goal by applying several kinds of These transformations simplify the goal by applying several kinds of
simplification. The transformations differ only by the kind of rules they simplification, described below. The transformations differ only by
apply: the kind of rules they apply:
\begin{description}
\verb|compute_in_goal| aggressively apply all known \item[compute\_in\_goal] aggressively applies all known
computation/simplification rules computation/simplification rules
\index{compute-in-goal@\verb+compute_in_goal+}
\index{compute-in-goal@\verb+compute_in_goal+}
\verb|compute_specified| perform rewriting using only built-in operators and
user-provided rules
\index{compute-specified@\verb+compute_specified+} \item[compute\_specified] performs rewriting using only built-in
operators and user-provided rules
\index{compute-specified@\verb+compute_specified+}
\end{description}
The kinds of simplification are as follows.
\begin{itemize} \begin{itemize}
\item Computations with built-in symbols, \eg operations on integers, \item Computations with built-in symbols, \eg operations on integers,
when applied to explicit constants, are evaluated. This includes when applied to explicit constants, are evaluated. This includes
...@@ -252,7 +255,6 @@ user-provided rules ...@@ -252,7 +255,6 @@ user-provided rules
logic symbol by attaching the meta \verb|rewrite_def| to the symbol. logic symbol by attaching the meta \verb|rewrite_def| to the symbol.
\begin{whycode} \begin{whycode}
function sqr (x:int) : int = x * x function sqr (x:int) : int = x * x
meta "rewrite_def" function sqr meta "rewrite_def" function sqr
\end{whycode} \end{whycode}
\item Rewriting using axioms or lemmas declared as rewrite rules. When \item Rewriting using axioms or lemmas declared as rewrite rules. When
...@@ -268,21 +270,22 @@ axiom a: forall ... f1 <-> f2 ...@@ -268,21 +270,22 @@ axiom a: forall ... f1 <-> f2
\begin{whycode} \begin{whycode}
meta "rewrite" axiom a meta "rewrite" axiom a
\end{whycode} \end{whycode}
to turn this axiom into a rewrite rules. Rewriting is always done to turn this axiom into a rewrite rule. Rewriting is always done
from left to right. Beware that there is no check for termination from left to right. Beware that there is no check for termination
nor for confluence of the set of rewrite rules declared. nor for confluence of the set of rewrite rules declared.
\item Bound on the number of reduction: the computations performed by \end{itemize}
this transformation can take an arbitrarily large number of steps,
or even not terminate. For this reason, the number of steps is \paragraph{Bound on the number of reductions}
bounded by a maximal value, which is set by default to 1000. This The computations performed by these transformations can take an
value can be increased by another meta, \eg arbitrarily large number of steps, or even not terminate. For this
reason, the number of steps is bounded by a maximal value, which is
set by default to 1000. This value can be increased by another meta,
\eg
\begin{whycode} \begin{whycode}
meta "compute_max_steps" 1_000_000 meta "compute_max_steps" 1_000_000
\end{whycode} \end{whycode}
When this upper limit is reached, the partly-reduced goal When this upper limit is reached, a warning is issued, and the
is returned as the result of the transformation. partly-reduced goal is returned as the result of the transformation.
\end{itemize}
\subsection{Other Non-Splitting Transformations} \subsection{Other Non-Splitting Transformations}
......
(** {1 Lagrange Identity, Cauchy-Schwarz and Triangle Inequalities} *)
theory LagrangeInequality theory LagrangeInequality
......
archive: "https://gforge.inria.fr/frs/download.php/file/33976/why3-0.84.tar.gz" archive: "https://gforge.inria.fr/frs/download.php/file/33976/why3-0.85.tar.gz"
checksum: "286ac2816f539f11e31f84fcafc32120" checksum: "f6d36c0dc43fe75af148d92d76b15937"
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