Commit dd040652 authored by Mário Pereira's avatar Mário Pereira

Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr/gitroot/why3/why3 into new_system

parents a99f7b84 0153170f
......@@ -164,7 +164,12 @@ pvsbin/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/Why3_Bool.thy
/lib/isabelle/Why3_BV.thy
/lib/isabelle/Why3_Int.thy
/lib/isabelle/Why3_List.thy
/lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_Set.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv
......@@ -283,10 +288,13 @@ pvsbin/
# Try Why3
/src/trywhy3/trywhy3.byte
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.map
/src/trywhy3/alt_ergo_worker.byte
/src/trywhy3/alt_ergo_worker.js
/src/trywhy3/alt_ergo_worker.map
/src/trywhy3/why3_worker.byte
/src/trywhy3/why3_worker.js
/src/trywhy3/why3_worker.map
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/index.html
......
......@@ -8,6 +8,20 @@ Tools
installed provers. These are available under name "Auto level 1"
and "Auto level 2" in why3 ide.
Version 0.87.3, January ??, 2017
=================================
bug fixes
o
Provers
o support for Alt-Ergo 1.30 (released ??, 2016)
o support for Coq 8.6 (released ?, 2016)
o support for Gappa 1.3 (released ?, 2016)
* discarded support for Isabelle 2015
o support for Isabelle 2016-1 (released Dec 2016)
o support for Z3 4.5.0 (released ? 2016)
Version 0.87.2, September 1, 2016
=================================
......
......@@ -610,7 +610,11 @@ clean::
.PHONY: gallery
gallery::
gallery:: gallery-simple gallery-subs
.PHONY: gallery-simple
gallery-simple::
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
@for x in examples/*/why3session.xml ; do \
d=`dirname $$x`; \
......@@ -627,7 +631,7 @@ gallery::
.PHONY: gallery-subs
GALLERYSUBS=avl
GALLERYSUBS=WP_revisited verifythis_2016_matrix_multiplication avl double_wp
gallery-subs::
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
......@@ -797,7 +801,7 @@ COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQPTREES = kernel interp intf lib library parsing pretyping proofs printing tactics toplevel
COQPTREES = engine interp intf kernel lib library ltac parsing pretyping printing proofs tactics toplevel
COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
......@@ -823,14 +827,20 @@ src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(SHOW) 'Camlp $<'
$(HIDE)$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3
ifeq (@coq_compat_version@,COQ86)
COQRTAC += -I lib/coq-tactic
endif
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
$(HIDE)WHY3CONFIG="" $(COQC) -byte $(COQRTAC) $< && \
touch src/coq-tactic/.why3-vo-byte
src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cmxs
$(SHOW) 'Coqc $<'
$(HIDE)WHY3CONFIG="" $(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 $< && \
$(HIDE)WHY3CONFIG="" $(COQC) -opt $(COQRTAC) $< && \
touch src/coq-tactic/.why3-vo-opt
# depend and clean targets
......@@ -1145,7 +1155,7 @@ clean::
ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=why3.ML Why3_BV.thy
ISABELLEVERSIONSPECIFIC=why3.ML Why3_Bool.thy Why3_BV.thy Why3_Int.thy Why3_List.thy Why3_Number.thy Why3_Set.thy
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))
......@@ -1436,9 +1446,17 @@ install_no_local::
# trywhy3
#########
ifeq ($(DEBUGJS),yes)
JSOO_DEBUG=--pretty --debug-info --source-map
JS_MAPS=alt_ergo_worker.map trywhy3.map why3_worker.map
else
JSOO_DEBUG=
JS_MAPS=
endif
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -g -package js_of_ocaml.syntax \
-syntax camlp4o -I src/trywhy3 \
-I $(ALTERGODIR)/src/util \
-I $(ALTERGODIR)/src/structures \
......@@ -1479,7 +1497,7 @@ TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
fontawesome/fonts/fontawesome-webfont.woff fontawesome/fonts/fontawesome-webfont.eot \
fontawesome/fonts/fontawesome-webfont.ttf fontawesome/fonts/fontawesome-webfont.woff2 \
ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \
ace-builds/src-min-noconflict/theme-chrome.js
ace-builds/src-min-noconflict/theme-chrome.js $(JS_MAPS)
trywhy3_package: trywhy3
tar czf trywhy3.tar.gz -C src $(addprefix trywhy3/, $(TRYWHY3FILES))
......@@ -1487,11 +1505,11 @@ trywhy3_package: trywhy3
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js src/trywhy3/examples/*.mlw
js_of_ocaml -I src/trywhy3 \
js_of_ocaml --extern-fs $(JSOO_DEBUG) -I src/trywhy3 \
--file=why3_worker.js:/ \
--file=alt_ergo_worker.js:/ \
--file=examples/index.txt:/ \
`find src/trywhy3/examples \( -name "*.mlw" -o -name "*.why" \) -printf " --file=examples/%P:/"` \
--file=examples/index.txt:/examples/index.txt \
`find src/trywhy3/examples \( -name "*.mlw" -o -name "*.why" \) -printf " --file=examples/%P:/examples/%P"` \
+weak.js +nat.js $<
src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
......@@ -1499,9 +1517,9 @@ src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/%p"` \
+weak.js +nat.js $<
src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
......@@ -1509,7 +1527,7 @@ src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/try
src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
js_of_ocaml $(JSOO_DEBUG) +weak.js +nat.js +dynlink.js +toplevel.js $<
src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) src/trywhy3/worker_proto.cmo src/trywhy3/alt_ergo_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
......@@ -1616,10 +1634,10 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
@rm -f test-session.opt why3session.xml why3shapes why3shapes.gz
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
$(COQC) -byte -R lib/coq-tactic Why3 -R lib/coq Why3 bench/coq-tactic/test.v
$(COQC) -byte $(COQRTAC) bench/coq-tactic/test.v
test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
$(COQC) -opt -R lib/coq-tactic Why3 -R lib/coq Why3 bench/coq-tactic/test.v
$(COQC) -opt $(COQRTAC) bench/coq-tactic/test.v
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
......
......@@ -52,6 +52,7 @@ drivers () {
pgm="bin/why3prove$suffix"
for f in $1/*.drv; do
if [[ $f == drivers/ocaml*.drv ]]; then continue; fi
if [[ $f == drivers/c.drv ]]; then continue; fi
echo -n " $f... "
# running Why
if ! echo "theory Test goal G : 1=2 end" | $pgm -F whyml --driver $f - > /dev/null; then
......@@ -234,7 +235,7 @@ goods examples/check-builtin
goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/hoare_logic
goods examples/WP_revisited
goods examples/avl "-L examples/avl"
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
......
......@@ -522,11 +522,16 @@ if test "$enable_coq_support" = yes; then
COQPPLIBS="$COQLIB/parsing/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.5*|trunk)
8.5*)
coq_compat_version="COQ85"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.6*|trunk)
coq_compat_version="COQ86"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded)
......@@ -638,9 +643,9 @@ else
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEDETECTEDVERSION in
2015*)
2016-1*)
enable_isabelle_support=yes
ISABELLEVERSION=2015
ISABELLEVERSION=2016-1
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2016*)
......@@ -651,8 +656,8 @@ else
*)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle 2015 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2015)"
AC_MSG_WARN(You need Isabelle 2016 or later; Isabelle discarded)
reason_isabelle_support=" (need version >= 2016)"
;;
esac
fi
......
......@@ -11,9 +11,9 @@ using ``Edit'' action in \texttt{why3 ide}.
\subsection{Installation}
You need version Isabelle2015 or Isabelle2016. Former versions are not
supported. We assume below that your version is 2016, please replace
2016 by 2015 otherwise.
You need version Isabelle2016 or Isabelle2016-1. Former versions are not
supported. We assume below that your version is 2016-1, please replace
2016-1 by 2016 otherwise.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......@@ -22,7 +22,7 @@ and installation of \why, you must manually add the path
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2016/etc/components
.isabelle/Isabelle2016-1/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......
......@@ -274,6 +274,18 @@ meta "rewrite" prop a
from left to right. Beware that there is no check for termination
nor for confluence of the set of rewrite rules declared.
\end{itemize}
Instead of using a meta, it is possible to declare an axiom as a
rewrite rule by adding the label \verb|"rewrite"| on the axiom name or
on the axiom itself, e.g.:
\begin{whycode}
axiom a "rewrite": forall ... t1 = t2
lemma b: "rewrite" forall ... f1 <-> f2
\end{whycode}
The second form allows some form of local rewriting, e.g.
\begin{whycode}
lemma l: forall x y. ("rewrite" x = y) -> f x = f y
\end{whycode}
can be proved by \verb|introduce_premises| followed by \verb|"compute_specified"|.
\paragraph{Bound on the number of reductions}
The computations performed by these transformations can take an
......
(* Driver for Alt-Ergo version >= 0.95 *)
(* Driver for Alt-Ergo versions >= 0.95.2 *)
import "alt_ergo_common.drv"
import "no-bv.gen"
theory BuiltIn
(* Alt-Ergo >= 0.95 supports enumerated datatypes and records *)
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
end
theory int.EuclideanDivision
(* protection against wrong semantics for negative arguments
last checked on 0.99.1: this is still needed
*)
prelude "logic safe_eucl_div: int, int -> int"
prelude "axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y"
prelude "logic safe_eucl_mod: int, int -> int"
prelude "axiom safe_eucl_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_mod(x,y) = x % y"
syntax function div "safe_eucl_div(%1,%2)"
syntax function mod "safe_eucl_mod(%1,%2)"
end
theory int.ComputerDivision
(* protection against wrong semantics for negative arguments
last checked on 0.99.1: this is still needed
*)
prelude "logic safe_comp_div: int, int -> int"
prelude "axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y"
prelude "logic safe_comp_mod: int, int -> int"
prelude "axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y"
syntax function div "safe_comp_div(%1,%2)"
syntax function mod "safe_comp_mod(%1,%2)"
end
(* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
valid "^Inconsistent assumption$"
(* Why drivers for Alt-Ergo: common part *)
prelude "(* this is the prelude for Alt-Ergo, any versions *)"
prelude "(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)"
printer "alt-ergo"
filename "%f-%t-%g.why"
valid "Valid"
invalid "Invalid"
unknown "I don't know" ""
timeout "Timeout"
steplimitexceeded "Steps limit reached"
valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
invalid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Invalid"
unknown "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:I don't know" ""
timeout "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Timeout"
timeout "^Timeout$"
steplimitexceeded "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Steps limit reached"
outofmemory "Fatal error: out of memory"
outofmemory "Fatal error: exception Stack_overflow"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
......@@ -39,6 +40,10 @@ theory BuiltIn
syntax type real "real"
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "keep_enums"
meta "eliminate_algebraic" "keep_recs"
end
theory int.Int
......@@ -84,6 +89,26 @@ theory int.Int
end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
theory int.ComputerDivision
prelude "logic comp_div: int, int -> int"
prelude "axiom comp_div_def: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y"
prelude "logic comp_mod: int, int -> int"
prelude "axiom comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y"
syntax function div "comp_div(%1,%2)"
syntax function mod "comp_mod(%1,%2)"
end
theory real.Real
......
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Fields.inverse_class.divide\"/>%1%2</app>"
end
theory number.Prime
syntax predicate prime "<app><const name=\"Factorial_Ring.normalization_semidom_class.prime\"/>%1</app>"
end
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Rings.divide_class.divide\"/>%1%2</app>"
theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
end
......@@ -156,14 +156,15 @@ theory number.Gcd
syntax function gcd "<app><const name=\"GCD.gcd_class.gcd\"/>%1%2</app>"
end
theory number.Prime
syntax predicate prime "<app><const name=\"Primes.prime\"/><app><const name=\"Int.nat\"/>%1</app></app>"
end
theory number.Coprime
syntax predicate coprime "<app><const name=\"GCD.gcd_class.coprime\"/>%1%2</app>"
end
theory algebra.Field
syntax function inv "<app><const name=\"Fields.inverse_class.inverse\"/>%1</app>"
syntax function (/) "<app><const name=\"Rings.divide_class.divide\"/>%1%2</app>"
end
theory real.Real
syntax function zero "<number val=\"0\"><type name=\"Real.real\"/></number>"
syntax function one "<number val=\"1\"><type name=\"Real.real\"/></number>"
......
......@@ -7,4 +7,4 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2015.gen"
import "isabelle-2016-1.gen"
......@@ -8,7 +8,7 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2015.gen"
import "isabelle-2016-1.gen"
transformation "simplify_trivial_quantification_in_goal"
......@@ -38,7 +38,7 @@
<proof prover="0" edited="blocking_semantics5_SemOp_steps_non_neg_1.v"><result status="valid" time="0.80"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="5386d426772b7907db51e574cfc3e48a">
<theory name="TestSemantics" sum="d19bd426b13b2949609e8ccb0829f621">
<goal name="Test13">
<proof prover="9"><result status="valid" time="0.02" steps="16"/></proof>
<proof prover="10"><result status="valid" time="0.03"/></proof>
......@@ -57,7 +57,7 @@
<proof prover="9"><result status="valid" time="0.05" steps="107"/></proof>
</goal>
<goal name="If42">
<proof prover="0" timelimit="6" edited="blocking_semantics5_TestSemantics_If42_1.v"><result status="valid" time="1.28"/></proof>
<proof prover="0" timelimit="6" edited="blocking_semantics5_TestSemantics_If42_1.v"><result status="valid" time="1.58"/></proof>
</goal>
</theory>
<theory name="Typing" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -90,14 +90,14 @@
<proof prover="9"><result status="valid" time="0.08" steps="143"/></proof>
</goal>
<goal name="eval_type_term.1.4" expl="4.">
<proof prover="0" edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"><result status="valid" time="1.57"/></proof>
<proof prover="0" edited="blocking_semantics5_TypingAndSemantics_eval_type_term_1.v"><result status="valid" time="2.24"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="type_preservation">
<proof prover="0" edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"><result status="valid" time="1.87"/></proof>
<proof prover="0" edited="blocking_semantics5_TypingAndSemantics_type_preservation_1.v"