Commit 57d1a4be authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'master' into new_system

Conflicts:
	Version
	doc/manual.tex
	examples/add_list/why3session.xml
	examples/algo63/why3session.xml
	examples/algo64/why3session.xml
	examples/algo65/why3session.xml
	examples/all_distinct/why3session.xml
	examples/arm/why3session.xml
	examples/assigning_meanings_to_programs/why3session.xml
	examples/binary_multiplication.mlw
	examples/binary_multiplication/why3session.xml
	examples/binary_multiplication/why3shapes.gz
	examples/binary_search/why3session.xml
	examples/binary_sqrt/why3session.xml
	examples/bitcount/why3session.xml
	examples/bitvector_examples/why3session.xml
	examples/bitwalker/why3session.xml
	examples/braun_trees/why3session.xml
	examples/bresenham/why3session.xml
	examples/bubble_sort/why3session.xml
	examples/coincidence_count/why3session.xml
	examples/conjugate/why3session.xml
	examples/counting_sort/why3session.xml
	examples/cursor/why3session.xml
	examples/cursor/why3shapes.gz
	examples/defunctionalization/why3session.xml
	examples/dfa_example/why3session.xml
	examples/dfs/why3session.xml
	examples/fibonacci/why3session.xml
	examples/finite_tarski/why3session.xml
	examples/flag2/why3session.xml
	examples/gcd/why3session.xml
	examples/gcd_bezout/why3session.xml
	examples/gcd_bezout/why3shapes.gz
	examples/hackers-delight/why3session.xml
	examples/linked_list_rev/why3session.xml
	examples/mccarthy.mlw
	examples/mccarthy/why3session.xml
	examples/mccarthy/why3shapes.gz
	examples/patience/why3session.xml
	examples/power/why3session.xml
	examples/power/why3shapes.gz
	examples/queens_bv/why3session.xml
	examples/register_allocation/why3session.xml
	examples/schorr_waite/why3session.xml
	examples/schorr_waite/why3shapes.gz
	examples/sudoku/why3session.xml
	examples/verifythis_fm2012_treedel/why3session.xml
	modules/array.mlw
	share/emacs/why3.el
	share/latex/why3lang.sty
	src/core/pretty.ml
	src/core/task.mli
	src/driver/autodetection.ml
	src/printer/alt_ergo.ml
	src/tools/why3prove.ml
	src/transform/eval_match.ml
	src/transform/prepare_for_counterexmp.ml
	src/transform/split_goal.ml
	src/util/strings.mli
	src/why3session/why3session_html.ml
