Commit 1d426465 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v1.1'

parents 9e2d3d9a b6ed7918
Pipeline #55687 passed with stages
in 75 minutes and 47 seconds
:x: marks a potential source of incompatibility
Next Version
------------
Transformations
* "split_vc" and "subst_all" now avoid substituting user symbols to generated
one (issue 235). It may breaks session :x:.
......@@ -18,6 +15,14 @@ IDE
* when clicking on the status of an unproved proofAttempt in the proof tree,
launch counterexamples.
Version 1.1.1, December 17, 2018
--------------------------------
Bug fixes
* prevented broken extraction of `any`
* fixed evaluation order when extracting nested mutators
* fixed extraction of nested recursive polymorphic functions
* fixed cloning of expressions raising exceptions
Version 1.1.0, October 17, 2018
-------------------------------
......
......@@ -1576,7 +1576,7 @@ endif
ALTERGODIR=src/trywhy3/alt-ergo
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.syntax \
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.ppx \
-package ocplib-simplex -I src/trywhy3 \
-I $(ALTERGODIR)/lib/util \
-I $(ALTERGODIR)/lib/structures \
......@@ -1700,8 +1700,6 @@ src/trywhy3/%.cmi: src/trywhy3/%.mli
src/trywhy3/%.cmo: BFLAGS += -w -48
src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo: BFLAGS += -syntax camlp4o
clean::
rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.cm* \
src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte src/trywhy3/why3_worker.cm* \
......
......@@ -109,116 +109,6 @@
** preuve sur l'assembleur
** support de Yices 2 ? interesserait Cesar
============ Making a release ============
* check the BTS
* check that nightly bench is OK
* check that "make xml-validate-local" is OK
(see below : copy the dtd on the web)
* 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 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
- 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"
* make a last commit:
- git commit -am "Version $VERSION"
- git tag $VERSION
* do "make dist"
* test distrib/why3-$VERSION.tar.gz
* push the commit:
- git push
- git push --tags
* 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-$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 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
- update why3{,-ide,-coq}.opam/descr if necessary
- update why3{,-ide,-coq}.opam/opam with correct dependencies on external packages
* upload the OPAM package
- clone https://github.com/ocaml/opam-repository if not already done:
git clone git@github.com:.../opam-repository.git
cd opam-repository/
git remote add opam https://github.com/ocaml/opam-repository.git
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:
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:
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
Fedora package
* produce the Why3 part of Toccata gallery
- have GALLERYDIR set to the sub-directory gallery/ of the git sources
of the Toccata web site, e.g.
export GALLERYDIR=/users/vals/filliatr/toccata/web/gallery
- in Why3 sources, do "make gallery"; it exports to GALLERYDIR all
Why3 programs for which there is a session
- now move to the Toccata web site sources, and
- update web/gallery/examples.rc to include new examples
- "git add" the files for these new examples (those currently untracked
in git) or simply remove them if they should not go on-line
- do "make" in web/gallery/
- do "make install-gallery" in web/
* Once the OPAM package is pulled in the main OPAM repository:
announce the distrib
What to put in the announcement: see New Features above
==================== Roadmap for next releases ========================
HighOrd: Coq output and OCaml extraction should produce lambda's from lambda's
......
......@@ -118,7 +118,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, October 2018
Version \whyversion{}, December 2018
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
# Making a release
* perform a sanity check
- check the BTS
- check that nightly bench is OK
- `make xml-validate-local`
(see below: copy the dtd on the web)
- `make trywhy3`
* change version number
```
VERSION=1.1.0
echo "VERSION=$VERSION" > Version
./config.status
```
- check/update the content of the About dialog in `src/ide/gconfig.ml`
around lines 600-650
- check headers
- check the file `CHANGES.md`, add the release date
* generate documentation
- update the date in `doc/manual.tex` (near `\whyversion{}`)
- check/update the authors in `doc/manual.tex`
- check that macro `\todo` is commented out in `doc/macros.tex`
- `make doc`
(check that manual in HTML is also generated, `doc/html/index.html`)
- `make stdlibdoc`
- `make apidoc`
* prepare the archive
- make a last commit:
```
git commit -am "Version $VERSION"
git tag $VERSION
```
- `make dist`
- test `distrib/why3-$VERSION.tar.gz`
- push the commit:
```
git push
git push --tag
```
- 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-$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 `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
```
* next commit: add `+git` to the version in file `Version`
* prepare the OPAM package
- update `why3{,-ide,-coq}.opam/descr` if necessary
- update `why3{,-ide,-coq}.opam/opam` with correct dependencies on external packages
- clone https://github.com/ocaml/opam-repository if not already done:
```
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 --all-switches --kind=git local .
```
- reinitialize the repository if not fresh:
```
git fetch opam
git reset --hard opam/master
git push
```
- create version directories:
- `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)
- 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:
```
git commit ...
opam update local
opam install why3 why3-ide why3-coq
```
- `git push`
- make a pull request on github
* produce the Why3 part of Toccata gallery
- have `GALLERYDIR` set to the sub-directory `gallery/` of the git sources
of the Toccata web site, e.g.
`export GALLERYDIR=/users/vals/filliatr/toccata/web/gallery`
- in Why3 sources, do `make gallery`; it exports to `$GALLERYDIR` all
Why3 programs for which there is a session
- now move to the Toccata web site sources, and
- update `web/gallery/examples.rc` to include new examples
- `git add` the files for these new examples (those currently untracked
in git) or simply remove them if they should not go on-line
- do `make` in `web/gallery/`
- do `make install-gallery` in `web/`
* once the OPAM package is pulled in the main OPAM repository:
- announce the release
- What to put in the announcement: see New Features above
......@@ -326,7 +326,7 @@ module Translate = struct
let args' = List.map (fun (_, ty, _) -> ty) args in
let svar = List.fold_left add_tvar Stv.empty args' in
add_tvar svar res in
let new_svar = Stv.diff svar new_svar in
let new_svar = Stv.diff new_svar svar in
let ef = expr info (Stv.union svar new_svar) ef.e_mask ef in
{ ML.rec_sym = rs1; ML.rec_args = args; ML.rec_exp = ef;
ML.rec_res = res; ML.rec_svar = new_svar; }
......
PKG js_of_ocaml js_of_ocaml.syntax ocplib-simplex
PKG js_of_ocaml js_of_ocaml.ppx ocplib-simplex
REC
......@@ -12,6 +12,7 @@
open Format
open Worker_proto
module Worker = Js_of_ocaml.Worker
module SAT = (val (Sat_solver.get_current ()) : Sat_solver_sig.S)
module FE = Frontend.Make (SAT)
......
This diff is collapsed.
......@@ -18,7 +18,8 @@ open Why3
open Format
open Worker_proto
module Sys_js = Js_of_ocaml.Sys_js
module Worker = Js_of_ocaml.Worker
let () = log_time ("Initialising why3 worker: start ")
......
......@@ -45,6 +45,6 @@ let status_of_result = function
let log s = ignore (Firebug.console ## log (Js.string s))
let log_time s =
let date = jsnew Js.date_now () in
let date_str = string_of_float ((date ## getTime ()) /. 1000.) in
let date = new%js Js.date_now in
let date_str = string_of_float (date ## getTime /. 1000.) in
log (date_str ^ " : " ^ s)
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