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

@@ -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}"

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();