|
| 1 | +From d8ca76a4cc493a2fe89c53fd9e2c5fd38c9dc2fb Mon Sep 17 00:00:00 2001 |
| 2 | +From: Emilio Jesus Gallego Arias <e+git@x80.org> |
| 3 | +Date: Mon, 1 Dec 2025 00:56:30 +0100 |
| 4 | +Subject: [PATCH] [jscoq] Interrupt and timeout Rocq patch |
| 5 | + |
| 6 | +--- |
| 7 | + lib/control.ml | 36 +++++++++++++++++++++++++++++++++--- |
| 8 | + lib/dune | 4 ++++ |
| 9 | + lib/jscoq_extern.c | 4 ++++ |
| 10 | + 3 files changed, 41 insertions(+), 3 deletions(-) |
| 11 | + create mode 100644 lib/jscoq_extern.c |
| 12 | + |
| 13 | +diff --git a/lib/control.ml b/lib/control.ml |
| 14 | +index 5321357a1c..513677565f 100644 |
| 15 | +--- a/lib/control.ml |
| 16 | ++++ b/lib/control.ml |
| 17 | +@@ -18,7 +18,19 @@ let enable_thread_delay = ref false |
| 18 | + |
| 19 | + exception Timeout |
| 20 | + |
| 21 | ++(* implemented in backend/jsoo/js_stub/interrupt.js *) |
| 22 | ++external interrupt_pending : unit -> bool = "interrupt_pending" |
| 23 | ++ |
| 24 | ++let timeout_deadline : (float * (unit -> unit)) option ref = ref None |
| 25 | ++ |
| 26 | ++let jscoq_event_yield () = |
| 27 | ++ if interrupt_pending() then interrupt := true; |
| 28 | ++ match !timeout_deadline with |
| 29 | ++ | Some (time, callback) -> if Unix.gettimeofday () > time then callback (); |
| 30 | ++ | None -> () |
| 31 | ++ |
| 32 | + let check_for_interrupt () = |
| 33 | ++ jscoq_event_yield (); |
| 34 | + if !interrupt then begin interrupt := false; raise Sys.Break end; |
| 35 | + if !enable_thread_delay then begin |
| 36 | + incr steps; |
| 37 | +@@ -93,11 +105,29 @@ let windows_timeout n f x = |
| 38 | + let () = killed := true in |
| 39 | + Exninfo.iraise e |
| 40 | + |
| 41 | ++let unwind ~(protect:unit -> unit) f = |
| 42 | ++ try let y = f () in protect (); y |
| 43 | ++ with e -> protect (); raise e |
| 44 | ++ |
| 45 | ++let jscoq_timeout n f x = |
| 46 | ++ let expired = ref false in |
| 47 | ++ timeout_deadline := Some (Unix.gettimeofday () +. n, |
| 48 | ++ fun () -> expired := true; interrupt := true); |
| 49 | ++ let protect () = jscoq_event_yield (); timeout_deadline := None; |
| 50 | ++ interrupt := false in |
| 51 | ++ let res = try Ok (unwind ~protect (fun () -> f x)) |
| 52 | ++ with Sys.Break -> if !expired then Error Exninfo.null else raise Sys.Break in |
| 53 | ++ if !expired then Error Exninfo.null |
| 54 | ++ else res |
| 55 | ++ |
| 56 | + type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> ('b, Exninfo.info) result } |
| 57 | + |
| 58 | +-let timeout_fun = match Sys.os_type with |
| 59 | +-| "Unix" | "Cygwin" -> { timeout = unix_timeout } |
| 60 | +-| _ -> { timeout = windows_timeout } |
| 61 | ++(* let timeout_fun = match Sys.os_type with *) |
| 62 | ++(* | "Unix" | "Cygwin" -> { timeout = unix_timeout } *) |
| 63 | ++(* | _ -> { timeout = windows_timeout } *) |
| 64 | ++ |
| 65 | ++let _ = windows_timeout, unix_timeout |
| 66 | ++let timeout_fun = { timeout = jscoq_timeout } |
| 67 | + |
| 68 | + let timeout_fun_ref = ref timeout_fun |
| 69 | + let set_timeout f = timeout_fun_ref := f |
| 70 | +diff --git a/lib/dune b/lib/dune |
| 71 | +index e86e9decb1..b3e2d070c9 100644 |
| 72 | +--- a/lib/dune |
| 73 | ++++ b/lib/dune |
| 74 | +@@ -4,6 +4,10 @@ |
| 75 | + (public_name rocq-runtime.lib) |
| 76 | + (wrapped false) |
| 77 | + (modules_without_implementation xml_datatype) |
| 78 | ++ (foreign_stubs |
| 79 | ++ (language c) |
| 80 | ++ (names jscoq_extern) |
| 81 | ++ (flags :standard (:include %{project_root}/config/dune.c_flags))) |
| 82 | + (libraries |
| 83 | + rocq-runtime.boot rocq-runtime.clib rocq-runtime.config |
| 84 | + (select instr.ml from |
| 85 | +diff --git a/lib/jscoq_extern.c b/lib/jscoq_extern.c |
| 86 | +new file mode 100644 |
| 87 | +index 0000000000..7d0bb8c8bc |
| 88 | +--- /dev/null |
| 89 | ++++ b/lib/jscoq_extern.c |
| 90 | +@@ -0,0 +1,4 @@ |
| 91 | ++#include <caml/mlvalues.h> |
| 92 | ++ |
| 93 | ++// jsCoq Stub; actual implementation is in backend/jsoo/js_stub/interrupt.js |
| 94 | ++value interrupt_pending() { return Val_false; } |
| 95 | +-- |
| 96 | +2.43.0 |
| 97 | + |
0 commit comments