Commit 40b25049 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v0.88'

parents 1a721b08 5c64f692
/examples/in_progress/ export-ignore
/examples/hoare_logic/draft/ export-ignore
/tests/ export-ignore
/bench/encoding/ export-ignore
/misc/ export-ignore
/ROADMAP export-ignore
/DEVELOPER.readme export-ignore
/opam/ export-ignore
.gitignore export-ignore
.gitattributes export-ignore
.gitignore export-ignore
.keepme export-ignore
/.gitlab-ci.yml export-ignore
/.mailmap export-ignore
/check.sh export-ignore
/DEVELOPER.readme export-ignore
/ROADMAP export-ignore
/TODO export-ignore
/bench/encoding/ export-ignore
/examples/in_progress/ export-ignore
/misc/ export-ignore
/opam/ export-ignore
/tests/ export-ignore
:x: marks a potential source of incompatibility
Version 0.88.1, ?, 2017
-----------------------
Version 0.88.1, November 6, 2017
--------------------------------
API
* exported function `forward_results` in `Call_provers` interface
* exported function `Call_provers.get_new_results`
Provers
* improved support for Isabelle 2017
* fixed support for Coq 8.7
Miscellaneous
* fixed compilation for OCaml 4.06
* improved support for nullary `val` declarations with regions
Version 0.88.0, October 6, 2017
-------------------------------
......
WHY 3
=====
WHY3
====
Why3 is a platform for deductive program verification. It provides
a rich language for specification and programming, called WhyML, and
......
......@@ -142,9 +142,11 @@
* upload distrib/why3-0.86.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
- cp share/why3session.dtd /users/www-perso/projets/why3/
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
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, October 2017
Version \whyversion{}, November 2017
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
......@@ -10,9 +10,9 @@ authors: [
homepage: "http://why3.lri.fr/"
license: "GNU Lesser General Public License version 2.1"
doc: "http://why3.lri.fr/#documentation"
bug-reports: "https://gforge.inria.fr/tracker/?func=browse&group_id=2990&atid=10293"
dev-repo: "https://scm.gforge.inria.fr/anonscm/git/why3/why3.git"
doc: "http://why3.lri.fr/doc/"
bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
dev-repo: "https://gitlab.inria.fr/why3/why3.git"
tags: [
"deductive"
......@@ -46,6 +46,7 @@ build-doc: [
depends: [
"ocamlfind"
"menhir"
"num"
]
depopts: [
......
archive: "https://gforge.inria.fr/frs/download.php/file/37147/why3-0.88.0.tar.gz"
checksum: "1aef885ff8eee34107585e11db623a8d"
......@@ -7,11 +7,13 @@ authors: [
"Guillaume Melquiond"
"Andrei Paskevich"
]
homepage: "http://why3.lri.fr/"
license: "GNU Lesser General Public License version 2.1"
doc: "http://why3.lri.fr/#documentation"
bug-reports: "https://gforge.inria.fr/tracker/?func=browse&group_id=2990&atid=10293"
dev-repo: "https://scm.gforge.inria.fr/anonscm/git/why3/why3.git"
doc: "http://why3.lri.fr/doc/"
bug-reports: "https://gitlab.inria.fr/why3/why3/issues"
dev-repo: "https://gitlab.inria.fr/why3/why3.git"
tags: [
"deductive"
"program verification"
......@@ -21,7 +23,7 @@ tags: [
]
available: [ ocaml-version >= "4.02.3" & ocaml-version < "4.06" ]
depends: [
"why3-base" { = "0.88.0" }
"why3-base" { = "0.88.1" }
"lablgtk"
"conf-gtksourceview"
"zarith"
......
......@@ -392,7 +392,7 @@ type prover_update =
let result_buffer : (server_id, prover_update) Hashtbl.t = Hashtbl.create 17
let get_new_results ~blocking = (* TODO: handle ProverStarted events *)
let fetch_new_results ~blocking = (* TODO: handle ProverStarted events *)
List.iter (fun (id, r) ->
let x = match r with
| Some r -> ProverFinished r
......@@ -400,8 +400,8 @@ let get_new_results ~blocking = (* TODO: handle ProverStarted events *)
Hashtbl.add result_buffer id x)
(wait_for_server_result ~blocking)
let forward_results ~blocking =
get_new_results ~blocking;
let get_new_results ~blocking =
fetch_new_results ~blocking;
let q = ref [] in
Hashtbl.iter (fun key element ->
if element = ProverStarted && blocking then
......@@ -427,7 +427,7 @@ let editor_result ret = {
let query_call = function
| ServerCall id ->
get_new_results ~blocking:false;
fetch_new_results ~blocking:false;
query_result_buffer id
| EditorCall pid ->
let pid, ret = Unix.waitpid [Unix.WNOHANG] pid in
......@@ -439,7 +439,7 @@ let rec wait_on_call = function
begin match query_result_buffer id with
| ProverFinished r -> r
| _ ->
get_new_results ~blocking:true;
fetch_new_results ~blocking:true;
wait_on_call pc
end
| EditorCall pid ->
......
......@@ -172,7 +172,7 @@ type prover_update =
| ProverStarted
| ProverFinished of prover_result
val forward_results: blocking:bool -> (prover_call * prover_update) list
val get_new_results: blocking:bool -> (prover_call * prover_update) list
(** returns new results from why3server, in an unordered fashion. *)
val query_call : prover_call -> prover_update
......
......@@ -376,7 +376,7 @@ let timeout_handler () =
(* When no tasks are there, probably no tasks were scheduled and the server
was not launched so getting results could fail. *)
if Hashtbl.length prover_tasks_in_progress != 0 then begin
let results = Call_provers.forward_results ~blocking:S.blocking in
let results = Call_provers.get_new_results ~blocking:S.blocking in
List.iter (fun (call, prover_update) ->
match Hashtbl.find prover_tasks_in_progress call with
| (ses,id,pr,callback,started,call,ores) ->
......
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