summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-15 12:36:33 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-15 12:36:33 +0100
commit5eb084011ecf23993159a2e1e057ecdb7d7aa06f (patch)
tree3665afe26c740400d8dd82d05be357552474c57a
parent899e0b980396967970b15d062985dca7e29c59d3 (diff)
Disable a test that uses too much memory
-rw-r--r--debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch30
-rw-r--r--debian/patches/series1
2 files changed, 31 insertions, 0 deletions
diff --git a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch
new file mode 100644
index 00000000..6969f7dd
--- /dev/null
+++ b/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch
@@ -0,0 +1,30 @@
+From: Stephane Glondu <steph@glondu.net>
+Date: Sun, 15 Jan 2012 12:34:19 +0100
+Subject: test-suite/success/Nsatz.v: comment out Ceva
+
+This lemma uses too much memory for many buildds...
+---
+ test-suite/success/Nsatz.v | 2 ++
+ 1 files changed, 2 insertions(+), 0 deletions(-)
+
+diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
+index d316e4a..d783b2a 100644
+--- a/test-suite/success/Nsatz.v
++++ b/test-suite/success/Nsatz.v
+@@ -461,6 +461,7 @@ idtac "chords".
+ (*Finished transaction in 4. secs (3.959398u,0.s)*)
+ Qed.
+
++(*
+ Lemma Ceva: forall A B C D E F M:point,
+ collinear M A D -> collinear M B E -> collinear M C F ->
+ collinear B C D -> collinear E A C -> collinear F A B ->
+@@ -472,6 +473,7 @@ idtac "Ceva".
+ Time nsatz.
+ (*Finished transaction in 105. secs (104.121171u,0.474928s)*)
+ Qed.
++*)
+
+ Lemma bissectrices: forall A B C M:point,
+ equaltangente C A M M A B ->
+--
diff --git a/debian/patches/series b/debian/patches/series
index 41965593..b0df385f 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,2 +1,3 @@
0001-Add-distclean-back-to-test-suite-Makefile.patch
0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch
+0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch