Commit 25247f43 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v0.87'

parents d4559eaf 0790887d
......@@ -8,8 +8,14 @@ Tools
installed provers. These are available under name "Auto level 1"
and "Auto level 2" in why3 ide.
Version 0.87.1, May 27, 2016
============================
bug fixes
o assorted bug fixes
Version 0.87.0, March 15, 2016
================================
==============================
Language
* Add new logical connectives "by" and "so" as keywords
......@@ -88,7 +94,7 @@ provers
bug fixes
o why3doc: garbled output
version 0.86, May 11, 2015
Version 0.86, May 11, 2015
==========================
core
......@@ -130,7 +136,7 @@ bug fixes
o IDE: proofs in progress should never be "cleaned"
o IDE: display warnings after reload
version 0.85, September 17, 2014
Version 0.85, September 17, 2014
================================
langage
......@@ -160,7 +166,7 @@ transformations
provers
o fixed wrong warning when detecting Isabelle2014
version 0.84, September 1, 2014
Version 0.84, September 1, 2014
===============================
tools
......@@ -202,7 +208,7 @@ transformations
o new transformation "compute_in_goal" that simplifies the goal, by
computation, as much as possible
version 0.83, March 14, 2014
Version 0.83, March 14, 2014
============================
syntax
......@@ -242,7 +248,7 @@ API
miscellaneous
o fixed compilation bug with lablgtk 2.18
version 0.82, December 12, 2013
Version 0.82, December 12, 2013
===============================
o lemma functions
......@@ -282,7 +288,7 @@ version 0.82, December 12, 2013
o [fix] syntax highlighting bugs: should be fixed by removing the old language
file alt-ergo.lang from alt-ergo distribution
version 0.81, March 25, 2013
Version 0.81, March 25, 2013
============================
o [prover] experimental support for SPASS >= 3.8 (with types)
......@@ -305,8 +311,9 @@ version 0.81, March 25, 2013
is not accepted anymore.
version 0.80, Oct 31, 2012
==========================
Version 0.80, October 31, 2012
==============================
* [whyml] modified syntax for mlw programs; a summary of changes is
given in Appendix A of the manual
o [whyml] support for type invariants and ghost code
......@@ -330,8 +337,9 @@ version 0.80, Oct 31, 2012
* [config] modifiers in --extra-config are now called [prover_modifier]
instead of just [prover]
version 0.73, Jul 19, 2012
==========================
Version 0.73, July 19, 2012
===========================
o [IDE] "Clean" was cleaning too much
* no more executable why3ml (why3 now handles WhyML files)
o [Provers] support for Z3 4.0
......@@ -349,8 +357,9 @@ version 0.73, Jul 19, 2012
o new option -e for "why3session latex" allows to specify when to
split tables in parts
version 0.72, May 11, 2012
Version 0.72, May 11, 2012
==========================
o [Coq] new tactic "why3" to call external provers as oracles
o [Coq output] new feature: theory realizations (see manual, chapter 9)
o new tool why3session (see manual, section 6.7)
......@@ -375,7 +384,7 @@ version 0.72, May 11, 2012
a single abstract function/predicate symbol and Dlogic for
a list of (mutually recursive) defined symbols.
version 0.71, October 13, 2011
Version 0.71, October 13, 2011
==============================
o [examples] a lot of new program examples in directory examples/programs
......@@ -390,7 +399,7 @@ version 0.71, October 13, 2011
marked obsolete if it was made by a prover with another version
than the current.
version 0.70, July 6, 2011
Version 0.70, July 6, 2011
==========================
New features
......@@ -432,8 +441,8 @@ version 0.70, July 6, 2011
So old code performing "prove_task t () ()" should be translated to
"wait_on_call (prove_task t ()) ()".
version 0.64, Feb 16, 2011
==========================
Version 0.64, February 16, 2011
===============================
o configure: if possible, use ocamlfind to find lablgtk2 and sqlite3
o algebraic types: must be well-founded, non-positive constructors
......@@ -463,12 +472,7 @@ version 0.64, Feb 16, 2011
repositories)
o better Gappa output: support for sqrt, for negative constants
version 0.63, Dec 21, 2010
==========================
Version 0.63, December 21, 2010
===============================
o first public release. See release notes in manual
# Emacs parameters
Local Variables:
mode: text
End:
......@@ -64,7 +64,8 @@ endif
DEPFLAGS = -slash -I lib/why3
ifeq (@OCAMLBEST@,opt)
DEPFLAGS += -native
# the semantics of the -native flag changed in ocaml 4.03.0
#DEPFLAGS += -native
endif
RUBBER = @RUBBER@
......@@ -117,8 +118,8 @@ EXTLIBS = str unix nums dynlink @ZIPLIB@
EXTCMA = $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
INSTALLED_LIB_EXTS = a cma cmi cmxa cmxs
COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti cmx annot dep conflicts
INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
TARGET_EMACS = share/emacs/why3.elc
......
......@@ -58,7 +58,6 @@
commentstyle=\itshape,
columns=[l]fullflexible,
showstringspaces=false,
literate=%
}
\lstnewenvironment{whycode}{\lstset{language=why3}}{}
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, March 2016
Version \whyversion{}, May 2016
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
......@@ -13,10 +13,10 @@ The XML file follows the DTD given in \texttt{share/why3session.dtd} and reprodu
\section{Prover Detection}
\label{sec:proverdetecttiondata}
All the necessary data configuration for the automatic detection of
The data configuration for the automatic detection of
installed provers is stored in the file
\texttt{provers-detection-data.conf} typically located in directory
\verb|/usr/local/share/why3| after installation. The contents of this
\verb|/usr/local/share/why3| after installation. The content of this
file is reproduced below.
%BEGIN LATEX
{\footnotesize
......@@ -185,9 +185,9 @@ each $x_1 \dots x_n$ occurs at most once in all the $e_i$.
\subsection{Induction Transformations}
\begin{description}
\item[induction\_ty\_lex]:
\item[induction\_ty\_lex]
\index{induction-ty-lex@\verb+induction_ty_lex+}
This transformation performs structural, lexicographic induction on
performs structural, lexicographic induction on
goals involving universally quantified variables of algebraic data
types, such as lists, trees, etc. For instance, it transforms the
following goal
......@@ -210,7 +210,7 @@ goal G :
goal G: forall l1 "induction" l2 l3: list 'a.
l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3
\end{whycode}
induction will be applied on \verb|l1|. If this label is attached on
induction will be applied on \verb|l1|. If this label is attached to
several variables, a lexicographic induction is performed on these
variables, from left to right.
......@@ -229,11 +229,11 @@ simplification, described below. The transformations differ only by
the kind of rules they apply:
\begin{description}
\item[compute\_in\_goal] aggressively applies all known
computation/simplification rules
computation/simplification rules.
\index{compute-in-goal@\verb+compute_in_goal+}
\item[compute\_specified] performs rewriting using only built-in
operators and user-provided rules
operators and user-provided rules.
\index{compute-specified@\verb+compute_specified+}
\end{description}
......@@ -249,8 +249,8 @@ The kinds of simplification are as follows.
\verb|true| and the transformations thus does not produce any sub-goal.
For example, a goal
like \verb|6*7=42| is solved by those transformations.
\item Unfolding of definitions, as done by \verb|inline_goal|.
\verb|compute_in_goal| unfold all definitions, including recursive ones.
\item Unfolding of definitions, as done by \verb|inline_goal|. Transformation
\verb|compute_in_goal| unfolds all definitions, including recursive ones.
For \verb|compute_specified|, the user can enable unfolding of a specific
logic symbol by attaching the meta \verb|rewrite_def| to the symbol.
\begin{whycode}
......@@ -322,7 +322,7 @@ definitions~\cite{paskevich09rr}.
\item[eliminate\_if\_term] replaces terms of the form \texttt{if
formula then t2 else t3} by lifting them at the level of formulas.
This may introduce \texttt{if then else } in formulas.
This may introduce \texttt{if then else} in formulas.
\index{eliminate-if-term@\verb+eliminate_if_term+}
\item[eliminate\_if\_fmla] replaces formulas of the form \texttt{if f1 then f2
......@@ -356,7 +356,7 @@ definitions~\cite{paskevich09rr}.
% \item[encoding\_enumeration]
\item[encoding\_smt]
encodes polymorphic types into monomorphic type~\cite{conchon08smt}.
encodes polymorphic types into monomorphic types~\cite{conchon08smt}.
\index{encoding-smt@\verb+encoding_smt+}
\item[encoding\_tptp]
......@@ -391,7 +391,7 @@ definitions~\cite{paskevich09rr}.
\item[simplify\_recursive\_definition] reduces mutually recursive
definitions if they are not really mutually recursive, \eg
\begin{whycode}
function f : ... = .... g ...
function f : ... = ... g ...
with g : ... = e
\end{whycode}
becomes
......@@ -405,18 +405,15 @@ if $f$ does not occur in $e$.
\item[simplify\_trivial\_quantification]
simplifies quantifications of the form
\begin{whycode}
forall x, x=t -> P(x)
\end{whycode}
or
\begin{whycode}
forall x, t=x -> P(x)
forall x, x = t -> P(x)
\end{whycode}
when $x$ does not occur in $t$ into
into
\begin{whycode}
P(t)
\end{whycode}
More generally, it applies this simplification whenever $x=t$ appears
in a negative position.
when $x$ does not occur in $t$.
More generally, this simplification is applied whenever $x=t$ or
$t=x$ appears in negative position.
\index{simplify-trivial-quantification@\verb+simplify_trivial_quantification+}
\item[simplify\_trivial\_quantification\_in\_goal]
......@@ -430,12 +427,16 @@ P(t)
linear in the size of that initial axiom.
\index{split-premise@\verb+split_premise+}
\item[split\_premise\_full]: This transformation is similar to \texttt{split\_premise}, but also converts the axioms to conjunctive normal form. The number of axioms generated per initial axiom may be exponential in the size of the initial axiom.
\item[split\_premise\_full] is similar to \texttt{split\_premise}, but it
also converts the axioms to conjunctive normal form. The number of
axioms generated per initial axiom may be exponential in the size of
the initial axiom.
\index{split-premise-full@\verb+split_premise_full+}
\end{description}
\subsection{Other Splitting Transformations}~\label{tech:trans:split}
\subsection{Other Splitting Transformations}
\label{tech:trans:split}
\begin{description}
......@@ -443,14 +444,14 @@ P(t)
but it also removes the goal if it is equivalent to true.
\index{simplify-formula-and-task@\verb+simplify_formula_and_task+}
\item[split\_goal]: if the goal is a conjunction of goals, returns the
\item[split\_goal] changes conjunctive goals into the
corresponding set of subgoals. In absence of case analysis labels,
the number of subgoals generated is linear in the size of the initial goal.
\paragraph{Behavior on asymmetric connectives and
\texttt{by}/\texttt{so}}
The transformation treat specially asymmetric and
The transformation treats specially asymmetric and
\texttt{by}/\texttt{so} connectives. Asymmetric conjunction
\verb|A && B| in goal position is handled as syntactic sugar for
\verb|A /\ (A -> B)|. The conclusion of the first subgoal can then
......@@ -519,10 +520,10 @@ Note that in the side-condition subgoal, the context is universally closed.
The \texttt{so} connective plays a similar role in hypothesis position, as it serves as a consequence indication. In goal position, \verb|A so B| is treated as if it were syntactic sugar for its regular interpretation \verb|A|. In hypothesis position, it is treated as if both \verb|A| and \verb|B| were true because \verb|B| is a consequence of \verb|A|. \verb|A so B| is replaced by \verb|A /\ B| and the transformation also generates a side-condition subgoal \verb|A -> B| corresponding to the consequence relation between formula.
As for the \texttt{by} connective, occurrences of \texttt{so} are unrestricted.
For instance:
\begin{itemize}
\item Splitting
As with the \texttt{by} connective, occurrences of \texttt{so} are
unrestricted. For instance:
\begin{itemize}
\item Splitting
\begin{whycode}
goal G : (((A so B) \/ C) -> D) && E
\end{whycode}
......@@ -537,6 +538,7 @@ goal G3 : A -> B (* side-condition *)
goal G : A by exists x. P x so Q x so R x by T x
(* reads: A by (exists x. P x so (Q x so (R x by T x))) *)
\end{whycode}
generates
\begin{whycode}
goal G1 : exists x. P x
goal G2 : forall x. P x -> Q x (* side-condition *)
......@@ -544,7 +546,7 @@ goal G3 : forall x. P x -> Q x -> T x (* side-condition *)
goal G4 : forall x. P x -> Q x -> T x -> R x (* side-condition *)
goal G5 : (exists x. P x /\ Q x /\ R x) -> A (* side-condition *)
\end{whycode}
In natural language, this corresponds to the following proof schema
In natural language, this corresponds to the following proof scheme
for \verb|A|: There exists a \verb|x| for which \verb|P| holds. Then,
for that witness \verb|Q| and \verb|R| also holds. The last one holds
because \verb|T| holds as well. And from those three conditions on
......@@ -575,11 +577,11 @@ generates the subgoals
goal G1 : A -> C
goal G2 : B -> C
\end{whycode}
Without the label, the transformation do nothing because undesired case analysis
Without the label, the transformation does nothing because undesired case analysis
may easily lead to an exponential blow-up.
Note that the precise behavior of splitting transformation in presence of
the \verb|"case_split"| is not yet specified
Note that the precise behavior of splitting transformations in presence of
the \verb|"case_split"| label is not yet specified
and is likely to change in future versions.
\index{split-goal@\verb+split_goal+}
......@@ -588,10 +590,12 @@ and is likely to change in future versions.
performs both \texttt{split\_premise} and \texttt{split\_goal}.
\index{split-all@\verb+split_all+}
\item[split\_intro]: Composition of \texttt{split\_goal} and \texttt{introduce\_premises}.
\item[split\_intro]
performs both \texttt{split\_goal} and \texttt{introduce\_premises}.
\index{split-intro@\verb+split_intro+}
\item[split\_goal\_full]: This transformation has a behavior similar
\item[split\_goal\_full]
has a behavior similar
to \texttt{split\_goal}, but also converts the goal to conjunctive normal form.
The number of subgoals generated may be exponential in the size of the initial goal.
\index{split-goal-full@\verb+split_goal_full+}
......
......@@ -1016,7 +1016,7 @@ module AVLSorted
then Right s
else Here
(* In an ideal world....
(* In an ideal world...
1) It would be nice to have the two cloned AVL modules unified
(they are intended to be the same), as well as the two (identical)
definitions of type way.
......
#!/usr/bin/env ocaml
(** a mini-mini-make or mini-mini-sub-make
just the protocole for parallelism
just the protocol for parallelism
*)
#load "unix.cma";;
......@@ -95,7 +95,7 @@ let () =
ignore (create_process cmd args i)
done;
ignore (create_process cmd args nb_run);
eprintf "run_wait: *** Attente des tâches non terminées....@.";
eprintf "run_wait: *** Attente des tâches non terminées...@.";
let remaining_child = ref nb_run in
while !remaining_child <> 0 do
ignore (Unix.wait ()); decr remaining_child;
......
opam-version: "1.2"
maintainer: "Claude.Marche@inria.fr"
maintainer: "guillaume.melquiond@inria.fr"
authors: [
"François Bobot"
"Jean-Christophe Filliâtre"
......@@ -7,9 +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"]
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"
tags: [
"deductive"
"program verification"
......@@ -18,13 +22,20 @@ tags: [
"interactive theorem prover"
]
available: [ ocaml-version >= "4.01.0" ]
# Jessie3 (frama-c plugin) is *disabled* because it is not ready
build: [
["./configure" "--prefix" prefix "--disable-frama-c"
"--disable-ide" { !conf-gtksourceview:installed }
"--disable-ide" { !conf-gtksourceview:installed }]
[make "-j%{jobs}%" "opt" "byte"]
]
[make "opt" "byte"]
[make "install" "install-lib"]
install: [make "install" "install-lib"]
remove: [
["rm" "%{bin}%/why3"]
["rm" "-r" "%{lib}%/why3"]
["rm" "-r" "%{share}%/why3"]
]
build-doc: [
......
archive: "https://gforge.inria.fr/frs/download.php/file/35643/why3-0.87.0.tar.gz"
checksum: "e587a45b94201de16529a15c72b978df"
archive: "https://gforge.inria.fr/frs/download.php/file/35893/why3-0.87.1.tar.gz"
checksum: "f1780c8579e6fec9a7ece3ecd05a01e2"
opam-version: "1.2"
maintainer: "Claude.Marche@inria.fr"
maintainer: "guillaume.melquiond@inria.fr"
authors: [
"François Bobot"
"Jean-Christophe Filliâtre"
......@@ -9,7 +9,9 @@ authors: [
]
homepage: "http://why3.lri.fr/"
license: "GNU Lesser General Public License version 2.1"
doc: ["http://why3.lri.fr/#documentation"]
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"
tags: [
"deductive"
"program verification"
......@@ -19,7 +21,7 @@ tags: [
]
available: [ ocaml-version >= "4.01.0" ]
depends: [
"why3-base" { = "0.87.0" }
"why3-base" { = "0.87.1" }
"lablgtk"
"conf-gtksourceview"
"zarith"
......
......@@ -17,7 +17,7 @@ string=[b]",%
%keywordstyle=[1]{\color{red}},%
morekeywords=[2]{true,false},%
%keywordstyle=[2]{\color{blue}},%
otherkeywords={},%
%otherkeywords={},%
commentstyle=\itshape,%
columns=[l]fullflexible,%
sensitive=true,%
......@@ -25,7 +25,7 @@ morecomment=[s]{(*}{*)},%
%breaks hevea
%escapeinside={*?}{?*},%
keepspaces=true,%
literate=%
%literate=%
% {'a}{$\alpha$}{1}%
% {'b}{$\beta$}{1}%
% {<}{$<$}{1}%
......@@ -36,17 +36,15 @@ literate=%
% {/\\}{$\land$}{1}%
% {\\/}{ $\lor$ }{3}%
% {\ or(}{ $\lor$(}{3}%
% {not\ }{$\lnot$ }{1}%
% {not(}{$\lnot$(}{1}%
% {+->}{\texttt{+->}}{2}%
% {not\ }{$\lnot$ }{2}%
% {not(}{$\lnot$(}{2}%
% {+->}{\texttt{+->}}{3}%
% {+->}{$\mapsto$}{2}%
% {-->}{\texttt{-\relax->}}{2}%
% {-->}{\texttt{-\relax->}}{3}%
% {-->}{$\longrightarrow$}{2}%
% {->}{$\rightarrow$}{2}%
% {<-}{$\leftarrow$}{2}%
% {<->}{$\leftrightarrow$}{2}%
%
%
}
\lstnewenvironment{why3}{\lstset{language=why3}}{}
......
......@@ -8,6 +8,7 @@
<!ATTLIST prover alternative CDATA #IMPLIED>
<!ATTLIST prover timelimit CDATA #IMPLIED>
<!ATTLIST prover memlimit CDATA #IMPLIED>
<!ATTLIST prover steplimit CDATA #IMPLIED>
<!ELEMENT file (theory*)>
<!ATTLIST file name CDATA #REQUIRED>
......@@ -40,6 +41,7 @@
<!ATTLIST proof prover CDATA #REQUIRED>
<!ATTLIST proof timelimit CDATA #IMPLIED>
<!ATTLIST proof memlimit CDATA #IMPLIED>
<!ATTLIST proof steplimit CDATA #IMPLIED>
<!ATTLIST proof edited CDATA #IMPLIED>
<!ATTLIST proof obsolete CDATA #IMPLIED>
<!ATTLIST proof archived CDATA #IMPLIED>
......
......@@ -51,7 +51,7 @@ val trivial : Task.task Trans.trans
(** [trivial] corresponds to the transformation "inline_trivial"
Inline only the trivial definition :
logic c : t = a
logic f(x : t,...., ) : t = g(y : t2,...) *)
logic f(x : t,...) : t = g(y : t2,...) *)
(*
(** Functions to use in other transformations if inlining is needed *)
......
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