Commit b24a340f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'new_ide'

parents a33dbf15 96f69b5e
.gitattributes export-ignore
.gitignore export-ignore
.keepme export-ignore
/.gitlab-ci.yml export-ignore
/.mailmap export-ignore
......
:x: marks a potential source of incompatibility
Version 0.88.3, January 11, 2018
--------------------------------
Provers
* support for Alt-Ergo 2.0.0 (released Nov 14, 2017)
* support for Coq 8.7.1 (released Dec 16, 2017)
* support for Z3 4.6.0 (released Dec 18, 2017)
Standard library
* fix compatibility of theory int.Exponentiation with instances
where multiplication is not commutative.
fix corresponding realizations in Coq and Isabelle/HOL :x:
* fixed soundness of theory `int.Exponentiation` when multiplication is not
commutative :x:
Bug fixes
* Fix issue #50:
share/Makefile.config is missing when enable_relocation=yes
Miscellaneous
* fixed support for `--enable_relocation=yes` (issue #50)
* fixed support for Windows (issue #70)
Version 0.88.2, December 7, 2017
--------------------------------
Bug fixes
Miscellaneous
* `why3 session html`: improved compliance of generated files
* `why3 doc`: fixed missing anchors for operator definitions
* improved build process when `coqtop.byte` is missing
......
This diff is collapsed.
......@@ -103,7 +103,7 @@ invalid_goals () {
execute () {
pgm="bin/why3execute$suffix"
printf "$1 $2... "
printf " $1 $2... "
if $pgm $1 $2 > /dev/null; then
echo "ok"
else
......@@ -119,7 +119,7 @@ extract_and_run () {
shift
prg=$1
shift
printf "$dir... "
printf " $dir... "
rm -f $dir/$prg
printf "clean... "
if BENCH=yes make -C $dir clean > /dev/null; then
......@@ -166,7 +166,7 @@ extract_and_run () {
list_stuff () {
pgm="bin/why3$suffix"
printf '%s ' "$1"
printf ' %s ' "$1"
if $pgm $1 > /dev/null; then
echo "ok"
else
......@@ -272,3 +272,7 @@ list_stuff --list-formats
list_stuff --list-metas
list_stuff --list-debug-flags
echo ""
echo "=== Checking realizations ==="
echo "temporarily disabled"
#exec bench/check_realizations.sh
#!/bin/bash
# temporary directory where we generate realizations
TMPREAL=$(mktemp -d /tmp/why3realizations-XXXXXXX)
mkdir -p $TMPREAL/lib
res=0
echo "Testing Isabelle realizations"
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
LANG=C diff lib/isabelle $TMPREAL/lib/isabelle/realizations.* > $TMPREAL/diff-isabelle
if test -s "$TMPREAL/diff-isabelle"; then
echo "Isabelle realizations FAILED, please regenerate and prove them"
cat $TMPREAL/diff-isabelle
res=1
else
echo "Isabelle realizations OK"
fi
echo "Testing Coq realizations"
# First copy current realizations in a tmp directory
cp -r lib/coq $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
LANG=C diff -r -q -x '*.bak' -x '*~' -x '*.aux' lib/coq $TMPREAL/lib/coq > $TMPREAL/diff-coq
if test -s "$TMPREAL/diff-coq"; then
echo "Coq realizations FAILED, please regenerate and prove them"
sed -e "s,$TMPREAL/lib/coq,new," $TMPREAL/diff-coq
res=1
else
echo "Coq realizations OK"
fi
rm -r $TMPREAL
exit $res
####################################################################
# #
# The Why3 Verification Platform / The Why3 Development Team #
# Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University #
# Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University #
# #
# This software is distributed under the terms of the GNU Lesser #
# General Public License version 2.1, with the special exception #
......
......@@ -5,7 +5,7 @@
\newcommand{\vfill}{}
\newcommand{\hrulefill}{}
\newcommand{\null}{}
\newcommand{\path}[1]{\texttt{#1}}
\def\path{\begingroup\urlstyle{tt}\Url}
\renewcommand{\framebox}[1]{#1}
\makeatletter
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, December 2017
Version \whyversion{}, January 2018
%BEGIN LATEX
\end{LARGE}
%END LATEX
......
......@@ -219,5 +219,9 @@ theory real.Trigonometry
syntax function tan "<app><const name=\"Transcendental.tan\"/>%1</app>"
end
theory bv.BV_Gen
syntax function to_int "<app><const name=\"Word.sint\"/>%1</app>"
end
(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "isabelle-realizations.aux"
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../12934.why" expanded="true">
<theory name="BTS12934" sum="a1c52743c237f96f62b5a441ad065efb" expanded="true">
<goal name="t" expl="" expanded="true">
<proof prover="1" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
<proof prover="0" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../13849.why" expanded="true">
<theory name="T" sum="9002cd307075906fccf3007350013be9" expanded="true">
<goal name="x" expl="" expanded="true">
<proof prover="1" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
<proof prover="0" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../13854.why">
<theory name="T" sum="b5806ff59fa2827b1dd2b7113af851bc" expanded="true">
<goal name="g" expl="" expanded="true">
<proof prover="1" edited="13854_T_g_1.v"><result status="valid" time="0.29"/></proof>
<proof prover="0" edited="13854_T_g_1.v"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="x" expl="" expanded="true">
<proof prover="1" edited="13854_T_x_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" edited="13854_T_x_1.v"><result status="valid" time="0.30"/></proof>
</goal>
</theory>
</file>
......
module Test
use import int.Int
constant c : int
axiom a : c * 0 + 15 = 2 + 3 + 6
goal g: True
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../13_compute_in.mlw">
<theory name="Test" sum="0f62b987219641c9a62fe01b2edf29de">
<goal name="g">
<transf name="compute_hyp" arg1="in" arg2="a">
<goal name="g.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
theory Test
goal g10: if true then 1=1 else 3=4
goal g11: let x=1 in x=1
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../14_simpl.mlw">
<theory name="Test" sum="22cf7419b518c45bfba8210f6a346e58">
<goal name="g10">
<transf name="step" arg1="in" arg2="g10">
<goal name="g10.0">
<transf name="step" arg1="in" arg2="g10">
<goal name="g10.0.0">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="g11" proved="true">
<transf name="step" proved="true" >
<goal name="g11.0" proved="true">
<transf name="step" proved="true" >
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
module M
use import int.Int
function (+) (x: int) (y : int) : int = x * y
goal g: 2 + 3 = Int.(+) 3 3
end
module M1
use import real.RealInfix
use import int.Int
constant x: int = 0 + 0
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M2
use import real.RealInfix
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M3
use import real.RealInfix
(*constant x: int = 0 + 0 'unbound symbol infix +' *)
goal g: True
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../71_disambiguation.mlw">
<theory name="M" proved="true" sum="bc734e8ea460fb0a12336599478f2cd1">
<goal name="g" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</theory>
<theory name="M1" proved="true" sum="03a869518d4c28a7d6c15bc9acecb5cd">
<goal name="g" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
<transf name="cut" arg1="(0 +^ 0 = 2)">
<goal name="g.0">
<transf name="cut" arg1="(1.0 + 1.3 = 2.2)">
<goal name="g.0.0">
</goal>
<goal name="g.0.1">
</goal>
</transf>
</goal>
<goal name="g.1">
</goal>
</transf>
</goal>
</theory>
<theory name="M2" sum="85517374ec06b4406222c7e84e769b16">
<goal name="g">
</goal>
</theory>
<theory name="M3" sum="85517374ec06b4406222c7e84e769b16">
<goal name="g">
</goal>
</theory>
</file>
</why3session>
......@@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../tree_max.mlw" expanded="true">
<theory name="BinTree" sum="ee452790cf53c4d1d94c22cdc8f4ad5e" expanded="true">
<goal name="ge_trans" expl="" expanded="true">
<proof prover="1" edited="tree_max_BinTree_ge_trans_1.v"><result status="valid" time="0.32"/></proof>
<proof prover="0" edited="tree_max_BinTree_ge_trans_1.v"><result status="valid" time="0.32"/></proof>
</goal>
</theory>
<theory name="TreeMax" sum="9589666354f0580b81b370398e7bdc0c" expanded="true">
......
......@@ -34,8 +34,8 @@
<prover id="29" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="30" name="Isabelle" version="2016-1" timelimit="100" steplimit="1" memlimit="1000"/>
<prover id="31" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="32" name="Coq" version="8.6.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="33" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="34" name="Coq" version="8.7.1" timelimit="5" steplimit="1" memlimit="4000"/>
<file name="../genealogy.why" expanded="true">
<theory name="Genealogy" sum="35e1439432a79e05534b2c5cf39ad9dc" expanded="true">
<goal name="Child_is_son_or_daughter" expl="" expanded="true">
......@@ -67,8 +67,8 @@
<proof prover="29"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="30" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.xml"><result status="valid" time="21.67"/></proof>
<proof prover="31"><result status="valid" time="0.00"/></proof>
<proof prover="32" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.51"/></proof>
<proof prover="33"><result status="valid" time="0.02"/></proof>
<proof prover="34" edited="genealogy_Genealogy_Child_is_son_or_daughter_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="Sibling_sym" expl="" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="4" steplimit="0" memlimit="0"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="4" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../hello_proof.why" expanded="true">
<theory name="HelloProof" sum="8ee14372c90511294fc78a9e191cf86a" expanded="true">
......@@ -13,7 +13,7 @@
<proof prover="2" timelimit="4" memlimit="0"><result status="unknown" time="0.00"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="G2.1" expl="" expanded="true">
<proof prover="1" edited="hello_proof_HelloProof_G2_1.v"><result status="unknown" time="0.29"/></proof>
<proof prover="0" edited="hello_proof_HelloProof_G2_1.v"><result status="unknown" time="0.29"/></proof>
<proof prover="2"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="G2.2" expl="" expanded="true">
......
......@@ -2,9 +2,9 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="5" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -31,11 +31,11 @@
<proof prover="11"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sqr_le_sqrt" expl="">
<proof prover="3" edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"><result status="valid" time="0.72"/></proof>
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"><result status="valid" time="0.97"/></proof>
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="CauchySchwarz" expl="">
<proof prover="3" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="0.59"/></proof>
<proof prover="0" edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="0.59"/></proof>
</goal>
</theory>
<theory name="TriangleInequality" sum="194a101f983bb8dbabab492d87078475" expanded="true">
......@@ -48,7 +48,7 @@
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="triangle" expl="">
<proof prover="3" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" memlimit="1000" edited="lagrange_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.33"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../coq.why" expanded="true">
<theory name="NonEmptyTypes" sum="6b86b8a8aa72f92129c5085f6b3f2b95" expanded="true">
<goal name="g1" expl="" expanded="true">
<proof prover="1" edited="coq_NonEmptyTypes_g1_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" edited="coq_NonEmptyTypes_g1_1.v"><result status="valid" time="0.30"/></proof>
</goal>
</theory>
</file>
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)