Commit 75e59ea1 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge branch 'bugfix/v1.1'

parents 22e5b9d0 dda5aa3c
:x: marks a potential source of incompatibility
Version 1.1.0, ...
------------------
Version 1.1.0, October 17, 2018
-------------------------------
Core
* variants can now be inferred on some lemma functions
* coercions are now supported for `if` and `match` branches
* `interrupt` command should now properly interrupt running provers.
* clearer typing error messages thanks to printing qualified names
* fixed handling of prover upgrades, resurected the policy
* fixed handling of prover upgrades, resurrected the policy
"duplicate" and added a policy "remove"
API
* added `Call_provers.interrupt_call` to interrupt a running prover
[contribution Pierre-Yves Strub <pierre-yves@strub.nu>]
(contribution by Pierre-Yves Strub)
Language
* program functions can now be marked `partial` to prevent them from
......@@ -25,7 +25,7 @@ Language
* range types have now a default ordering to be used in `variant` clause
Standard library
* library `Ieee_float`: floating-point operations can now be used in
* library `ieee_float`: floating-point operations can now be used in
programs
Transformations
......@@ -35,10 +35,11 @@ Provers
* support for Alt-Ergo 2.1.0 (released Mar 14, 2018)
* support for Alt-Ergo 2.2.0 (released Apr 26, 2018)
* support for Coq 8.8.1 (released Jun 29, 2018)
* support for Coq 8.8.2 (released Sep 26, 2018)
* support for CVC4 1.6 (released Jun 25, 2018)
* support for Z3 4.7.1 (released May 23, 2018)
* support for Isabelle 2018 (released Aug 2018)
[Contribution Stefan Berghofer <stefan.berghofer@secunet.com>]
(contribution by Stefan Berghofer)
* dropped support for Isabelle 2016 (2017 still supported) :x:
* dropped support for Alt-Ergo versions < 2.0.0 :x:
......
......@@ -116,12 +116,16 @@
* 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
* change version number
- VERSION=1.1.0
- put 1.1.0 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
around lines 600-650
* check headers
* check the file CHANGES.md, add the release date
* check that "make trywhy3" is OK
* generate documentation
- update the date in doc/manual.tex (near \whyversion{})
- check/update the authors in doc/manual.tex
......@@ -132,32 +136,37 @@
- do "make apidoc"
* make a last commit:
- git commit -am "Version 0.86"
- git tag 0.86
- git commit -am "Version $VERSION"
- git tag $VERSION
* do "make dist"
* test distrib/why3-0.86.tar.gz
* test distrib/why3-$VERSION.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 distrib/why3-$VERSION.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
* upload the documentation on the web page
- cp share/why3session.dtd /users/www-perso/projets/why3/
- cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.86.pdf
ln -s -n -f download/manual-0.86.pdf /users/www-perso/projets/why3/manual.pdf
- cp -r doc/html /users/www-perso/projets/why3/doc-0.86
ln -s -n -f doc-0.86 /users/www-perso/projets/why3/doc
- 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
- 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
cp share/why3session.dtd /users/www-perso/projets/why3/
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-$VERSION.pdf
ln -s -n -f download/manual-$VERSION.pdf /users/www-perso/projets/why3/manual.pdf
cp -r doc/html /users/www-perso/projets/why3/doc-$VERSION
ln -s -n -f doc-$VERSION /users/www-perso/projets/why3/doc
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-$VERSION
ln -s -n -f stdlib-$VERSION /users/www-perso/projets/why3/stdlib
cp -r doc/apidoc /users/www-perso/projets/why3/api-$VERSION
ln -s -n -f api-$VERSION /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
- edit index.html, change at least all occurrences of 1.0.0 by 1.1.0, and
update the url for download
- make (to check validity)
- make export
* update TryWhy3
make trywhy3
make trywhy3_package
tar xzf trywhy3.tar.gz -C /users/www-perso/projets/why3/try/ --strip-components=1
* The next commit : add +git to the version in file Version
* prepare the OPAM package
......@@ -169,24 +178,24 @@
git clone git@github.com:.../opam-repository.git
cd opam-repository/
git remote add opam https://github.com/ocaml/opam-repository.git
opam repository add --kind=git local .
opam2 repository add --all-switches --kind=git local .
- reinitialize the repository if not fresh:
git fetch opam
git reset --hard opam/master
git push
- create version directories:
cp -r .../why3.opam packages/why3/why3.1.0.0
cp -r .../why3-ide.opam packages/why3-ide/why3-ide.1.0.0
cp -r .../why3-coq.opam why3-coq/why3-coq.1.0.0
- update why3{-ide,-coq}.1.0.0/opam with the dependency on why3
- create why3/why3.1.0.0/url: url and checksum of why-1.0.0.tar.gz
md5sum .../distrib/why3-1.0.0.tar.gz
cp why3/why3.1.0.0/url why3-ide/why3-ide.1.0.0/url
cp why3/why3.1.0.0/url why3-coq/why3-coq.1.0.0/url
mkdir packages/why3/why3.$VERSION packages/why3-coq/why3-coq.$VERSION packages/why3-ide/why3-ide.$VERSION
copy the opam files from the directories of the previous release (Opam 2.0 format)
merge the changes from the why3.opam, why3-ide.opam, and why3-coq.opam directories (Opam 1.2 format)
- update why3{-ide,-coq}.$VERSION/opam with the dependency on why3
- url and checksum of why3.tar.gz:
md5sum .../distrib/why3-$VERSION.tar.gz
update the "url" section of all three opam files
- test opam files:
opam update local
opam install why3 why3-ide why3-coq
- commit and push
git commit ...
opam2 update local
opam2 install why3 why3-ide why3-coq
- git push
- make a pull request on github
* inform Jerry James <loganjerry@gmail.com> so that he can produce the
......
VERSION=1.0.0
VERSION=1.1.0+git
......@@ -118,7 +118,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, June 2018
Version \whyversion{}, October 2018
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
......@@ -572,7 +572,7 @@ support_library = "%l/coq/version"
exec = "coqtop"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "^8\.8\.[0-1]$"
version_ok = "^8\.8\.[0-2]$"
version_ok = "^8\.7\.[0-2]$"
version_ok = "8.6.1"
version_ok = "8.6"
......
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