From 066baeccc0997da002d8f7e6ff40b29b8847fa03 Mon Sep 17 00:00:00 2001
From: Christian Pehle <christian.pehle@gmail.com>
Date: Sat, 16 Jan 2021 17:05:54 +0100
Subject: [PATCH] fix: pass (some) cmdline arguments to watchdog and workers

Capture some of the command line arguments in an argument
vector, that then gets passed to the watchdog and
subsequently the worker processes. Currently flags like
"-T" and "-j2" are not passed on to the watchdog and
worker processes.

Addresses #246
---
 src/Lean/Server/Watchdog.lean | 10 ++++++----
 src/shell/lean.cpp            | 15 ++++++++++-----
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index d8ca093930..14ff2ed8ec 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -153,6 +153,7 @@ section ServerM
     hIn            : FS.Stream
     hOut           : FS.Stream
     hLog           : FS.Stream
+    args           : List String
     fileWorkersRef : IO.Ref FileWorkerMap
     -- We store these to pass them to workers.
     initParams     : InitializeParams
@@ -213,7 +214,7 @@ section ServerM
       toStdioConfig := workerCfg
       cmd           := st.workerPath
       -- append file and imports for Nix support; ignored otherwise
-      args          := #["--worker"] ++ (Lean.Elab.headerToImports headerAst).toArray.map (toString ·.module)
+      args          := #["--worker"] ++ (Lean.Elab.headerToImports headerAst).toArray.map (toString ·.module) ++ st.args.toArray
     }
     let pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap)
     -- The task will never access itself, so this is fine
@@ -449,7 +450,7 @@ def initAndRunWatchdogAux : ServerM Unit := do
     shutdown
     throw err
 
-def initAndRunWatchdog (i o e : FS.Stream) : IO Unit := do
+def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   let workerPath ← match (←IO.getEnv "LEAN_WORKER_PATH") with
     | none   => IO.appPath
     | some p => p
@@ -473,6 +474,7 @@ def initAndRunWatchdog (i o e : FS.Stream) : IO Unit := do
     hIn            := i
     hOut           := o
     hLog           := e
+    args           := args
     fileWorkersRef := fileWorkersRef
     initParams     := initRequest.param
     workerPath     := workerPath
@@ -480,12 +482,12 @@ def initAndRunWatchdog (i o e : FS.Stream) : IO Unit := do
   }
 
 @[export lean_server_watchdog_main]
-def watchdogMain : IO UInt32 := do
+def watchdogMain (args : List String) : IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
   let e ← IO.getStderr
   try
-    initAndRunWatchdog i o e
+    initAndRunWatchdog args i o e
     return 0
   catch err =>
     e.putStrLn s!"Watchdog error: {err}"
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 7eb4659fd1..f014faaaf8 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -334,10 +334,11 @@ uint32_t run_server_worker() {
     return get_io_scalar_result<uint32_t>(lean_server_worker_main(io_mk_world()));
 }
 
-/* def watchdogMain : IO Uint32 */
-extern "C" object* lean_server_watchdog_main(object* w);
-uint32_t run_server_watchdog() {
-    return get_io_scalar_result<uint32_t>(lean_server_watchdog_main(io_mk_world()));
+/* def watchdogMain (args : List String) : IO Uint32 */
+extern "C" object* lean_server_watchdog_main(object* args, object* w);
+uint32_t run_server_watchdog(buffer<string_ref> const & args) {
+    list_ref<string_ref> arglist = to_list_ref(args);
+    return get_io_scalar_result<uint32_t>(lean_server_watchdog_main(arglist.to_obj_arg(), io_mk_world()));
 }
 
 extern "C" object* lean_init_search_path(object* opt_path, object* w);
@@ -434,6 +435,8 @@ int main(int argc, char ** argv) {
     std::string native_output;
     optional<std::string> c_output;
     optional<std::string> root_dir;
+    buffer<string_ref> forwarded_args;
+
     while (true) {
         int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
         if (c == -1)
@@ -444,6 +447,7 @@ int main(int argc, char ** argv) {
                 break;
             case 'j':
                 num_threads = static_cast<unsigned>(atoi(optarg));
+                forwarded_args.push_back(string_ref("-j" + std::string(optarg)));
                 break;
             case 'v':
                 display_header(std::cout);
@@ -480,6 +484,7 @@ int main(int argc, char ** argv) {
                 break;
             case 'T':
                 check_optarg("T");
+                forwarded_args.push_back(string_ref("-T" + std::string(optarg)));
                 opts = opts.update(get_timeout_opt_name(), static_cast<unsigned>(atoi(optarg)));
                 break;
             case 't':
@@ -555,7 +560,7 @@ int main(int argc, char ** argv) {
 
     try {
         if (run_server == 1)
-            return run_server_watchdog();
+            return run_server_watchdog(forwarded_args);
         else if (run_server == 2)
             return run_server_worker();