Commit 190492a8 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Update configure and regtests / nightly-build so that realization are

generated again.

* Makefile.in
Realizations for isabelle are generated even if Isabelle is not installed.
The .thy file are checked only if isabelle is installed. This allows us
to treat it as with coq and be able to detect changes in realizations
with a script.
Dont erase xml generated file during clean.

* configure.in
Changed the configure to always generate a default isabelle version (set
to 2017) for generation of the realization driver (needed even when no
isablle support is given).

* examples/regtests.sh
Adding option --check-realization and --only-realization which add a test
the compares the output of the new realization compared to the one
recorded. It complains if they are different forcing the user to update the
realization files.

* lib/isabelle/*
Adding xml files corresponding to generated realization for Isabelle. This
allows for the abovementionned script to work even if Isabelle is not
installed (which is the case for most people editing theories).

* examples/nightly-bench.sh
Add the option for realization check

* misc/ci-bench
Calls the test for realization

Conflicts:
	examples/regtests.sh
parent 7fc712ae
......@@ -124,6 +124,10 @@ COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
TOTARGET = > "$@" || (RV=$$?; rm -f "$@"; exit $${RV})
# Variables added for checking realizations
GENERATED_PREFIX_COQ="lib/coq"
GENERATED_PREFIX_ISABELLE="lib/isabelle"
###############
# main target
###############
......@@ -895,11 +899,6 @@ endif
# Coq realizations
####################
ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
COQVERSIONSPECIFIC=
COQVERSIONSPECIFICTARGETS=$(addprefix lib/coq/, $(COQVERSIONSPECIFIC))
......@@ -995,6 +994,49 @@ drivers/coq-realizations.aux: Makefile
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bool.why
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bool.$$f -o $(GENERATED_PREFIX_COQ)/bool/; done
update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/real.why
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T real.$$f -o $(GENERATED_PREFIX_COQ)/real/; done
update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/number.why
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T number.$$f -o $(GENERATED_PREFIX_COQ)/number/; done
update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T set.$$f -o $(GENERATED_PREFIX_COQ)/set/; done
update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T map.$$f -o $(GENERATED_PREFIX_COQ)/map/; done
update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T list.$$f -o $(GENERATED_PREFIX_COQ)/list/; done
update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o $(GENERATED_PREFIX_COQ)/option/; done
update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/seq.why
for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T seq.$$f -o $(GENERATED_PREFIX_COQ)/seq/; done
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bv.why
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done
update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/ieee_float.why
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o $(GENERATED_PREFIX_COQ)/floating_point/; done
ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
install_no_local::
$(MKDIR_P) $(LIBDIR)/why3/coq
$(INSTALL_DATA) lib/coq/BuiltIn.vo lib/coq/HighOrd.vo $(LIBDIR)/why3/coq/
......@@ -1025,52 +1067,6 @@ ifeq (@enable_coq_fp_libs@,yes)
$(INSTALL_DATA) $(addsuffix .vo, $(COQLIBS_IEEEFLOAT)) $(LIBDIR)/why3/coq/ieee_float/
endif
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-seq update-coq-bv update-coq-ieee_float
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
update-coq-bool: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bool.why
for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bool.$$f -o lib/coq/bool/; done
update-coq-real: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/real.why
for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
update-coq-number: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/number.why
for f in $(COQLIBS_NUMBER_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
update-coq-set: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
update-coq-map: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T map.$$f -o lib/coq/map/; done
update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T list.$$f -o lib/coq/list/; done
update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o lib/coq/option/; done
update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/seq.why
for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T seq.$$f -o lib/coq/seq/; done
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bv.why
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bv.$$f -o lib/coq/bv/; done
update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/ieee_float.why
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T ieee_float.$$f -o lib/coq/ieee_float/; done
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
drivers/coq-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)echo "(* generated automatically at compilation time *)" > $@
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd
endif
COQV = $(addsuffix .v, $(COQLIBS_FILES))
......@@ -1100,12 +1096,6 @@ clean-coq:
clean:: clean-coq
else
drivers/coq-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)echo "(* generated automatically at compilation time *)" > $@
endif
all: drivers/coq-realizations.aux
......@@ -1197,7 +1187,6 @@ clean::
# Isabelle realizations
#######################
ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=ROOT why3.ML Why3_BV.thy Why3_Number.thy Why3_Real.thy Why3_Set.thy
......@@ -1268,82 +1257,87 @@ 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) $(ISABELLELIBS_BV)
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
endif
@(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
echo "Building the Why3 heap for Isabelle/HOL:"; \
isabelle build -bc Why3; \
touch $@; \
else \
echo "[Warning] Cannot pre-build the Isabelle heap because"; \
echo " the Isabelle component configuration does not contain"; \
echo " [$(ISABELLE_TARGET_DIR)]"; \
fi)
install_no_local::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
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) $(ISABELLELIBS_BV)
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
$(SHOW) "Generating Isabelle realization for int.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/int
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/int/
$(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bool.why
$(SHOW) "Generating Isabelle realization for bool.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/bool
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bool/
$(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/real.why
$(SHOW) "Generating Isabelle realization for real.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/real
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/real/
$(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/number.why
$(SHOW) "Generating Isabelle realization for number.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/number
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/number/
$(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/set.why
$(SHOW) "Generating Isabelle realization for set.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/set
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/set/
$(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/map.why
$(SHOW) "Generating Isabelle realization for map.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/map
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/map/
$(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/list.why
$(SHOW) "Generating Isabelle realization for list.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/list
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/list/
$(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/option.why
$(SHOW) "Generating Isabelle realization for option.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/option
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/option/
$(ISABELLELIBS_BV): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bv.why
$(SHOW) "Generating Isabelle realization for bv.$(notdir $(basename $@))"
$(HIDE)mkdir -p lib/isabelle/bv
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o lib/isabelle/bv/
$(HIDE)WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bv.$(notdir $(basename $@)) -o $(GENERATED_PREFIX_ISABELLE)/bv/
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS)
# $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
ifeq (@enable_isabelle_libs@,yes)
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
endif
@(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
echo "Building the Why3 heap for Isabelle/HOL:"; \
isabelle build -bc Why3; \
touch $@; \
else \
echo "[Warning] Cannot pre-build the Isabelle heap because"; \
echo " the Isabelle component configuration does not contain"; \
echo " [$(ISABELLE_TARGET_DIR)]"; \
fi)
install_no_local::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
install_no_local:: lib/isabelle/last_build
install_local:: lib/isabelle/last_build
# do not update isabelle realizations systematically
# all: update-isabelle
......@@ -1353,13 +1347,20 @@ clean::
else
drivers/isabelle-realizations.aux: Makefile
$(SHOW) 'Generate $@'
$(HIDE)echo "(* generated automatically at compilation time *)" > $@
install_no_local::
$(INSTALL_DATA) drivers/isabelle-realizations.aux $(DATADIR)/why3/drivers/
install_no_local:: lib/isabelle/last_build
install_local:: lib/isabelle/last_build
# do not update isabelle realizations systematically
# all: update-isabelle
# Removed cleaning of xml
#clean::
# rm -f lib/isabelle/*/*.xml
endif
all: drivers/isabelle-realizations.aux
......
......@@ -640,15 +640,19 @@ fi
# Isabelle
# Default version used for generation of realization in the case Isabelle is not
# detected or Why3 is compiled with disable-isabelle.
ISABELLEVERSION=2017
if test "$enable_isabelle_libs" = no; then
enable_isabelle_support=no
reason_isabelle_support=" (disabled by user)"
else
AC_CHECK_PROG(ISABELLE,isabelle,isabelle,no)
if test "$ISABELLE" = no ; then
enable_isabelle_support=no
AC_MSG_WARN(Cannot find isabelle.)
reason_isabelle_support=" (isabelle not found)"
enable_isabelle_support=no
AC_MSG_WARN(Cannot find isabelle.)
reason_isabelle_support=" (isabelle not found)"
else
AC_MSG_CHECKING(Isabelle version)
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
......
......@@ -121,7 +121,7 @@ fi
# replay proofs
examples/regtests.sh &> $OUT
examples/regtests.sh --check-realization &> $OUT
if test "$?" != "0" ; then
SUBJECT="$SUBJECT failed"
echo "Proof replay failed" >> $REPORT
......
......@@ -2,6 +2,10 @@
# regression tests for why3
REPLAYOPT=""
# Test realization too
CHECK_REALIZATION=""
# Don't test the rest of examples, only the realizations
ONLY_REALIZATION=""
while test $# != 0; do
case "$1" in
......@@ -15,6 +19,13 @@ case "$1" in
REPLAYOPT="$REPLAYOPT --prover $2"
shift
;;
"--check-realization")
CHECK_REALIZATION="true"
;;
"--only-realization")
ONLY_REALIZATION="true"
CHECK_REALIZATION="true"
;;
*)
echo "$0: Unknown option '$1'"
exit 2
......@@ -24,7 +35,9 @@ done
TMP=$PWD/why3regtests.out
TMPERR=$PWD/why3regtests.err
TMPREAL=/tmp
# Current directory is /examples
cd `dirname $0`
# too early to do that
......@@ -36,68 +49,111 @@ export total=0
export sessions=""
export shapes=""
test_generated () {
# Current directory is /why3
mkdir -p $TMPREAL/lib
echo "Testing isabelle realization"
# First copy current realization in a tmp directory
cp -r ../lib/isabelle/ $TMPREAL/lib/
# We want to use the makefile to be sure to check exhaustively the
# realizations that are built
make -C .. GENERATED_PREFIX_ISABELLE="$TMPREAL/lib/isabelle" update-isabelle > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' ../lib/isabelle $TMPREAL/lib/isabelle`
if test "$TMPDIFF" = "" ; then
printf "ISABELLE realization OK\n"
else
printf "ISABELLE REALIZATION FAILED, please regenerate and prove it\n"
printf "$TMPDIFF\n"
printf "Generated realization are in /tmp. Use --only-realization to only test realization\n"
res=1
fi
echo "Testing coq realization"
# First copy current realization 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 -C .. GENERATED_PREFIX_COQ="$TMPREAL/lib/coq" update-coq > /dev/null 2> /dev/null
TMPDIFF=`diff -r -q -x '*.bak' ../lib/coq $TMPREAL/lib/coq`
if test "$TMPDIFF" = "" ; then
printf "COQ realization OK\n"
else
printf "COQ REALIZATION FAILED, please regenerate and prove it\n"
printf "$TMPDIFF\n"
printf "Generated realization are in /tmp. Use --only-realization to only test realization\n"
res=1
fi
}
run_dir () {
for f in `ls $1/*/why3session.xml`; do
d=`dirname $f`
echo -n "Replaying $d ... "
printf "Replaying $d ... "
../bin/why3replay.opt -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP
ret=$?
if test "$ret" != "0" ; then
echo -n "FAILED (ret code=$ret):"
if test "$ret" != "0" ; then
printf "FAILED (ret code=$ret):"
out=`head -1 $TMP`
if test -z "$out" ; then
echo "standard error: (standard output empty)"
cat $TMPERR
else
cat $TMP
cat $TMP
fi
res=1
else
echo -n "OK"
cat $TMP $TMPERR
res=1
else
printf "OK"
cat $TMP $TMPERR
success=`expr $success + 1`
fi
fi
total=`expr $total + 1`
done
sessions="$sessions $1/*/why3session.xml"
shapes="$shapes $1/*/why3shapes.*"
}
echo "=== Standard Library ==="
run_dir stdlib
echo ""
echo "=== Tests ==="
# there's no session there...
# run_dir tests
run_dir tests-provers
echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
echo "=== BTS ==="
run_dir bts
echo ""
echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-L bitvectors"
echo ""
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir WP_revisited
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir avl "-L avl"
run_dir double_wp "-L double_wp"
run_dir prover "-L prover"
echo ""
echo "Summary : $success/$total"
echo "Sessions size : "`wc -cl $sessions | tail -1`
echo "Shapes size : "`wc -cl $shapes | tail -1`
if test "$ONLY_REALIZATION" = "" ; then
echo "=== Standard Library ==="
run_dir stdlib
echo ""
echo "=== Tests ==="
# there's no session there...
# run_dir tests
run_dir tests-provers
echo ""
echo "=== Check Builtin translation ==="
run_dir check-builtin
echo ""
echo "=== BTS ==="
run_dir bts
echo ""
echo "=== Logic ==="
run_dir logic
run_dir bitvectors "-L bitvectors"
echo ""
echo "=== Programs ==="
run_dir .
run_dir foveoos11-cm
run_dir WP_revisited
run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
run_dir avl "-L avl"
run_dir double_wp "-L double_wp"
run_dir prover "-L prover"
echo ""
echo "Summary : $success/$total"
echo "Sessions size : "`wc -cl $sessions | tail -1`
echo "Shapes size : "`wc -cl $shapes | tail -1`
fi
if test "$CHECK_REALIZATION" = "true" ; then
test_generated
fi
exit $res
<theory name="bool.Bool" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/></realized><lemma name="andb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.conj"/><var name="x"><type name="HOL.bool"/></var><var name="y"><type name="HOL.bool"/></var></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.True"/><var name="y"><type name="HOL.bool"/></var></pat><pat><const name="HOL.False"/><const name="HOL.False"/></pat></case></app></concls></lemma><lemma name="orb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.disj"/><var name="x"><type name="HOL.bool"/></var><var name="y"><type name="HOL.bool"/></var></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.False"/><var name="y"><type name="HOL.bool"/></var></pat><pat><const name="HOL.True"/><const name="HOL.True"/></pat></case></app></concls></lemma><lemma name="notb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.Not"/><var name="x"><type name="HOL.bool"/></var></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.False"/><const name="HOL.True"/></pat><pat><const name="HOL.True"/><const name="HOL.False"/></pat></case></app></concls></lemma><lemma name="xorb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="x"><type name="HOL.bool"/></var><var name="y"><type name="HOL.bool"/></var></app></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.False"/><var name="y"><type name="HOL.bool"/></var></pat><pat><const name="HOL.True"/><app><const name="HOL.Not"/><var name="y"><type name="HOL.bool"/></var></app></pat></case></app></concls></lemma><lemma name="implb_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="HOL.implies"/><var name="x"><type name="HOL.bool"/></var><var name="y"><type name="HOL.bool"/></var></app><case><var name="x"><type name="HOL.bool"/></var><pat><const name="HOL.False"/><const name="HOL.True"/></pat><pat><const name="HOL.True"/><var name="y"><type name="HOL.bool"/></var></pat></case></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
<theory name="bv.BVConverter_16_32" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV32"/><require name="bv.BV16"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_16_32"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV32"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_16_32"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV16"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_16_32"><prems><app><const name="ule" path="bv.BV32"><pred><type name="t" path="bv.BV32"/><type name="t" path="bv.BV32"/></pred></const><var name="x"><type name="t" path="bv.BV32"/></var><num val="65535"><type name="t" path="bv.BV32"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV16"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_16_32"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV32"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_16_64" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV64"/><require name="bv.BV16"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_16_64"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV64"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_16_64"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV16"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_16_64"><prems><app><const name="ule" path="bv.BV64"><pred><type name="t" path="bv.BV64"/><type name="t" path="bv.BV64"/></pred></const><var name="x"><type name="t" path="bv.BV64"/></var><num val="65535"><type name="t" path="bv.BV64"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV16"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_16_64"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV64"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_32_64" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV64"/><require name="bv.BV32"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_32_64"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV64"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_32_64"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV32"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_32_64"><prems><app><const name="ule" path="bv.BV64"><pred><type name="t" path="bv.BV64"/><type name="t" path="bv.BV64"/></pred></const><var name="x"><type name="t" path="bv.BV64"/></var><num val="4294967295"><type name="t" path="bv.BV64"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV32"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_32_64"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV64"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_8_16" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV16"/><require name="bv.BV8"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_8_16"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV16"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_8_16"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV8"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_8_16"><prems><app><const name="ule" path="bv.BV16"><pred><type name="t" path="bv.BV16"/><type name="t" path="bv.BV16"/></pred></const><var name="x"><type name="t" path="bv.BV16"/></var><num val="255"><type name="t" path="bv.BV16"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV16"/><type name="t" path="bv.BV8"/></fun></const><var name="x"><type name="t" path="bv.BV16"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_8_16"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app><app><const name="tqtint" path="bv.BV16"><fun><type name="t" path="bv.BV16"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV16"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_8_32" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV32"/><require name="bv.BV8"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_8_32"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV32"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_8_32"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV8"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_8_32"><prems><app><const name="ule" path="bv.BV32"><pred><type name="t" path="bv.BV32"/><type name="t" path="bv.BV32"/></pred></const><var name="x"><type name="t" path="bv.BV32"/></var><num val="255"><type name="t" path="bv.BV32"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV32"/><type name="t" path="bv.BV8"/></fun></const><var name="x"><type name="t" path="bv.BV32"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_8_32"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app><app><const name="tqtint" path="bv.BV32"><fun><type name="t" path="bv.BV32"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV32"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="bv.BVConverter_8_64" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="bool.Bool"/><require name="int.Int"/><require name="int.Abs"/><require name="int.EuclideanDivision"/><require name="bv.Pow2int"/><require name="bv.BV64"/><require name="bv.BV8"/></realized><param name="toBig" altname="toBig" path="bv.BVConverter_8_64"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV64"/></fun></param><param name="toSmall" altname="toSmall" path="bv.BVConverter_8_64"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV8"/></fun></param><lemma name="toSmall_to_uint" altname="toSmall_to_uint" path="bv.BVConverter_8_64"><prems><app><const name="ule" path="bv.BV64"><pred><type name="t" path="bv.BV64"/><type name="t" path="bv.BV64"/></pred></const><var name="x"><type name="t" path="bv.BV64"/></var><num val="255"><type name="t" path="bv.BV64"/></num></app></prems><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><app><const name="toSmall" local="true"><fun><type name="t" path="bv.BV64"/><type name="t" path="bv.BV8"/></fun></const><var name="x"><type name="t" path="bv.BV64"/></var></app></app></app></concls></lemma><lemma name="toBig_to_uint" altname="toBig_to_uint" path="bv.BVConverter_8_64"><prems/><concls><app><const name="HOL.eq"/><app><const name="tqtint" path="bv.BV8"><fun><type name="t" path="bv.BV8"/><type name="Int.int"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app><app><const name="tqtint" path="bv.BV64"><fun><type name="t" path="bv.BV64"/><type name="Int.int"/></fun></const><app><const name="toBig" local="true"><fun><type name="t" path="bv.BV8"/><type name="t" path="bv.BV64"/></fun></const><var name="x"><type name="t" path="bv.BV8"/></var></app></app></app></concls></lemma></theory>
\ No newline at end of file
This diff is collapsed.
<theory name="int.Abs" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/></realized><lemma name="abs_def"><prems/><concls><app><const name="HOL.eq"/><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Int.int"/></var></app><app><const name="HOL.If"/><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var><app><const name="Groups.uminus_class.uminus"/><var name="x"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Abs_le" altname="Abs_le" path="int.Abs"><prems/><concls><app><const name="HOL.eq"/><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Int.int"/></var></app><var name="y"><type name="Int.int"/></var></app><app><const name="HOL.conj"/><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.uminus_class.uminus"/><var name="y"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Abs_pos" altname="Abs_pos" path="int.Abs"><prems/><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="Groups.abs_class.abs"/><var name="x"><type name="Int.int"/></var></app></app></concls></lemma></theory>
\ No newline at end of file
<theory name="int.ComputerDivision" realize="true"><realized><require name="why3.BuiltIn.BuiltIn"/><require name="int.Int"/><require name="int.Abs"/></realized><param name="div" altname="div" path="int.ComputerDivision"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></param><param name="mod" altname="mod" path="int.ComputerDivision"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></param><lemma name="Div_mod" altname="Div_mod" path="int.ComputerDivision"><prems><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="y"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></app></prems><concls><app><const name="HOL.eq"/><var name="x"><type name="Int.int"/></var><app><const name="Groups.plus_class.plus"/><app><const name="Groups.times_class.times"/><var name="y"><type name="Int.int"/></var><app><const name="div" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app><app><const name="mod" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app></app></concls></lemma><lemma name="Div_bound" altname="Div_bound" path="int.ComputerDivision"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Int.int"/></num><var name="y"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="div" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app><app><const name="Orderings.ord_class.less_eq"/><app><const name="div" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><var name="x"><type name="Int.int"/></var></app></concls></lemma><lemma name="Mod_bound" altname="Mod_bound" path="int.ComputerDivision"><prems><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="y"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></app></prems><concls><app><const name="Orderings.ord_class.less"/><app><const name="Groups.uminus_class.uminus"/><app><const name="Groups.abs_class.abs"/><var name="y"><type name="Int.int"/></var></app></app><app><const name="mod" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app><app><const name="Orderings.ord_class.less"/><app><const name="mod" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><app><const name="Groups.abs_class.abs"/><var name="y"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Div_sign_pos" altname="Div_sign_pos" path="int.ComputerDivision"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Int.int"/></num><var name="y"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="div" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Div_sign_neg" altname="Div_sign_neg" path="int.ComputerDivision"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app><app><const name="Orderings.ord_class.less"/><num val="0"><type name="Int.int"/></num><var name="y"><type name="Int.int"/></var></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="div" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><num val="0"><type name="Int.int"/></num></app></concls></lemma><lemma name="Mod_sign_pos" altname="Mod_sign_pos" path="int.ComputerDivision"><prems><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><var name="x"><type name="Int.int"/></var></app><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="y"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><num val="0"><type name="Int.int"/></num><app><const name="mod" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app></app></concls></lemma><lemma name="Mod_sign_neg" altname="Mod_sign_neg" path="int.ComputerDivision"><prems><app><const name="Orderings.ord_class.less_eq"/><var name="x"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="y"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="mod" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/></var><var name="y"><type name="Int.int"/></var></app><num val="0"><type name="Int.int"/></num></app></concls></lemma><lemma name="Rounds_toward_zero" altname="Rounds_toward_zero" path="int.ComputerDivision"><prems><app><const name="HOL.Not"/><app><const name="HOL.eq"/><var name="y"><type name="Int.int"/></var><num val="0"><type name="Int.int"/></num></app></app></prems><concls><app><const name="Orderings.ord_class.less_eq"/><app><const name="Groups.abs_class.abs"/><app><const name="Groups.times_class.times"/><app><const name="div" local="true"><fun><type name="Int.int"/><type name="Int.int"/><type name="Int.int"/></fun></const><var name="x"><type name="Int.int"/>&