Merge PR #11123: Fix signal polling for OCaml 4.10

Ack-by: ejgallego

2 files changed, 23 insertions, 3 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 754b977f89..606cce0127 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,27 @@ 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; }
+        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;
 
       Instruct(ENSURESTACKCAPACITY) {
@@ -1743,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);
     }
   }