From d0e2f14a9b15bbfbc2189a6085808ca20e81d4da Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 18 Oct 2024 12:58:28 -0700
Subject: [PATCH 1/3] FStarC.OCaml: some refactoring

---
 src/fstar/FStarC.OCaml.fst | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/fstar/FStarC.OCaml.fst b/src/fstar/FStarC.OCaml.fst
index e40a621293d..a2cd0ce30b5 100644
--- a/src/fstar/FStarC.OCaml.fst
+++ b/src/fstar/FStarC.OCaml.fst
@@ -16,6 +16,7 @@
 module FStarC.OCaml
 
 open FStarC
+open FStar.List.Tot.Base
 open FStarC.Compiler
 open FStarC.Compiler.Effect
 
@@ -45,18 +46,25 @@ let exec_in_ocamlenv #a (cmd : string) (args : list string) : a =
   Util.execvp cmd (cmd :: args);
   failwith "execvp failed"
 
+let app_lib = "fstar.lib"
+let plugin_lib = "fstar.lib"
+
 (* OCaml Warning 8: this pattern-matching is not exhaustive.
 This is usually benign as we check for exhaustivenss via SMT. *)
+let wstr = "-8"
+
+let common_args =
+  "-w" :: wstr ::
+  []
 
 let exec_ocamlc args =
   exec_in_ocamlenv "ocamlfind"
-    ("c" :: "-w" :: "-8" :: "-linkpkg" :: "-package" :: "fstar.lib" :: args)
+    ("c" :: common_args @ "-linkpkg" :: "-package" :: app_lib :: args)
 
 let exec_ocamlopt args =
   exec_in_ocamlenv "ocamlfind"
-    ("opt" :: "-w" :: "-8" :: "-linkpkg" :: "-package" :: "fstar.lib" :: args)
+    ("opt" :: common_args @ "-linkpkg" :: "-package" :: app_lib :: args)
 
 let exec_ocamlopt_plugin args =
   exec_in_ocamlenv "ocamlfind"
-    ("opt" :: "-w" :: "-8" :: "-shared" :: "-package" :: "fstar.lib" ::
-    args)
+    ("opt" :: common_args @ "-shared" :: "-package" :: plugin_lib :: args)

From 0a5b8a4a230bbc2a8d02da58ddb21691f44fc950 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 18 Oct 2024 12:58:43 -0700
Subject: [PATCH 2/3] FStarC.OCaml: pass -thread

This is needed to avoid warnings.
---
 src/fstar/FStarC.OCaml.fst | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/fstar/FStarC.OCaml.fst b/src/fstar/FStarC.OCaml.fst
index a2cd0ce30b5..53c59f8d690 100644
--- a/src/fstar/FStarC.OCaml.fst
+++ b/src/fstar/FStarC.OCaml.fst
@@ -55,6 +55,7 @@ let wstr = "-8"
 
 let common_args =
   "-w" :: wstr ::
+  "-thread" ::
   []
 
 let exec_ocamlc args =

From 7b342668b084e397b2e39ab132442f071687cc6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 18 Oct 2024 13:04:16 -0700
Subject: [PATCH 3/3] snap

---
 ocaml/fstar-lib/generated/FStarC_OCaml.ml | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/ocaml/fstar-lib/generated/FStarC_OCaml.ml b/ocaml/fstar-lib/generated/FStarC_OCaml.ml
index b780e413aec..007f1e660eb 100644
--- a/ocaml/fstar-lib/generated/FStarC_OCaml.ml
+++ b/ocaml/fstar-lib/generated/FStarC_OCaml.ml
@@ -38,15 +38,22 @@ let exec_in_ocamlenv : 'a . Prims.string -> Prims.string Prims.list -> 'a =
       FStarC_Compiler_Util.putenv "OCAMLPATH" new_ocamlpath1;
       FStarC_Compiler_Util.execvp cmd (cmd :: args);
       failwith "execvp failed"
+let (app_lib : Prims.string) = "fstar.lib"
+let (plugin_lib : Prims.string) = "fstar.lib"
+let (wstr : Prims.string) = "-8"
+let (common_args : Prims.string Prims.list) = ["-w"; wstr; "-thread"]
 let exec_ocamlc : 'a . Prims.string Prims.list -> 'a =
   fun args ->
-    exec_in_ocamlenv "ocamlfind" ("c" :: "-w" :: "-8" :: "-linkpkg" ::
-      "-package" :: "fstar.lib" :: args)
+    exec_in_ocamlenv "ocamlfind"
+      (FStar_List_Tot_Base.op_At ("c" :: common_args) ("-linkpkg" ::
+         "-package" :: app_lib :: args))
 let exec_ocamlopt : 'a . Prims.string Prims.list -> 'a =
   fun args ->
-    exec_in_ocamlenv "ocamlfind" ("opt" :: "-w" :: "-8" :: "-linkpkg" ::
-      "-package" :: "fstar.lib" :: args)
+    exec_in_ocamlenv "ocamlfind"
+      (FStar_List_Tot_Base.op_At ("opt" :: common_args) ("-linkpkg" ::
+         "-package" :: app_lib :: args))
 let exec_ocamlopt_plugin : 'a . Prims.string Prims.list -> 'a =
   fun args ->
-    exec_in_ocamlenv "ocamlfind" ("opt" :: "-w" :: "-8" :: "-shared" ::
-      "-package" :: "fstar.lib" :: args)
\ No newline at end of file
+    exec_in_ocamlenv "ocamlfind"
+      (FStar_List_Tot_Base.op_At ("opt" :: common_args) ("-shared" ::
+         "-package" :: plugin_lib :: args))
\ No newline at end of file