From 829f9385813b3d2ff45b8bec5f8741d51333c270 Mon Sep 17 00:00:00 2001
From: Guillaume Munch-Maccagnoni
Date: Thu, 14 Nov 2019 19:36:06 +0100
Subject: Fix signal polling for OCaml 4.10

Issue #10603
---
 kernel/byterun/coq_interp.c | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 754b977f89..9a1149bd86 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -17,6 +17,8 @@
 #include <signal.h>
 #include <stdint.h>
 #include <caml/memory.h>
+#include <caml/signals.h>
+#include <caml/version.h>
 #include <math.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
@@ -203,11 +205,13 @@ if (sp - num_args < coq_stack_threshold) {                                     \
     *sp = swap_accu_sp_tmp__;                   \
   }while(0)
 
+#if OCAML_VERSION < 41000
 /* For signal handling, we hijack some code from the caml runtime */
 
 extern intnat volatile caml_signals_are_pending;
 extern intnat volatile caml_pending_signals[];
 extern void caml_process_pending_signals(void);
+#endif
 
 /* The interpreter itself */
 
@@ -506,11 +510,22 @@ value coq_interprete
       print_instr("check_stack");
       CHECK_STACK(0);
       /* We also check for signals */
+#if OCAML_VERSION >= 41000
+      {
+        value res = caml_process_pending_actions_exn();
+        if (Is_exception_result(res)) {
+          /* If there is an asynchronous exception, we reset the vm */
+          coq_sp = coq_stack_high;
+          caml_raise(Extract_exception(res));
+        }
+      }
+#else
       if (caml_signals_are_pending) {
         /* If there's a Ctrl-C, we reset the vm */
         if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
         caml_process_pending_signals();
       }
+#endif
       Next;
 
       Instruct(ENSURESTACKCAPACITY) {
-- 
cgit v1.2.3


From 2bac2cf5ec97a0b0f9a509368077984d6e399038 Mon Sep 17 00:00:00 2001
From: Guillaume Munch-Maccagnoni
Date: Sat, 16 Nov 2019 22:48:49 +0100
Subject: Fatal error in VM if SIGINT was seen but no exception occured.

---
 kernel/byterun/coq_interp.c | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 9a1149bd86..dd3ff0302e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -522,8 +522,13 @@ value coq_interprete
 #else
       if (caml_signals_are_pending) {
         /* If there's a Ctrl-C, we reset the vm */
-        if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
+        intnat sigint = caml_pending_signals[SIGINT];
+        if (sigint) { coq_sp = coq_stack_high; }
         caml_process_pending_signals();
+        if (sigint) {
+          caml_failwith("Coq VM: Fatal error: SIGINT signal detected "
+                        "but no exception was raised");
+        }
       }
 #endif
       Next;
-- 
cgit v1.2.3


From 93f45c7349e64b3acfddbb2c4d2767980a3a5b44 Mon Sep 17 00:00:00 2001
From: Guillaume Munch-Maccagnoni
Date: Sat, 16 Nov 2019 22:50:35 +0100
Subject: failwith -> caml_failwith

---
 kernel/byterun/coq_interp.c | 2 +-
 kernel/byterun/coq_values.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/byterun')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index dd3ff0302e..606cce0127 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1763,7 +1763,7 @@ value coq_interprete
 #ifndef THREADED_CODE
     default:
       /*fprintf(stderr, "%d\n", *pc);*/
-      failwith("Coq VM: Fatal error: bad opcode");
+      caml_failwith("Coq VM: Fatal error: bad opcode");
     }
   }
 #endif
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 3613bc07a6..bbe91da628 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -40,7 +40,7 @@ value coq_closure_arity(value clos) {
     c++;
     if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
     else {
-      if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity");
+      if (Wosize_val(clos) != 2) caml_failwith("Coq Values : coq_closure_arity");
       return Val_int(1);
     }
   }
-- 
cgit v1.2.3