From 59dd69976bfcc6688d4183dfe032aa02e972df00 Mon Sep 17 00:00:00 2001
From: Pierrot <pierre.villemot@ocamlpro.com>
Date: Fri, 9 Aug 2024 09:52:39 +0200
Subject: [PATCH] Ignore :reproducible-resource-limit on non-Unix plateform
 (#1200)

Our implementation of this option relies on Unix signals, which are not
available on Windows for instance.

We ignore this option on Windows and emit a warning message. Notice that
we already ignore the cli option `--timelimit` in `parse_commands`.
---
 src/bin/common/solving_loop.ml | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 8c14a00f5..2f0a5d038 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -574,16 +574,20 @@ let main () =
       st
     | ":reproducible-resource-limit", Symbol { name = Simple level; _ } ->
       begin
-        match int_of_string_opt level with
-        | Some i when i > 0 ->
-          Options.set_timelimit_per_goal true;
-          Options.set_timelimit (float_of_int i /. 1000.)
-        | Some 0 ->
-          Options.set_timelimit_per_goal false;
-          Options.set_timelimit 0.
-        | None | Some _ ->
-          print_wrn_opt ~name:":reproducible-resource-limit" st_loc
-            "nonnegative integer" value
+        if Sys.unix then
+          match int_of_string_opt level with
+          | Some i when i > 0 ->
+            Options.set_timelimit_per_goal true;
+            Options.set_timelimit (float_of_int i /. 1000.)
+          | Some 0 ->
+            Options.set_timelimit_per_goal false;
+            Options.set_timelimit 0.
+          | None | Some _ ->
+            print_wrn_opt ~name:":reproducible-resource-limit" st_loc
+              "nonnegative integer" value
+        else
+          warning "%a :reproducible-resource-limit is only supported on Unix"
+            Loc.report st_loc
       end;
       st
     | ":sat-solver", Symbol { name = Simple solver; _ } -> (