Merge PR #11102: Use the Alloc_small macro from the OCaml runtime rather than our own.

Ack-by: aaronpuchert
Ack-by: gadmm
Reviewed-by: maximedenes
Ack-by: ppedrot
Reviewed-by: proux01

3 files changed, 26 insertions, 62 deletions

diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
deleted file mode 100644
index 38eda4d11f..0000000000
--- a/kernel/byterun/coq_gc.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/***********************************************************************/
-/*                                                                     */
-/*                           Coq Compiler                              */
-/*                                                                     */
-/*        Benjamin Gregoire, projets Logical and Cristal               */
-/*                        INRIA Rocquencourt                           */
-/*                                                                     */
-/*                                                                     */
-/***********************************************************************/
-
-#ifndef _COQ_CAML_GC_
-#define _COQ_CAML_GC_
-#include <caml/mlvalues.h>
-#include <caml/alloc.h>
-#include <caml/memory.h>
-
-typedef void (*scanning_action) (value, value *);
-
-
-CAMLextern char *young_ptr;
-CAMLextern char *young_limit;
-CAMLextern void (*scan_roots_hook) (scanning_action);
-CAMLextern void minor_collection (void);
-
-#define Caml_white (0 << 8)
-#define Caml_black (3 << 8)
-
-#ifdef HAS_OCP_MEMPROF
-
-/*  This code is necessary to make the OCamlPro memory profiling branch of
-    OCaml compile. */
-
-#define Make_header(wosize, tag, color)                                 \
-  caml_make_header(wosize, tag, color)
-
-#else
-
-#define Make_header(wosize, tag, color)                                 \
-  (((header_t) (((header_t) (wosize) << 10)                             \
-                + (color)                                               \
-                + (tag_t) (tag)))                                       \
-   )
-#endif
-
-#define Alloc_small(result, wosize, tag) do{                            \
-  young_ptr -= Bhsize_wosize (wosize);                                  \
-  if (young_ptr < young_limit){                                         \
-    young_ptr += Bhsize_wosize (wosize);                                \
-    Setup_for_gc;                                                       \
-    minor_collection ();                                                \
-    Restore_after_gc;                                                   \
-    young_ptr -= Bhsize_wosize (wosize);                                \
-  }                                                                     \
-  Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black);        \
-  (result) = Val_hp (young_ptr);                                        \
-  }while(0)
-
-
-#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 606cce0127..7588c1ce07 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -16,17 +16,37 @@
 #include <stdio.h>
 #include <signal.h>
 #include <stdint.h>
+#include <math.h>
+
+#define CAML_INTERNALS
 #include <caml/memory.h>
 #include <caml/signals.h>
 #include <caml/version.h>
-#include <math.h>
-#include "coq_gc.h"
+
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 #include "coq_memory.h"
 #include "coq_values.h"
 #include "coq_float64.h"
 
+#if OCAML_VERSION < 41000
+extern void caml_minor_collection(void);
+
+#undef Alloc_small
+#define Alloc_small(result, wosize, tag) do{                            \
+  caml_young_ptr -= Bhsize_wosize(wosize);                              \
+  if (caml_young_ptr < caml_young_limit) {                              \
+    caml_young_ptr += Bhsize_wosize(wosize);                            \
+    Setup_for_gc;                                                       \
+    caml_minor_collection();                                            \
+    Restore_after_gc;                                                   \
+    caml_young_ptr -= Bhsize_wosize(wosize);                            \
+  }                                                                     \
+  Hd_hp(caml_young_ptr) = Make_header((wosize), (tag), Caml_black);     \
+  (result) = Val_hp(caml_young_ptr);                                    \
+  }while(0)
+#endif
+
 #ifdef ARCH_SIXTYFOUR
 #include "coq_uint63_native.h"
 #else
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 91d6773b1f..6233675c66 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -10,9 +10,12 @@
 
 #include <stdio.h>
 #include <string.h>
+
+#define CAML_INTERNALS
 #include <caml/alloc.h>
 #include <caml/address_class.h>
-#include "coq_gc.h"
+#include <caml/roots.h>
+
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 #include "coq_memory.h"