Commit bb910a4b authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into itp

parents 828e386d c8bbcd4b
......@@ -2,9 +2,6 @@
/examples/hoare_logic/draft/ export-ignore
/tests/ export-ignore
/bench/encoding/ export-ignore
/share/images/boomy/ export-ignore
/share/images/boomy.rc export-ignore
/share/javascript/ export-ignore
/misc/ export-ignore
/ROADMAP export-ignore
/DEVELOPER.readme export-ignore
......@@ -12,5 +9,4 @@
.gitignore export-ignore
.gitattributes export-ignore
/check.sh export-ignore
/.merlin.in export-ignore
/TODO export-ignore
......@@ -29,6 +29,7 @@ why3.conf
/autom4te.cache
/Makefile
/configure
/install-sh
/semantic.cache
/TAGS
/output_why3
......@@ -121,8 +122,10 @@ why3.conf
/doc/stdlibdoc/
# /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe
/lib/why3cpulimit
/lib/why3cpulimit.exe
/lib/why3server
/lib/why3server.exe
# /lib/why3/
/lib/why3/META
......@@ -278,14 +281,19 @@ pvsbin/
/modules/mach/int/
# Try Why3
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.byte
/src/trywhy3/trywhy3.js
/src/trywhy3/alt_ergo_worker.byte
/src/trywhy3/alt_ergo_worker.js
/src/trywhy3/why3_worker.byte
/src/trywhy3/why3_worker.js
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/index.html
/src/trywhy3/ace-builds
/src/trywhy3/ace-builds/
/src/trywhy3/*.png
/src/trywhy3/alt-ergo-1.00-private-2015-01-29
/src/trywhy3/fontawesome/
# jessie3
/src/jessie/config.log
......@@ -296,3 +304,4 @@ pvsbin/
/src/jessie/tests/demo/result/*.log
/trash
trywhy3.tar.gz
* marks an incompatible change
Tools
o why3 config now generates default proof strategies using the
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
......@@ -8,6 +24,7 @@ Tools
o add a command-line option --extra-expl-prefix to specify
additional possible prefixes for VC explanations. (Available for
why3 commands "prove" and "ide".)
* removed "jstree" style from the "session" command
Transformations
* All split transformations respect the "stop_split" label now.
......@@ -45,7 +62,7 @@ Provers
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
Distribution
* non-free files are distributed in an extra tar file: "boomy" icon set,
* non-free files have been removed: "boomy" icon set,
javascript helpers for "why3 session html --style jstree"
Version 0.86.3, February 8, 2016
......@@ -77,7 +94,7 @@ provers
bug fixes
o why3doc: garbled output
version 0.86, May 11, 2015
Version 0.86, May 11, 2015
==========================
core
......@@ -119,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
......@@ -149,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
......@@ -191,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
......@@ -231,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
......@@ -271,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)
......@@ -294,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
......@@ -319,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
......@@ -338,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)
......@@ -364,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
......@@ -379,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
......@@ -421,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
......@@ -452,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:
......@@ -23,9 +23,10 @@ Installation from the git repository
First run
autoconf
automake --add-missing
to build the file ./configure, then follow instructions from the
section above.
to build the ./configure file and install the helper scripts, then follow
instructions from the section above.
Detailed instructions
......
This diff is collapsed.
This diff is collapsed.
# Why version
VERSION=0.86+git
VERSION=0.87+git
####################################################################
# #
# The Why3 Verification Platform / The Why3 Development Team #
# Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University #
# Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University #
# #
# This software is distributed under the terms of the GNU Lesser #
# General Public License version 2.1, with the special exception #
......@@ -140,23 +140,22 @@ AC_MSG_CHECKING(executable suffix)
if uname -s | grep -q CYGWIN ; then
EXE=.exe
STRIP='echo "no strip "'
CPULIMIT=cpulimit-win
AC_MSG_RESULT(.exe <Cygwin>)
else
if uname -s | grep -q MINGW ; then
EXE=.exe
STRIP=strip
CPULIMIT=cpulimit-win
AC_MSG_RESULT(.exe <MinGW>)
else
EXE=
STRIP=strip
CPULIMIT=cpulimit
AC_MSG_RESULT(<none>)
fi
fi
AC_PROG_CC()
AC_PROG_CC
AC_PROG_MKDIR_P
AC_PROG_INSTALL
# Check for Ocaml compilers
......@@ -709,17 +708,13 @@ dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
VERSION=$PACKAGE_VERSION
BUILDDATE="$(date)"
# substitutions to perform
AC_SUBST(VERSION)
AC_SUBST(BUILDDATE)
AC_SUBST(enable_verbose_make)
AC_SUBST(EXE)
AC_SUBST(STRIP)
AC_SUBST(CPULIMIT)
AC_SUBST(OCAMLC)
AC_SUBST(OCAMLOPT)
......
......@@ -6,6 +6,8 @@
| formula "&&" formula ; asymmetric conj.
| formula "\/" formula ; disjunction
| formula "||" formula ; asymmetric disj.
| formula "by" formula ; proof indication
| formula "so" formula ; consequence indication
| "not" formula ; negation
| lqualid ; symbol
| prefix-op term ;
......
......@@ -42,8 +42,12 @@
%%% listings for Why3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\RequirePackage{listings}
\RequirePackage{amssymb}
% cannot use \usepackage here because it breaks hevea (no colored keywords anymore :-()
\input{../share/latex/why3lang.sty}
% \RequirePackage{listings}
% \RequirePackage{amssymb}
\lstset{
basicstyle={\ttfamily},
......@@ -56,39 +60,6 @@
showstringspaces=false,
}
\lstdefinelanguage{why3}
{
morekeywords={namespace,predicate,function,inductive,type,use,clone,%
import,export,theory,module,end,in,with,%
let,rec,for,to,do,done,match,if,then,else,while,try,invariant,variant,%
absurd,raise,assert,exception,private,abstract,mutable,ghost,%
downto,raises,writes,reads,requires,ensures,returns,val,model,%
goal,axiom,lemma,forall,meta},%
string=[b]",%
sensitive=true,%
morecomment=[s]{(*}{*)},%
keepspaces=true,
}
%literate=%
%{'a}{$\alpha$}{1}%
%{'b}{$\beta$}{1}%
%{<}{$<$}{1}%
%{>}{$>$}{1}%
%{<=}{$\le$}{1}%
%{>=}{$\ge$}{1}%
% {<>}{$\ne$}{1}%
% {/\\}{$\land$}{1}%
% {\\/}{ $\lor$ }{3}%
% {\ or(}{ $\lor$(}{3}%
% {not\ }{$\lnot$ }{1}%
% {not(}{$\lnot$(}{1}%
% {+->}{\texttt{+->}}{2}%
% % {+->}{$\mapsto$}{2}%
% {-->}{\texttt{-\relax->}}{2}%
% %{-->}{$\longrightarrow$}{2}%
% {->}{$\rightarrow$}{2}%
% {<->}{$\leftrightarrow$}{2}%
\lstnewenvironment{whycode}{\lstset{language=why3}}{}
\lstnewenvironment{ocamlcode}{\lstset{language={[Objective]Caml}}}{}
......
......@@ -307,17 +307,36 @@ proof obligations, the corresponding proof attempts are marked obsolete.
actions are performed even if the goal is already proved. The second
choice allows to compare provers on the same goal.
\item[Strategies] section provides a set of actions that are
performed on the selected goal(s):
\begin{description}
\item[Split] splits the current goal into subgoals if it is a
conjunction of two or more goals. It corresponds to the
\verb|split_goal_wp| transformation.
\item[Inline] inlines the definitions in the conclusion of the goal.
It corresponds to the \verb|introduce_premises| transformation
follwoed by \verb|inline_goal|.
\item[Auto level 1] is a strategy that first applies a few provers
on the goal with a short time limit, then splits the goal and
tries again on the subgoals
\item[Auto level 2] is a strategy more elaborate than level 1, that
attempts to apply a few transformations that are typically
useful. It also tries the provers with a larger time limit.
\end{description}
A more detailed description of strategies is given in
Section~\ref{sec:strategies}, as well as a description on how to
design strategies of your own.
\item[Provers] provide a button for each detected prover. Clicking on such a
button starts the corresponding prover on the selected goal(s).
\item[Split] splits the current goal into subgoals if it is a
conjunction of two or more goals. It corresponds to the
\verb|split_goal_wp| transformation.
\item[Inline] replaces the head predicate symbol of the goal with its
definition. It corresponds to the
\verb|inline_goal| transformation.
% \item[Inline] replaces the head predicate symbol of the goal with its