parents 753b4a78 b48938dc
......@@ -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.
......@@ -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
% definition. It corresponds to the
% \verb|inline_goal| transformation.
\item[Tools] section provides a set of specific action that are
typically performed on the selected goal(s). :
\begin{description}
\item[Edit] starts an editor on the selected task.
For automatic provers, this allows to see the file sent to the
......@@ -340,6 +359,7 @@ proof obligations, the corresponding proof attempts are marked obsolete.
\item[Interrupt] cancels all the proof attempts currently scheduled
but not yet started.
\end{description}
\end{description}
......@@ -350,7 +370,7 @@ proof obligations, the corresponding proof attempts are marked obsolete.
\begin{description}
\item[Add File] adds a file in the GUI.
%\item[Detect provers] runs provers auto-detection
\item[Preferences] opens a window for modifying preferred
]\item[Preferences] opens a window for modifying preferred
configuration parameters, see details below.
\item[Reload] reloads the input files from disk, and update the session state accordingly.
\item[Save session] saves current session state on disk. The policy to decide when to save the session is configurable, as described in the preferences below.
......@@ -864,8 +884,8 @@ Section~\ref{chap:starting}, respectively with style 1 and 2.
\subsection{Command \texttt{html}}
This command produces a summary of the proof session in HTML syntax.
There are three styles of output: `table', `simpletree', and
`jstree'. The default is `table'.
There are two styles of output: `table' and `simpletree'. The default is
`table'.
The file generated is named \texttt{why3session.html} and is written
in the session directory by default (see option \texttt{-o} to
......@@ -908,16 +928,10 @@ The style `simpletree' displays the contents of the session under the
form of tree, similar to the tree view in the IDE. It uses only basic
HTML tags such as \verb|<ul>| and \verb|<li>|.
The style `jstree' displays a dynamic tree view of the session, where
you can click on various parts to expand or shrink some parts of the
tree. Clicking on an edited proof script also shows the contents of
this script. Technically, it uses the `jstree' plugin of the javascript
library `jquery'.
Specific options for this command are as follows.
\begin{description}
\item[\texttt{-{}-style \textsl{<style>}}] sets the style to use, among
\texttt{simpletree}, \texttt{jstree}, and \texttt{table}; defaults to
\texttt{simpletree} and \texttt{table}; defaults to
\texttt{table}.
\item[\texttt{-o \textsl{<dir>}}] sets the directory where to output
......
......@@ -322,6 +322,9 @@ problem''.%
\footnote{This \why example was contributed by St\'ephane Lescuyer.}
%END LATEX
%HEVEA {} (This \why example was contributed by St\'ephane Lescuyer.)
The code given below is available in the source distribution in
directory \verb|examples/logic/einstein.why|.
The problem is stated as follows. Five persons, of five
different nationalities, live in five houses in a row, all
painted with different colors.
......@@ -371,10 +374,10 @@ theory Bijection
type u
function of t : u
function to u : t
function to_ u : t
axiom To_of : forall x : t. to (of x) = x
axiom Of_to : forall y : u. of (to y) = y
axiom To_of : forall x : t. to_ (of x) = x
axiom Of_to : forall y : u. of (to_ y) = y
end
\end{whycode}
......@@ -399,7 +402,7 @@ by cloning the \texttt{Bijection} theory appropriately.
clone Bijection as Color with type t = house, type u = color
\end{whycode}
It introduces two functions, namely \texttt{Color.of} and
\texttt{Color.to}, from houses to colors and colors to houses,
\texttt{Color.to\_}, from houses to colors and colors to houses,
respectively, and the two axioms relating them.
Similarly, we express that each house is associated bijectively to a
person
......@@ -442,11 +445,11 @@ theory \texttt{Einstein}.
theory EinsteinHints "Hints"
use import Einstein
\end{whycode}
Then each hypothesis is stated in terms of \texttt{to} and \texttt{of}
Then each hypothesis is stated in terms of \texttt{to\_} and \texttt{of}
functions. For instance, the hypothesis ``The Englishman lives in a
red house'' is declared as the following axiom.
\begin{whycode}
axiom Hint1: Color.of (Owner.to Englishman) = Red
axiom Hint1: Color.of (Owner.to_ Englishman) = Red
\end{whycode}
And so on for all other hypotheses, up to
``The man who smokes Blends has a neighbour who drinks water'', which completes
......@@ -454,7 +457,7 @@ this theory.
\begin{whycode}
...
axiom Hint15:
neighbour (Owner.to (Cigar.to Blend)) (Owner.to (Drink.to Water))
neighbour (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Drink.to_ Water))
end
\end{whycode}
Finally, we declare the goal in the fourth theory:
......@@ -463,7 +466,7 @@ theory Problem "Goal of Einstein's problem"
use import Einstein
use import EinsteinHints
goal G: Pet.to Fish = German
goal G: Pet.to_ Fish = German
end
\end{whycode}
and we are ready to use \why to discharge this goal with any prover
......
......@@ -128,6 +128,7 @@ associativities, from lowest to greatest priority:
\texttt{if then else} / \texttt{let in} & -- \\
label & -- \\
\texttt{->} / \texttt{<->} & right \\
\texttt{by} / \texttt{so} & right \\
\verb!\/! / \verb!||! & right \\
\verb|/\| / \verb!&&! & right \\
\texttt{not} & -- \\
......@@ -156,6 +157,11 @@ transformations. For instance, \texttt{split} transforms the goal
\verb|A && B| into subgoals \verb|A| and \verb|A -> B|. Similarly, it
transforms \verb!not (A || B)! into subgoals \verb|not A| and
\verb|not ((not A) /\ B)|.
The \texttt{by}/\texttt{so} connectives are proof indications. They are
logically equivalent to their first argument, but may affect the result
of some transformations. For instance, the \texttt{split\_goal}
transformations interpret those connectives as introduction of logical cuts
(see~\ref{tech:trans:split} for details).
\subsection{Theories}
......
This diff is collapsed.
......@@ -5,7 +5,7 @@ invalid "Completion found"
timeout "Ran out of time"
timeout "CPU time limit exceeded"
outofmemory "Out of Memory"
unknown "No Proof Found" ""
unknown "No proof found" ""
fail "Failure.*" "\"\\0\""
time "why3cpulimit time : %s s"