diff options
| -rw-r--r-- | debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch | 23 | ||||
| -rw-r--r-- | debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch (renamed from debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch) | 2 | ||||
| -rw-r--r-- | debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch | 31 | ||||
| -rw-r--r-- | debian/patches/series | 4 |
4 files changed, 2 insertions, 58 deletions
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 <steph@glondu.net> -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/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch index 6969f7dd..722ab00c 100644 --- a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch +++ b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch @@ -5,7 +5,7 @@ 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(-) + 1 file changed, 2 insertions(+) diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index d316e4a..d783b2a 100644 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 <steph@glondu.net> -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/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 |