Commit 97d32b08 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Merge branch 'master' into realization

Conflicts:
	Makefile.in
	src/bench/benchdb.ml
	src/bench/benchrc.ml
	src/driver/whyconf.mli
	src/ide/gconfig.ml
	src/ide/session.ml
	src/main.ml
parents c130fd8a 216e869f
......@@ -9,6 +9,7 @@ why3.conf
*.cmi
*.cmxs
*.annot
*.dep
\#*\#
# /
......@@ -17,7 +18,7 @@ why3.conf
/autom4te.cache
/Makefile
/configure
/.depend.*
/.depend.coq-libs
/semantic.cache
/TAGS
/output_why3
......@@ -75,6 +76,9 @@ why3.conf
/bin/why3stats.byte
/bin/why3stats.opt
/bin/why3stats
/bin/why3session.opt
/bin/why3session.byte
/bin/why3session
# /doc/
/doc/version.tex
......@@ -135,14 +139,6 @@ why3.conf
/src/parser/parser.mli
/src/parser/parser.output
# /src/tptp2why/
/src/tptp2why/tptpLexer.ml
/src/tptp2why/tptpParser.ml
/src/tptp2why/tptpParser.mli
/src/tptp2why/tptpParser.output
/src/tptp2why/tptpParser.automaton
/src/tptp2why/tptpParser.conflicts
# /src/ide/
/src/ide/xml.ml
......@@ -152,6 +148,15 @@ why3.conf
# /src/util/
/src/util/rc.ml
# /src/session
/src/session/xml.ml
# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
/plugins/tptp/tptp_parser.output
# /tests/
/tests/test-jcf/
/tests/test-pgm-jcf/
......@@ -162,7 +167,6 @@ why3.conf
/examples/programs/course/
/examples/programs/wcet_hull/
/examples/programs/binary_search2/
/examples/programs/vacid_0_red_black_trees/
/examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/
/examples/programs/algo63/
......
* marks an incompatible change
o fix BTS 13854
o fix BTS 13849
o [syntax] new syntax "constant x:ty" and "constant x:ty = e" to
introduce constants, as an alternative to "function"
version 0.71, October 13, 2011
==============================
o [examples] a lot of new program examples in directory examples/programs
o [Why3replayer] new option -latex to output a proof session in LaTeX format
o [WhyML] significant improvement of the efficiency of the WP calculus
o [WhyIDE] better coloring and source positioning including from front-ends
o [WhyIDE] better coloring and source positioning including from front-ends
such as Krakatoa and Jessie plugin of Frama-C
o [WhyML] fixed labels and source locations in WPs
o [Session] during reload, new method for pairing old and new subgoals
......
Installation instructions
Shortly, installation is done by
./configure
make
make install (as root)
Installation from a source distribution (tarball)
-------------------------------------------------
After unpacking, installation is done by
./configure
make
make install (as root)
To install also the Ocaml library do
make byte
make install-lib (as root)
make byte
make install-lib (as root)
Installation from the git repository
------------------------------------
First run
autoconf
to build the file ./configure, then follow instructions from the
section above.
Detailed instructions
---------------------
For detailed instructions and required dependencies, please see
the manual (doc/manual.pdf), Section 8.1 "Compilation, Installation".
This diff is collapsed.
......@@ -23,6 +23,9 @@
commande why3 et why3bench + le path
* Add more examples in the regression tests and in the proval gallery
** add all examples from the VSTTE 2012 competition (JCF, ANDREI)
* A literate programming tool for Why3 (JCF)
* Papers to write
......@@ -52,7 +55,10 @@
** M2. Lieur en Why3, POPLmark challenge. vers
un theorie et/ou un module réutilisable de lieurs
** (M2?) Stage Airbus, "TIP" avec Frama-C/Jessie ou WP/Why/Coq
besoin du plugin Coq?
besoin du plugin Coq?
* INSTALLATION
** configure.in: detect dynlink.cmxa, and switch to bytecode if not found
* PRIORITAIRE, JCF et ANDREI, clone de module
** demarche: ecrire une API avec smart constructors garantissant
......@@ -65,7 +71,7 @@ NON PRIORITAIRE ?
** logic symbols used in programs
* extraction vers Caml
** PRIORITAIRE, JCF, ANDREI, besoin pour cours aux JFLA en janvier 2012
** PRIORITAIRE, JCF, ANDREI
* FRANCOIS new tools
** merge why3html and why3stats into a new executable why3report
......@@ -83,6 +89,9 @@ NON PRIORITAIRE ?
meaning like twice the value of %t ?), because we cannot be sure they always
honor their own -timeout option.
** fix CVC3 printer: prints predicate def using LAMBDA
** better use of Alt-Ergo's builtin theories: records, enumeration types
(Alt-Ergo >= 0.94) => at least two drivers for Alt-Ergo, depending on its
version number
* FRANCOIS CLAUDE, move Session module and its dependencies into the Why3 library
** but avoid duplication with session_ro
......@@ -94,6 +103,8 @@ NON PRIORITAIRE ?
* efficiency issues
** understand problems when large number of goals (cf D Mentré examples)
** also: BTS 13736
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
* ALL fix bug and update the BTS
** reject global "val"s in typing environment for logic decls.
......@@ -119,6 +130,8 @@ NON PRIORITAIRE ?
** make the glossary available
* IDE:
** enlarge font (menu + shortcut Ctrl-+)
** Ctrl-A to select all rows
** saving session
* add "ctrl-S" to save the session explicitly
(partially done, but no shortcut)
......@@ -126,7 +139,10 @@ NON PRIORITAIRE ?
** restore provers detection in the middle of a session.
+ todo: run detection immediately at start up if conf file absent or
outdated. should become doable with the new Session module
** syntax highlighting
some keywords are not colored in the bottom-right window
(but they are in the top-right window)
** add a scrollbar for the left panel
=== Roadmap for release 0.71 ========================
......
......@@ -28,6 +28,10 @@ s
is not changed by a transformation, it will stay in the hash table forever,
since the key is the value. Should we use generation numbers in arguments
and results of transformations?
François -- I don't get that point the weak Hashtbl that we use
are designed to work on this case, even with the identity function.
What we should do is a way to remove the task from a session when
they are not needed anymore.
- uses : pour l'instant, l'ordre des théories dans le fichier est important
i.e. les théories mentionnées par uses doivent être définies précédemment
......@@ -41,3 +45,17 @@ error reporting
- should we create a common [exception Why.Error of exn] to facilitate
integration of the library? This would require a special [raise] call:
why_raise e = raise (Why.Error e)
session
-------
- save the output of the prover
- escape the string in the xml
tools
-----
- the tools should verify that the provers have the same version
than reported in the configuration
- Maybe : make something generic for the dialog box with memory.
- autodetection can be modified now that only name/version/altern
are taken into account in session.
\ No newline at end of file
# Why version
VERSION=0.71
VERSION=0.71+git
module T
use import int.Int
exception MyExc
(* g can raise MyExc *)
let rec f (x: int) : int = {} raise MyExc {} | MyExc -> {}
with g (x: int) : int = {} f x {} | MyExc -> {}
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/mutual_exns"
End:
*)
module T
let test () =
let a,b,c,d = (1,2,3,4) in ()
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/tuples"
End:
*)
......@@ -65,6 +65,12 @@ AC_ARG_ENABLE(local,
[ --enable-local use Why3 in the build directory (no installation)],,
enable_local=no)
# NATIVE
AC_ARG_ENABLE(native-code,
[ --enable-native-code use the native-code compiler if available],,
enable_native_code=yes)
# IDE
AC_ARG_ENABLE(ide,
......@@ -87,18 +93,6 @@ AC_ARG_ENABLE(coq-libs,
[ --enable-coq-libs enable Coq realizations],,
enable_coq_libs=yes)
# TPTP parser
AC_ARG_ENABLE(whytptp,
[ --enable-whytptp enable TPTP parser (requires Menhir)],,
enable_whytptp=yes)
# Menhir library
AC_ARG_ENABLE(menhirlib,
[ --enable-menhirlib enable Menhir library],,
enable_menhirlib=no)
# hypothesis selection
AC_ARG_ENABLE(hypothesis-selection,
......@@ -182,6 +176,13 @@ else
fi
fi
# checking for native-code
if test "$enable_native_code" != yes || test "$OCAMLBEST" = byte ; then
enable_native_code=no
OCAMLBEST=byte
OCAMLOPT=no
fi
# checking for ocamlc.opt
AC_CHECK_PROG(OCAMLCDOTOPT,ocamlc.opt,ocamlc.opt,no)
if test "$OCAMLCDOTOPT" != no ; then
......@@ -263,29 +264,6 @@ if test "$USEOCAMLFIND" = yes; then
fi
fi
AC_CHECK_PROG(MENHIR,menhir,menhir,no)
if test "$MENHIR" = no ; then
enable_whytptp=no
enable_menhirlib=no
AC_MSG_WARN(cannot find menhir.)
fi
# checking for libmenhir
if test "$enable_menhirlib" = yes ; then
if test "$USEOCAMLFIND" = yes; then
MENHIRLIB=$(ocamlfind query menhirLib)
fi
if test -n "$MENHIRLIB"; then
echo "ocamlfind found menhir library in $MENHIRLIB"
else
MENHIRLIB="+menhirLib"
AC_CHECK_FILE($OCAMLLIB/menhirLib,,enable_menhirlib=no)
if test "$enable_menhirlib" = no; then
AC_MSG_WARN(Lib menhir not found.)
fi
fi
fi
# checking for rubber
AC_CHECK_PROG(RUBBER,rubber,rubber,no)
if test "$enable_doc" = yes ; then
......@@ -502,7 +480,6 @@ AC_SUBST(OCAMLOPT)
AC_SUBST(OCAMLDEP)
AC_SUBST(OCAMLLEX)
AC_SUBST(OCAMLYACC)
AC_SUBST(MENHIR)
AC_SUBST(OCAMLDOC)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
......@@ -517,7 +494,6 @@ AC_SUBST(enable_profiling)
AC_SUBST(CAMLP5O)
AC_SUBST(enable_ide)
AC_SUBST(MENHIRLIB)
AC_SUBST(LABLGTK2LIB)
AC_SUBST(SQLITE3LIB)
AC_SUBST(enable_bench)
......@@ -532,9 +508,6 @@ AC_SUBST(COQDEP)
AC_SUBST(COQLIB)
AC_SUBST(COQVERSION)
AC_SUBST(enable_whytptp)
AC_SUBST(enable_menhirlib)
AC_SUBST(enable_hypothesis_selection)
AC_SUBST(enable_doc)
......@@ -566,6 +539,7 @@ echo " Summary"
echo "-----------------------------------------"
echo "OCaml version : $OCAMLVERSION"
echo "OCaml library path : $OCAMLLIB"
echo "Compile in native code : $enable_native_code"
echo "Verbose make : $enable_verbose_make"
echo "Why IDE : $enable_ide $reason_ide"
echo "Why bench tool : $enable_bench"
......@@ -580,8 +554,6 @@ if test "$enable_coq_support" = "yes" ; then
echo " FP arithmetic : $enable_coq_fp_libs $reason_coq_fp_libs"
fi
fi
echo "TPTP parser : $enable_whytptp"
echo "Menhir library : $enable_menhirlib"
echo "hypothesis selection : $enable_hypothesis_selection"
echo "profiling : $enable_profiling"
echo "localdir : $enable_local"
......@@ -161,18 +161,42 @@ let config : Whyconf.config = Whyconf.read_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Util.Mstr.t =
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
\end{verbatim}
The type \texttt{'a Util.Mstr.t} is a map indexed by strings. This map
can provide the set of existing provers. In the following, we directly
The type \texttt{'a Whyconf.Mprover.t} is a map indexed by provers. A
provers is a record with a name, a version and an alternative description
(if someone want to compare different command line options of the same
provers for example). It's definition is in the module
\texttt{Whyconf} :
\begin{verbatim}
type prover =
{ prover_name : string; (* "Alt-Ergo" *)
prover_version : string; (* "2.95" *)
prover_altern : string; (* "special" *)
}
\end{verbatim}
The map \texttt{provers} provides the set of existing provers.
In the following, we directly
attempt to access the prover Alt-Ergo, which is known to be identified
with id \texttt{"alt-ergo"}.
\begin{verbatim}
(* the [prover alt-ergo] section of the config file *)
let alt_ergo : Whyconf.config_prover =
try
Util.Mstr.find "alt-ergo" provers
Whyconf.prover_by_id config "alt-ergo"
with Whyconf.ProverNotFound _ ->
eprintf "Prover alt-ergo not installed or not configured@.";
exit 0
\end{verbatim}
We could also get a specific version with :
\begin{verbatim}
let alt_ergo : Whyconf.config_prover =
try
let prover = {Whyconf.prover_name = "Alt-Ergo";
prover_version = "0.92.3";
prover_altern = ""} in
Whyconf.Mprover.find prover provers
with Not_found ->
eprintf "Prover alt-ergo not installed or not configured@.";
exit 0
......
......@@ -52,7 +52,7 @@ make install
Installation can be tested as follows:
\begin{enumerate}
\item install some external provers (see~Section\ref{provers} below)
\item run \texttt{why3config --detect}
\item run \verb|why3config --detect|
\item run some examples from the distribution, \emph{e.g.} you should
obtain the following:
\begin{verbatim}
......@@ -164,10 +164,10 @@ printer, as explained in the corresponding section.
If the user's configuration file is already present,
\texttt{why3config} will only reset unset variables to default value,
but will not try to detect provers.
The option \texttt{--detect-provers} should be used to force
The option \verb|--detect-provers| should be used to force
\why to detect again the available
provers and to replace them in the configuration file. The option
\texttt{--detect-plugins} will do the same for plugins.
\verb|--detect-plugins| will do the same for plugins.
\section{The \texttt{why3} command-line tool}
\label{sec:why3ref}
......@@ -187,28 +187,28 @@ The \texttt{why3} tool executes the following steps:
stop if some plugin fails to load.
\item Parse and typecheck the given files using the correct parser in order
to obtain a set of \why theories for each file. It uses
the filename extension or the \texttt{--format} option to choose
among the available parsers. The \texttt{--list-format} option gives
the filename extension or the \verb|--format| option to choose
among the available parsers. The \verb|--list-format| option gives
the list of registered parsers.
\item Extract the selected goals inside each of the selected theories
into tasks. The goals and theories are selected using the options
\texttt{-G/--goal} and \texttt{-T/--theory}. The option
\texttt{-T/--theory} applies to the last file appearing on the
command line, the option \texttt{-G/--goal} applies to the last theory
\verb|-G/--goal| and \verb|-T/--theory|. The option
\verb|-T/--theory| applies to the last file appearing on the
command line, the option \verb|-G/--goal| applies to the last theory
appearing on the command line. If no theories are selected in a file,
then every theory is considered as selected. If no goals are selected
in a theory, then every goal is considered as selected.
\item Apply the transformation requested
with \texttt{-a/--apply-transform} in their order of appearance on the
command line. \texttt{--list-transforms} list the known
with \verb|-a/--apply-transform| in their order of appearance on the
command line. \verb|--list-transforms| list the known
transformations, plugins can add more of them.
\item Apply the driver selected with the \texttt{-D/--driver} option,
or the driver of the prover selected with \texttt{-P/--prover}
option. \texttt{--list-provers} lists the known provers, i.e.~the ones
\item Apply the driver selected with the \verb|-D/--driver| option,
or the driver of the prover selected with \verb|-P/--prover|
option. \verb|--list-provers| lists the known provers, i.e.~the ones
which appear in the configuration file.
\item If the option \texttt{-P/--prover} is given, call the selected prover
\item If the option \verb|-P/--prover| is given, call the selected prover
on each generated task and print the results. If the option
\texttt{-D/--driver} is given, print each generated task using
\verb|-D/--driver| is given, print each generated task using
the format specified in the selected driver.
\end{enumerate}
......@@ -231,15 +231,15 @@ The provers can answer the following output:
% \item TO BE COMPLETED *)
% \end{itemize} *)
The option \texttt{--bisect} change the behaviors of why3. With this
option, \texttt{-P/--prover} and \texttt{-o/--output} must be given
The option \verb|--bisect| change the behaviors of why3. With this
option, \verb|-P/--prover| and \verb|-o/--output| must be given
and a valid goal must be selected. The last step executed by why3 is
replaced by computing a minimal set (in the great majority of the
case) of declarations which still prove the goal. Currently it doesn't
use any information provided by the prover, it call the prover
multiple time with reduced context. The minimal set of declarations is
then written in the prover syntax into a file located in the directory
given to the \texttt{-o/--output} option.
given to the \verb|-o/--output| option.
\section{The \texttt{why3ide} GUI}
\label{sec:ideref}
......@@ -487,9 +487,9 @@ not and you have to use the IDE to update it.
\begin{itemize}
\item The exit code is 0 if no difference was detected, 1 if there
was. Other exit codes mean some failure in running the replay.
\item option \texttt{-s}: suppresses the output of the final tree view.
\item option \verb|-s|: suppresses the output of the final tree view.
\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath.
\item option \texttt{-force}: force writing a new session file even if
\item option \verb|-force|: force writing a new session file even if
some proofs did not replay correctly.
\item option \texttt{-smoke-detector \{none|top|deep\}} try to detect
if the context is self-contradicting.
......@@ -568,8 +568,117 @@ output.
Figure~\ref{fig:replayer} proposes some suggestions for these macros, together
with the table obtained from the hello proof example of Section~\ref{chap:starting}.
\section{The \texttt{why3session} tool}
\label{sec:why3session}
The program \texttt{why3session} allows to manipulate why3 session on
the command line. It thus allow to batch modifications to several
sessions at once. This tool is subdivided into sub-commands:
\texttt{info}, \texttt{rm}, \texttt{copy}, \texttt{mod}.
Currently this tool report or modify only proof attempts.
\texttt{why3session info} reports informations:
\begin{itemize}
\item the option \verb|--provers| prints the provers which appear
inside the session. One by line.
\item the option \verb|--edited-files| prints all the files which
appear in the session as edited proofs.
\item the option \verb|--tree| print the structure of the session as
an ASCII tree. The files, theories, goals are marked with a question
mark \verb|?|, if they are not verified. A proof is usually said verified
if it the proof result is \verb|valid| and the proof is not
obsolete. However here specially
we separate these two properties. On the one hand if the proof suffers from an internal
failure we mark it with an exclamation mark \verb|!|, otherwise if
it's not valid we mark it with a question mark \verb|?|, finally
if it's valid we add nothing. On the other hand if the proof is obsolete we mark it
with an \verb|O| and if it is archived we mark it with a
\verb|A|.
\item the option \verb|--print0| separates the results of the options
\verb|provers| and \verb|--edited-files| by the character number
0 instead of end of line \verb|\n|. That can allows you to
safely use (even if the filename contains space or carriage return)
the result with other commands. For example you can count the number
of proof line in all the coq edited files in a session with:
\begin{verbatim}
why3session info --edited-files vstte12_bfs --print0 | xargs -0 coqwc
\end{verbatim}
or you can add all the edited files in your favorite repository
with:
\begin{verbatim}
why3session info --edited-files --print0 vstte12_bfs.mlw | \
xargs -0 git add
\end{verbatim}
\end{itemize}
The sub-commands \verb|why3session mod|, \verb|why3session copy|,
\verb|why3session rm| share the same set of commands for selecting the
proof attempts to work on:
\begin{itemize}
\item the option \verb|--filter-prover| selects only the proof attempt with
the given prover. This option can be specified multiple times to
allow to select all the proofs that corresponds to one of the given
prover. If this option is not specified the proof are simply not
filtered by there corresponding prover.
\item the option \verb|--filter-verified yes| restricts the selection to
the proofs that are valids and not obsoletes. On contrary the option
\verb|--filter-verified no| select the ones that are not verified.
\verb|--filter-verified all|, the default, doesn't select on this property.
\item the option \verb|--filter-verified-goal yes| restricts the selection
to the proofs of verified goals (that doesn't mean that the proof is
verified). Same for the other cases \verb|no| and \verb|all|.
\item the option \verb|--filter-archived yes| restricts the selection
to the proofs that are archived. Same for the other cases \verb|no|
and \verb|all| except the default is \verb|no|.
\end{itemize}
The sub-command \verb|why3session mod| modifies properties of proof
attempts:
\begin{itemize}
\item the option \verb|--set-obsolete| set the selected proofs to
obsolete
\item the option \verb|--set-archived| set the selected proofs to archived
\item the option \verb|--unset-archived| unset the selected proofs
from the archived
\end{itemize}
The commands \verb|why3session copy| copies a proof attempt to another
provers but to the same goal. The new prover is specified by the option
\verb|--to-prover|, for example \verb|--to-prover Alt-Ergo,0.94|.
A question can arise if a proof with this prover already exists.
You can choose between four behaviors of why3session:
\begin{itemize}
\item replace the proof regardless of it (\verb|-f, --force|)
\item never replace such a proof (\verb|-n, --never|)
\item replace the proof except if the proof is verified (valid and not
obsolete) (\verb|-c, --conservative|). It's the default
\item ask the user each time the case arise (\verb|-i, --interactive|)
\end{itemize}
If you just want to update one session with updated provers you can
use \verb|--convert-unknown| instead of the option \verb|--to-prover|.
\begin{verbatim}
why3session copy --convert-unknown
\end{verbatim}
For each proof attempt not archived which correspond to an unknown
prover, a prover which is not in \verb|.why3.conf|, it will try to find
a known prover with the same name. If it finds one the proof is copied
(the corresponding edited files are copied and regenerated for the known