[Pkg-ocaml-maint-commits] [why] 17/21: drop tests of why binary

[Ralf Treinen]

This is an automated email from the git hooks/post-receive script.

treinen pushed a commit to branch master
in repository why.

commit 420f2d7e18dfe4d595f4a8fd4e30aebbd30d0ea0
Author: Ralf Treinen <treinen at free.fr>
Date:   Sat Oct 1 14:11:56 2016 +0200

    drop tests of why binary
---
 debian/changelog             |  6 ++++--
 debian/tests/control         |  9 ---------
 debian/tests/why+alt-ergo    | 18 ------------------
 debian/tests/why+coq         | 19 -------------------
 debian/tests/why+cvc3        | 17 -----------------
 debian/tests/why/gauss.why   | 18 ------------------
 debian/tests/why/minimum.why |  4 ----
 debian/tests/why/racine.why  | 20 --------------------
 8 files changed, 4 insertions(+), 107 deletions(-)

diff --git a/debian/changelog b/debian/changelog
index 6db23a7..e261c26 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -21,9 +21,11 @@ why (2.36-1) UNRELEASED; urgency=medium
     - remove d/why.manpages
   * remove d/why.links as upstream does not ship the why manpage any more.
   * remove d/README.docs which is obsolete.
-  * d/control: drop redundant XS-Testsuite
+  * d/tests:
+    - remove redundant XS-Testsuite field from d/control
+    - remove tests why+{alt-ergo,coq,cvc3} as the binary why is dropped 
 
- -- Ralf Treinen <treinen at debian.org>  Sat, 01 Oct 2016 14:07:38 +0200
+ -- Ralf Treinen <treinen at debian.org>  Sat, 01 Oct 2016 14:11:19 +0200
 
 why (2.34-4) unstable; urgency=medium
 
diff --git a/debian/tests/control b/debian/tests/control
index 7205044..38c11fd 100644
--- a/debian/tests/control
+++ b/debian/tests/control
@@ -1,11 +1,2 @@
-Tests: why+alt-ergo
-Depends: why, alt-ergo
-
-Tests: why+cvc3
-Depends: why, cvc3
-
-Tests: why+coq
-Depends: why, libwhy-coq, coq
-
 Tests: frama-c+jessie+alt-ergo
 Depends: why, frama-c-base, alt-ergo
diff --git a/debian/tests/why+alt-ergo b/debian/tests/why+alt-ergo
deleted file mode 100755
index 7acf8d8..0000000
--- a/debian/tests/why+alt-ergo
+++ /dev/null
@@ -1,18 +0,0 @@
-#!/bin/sh
-
-set -e
-
-this=why+alt-ergo
-indir=debian/tests/why
-outdir=${ADT_ARTIFACTS}/${this}
-mkdir -p ${outdir}
-
-# alt-ergo cannot prove the VC of racine :-(
-for infile in $indir/minimum.why $indir/gauss.why
-do
-    base=$(basename $infile)
-    whyoutfile=$outdir/${base%.why}_why.why
-    altoutfile=$outdir/${base%.why}.ae
-    why --alt-ergo --output $whyoutfile $infile
-    alt-ergo $whyoutfile | tee $altoutfile | grep -q "Valid"
-done
diff --git a/debian/tests/why+coq b/debian/tests/why+coq
deleted file mode 100755
index 883c8a7..0000000
--- a/debian/tests/why+coq
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/bin/sh
-
-set -e
-
-this=why+coq
-indir=debian/tests/why
-outdir=${ADT_ARTIFACTS}/${this}
-mkdir -p ${outdir}
-
-for infile in $indir/minimum.why
-do
-    base=$(basename $infile)
-    whyoutfile=$outdir/${base%.why}
-    coqinfile=${whyoutfile}_proof.v
-    why --coq --no-coq-use-dp --output $whyoutfile $infile
-    sed -e 's/(\* FILL PROOF HERE \*)/intros; subst; auto using min_ax./' \
-	< ${whyoutfile}_why.v > ${coqinfile}
-    coqc ${coqinfile}
-done
diff --git a/debian/tests/why+cvc3 b/debian/tests/why+cvc3
deleted file mode 100755
index 2badcf7..0000000
--- a/debian/tests/why+cvc3
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/bin/sh
-
-set -e
-
-this=why+cvc3
-indir=debian/tests/why
-outdir=${ADT_ARTIFACTS}/${this}
-mkdir -p ${outdir}
-
-for infile in $indir/*.why
-do
-    base=$(basename $infile)
-    whyoutfile=$outdir/${base%.why}_why.cvc
-    cvcoutfile=$outdir/${base%.why}.cvcout
-    why --cvcl --output $whyoutfile $infile
-    cvc3 $whyoutfile | tee $cvcoutfile | grep -q "Valid" 
-done
diff --git a/debian/tests/why/gauss.why b/debian/tests/why/gauss.why
deleted file mode 100644
index d6c1517..0000000
--- a/debian/tests/why/gauss.why
+++ /dev/null
@@ -1,18 +0,0 @@
-let gauss (y: int) =
-
-{y > 0}
-     let x = ref 0 in
-     let z = ref 0 in
-     
-     while ( !z < y) do
-
-       {invariant z <= y and 2*x = z*(z+1)}
-
-       z := !z + 1;
-       x := !x + !z
-
-     done;
-
-     !x
-
-{2*result = y*(y+1)}
diff --git a/debian/tests/why/minimum.why b/debian/tests/why/minimum.why
deleted file mode 100644
index 602e478..0000000
--- a/debian/tests/why/minimum.why
+++ /dev/null
@@ -1,4 +0,0 @@
-logic min: int, int -> int
-axiom min_ax: forall x,y:int. min(x,y) <= x
-parameter r: int ref
-let f (n:int) = r := min !r n { r <= r@ }
diff --git a/debian/tests/why/racine.why b/debian/tests/why/racine.why
deleted file mode 100644
index 1d5f525..0000000
--- a/debian/tests/why/racine.why
+++ /dev/null
@@ -1,20 +0,0 @@
-let racine (x: int) =
-{x >= 0}
-
-     let y1 = ref 0 in
-     let y2 = ref 1 in
-     let y3 = ref 1 in
-     
-     while ( !y3 <= x) do
-
-       {invariant y2 = 2*y1+1 and y3 = (y1+1)*(y1+1) and y1*y1 <= x}
-
-       y1 := !y1 + 1;
-       y2 := !y2 + 2;
-       y3 := !y3 + !y2
-
-     done;
-
-     !y1
-
-{result*result<=x and (result+1)*(result+1)>x}     

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git