Commit 218e736a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v0.86'

parents 4737eb90 2fa1b306
......@@ -16,6 +16,12 @@ provers
o support for Coq 8.4pl6 (released April 9, 2015)
o discarded support for Alt-Ergo versions older than 0.95.2
Version 0.86.2, October 13, 2015
================================
bug fixes
o assorted bug fixes
Version 0.86.1, May 22, 2015
============================
......
......@@ -259,58 +259,50 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
== Final preparation ==
* faire une passe sur le BTS
* check the 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.86 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.86.tar.gz
* move distrib from Why3 site to Inria forge:
** 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
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.86.pdf
- the HTML version of the manual (content of doc/html)
cp -r doc/html /users/www-perso/projets/why3/doc-0.86
- why3session.dtd
cp -f share/why3session.dtd /users/www-perso/projets/why3/
* generate documentation
- update the date in doc/manual.tex (near \whyversion{})
- check that macro \todo is commented out in doc/macros.tex
- do "make doc"
(check that manual in HTML is also generated, doc/html/index.html)
- do "make stdlibdoc"
- do "make apidoc"
- 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
* make a last commit:
- git commit -am "release 0.86"
- git tag 0.86
* do "make dist"
* test distrib/why3-0.86.tar.gz
* push the commit:
- git push
- git push --tags
* upload distrib/why3-0.86.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
* upload the documentation on the web page
- cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.86.pdf
- cp -r doc/html /users/www-perso/projets/why3/doc-0.86
- cp share/why3session.dtd /users/www-perso/projets/why3/
- cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.86
ln -s -n -f 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
- cp -r doc/apidoc /users/www-perso/projets/why3/api-0.86
ln -s -n -f api-0.86 /users/www-perso/projets/why3/api
- update the main HTML page (sources are in repository why3-www)
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
* make a last commit:
- git commit -am "release 0.86"
- add tag 0.86 to the git repository, using
git tag 0.86
- do not forget to push it using
git push
git push --tags
* update the main HTML page (sources are in repository why3-www)
- 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 a new version to the bugtracker:
https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
......@@ -318,45 +310,27 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
* The next commit : add +git to the version in file Version
* prepare the OPAM package
. obtain a local copy of opam repository, or obtain a former one :
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 fetch opam
git reset --hard opam/master
git push
. copy former files:
cp -r packages/why3-base/why3-base-0.85 packages/why3-base/why3-base-0.86
cp -r packages/why3/why3-0.85 packages/why3/why3-0.86
. update packages/why3-base/why3-base-0.86/url:
url and checksum of why-0.86.tar.gz obtained via
md5sum distrib/why3-0.86.tar.gz
. update packages/why3-base/why3-base-0.86/descr if necessary
. update packages/why3/why3-0.86/descr if necessary
. update packages/why3-base/why3-base-0.86/opam with correct dependencies and such
. update packages/why3/why3-0.86/opam with correct dependencies and such
(at least the dependency on why3-base should be fixed)
* test the OPAM package (requires opam 1.2)
opam pin why3 ./.git
opam install why3
* make a pull request on OPAM
git add why3.0.86
git commit -am "new package version why3 0.86"
git push
sur github: creer un pull request
- update opam/why3-base/url: url and checksum of why-0.86.tar.gz
(use "md5sum distrib/why3-0.86.tar.gz")
- update opam/why3-base/descr and opam/why3/descr if necessary
- update opam/why3-base/opam with correct dependencies
- update opam/why3/opam with the dependency on why3-base
- test with "opam pin add why3 --kind=git .../why3/.git"
(it runs "opam install why3")
* upload the OPAM package
- clone https://github.com/ocaml/opam-repository
git clone git@github.com:.../opam-repository.git
cd opam-repository/
git remote add opam https://github.com/ocaml/opam-repository.git
- reinitialize the repository if not fresh:
git fetch opam
git reset --hard opam/master
git push
- cd packages/why3-base; cp -r .../opam/why3-base why3-base.0.86
- cd packages/why3; cp -r .../opam/why3 why3.0.86
- commit and push
- make a pull request on github
* inform Jerry James <loganjerry@gmail.com> so that he can produce the
Fedora package
......
......@@ -552,13 +552,13 @@ if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
[ echo "Require Import Flocq.Flocq_version BinNat." \
"Goal (20200 <= Flocq_version)%N. easy. Qed." > conftest.v
"Goal (20500 <= Flocq_version)%N. easy. Qed." > conftest.v
"$COQC" conftest.v > conftest.err ],
[ AC_MSG_RESULT(yes) ],
[ AC_MSG_RESULT(no)
enable_coq_fp_libs=no
AC_MSG_WARN(Cannot find Flocq.)
reason_coq_fp_libs=" (Flocq >= 2.2 not found)" ])
reason_coq_fp_libs=" (Flocq >= 2.5 not found)" ])
rm -f conftest.v conftest.vo conftest.err
fi
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, May 2015
Version \whyversion{}, October 2015
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
......@@ -305,9 +305,9 @@ apply generic_format_B2R.
apply generic_format_bpow.
unfold FLT_exp, emin.
zify ; generalize Hprec' Hemax' ; omega.
apply bpow_gt_0.
apply abs_B2R_lt_emax.
unfold pred.
rewrite pred_eq_pos.
unfold pred_pos.
rewrite ln_beta_bpow.
ring_simplify (emax+1-1)%Z.
rewrite Req_bool_true by easy.
......@@ -322,6 +322,7 @@ simpl; ring.
apply Zlt_le_weak.
exact Hprec'.
generalize Hprec' Hemax' ; omega.
apply bpow_ge_0.
Qed.
(* Why3 goal *)
......
archive: "https://gforge.inria.fr/frs/download.php/file/34797/why3-0.86.1.tar.gz"
checksum: "43ab4c224b025c2e3dd5526fa6bef181"
archive: "https://gforge.inria.fr/frs/download.php/file/35214/why3-0.86.2.tar.gz"
checksum: "ef0f4c133fc0da25a6b90adefddefa9a"
......@@ -19,7 +19,7 @@ tags: [
]
available: [ ocaml-version >= "4.01.0" ]
depends: [
"why3-base" { = "0.86" }
"why3-base" { = "0.86.2" }
"lablgtk"
"conf-gtksourceview"
"zarith"
......
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