Skip to content
Browse files

configure: always define ARCH_INT64_TYPE in config/m.h because Coq

  and maybe others rely on it
byterun/config.h: select "long long" in preference to "long" for "int64",
  just because this is how it was done in earlier versions.
  (Minimizing suprises.)


git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14635 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
  • Loading branch information...
1 parent e3aaa68 commit 86bd9990f46272873db0d5f897201324279a355c @xavierleroy xavierleroy committed Apr 18, 2014
Showing with 17 additions and 4 deletions.
  1. +4 −4 byterun/config.h
  2. +13 −0 configure
View
8 byterun/config.h
@@ -47,14 +47,14 @@ typedef unsigned short uint32;
#if defined(ARCH_INT64_TYPE)
typedef ARCH_INT64_TYPE int64;
typedef ARCH_UINT64_TYPE uint64;
-#elif SIZEOF_LONG == 8
-typedef long int64;
-typedef unsigned long uint64;
-#define ARCH_INT64_PRINTF_FORMAT "l"
#elif SIZEOF_LONGLONG == 8
typedef long long int64;
typedef unsigned long long uint64;
#define ARCH_INT64_PRINTF_FORMAT "ll"
+#elif SIZEOF_LONG == 8
+typedef long int64;
+typedef unsigned long uint64;
+#define ARCH_INT64_PRINTF_FORMAT "l"
#else
#error "No 64-bit integer type available"
#endif
View
13 configure
@@ -529,6 +529,19 @@ echo "#define SIZEOF_PTR $3" >> m.h
echo "#define SIZEOF_SHORT $4" >> m.h
echo "#define SIZEOF_LONGLONG $5" >> m.h
+# Temporary fix: some OCaml programs, e.g. Coq, assume that
+# ARCH_INT64_TYPE is defined in config/m.h. Put a definition
+# there, even if it duplicates the logic present in config.h
+if test $5 = 8; then
+ echo '#define ARCH_INT64_TYPE long long' >> m.h
+ echo '#define ARCH_UINT64_TYPE unsigned long long' >> m.h
+ echo '#define ARCH_INT64_PRINTF_FORMAT "ll"' >> m.h
+else
+ echo '#define ARCH_INT64_TYPE long' >> m.h
+ echo '#define ARCH_UINT64_TYPE unsigned long' >> m.h
+ echo '#define ARCH_INT64_PRINTF_FORMAT "l"' >> m.h
+fi
+
# Determine endianness
sh ./runtest endian.c

0 comments on commit 86bd999

Please sign in to comment.
Something went wrong with that request. Please try again.