From 4c3793181d62c1e4c883cea7547ee04ea423fbe4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:28:06 +0200 Subject: Refresh patches --- ...Add-distclean-back-to-test-suite-Makefile.patch | 23 ---------------- ...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 30 +++++++++++++++++++++ ...ga.ml-fix-order-of-recursive-calls-to-rco.patch | 31 ---------------------- ...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 30 --------------------- debian/patches/series | 4 +-- 5 files changed, 31 insertions(+), 87 deletions(-) delete mode 100644 debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch create mode 100644 debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch delete mode 100644 debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch delete mode 100644 debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch (limited to 'debian/patches') diff --git a/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch b/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch deleted file mode 100644 index 80cd27ae..00000000 --- a/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch +++ /dev/null @@ -1,23 +0,0 @@ -From: Stephane Glondu -Date: Thu, 12 Jan 2012 16:30:10 +0100 -Subject: Add distclean back to test-suite/Makefile - ---- - test-suite/Makefile | 3 +++ - 1 files changed, 3 insertions(+), 0 deletions(-) - -diff --git a/test-suite/Makefile b/test-suite/Makefile -index cd5886f..f3013c0 100644 ---- a/test-suite/Makefile -+++ b/test-suite/Makefile -@@ -97,6 +97,9 @@ clean: - -name '*.stamp' -o -name '*.vo' -o -name '*.log' \ - \) -print0 | xargs -0 rm -f - -+distclean: clean -+ $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f -+ - ####################################################################### - # Per-subsystem targets - ####################################################################### --- diff --git a/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch new file mode 100644 index 00000000..722ab00c --- /dev/null +++ b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch @@ -0,0 +1,30 @@ +From: Stephane Glondu +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 file changed, 2 insertions(+) + +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/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch b/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch deleted file mode 100644 index 3307023d..00000000 --- a/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch +++ /dev/null @@ -1,31 +0,0 @@ -From: Stephane Glondu -Date: Sat, 14 Jan 2012 01:24:30 +0100 -Subject: coq_micromega.ml: fix order of recursive calls to rconstant - -Some tests were failing on architectures without native code because -the evaluation order of arguments in a function call is not the same -on bytecode, leading to different behaviours for the psatzl tactic. ---- - plugins/micromega/coq_micromega.ml | 8 ++++++-- - 1 files changed, 6 insertions(+), 2 deletions(-) - -diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml -index 1ad49bb..543ab1b 100644 ---- a/plugins/micromega/coq_micromega.ml -+++ b/plugins/micromega/coq_micromega.ml -@@ -991,8 +991,12 @@ struct - else raise ParseError - | App(op,args) -> - begin -- try -- (assoc_const op rconst_assoc) (rconstant args.(0)) (rconstant args.(1)) -+ try -+ (* the evaluation order is important in the following *) -+ let f = assoc_const op rconst_assoc in -+ let a = rconstant args.(0) in -+ let b = rconstant args.(1) in -+ f a b - with - ParseError -> - match op with --- 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 deleted file mode 100644 index 6969f7dd..00000000 --- a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch +++ /dev/null @@ -1,30 +0,0 @@ -From: Stephane Glondu -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 b0df385f..53d51a16 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,3 +1 @@ -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 +0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch -- cgit v1.2.3