Commit b77c9cf1 authored by MARCHE Claude's avatar MARCHE Claude

Cleaning, doc and such

parent ceea10c2
......@@ -9,10 +9,10 @@ make install (as root)
To install also the Ocaml library do
make byte
make byte
make install-lib (as root)
For detailed instructions and required dependencies, please see
the manual (doc/manual.pdf), Section 6.1 "Compilation, Installation".
\ No newline at end of file
the manual (doc/manual.pdf), Section 8.1 "Compilation, Installation".
......@@ -41,11 +41,6 @@
* choose a logo -> done ?
* DOC:
** complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F)
=== Roadmap for fourth release ========================
* Coq plugin
......@@ -74,6 +69,12 @@
* replayer: don't replay a goal that has changed, just display as an
unsuccessful replay
* DOC:
** complete api.tex: explain how to build theories, apply
transformations, write new functions on terms (A)
** complete manpages.tex: section "Drivers of external provers" (A+F)
** make the glossary available
* DONE reload: improve matching of new and old goals by use a kind a distance
between some notion of shape of a goal
......
......@@ -105,9 +105,9 @@ formalizations or to add support for a new external prover if wanted.
\subsection*{Availability}
\why project page is \url{http://why3.lri.fr/}. The last
distribution is available, in source format, together with this
documentation and several examples.
\why project page is \url{http://why3.lri.fr/}. The last distribution
is available there, in source format, together with this documentation
and several examples.
\why is distributed as open source and freely available under the
terms of the GNU LGPL 2.1. See the file \texttt{LICENSE}.
......@@ -129,9 +129,11 @@ Report any bug to the \why Bug Tracking System:
We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Simon Cruanes, Johannes Kanig, St\'ephane
Lescuyer, Sim\~ao Melo de Sousa, Guillaume Melquiond, Asma Tafat.
Lescuyer, Sim\~ao Melo de Sousa, Guillaume Melquiond, Benjamin Monate,
Asma Tafat.
\subsection*{Summary of Changes w.r.t. Why 2}
The main new features with respect to Why 2.xx
are the following.
\begin{enumerate}
......@@ -153,7 +155,7 @@ are the following.
\item generic approach for communicating with external provers
\end{itemize}
\item Source code organized as a library with a documented API, to
allow access to Why3 features programmatically.
allow access to \why features programmatically.
\item GUI with new features w.r.t. the former GWhy
\begin{itemize}
......
......@@ -1105,26 +1105,6 @@ let reload_proof obsolete goal pid old_a =
in
!notify_fun (Goal a.proof_goal)
(*
let reload_proof ~provers obsolete goal pid old_a =
try
let p = Util.Mstr.find pid provers in
let old_res = old_a.proof_state in
let obsolete = obsolete or old_a.proof_obsolete in
(* eprintf "proof_obsolete : %b@." obsolete; *)
let a =
raw_add_external_proof ~obsolete ~timelimit:old_a.timelimit
~edit:old_a.edited_as goal p old_res
in
!notify_fun (Goal a.proof_goal)
with Not_found ->
eprintf
"Warning: prover %s appears in database but is not installed.@."
pid
*)
let rec reload_any_goal parent gid gname sum shape t old_goal goal_obsolete =
let info = get_explanation gid (Task.task_goal_fmla t) in
let exp = match old_goal with None -> true | Some g -> g.goal_expanded in
......
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