[coq] Fix to int types in OCaml > 4.02.0 and Fedora.

Richard W.M. Jones rjones at fedoraproject.org
Sat Aug 30 20:41:32 UTC 2014


commit 0082780887e391f7d2c587e14cced791e7c05d9e
Author: Richard W.M. Jones <rjones at redhat.com>
Date:   Sat Aug 30 21:27:37 2014 +0100

    Fix to int types in OCaml > 4.02.0 and Fedora.

 coq-8.4pl4-fix-ints.patch |   28 ++++++++++++++++++++++++++++
 coq.spec                  |    8 ++++++--
 2 files changed, 34 insertions(+), 2 deletions(-)
---
diff --git a/coq-8.4pl4-fix-ints.patch b/coq-8.4pl4-fix-ints.patch
new file mode 100644
index 0000000..bb89bbb
--- /dev/null
+++ b/coq-8.4pl4-fix-ints.patch
@@ -0,0 +1,28 @@
+--- coq-8.4pl4.old/kernel//byterun/coq_interp.c	2014-04-24 16:13:03.000000000 +0100
++++ coq-8.4pl4/kernel//byterun/coq_interp.c	2014-08-30 21:26:04.912672254 +0100
+@@ -29,6 +29,11 @@
+ #include "int64_emul.h"
+ #endif
+ 
++#define int64 int64_t
++#define uint64 uint64_t
++#define int32 int32_t
++#define uint32 uint32_t
++
+ /* spiwack: I append here a few macros for value/number manipulation */
+ #define uint32_of_value(val) (((uint32)val >> 1))
+ #define value_of_uint32(i)   ((value)(((uint32)(i) << 1) | 1))
+--- coq-8.4pl4.old/kernel//byterun/coq_fix_code.c	2014-04-24 16:13:03.000000000 +0100
++++ coq-8.4pl4/kernel//byterun/coq_fix_code.c	2014-08-30 21:28:58.174844206 +0100
+@@ -21,6 +21,11 @@
+ #include "coq_instruct.h"
+ #include "coq_fix_code.h"
+ 
++#define int64 int64_t
++#define uint64 uint64_t
++#define int32 int32_t
++#define uint32 uint32_t
++
+ #ifdef THREADED_CODE
+ char ** coq_instr_table;
+ char * coq_instr_base;
diff --git a/coq.spec b/coq.spec
index c92928c..e473609 100644
--- a/coq.spec
+++ b/coq.spec
@@ -18,7 +18,7 @@
 
 Name:           coq
 Version:        8.4pl4
-Release:        15%{?dist}
+Release:        16%{?dist}
 Summary:        Proof management system
 
 License:        LGPLv2
@@ -31,6 +31,8 @@ Source5:        coqide.appdata.xml
 
 # Fix for OCaml 4.02.
 Patch1:         coq-comment-string-literal.patch
+# Fix for OCaml > 4.02.0 and Fedora.
+Patch2:         coq-8.4pl4-fix-ints.patch
 
 BuildRequires:  ocaml
 BuildRequires:  ocaml-camlp5-devel
@@ -134,6 +136,7 @@ This package is not needed to use the Emacs interface.
 %setup -q
 
 %patch1 -p1
+%patch2 -p1
 
 %ifarch aarch64
 # These files cause a segfault on aarch64, so don't build them.
@@ -318,8 +321,9 @@ mktexlsr &> /dev/null
 %{_emacs_sitelispdir}/coq/*.el
 
 %changelog
-* Sat Aug 30 2014 Richard W.M. Jones <rjones at redhat.com> - 8.4pl4-15
+* Sat Aug 30 2014 Richard W.M. Jones <rjones at redhat.com> - 8.4pl4-16
 - Bump release and rebuild.
+- Fix to int types in OCaml > 4.02.0 and Fedora.
 
 * Sat Aug 30 2014 Richard W.M. Jones <rjones at redhat.com> - 8.4pl4-14
 - ocaml-4.02.0 final rebuild.


More information about the scm-commits mailing list