Merge branch 'bugfix/v0.87'

CHANGES

@@ -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
 =================================
 

Makefile.in

@@ -805,7 +805,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
@@ -831,14 +831,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
@@ -1629,10 +1635,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

configure.in

@@ -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)

doc/technical.tex

@@ -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

lib/coq/map/Occ.v

@@ -57,7 +57,7 @@ Proof.
 intros a a_WT v m l u h1.
 assert (u - l <= 0)%Z as h1' by omega.
 unfold occ.
-destruct (u - l)%Z ; try easy.
+destruct (u - l)%Z ; try reflexivity.
 now elim h1'.
 Qed.
 

share/provers-detection-data.conf

@@ -193,6 +193,7 @@ use_at_auto_level = 2
 [ATP gappa]
 name = "Gappa"
 exec = "gappa"
+exec = "gappa-1.3.1"
 exec = "gappa-1.3.0"
 exec = "gappa-1.2.2"
 exec = "gappa-1.2.0"
@@ -341,10 +342,12 @@ version_old = "201310"
 [ATP z3]
 name = "Z3"
 exec = "z3"
+exec = "z3-4.5.0"
 exec = "z3-4.4.1"
 exec = "z3-4.4.0"
 version_switch = "-version"
 version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_ok  = "4.5.0"
 version_ok  = "4.4.1"
 version_ok  = "4.4.0"
 driver = "drivers/z3_440.drv"
@@ -357,10 +360,12 @@ use_at_auto_level = 1
 name = "Z3"
 alternative = "noBV"
 exec = "z3"
+exec = "z3-4.5.0"
 exec = "z3-4.4.1"
 exec = "z3-4.4.0"
 version_switch = "-version"
 version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_ok  = "4.5.0"
 version_ok  = "4.4.1"
 version_ok  = "4.4.0"
 driver = "drivers/z3_432.drv"
@@ -505,6 +510,18 @@ version_ok = "7.0"
 command = "%e -noprompt"
 driver = "drivers/mathematica.drv"
 
+# Coq 8.6: do not limit memory
+[ITP coq]
+name = "Coq"
+compile_time_support = true
+exec = "coqtop -batch"
+version_switch = "-v"
+version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
+version_ok = "8.6"
+command = "%e -I %l/coq-tactic -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
+driver = "drivers/coq.drv"
+editor = "coqide"
+
 # Coq 8.5: do not limit memory
 [ITP coq]
 name = "Coq"
@@ -512,6 +529,8 @@ compile_time_support = true
 exec = "coqtop -batch"
 version_switch = "-v"
 version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
+version_ok = "8.5pl3"
+version_ok = "8.5pl2"
 version_ok = "8.5pl1"
 version_ok = "8.5"
 command = "%e -R %l/coq-tactic Why3 -R %l/coq Why3 -l %f"
@@ -550,6 +569,7 @@ version_switch = "version"
 version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
 version_ok = "2016-1"
 version_bad = "2016"
+version_bad = "2015"
 command = "%e why3 -b %f"
 driver = "drivers/isabelle2016-1.drv"
 in_place = true
@@ -562,6 +582,7 @@ version_switch = "version"
 version_regexp = "Isabelle\\([0-9]+\\(-[0-9]+\\)?\\)"
 version_ok = "2016"
 version_bad = "2016-1"
+version_bad = "2015"
 command = "%e why3 -b %f"
 driver = "drivers/isabelle2016.drv"
 in_place = true

src/coq-tactic/why3tac.ml4

@@ -58,12 +58,24 @@ let is_global c t =
   | VarRef id, Var id' -> id = id'
   | _ -> false
 
+let push_named = Environ.push_named
+
+let betadeltaiota = Closure.betadeltaiota
+
+module RedFlags = Closure.RedFlags
+
 ELSE
 
 open Universes
 open Globnames
 open Vars
+
+IFDEF COQ85 THEN
 open Errors
+ELSE
+open CErrors
+open Stdarg
+END
 
 let declare_summary name freeze unfreeze init =
   Summary.declare_summary name
@@ -112,6 +124,34 @@ let find_reference t1 t2 =
 
 let is_global c t = is_global (Lazy.force c) t
 
+IFDEF COQ85 THEN
+
+let push_named = Environ.push_named
+let betadeltaiota = Closure.betadeltaiota
+
+module RedFlags = Closure.RedFlags
+
+ELSE
+
+let push_named (id, c, t) env =
+  Environ.push_named
+    (match c with
+     | None -> Context.Named.Declaration.LocalAssum (id, t)
+     | Some b -> Context.Named.Declaration.LocalDef (id, b, t))
+    env
+
+let pf_hyps gl =
+  List.map (function
+    | Context.Named.Declaration.LocalAssum (id, t) -> (id, None, t)
+    | Context.Named.Declaration.LocalDef (id, b, t) -> (id, Some b, t))
+    (pf_hyps gl)
+
+let betadeltaiota = CClosure.all
+
+module RedFlags = CClosure.RedFlags
+
+END
+
 DECLARE PLUGIN "why3tac"
 
 END
@@ -260,7 +300,7 @@ let coq_rename_vars env vars =
 let coq_rename_var env na t =
   let avoid = ids_of_named_context (Environ.named_context env) in
   let id = next_name_away na avoid in
-  id, Environ.push_named (id, None, t) env
+  id, push_named (id, None, t) env
 
 let preid_of_id id = Ident.id_fresh (string_of_id id)
 
@@ -524,8 +564,8 @@ let rec tr_arith_constant dep t = match kind_of_term t with
 
 let rec tr_type dep tvm env evd t =
   let t = Reductionops.clos_norm_flags
-      (Closure.RedFlags.red_add_transparent
-	 Closure.betadeltaiota (get_transp_state env))
+      (RedFlags.red_add_transparent
+	 betadeltaiota (get_transp_state env))
       env evd t in
   if is_global coq_Z t then
     Ty.ty_int
@@ -1356,7 +1396,9 @@ let why3tac ?(timelimit=timelimit) s gl =
   | StepLimitExceeded -> error "Step Limit Exceeded"
   | HighFailure -> error ("Prover failure\n" ^ res.pr_output ^ "\n")
 
-IFDEF COQ85 THEN
+IFDEF COQ84 THEN
+
+ELSE
 
 let why3tac ?timelimit s = Proofview.V82.tactic (why3tac ?timelimit s)
 

src/transform/compute.ml

@@ -41,7 +41,9 @@ let collect_rules p env km prs t =
   let acc = Task.task_fold
     (fun acc td -> match td.Theory.td_node with
       | Theory.Decl { d_node = Dprop((Plemma|Paxiom), pr, t) }
-        when Decl.Spr.mem pr prs || Ident.Slab.mem rule_label t.t_label ->
+        when Decl.Spr.mem pr prs ||
+           Ident.Slab.mem rule_label pr.pr_name.Ident.id_label ||
+             Ident.Slab.mem rule_label t.t_label ->
           (pr,t) :: acc
       | _ -> acc)
     [] t

theories/floating_point.why

@@ -490,7 +490,7 @@ theory GenFloatSpecFull
     (is_NaN x -> is_NaN r)
     /\ (is_infinite x -> is_infinite r)
     /\ (is_finite x -> is_finite r /\ value r = - value x)
-    /\ (not is_NaN x -> diff_sign r x)
+    /\ (not is_NaN r -> diff_sign r x)
     /\ exact r = - exact x
     /\ model r = - model x