diff options
| author | Guillaume Munch-Maccagnoni | 2019-11-14 19:36:06 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-12-17 17:05:06 +0100 |
| commit | 829f9385813b3d2ff45b8bec5f8741d51333c270 (patch) | |
| tree | 90c70a922234b4dc8650546dc107c11acdb034a7 /kernel | |
| parent | c1271dbc7763225dd1eadae8b5c8ba45b8ac5433 (diff) | |
Fix signal polling for OCaml 4.10
Issue #10603
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 15 |
1 files changed, 15 insertions, 0 deletions
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) { |