[Pkg-ocaml-maint-commits] [why] 01/02: package test with coq

[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 c3c3b9068dbe83ee8283bdda93e8a51629842998
Author: Ralf Treinen <treinen at debian.org>
Date:   Thu Feb 13 12:25:16 2014 +0100

    package test with coq
---
 debian/changelog     |  5 ++++-
 debian/tests/control |  4 ++++
 debian/tests/why+coq | 18 ++++++++++++++++++
 3 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/debian/changelog b/debian/changelog
index 7adfb7c..17acfff 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -18,7 +18,10 @@ why (2.33-1) unstable; urgency=low
   * New patch frama-c-versions: update accepted version of frama-c
   * Add myself to uploaders.
   * Standards-Version 3.9.5 (no change)
-  * Add DEP8-style package tests for why with alt-ergo, and why with cvc3.
+  * Add DEP8-style package tests 
+    - why with alt-ergo
+    - why with cvc3
+    - why with coq (thanks to Pierre Letouzey for his help!)
   * Bump build-dependency on frama-c-base to the latest version.
 
  -- Ralf Treinen <treinen at debian.org>  Tue, 04 Feb 2014 12:33:02 +0100
diff --git a/debian/tests/control b/debian/tests/control
index f09e8f9..88f892c 100644
--- a/debian/tests/control
+++ b/debian/tests/control
@@ -5,3 +5,7 @@ Restrictions: allow-stderr
 Tests: why+cvc3
 Depends: @, cvc3
 Restrictions: allow-stderr
+
+Tests: why+coq
+Depends: @, coq
+Restrictions: allow-stderr
diff --git a/debian/tests/why+coq b/debian/tests/why+coq
new file mode 100755
index 0000000..7cdbffd
--- /dev/null
+++ b/debian/tests/why+coq
@@ -0,0 +1,18 @@
+#!/bin/sh
+
+set -e
+
+indir=debian/tests/why
+outdir=${TMPDIR-/tmp}
+
+for infile in $indir/minimum.why
+do
+    base=$(basename $infile)
+    echo "Testing why + coq on $base" >&2
+    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
\ No newline at end of file

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