Commit b5883169 authored by David Hauzar's avatar David Hauzar

Merge branch 'master' into counter-examples

Conflicts:
	doc/manpages.tex
parents 809ed52e ac867b29
......@@ -155,11 +155,13 @@ pvsbin/
/lib/isabelle/number/
/lib/isabelle/list/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/Tools/why3
/lib/isabelle/Why3_Number.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv
# /src/driver/
/src/driver/driver_lexer.ml
......@@ -218,6 +220,10 @@ pvsbin/
/examples/in_progress/binary_search2/
/examples/in_progress/binary_search_c/
/examples/in_progress/vacid_0_red_black_trees_harness/
/examples/in_progress/prover/bench/*/*.out
/examples/in_progress/prover/bench/*/*.txt
/examples/in_progress/prover/bench1
/examples/in_progress/prover/bench2
/examples/why3bench.html
/examples/why3regtests.err
/examples/why3regtests.out
......@@ -271,7 +277,12 @@ pvsbin/
# Try Why3
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.byte
/src/trywhy3/theories.ml
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/index.html
/src/trywhy3/ace-builds
/src/trywhy3/*.png
/src/trywhy3/alt-ergo-1.00-private-2015-01-29
# jessie3
/src/jessie/config.log
......
......@@ -22,4 +22,3 @@ with contributions of
Asma Tafat
Piotr Trojanek
Makarius Wenzel
* marks an incompatible change
library
Tools
* add a command-line option --extra-expl-prefix to specify
additional possible prefixes for VC explanations. (Available for
why3 commands "prove" and "ide".)
Library
* improved bitvectors theories
Encodings
......@@ -9,12 +14,20 @@ Encodings
cases of equality and maps) then the translation to SMT-LIB
format is direct
provers
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Isabelle 2015 (released May 25, 2015)
o support for Coq 8.4pl6 (released April 9, 2015)
Provers
o discarded support for Alt-Ergo versions older than 0.95.2
o support for Coq 8.4pl6 (released Apr 9, 2015)
o support for Gappa 1.2.0 (released May 19, 2015)
o support for Isabelle 2015 (released May 25, 2015)
o support for Z3 4.4.0 (released Apr 29, 2015)
o support for Zenon 0.8.0 (released Oct 21, 2014)
o support for Zenon_modulo 0.4.1 (released Jul 2, 2015)
Version 0.86.2, October 13, 2015
================================
bug fixes
o assorted bug fixes
Version 0.86.1, May 22, 2015
============================
......
......@@ -14,9 +14,13 @@ of the Library that is distributed under the conditions defined in clause
however invalidate any other reasons why the executable file might be
covered by the GNU Lesser General Public License.
The files src/util/extmap.ml{i} are derived from the sources of
OCaml 3.12 standard library, and are distributed under the GNU
LGPL version 2 (see file OCAML-LICENSE).
Icon sets for the graphical interface of Why3 are subject to specific
licenses, some of them may forbid commercial usage. These specific
licenses are detailed in files share/icons/*/*.txt
licenses are detailed in files share/images/*/*.txt
======================================================================
......
......@@ -71,7 +71,24 @@ EMACS = @EMACS@
#PDFVIEWER = @PDFVIEWER@
INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
WARNINGS = Aer-41-44-45@5
# warnings are enabled and non fatal by default, except:
# - disabled:
# 4 Fragile pattern matching: matching that will remain complete even
# if additional constructors are added to one of the variant types
# matched.
# 9 Missing fields in a record pattern.
# 41 Ambiguous constructor or label name.
# 44 Open statement shadows an already defined identifier.
# 45 Open statement shadows an already defined label or constructor.
# 50 Unexpected documentation comment.
# - fatal:
# 5 Partially applied function: expression whose result has function
# type and is ignored.
# 48 Implicit elimination of optional arguments.
WARNINGS = A-4-9-41-44-45-50@5@48
OFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -dtypes -g -I lib/why3 $(INCLUDES)
......@@ -621,6 +638,7 @@ gallery::
GALLERYSUBS=avl
gallery-subs::
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
@for d in $(GALLERYSUBS) ; do \
echo "exporting examples/$$d"; \
rm -f $(GALLERYDIR)/$$d/$$d.zip; \
......@@ -637,7 +655,8 @@ gallery-subs::
x=$*/why3session.xml; \
d=`dirname $$x`; \
f=`basename $$d`; \
why3 session html $$x; \
why3 session html $$d; \
rm $$d/*.bak; \
echo "exporting $$f"; \
mkdir -p $(GALLERYDIR)/$$f; \
if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \
......@@ -1140,13 +1159,13 @@ $(ISABELLEVERSIONSPECIFICTARGETS): $(ISABELLEVERSIONSPECIFICSOURCES)
clean::
rm -f $(ISABELLEVERSIONSPECIFICTARGETS)
ISABELLELIBS_INT_FILES = Exponentiation Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
ISABELLELIBS_BOOL_FILES = Bool
ISABELLELIBS_BOOL = $(addsuffix .xml, $(addprefix lib/isabelle/bool/, $(ISABELLELIBS_BOOL_FILES)))
ISABELLELIBS_REAL_FILES = # not yet realized : Abs ExpLog FromInt MinMax PowerInt Real Square RealInfix
ISABELLELIBS_REAL_FILES = Real RealInfix Abs MinMax FromInt Truncate Square ExpLog Trigonometry PowerInt # not yet realized : PowerReal Hyperbolic Polar
ISABELLELIBS_REAL = $(addsuffix .xml, $(addprefix lib/isabelle/real/, $(ISABELLELIBS_REAL_FILES)))
ISABELLELIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
......@@ -1161,6 +1180,9 @@ ISABELLELIBS_MAP = $(addsuffix .xml, $(addprefix lib/isabelle/map/, $(ISABELLELI
ISABELLELIBS_LIST_FILES = List Length Mem Nth NthNoOpt NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt RevAppend Combine Distinct NumOcc Permut
ISABELLELIBS_LIST = $(addsuffix .xml, $(addprefix lib/isabelle/list/, $(ISABELLELIBS_LIST_FILES)))
ISABELLELIBS_BV_FILES = Pow2int BV8 BV16 BV32 BV64 BVConverter_32_64 BVConverter_16_64 BVConverter_8_64 BVConverter_16_32 BVConverter_8_32 BVConverter_8_16
ISABELLELIBS_BV = $(addsuffix .xml, $(addprefix lib/isabelle/bv/, $(ISABELLELIBS_BV_FILES)))
drivers/isabelle-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
(echo "(* generated automatically at compilation time *)"; \
......@@ -1181,6 +1203,8 @@ drivers/isabelle-realizations.aux: Makefile
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_OPTION_FILES); do \
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_BV_FILES); do \
echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
) > $@
ifeq (@enable_local@,yes)
......@@ -1189,7 +1213,7 @@ else
ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
endif
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
endif
......@@ -1210,7 +1234,7 @@ install_no_local:: lib/isabelle/last_build
install_local:: lib/isabelle/last_build
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
......@@ -1252,6 +1276,11 @@ $(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realization
mkdir -p lib/isabelle/option
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
$(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bv.why
mkdir -p lib/isabelle/bv
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
# do not update isabelle realizations systematically
# opt byte: update-isabelle
......@@ -1426,21 +1455,58 @@ install_local:: bin/why3doc
# trywhy3
#########
ALTERGODIR=src/trywhy3/alt-ergo-0.99.1
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3 -I $(ALTERGODIR)/src/parsing
ALTERGOMODS=util/numbers util/version util/options parsing/why_parser parsing/why_lexer
TRYWHY3CMO=lib/why3/why3.cma
# $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
-syntax camlp4o -I src/trywhy3 \
-I $(ALTERGODIR)/src/util \
-I $(ALTERGODIR)/src/structures \
-I $(ALTERGODIR)/src/parsing \
-I $(ALTERGODIR)/src/preprocess \
-I $(ALTERGODIR)/src/theories \
-I $(ALTERGODIR)/src/instances \
-I $(ALTERGODIR)/src/sat \
-I $(ALTERGODIR)/src/main
ALTERGOMODS=util/numsNumbers util/numbers \
util/version util/myUnix util/config util/options \
util/hashcons util/hstring util/lists util/loc \
util/profiling_default util/profiling \
util/util \
structures/parsed structures/symbols \
structures/ty structures/errors \
structures/term structures/literal structures/formula \
structures/explanation structures/exception \
parsing/why_parser parsing/why_lexer \
preprocess/existantial preprocess/triggers \
preprocess/why_typing preprocess/cnf \
theories/polynome theories/ac \
theories/intervals theories/inequalities \
theories/intervalCalculus \
theories/arith theories/records theories/bitv \
theories/arrays theories/sum theories/uf theories/use \
theories/combine theories/ccx theories/theory \
instances/matching \
sat/sat_solvers \
main/frontend
TRYWHY3CMO=lib/why3/why3.cma $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
%.fr.html: %.prehtml
yamlpp -l fr $< -o $@
%.en.html: %.prehtml
yamlpp -l en $< -o $@
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
--file=drinkers.why:/ \
--file=simplearith.why:/ \
--file=bin_mult.mlw:/ \
--file=fact.mlw:/ \
--file=isqrt.mlw:/ \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+weak.js +nat.js $^
......
......@@ -42,6 +42,10 @@ The files src/util/extmap.ml{i} are derived from the sources of
OCaml 3.12 standard library, and are distributed under the GNU
LGPL version 2 (see file OCAML-LICENSE).
Icon sets for the graphical interface of Why3 are subject to specific
licenses, some of them may forbid commercial usage. These specific
licenses are detailed in files share/images/*/*.txt
INSTALLATION
============
......
......@@ -161,7 +161,12 @@ Release Notes (details in file CHANGES):
* fix bug 18953 : (<>) not allowed as prefix form
* finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
solution possible: symbol builtin t_neq, inlining systematique au typage
(ou laisser inline_trivial le faire)
* DONE finalize detect_polymorphism. Allow polymorphic tuples (supported by SMT ?)
C'est finalisé. Mais les tuples restent polymorphes.
* integrate server feature done by Johannes
......@@ -180,6 +185,8 @@ Release Notes (details in file CHANGES):
alt-ergo -replay <file>.agr
-> on pourrait le faire en considerant altgr-ergo comme un prouveur interactif
* make the strategy feature public and documented. Possibly generate
default strategies dynamically at the time of why3 config --detect,
using the provers detected : for that, we can annotated the provers in
......@@ -252,58 +259,50 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
== Final preparation ==
* faire une passe sur le BTS
* check the BTS
* do "make update-coq" and "make", fix Coq realizations if needed
* check that nightly bench is OK
* check that "make xml-validate-local" is OK
(see below : copy the dtd on the web)
* put 0.86 in file Version, and then run ./config.status
* check/update the content of the About dialog in src/ide/gconfig.ml
around lines 550-600
* check headers
* check the file CHANGES, add the release date
* manual in PDF:
** update the date in doc/manual.tex (near \whyversion{})
** check that macro \todo is commented out in doc/macros.tex
** and then "make doc"
(check that manual in HTML is also generated, doc/html/index.html)
* do "make dist"
* test distrib/why3-0.86.tar.gz
* move distrib from Why3 site to Inria forge:
** upload distrib/why3-0.86.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
* put on the web page
- the manual in PDF
cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.86.pdf
- the HTML version of the manual (content of doc/html)
cp -r doc/html /users/www-perso/projets/why3/doc-0.86
- why3session.dtd
cp -f share/why3session.dtd /users/www-perso/projets/why3/
* generate documentation
- update the date in doc/manual.tex (near \whyversion{})
- check that macro \todo is commented out in doc/macros.tex
- do "make doc"
(check that manual in HTML is also generated, doc/html/index.html)
- do "make stdlibdoc"
- do "make apidoc"
- standard library online, using why3doc, to http://why3.lri.fr/stdlib/
make stdlibdoc
cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.86
* make a last commit:
- git commit -am "release 0.86"
- git tag 0.86
* do "make dist"
* test distrib/why3-0.86.tar.gz
* push the commit:
- git push
- git push --tags
* upload distrib/why3-0.86.tar.gz to https://gforge.inria.fr/frs/?group_id=2990
* upload the documentation on the web page
- cp doc/manual.pdf /users/www-perso/projets/why3/download/manual-0.86.pdf
- cp -r doc/html /users/www-perso/projets/why3/doc-0.86
- cp share/why3session.dtd /users/www-perso/projets/why3/
- cp -r doc/stdlibdoc /users/www-perso/projets/why3/stdlib-0.86
ln -s -n -f stdlib-0.86 /users/www-perso/projets/why3/stdlib
- API doc, produced using ocamldoc, to http://why3.lri.fr/api/
make apidoc
cp -r doc/apidoc /users/www-perso/projets/why3/api-0.86
- cp -r doc/apidoc /users/www-perso/projets/why3/api-0.86
ln -s -n -f api-0.86 /users/www-perso/projets/why3/api
- update the main HTML page (sources are in repository why3-www)
edit index.html, change at least all occurrences of 0.85 by 0.86, and
update the url for download
make (to check validity)
make export
* make a last commit:
- git commit -am "release 0.86"
- add tag 0.86 to the git repository, using
git tag 0.86
- do not forget to push it using
git push
git push --tags
* update the main HTML page (sources are in repository why3-www)
- edit index.html, change at least all occurrences of 0.85 by 0.86, and
update the url for download
- make (to check validity)
- make export
* add a new version to the bugtracker:
https://gforge.inria.fr/tracker/admin/?group_id=2990&atid=10293&add_extrafield=1
......@@ -311,45 +310,27 @@ DONE * sauvegarde de la configuration : à quel endroit dans l'IDE ?
* The next commit : add +git to the version in file Version
* prepare the OPAM package
. obtain a local copy of opam repository, or obtain a former one :
git clone git@github.com:claudemarche/opam-repository.git
cd opam-repository/
git remote add opam https://github.com/ocaml/opam-repository.git
or, if you already have one, make sure it is up-to-date:
git fetch opam
git reset --hard opam/master
git push
. copy former files:
cp -r packages/why3-base/why3-base-0.85 packages/why3-base/why3-base-0.86
cp -r packages/why3/why3-0.85 packages/why3/why3-0.86
. update packages/why3-base/why3-base-0.86/url:
url and checksum of why-0.86.tar.gz obtained via
md5sum distrib/why3-0.86.tar.gz
. update packages/why3-base/why3-base-0.86/descr if necessary
. update packages/why3/why3-0.86/descr if necessary
. update packages/why3-base/why3-base-0.86/opam with correct dependencies and such
. update packages/why3/why3-0.86/opam with correct dependencies and such
(at least the dependency on why3-base should be fixed)
* test the OPAM package (requires opam 1.2)
opam pin why3 ./.git
opam install why3
* make a pull request on OPAM
git add why3.0.86
git commit -am "new package version why3 0.86"
git push
sur github: creer un pull request
- update opam/why3-base/url: url and checksum of why-0.86.tar.gz
(use "md5sum distrib/why3-0.86.tar.gz")
- update opam/why3-base/descr and opam/why3/descr if necessary
- update opam/why3-base/opam with correct dependencies
- update opam/why3/opam with the dependency on why3-base
- test with "opam pin add why3 --kind=git .../why3/.git"
(it runs "opam install why3")
* upload the OPAM package
- clone https://github.com/ocaml/opam-repository
git clone git@github.com:.../opam-repository.git
cd opam-repository/
git remote add opam https://github.com/ocaml/opam-repository.git
- reinitialize the repository if not fresh:
git fetch opam
git reset --hard opam/master
git push
- cd packages/why3-base; cp -r .../opam/why3-base why3-base.0.86
- cd packages/why3; cp -r .../opam/why3 why3.0.86
- commit and push
- make a pull request on github
* inform Jerry James <loganjerry@gmail.com> so that he can produce the
Fedora package
......
......@@ -552,13 +552,13 @@ if test "$enable_coq_libs" = yes; then
AC_MSG_CHECKING([for Flocq])
AS_IF(
[ echo "Require Import Flocq.Flocq_version BinNat." \
"Goal (20200 <= Flocq_version)%N. easy. Qed." > conftest.v
"Goal (20500 <= Flocq_version)%N. easy. Qed." > conftest.v
"$COQC" conftest.v > conftest.err ],
[ AC_MSG_RESULT(yes) ],
[ AC_MSG_RESULT(no)
enable_coq_fp_libs=no
AC_MSG_WARN(Cannot find Flocq.)
reason_coq_fp_libs=" (Flocq >= 2.2 not found)" ])
reason_coq_fp_libs=" (Flocq >= 2.5 not found)" ])
rm -f conftest.v conftest.vo conftest.err
fi
......
......@@ -185,7 +185,7 @@ The \texttt{prove} command executes the following steps:
%\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
%you want to call the provers concurrently. *)
\noindent
\subsection{Prover Results}
The provers can give the following output:
\begin{description}
\item[Valid] The goal is proved in the given context.
......@@ -212,6 +212,17 @@ The provers can give the following output:
%then written in the prover syntax into a file located in the directory
%given to the \verb|-o/--output| option.
\subsection{Additional Options}
\label{sec:proveoptions}
\begin{description}
\item[\texttt{-{}-get-ce}] activates the generation of a potential counter-example when a proof does not succeed (experimental).
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}] specifies
\textsl{s} as an additional prefix for labels that denotes VC
explanations. The option can be used several times to specify
several prefixes.
\end{description}
\section{The \texttt{ide} Command}
\label{sec:ideref}
......@@ -440,19 +451,26 @@ are grouped together under several tabs.
\end{description}
% \subsection{Displaying Counterexamples}
%
%
% how to use counterexamples - explain labels, projections, the option --get-ce of why3prove and the setting in why3ide
%
%
% problem with set logic and counterexamples
%
%
% which provers
%
%
% where it is displayed
%
%
% how to interpret the display
%
%
% example
\subsection{Additional Command-Line Options}
The \texttt{ide} command also accepts the following options described for the command \texttt{prove} in Section~\ref{sec:proveoptions}.
\begin{description}
\item[\texttt{-{}-extra-expl-prefix \textsl{<s>}}]
\end{description}
\section{The \texttt{bench} Command}
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX