File ocaml-410-build.patch of Package coq

Overview Repositories Revisions Requests Users Attributes Meta

File ocaml-410-build.patch of Package coq (Revision d011401c006dfcf8d277daedb0535ef2)

Currently displaying revision d011401c006dfcf8d277daedb0535ef2 , Show latest

From 31ad892b8c9697704af70644b66ce01dd052f12e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 12 Nov 2019 10:57:23 +0100
Subject: [PATCH 1/2] Use the Alloc_small macro from the OCaml runtime rather
 than our own.

We cannot use caml_alloc_small because the macros Setup_for_gc and
Restore_after_gc are still relevant (and critical). This means defining
the CAML_INTERNALS macro, but it is a legit use and actually documented
in the OCaml manual.

This will help with forward compatibility with OCaml compilers, e.g.,
issue #10603. Unfortunately, it also means that we can no longer use #9914
to prevent memory corruption.

The old macro is still used for OCaml versions prior to 4.10, as the
upstream macro might process Ctrl+C when it is called.

(cherry picked from commit a028a97005b88a66a9d6dbaa4f0ade38859beffb)
---
 kernel/byterun/coq_interp.c | 22 ++++++++++++++++++++--
 kernel/byterun/coq_memory.c |  7 +++++--
 2 files changed, 25 insertions(+), 4 deletions(-)

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index e3283931898..3efc55c6b44 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -16,17 +16,35 @@
 #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
+#undef Alloc_small
+#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
+
 #ifdef ARCH_SIXTYFOUR
 #include "coq_uint63_native.h"
 #else
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index a1c49bee95b..76a24f6f2b8 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -9,10 +9,13 @@
 /***********************************************************************/
 
 #include <stdio.h>
-#include <string.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"

From fb48d0823fbb6507299ec53bc324fa3550e6d327 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 9 Mar 2020 15:15:44 +0100
Subject: [PATCH 2/2] Do not rely on the implicit declaration of
 caml_minor_collection.

This commit also prefixes young_ptr and young_limit along the way, so as
to not rely on OCaml's compatibility layer. This is a gratuitous change,
since this code is only meant to be compiled with OCaml < 4.10 anyway.

(cherry picked from commit 4666a8b9596f8cb87b63c345f6e57348f0bfda6d)
---
 kernel/byterun/coq_interp.c | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 3efc55c6b44..776a7c33430 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -30,18 +30,20 @@
 #include "coq_float64.h"
 
 #if OCAML_VERSION < 41000
+extern void caml_minor_collection(void);
+
 #undef Alloc_small
 #define Alloc_small(result, wosize, tag) do{                            \
-  young_ptr -= Bhsize_wosize (wosize);                                  \
-  if (young_ptr < young_limit){                                         \
-    young_ptr += Bhsize_wosize (wosize);                                \
+  caml_young_ptr -= Bhsize_wosize(wosize);                              \
+  if (caml_young_ptr < caml_young_limit) {                              \
+    caml_young_ptr += Bhsize_wosize(wosize);                            \
     Setup_for_gc;                                                       \
-    minor_collection ();                                                \
+    caml_minor_collection();                                            \
     Restore_after_gc;                                                   \
-    young_ptr -= Bhsize_wosize (wosize);                                \
+    caml_young_ptr -= Bhsize_wosize(wosize);                            \
   }                                                                     \
-  Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black);        \
-  (result) = Val_hp (young_ptr);                                        \
+  Hd_hp(caml_young_ptr) = Make_header((wosize), (tag), Caml_black);     \
+  (result) = Val_hp(caml_young_ptr);                                    \
   }while(0)
 #endif

Places

File ocaml-410-build.patch of Package coq (Revision d011401c006dfcf8d277daedb0535ef2)

Places