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(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(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 const & args) { + list_ref arglist = to_list_ref(args); + return get_io_scalar_result(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 c_output; optional root_dir; + buffer 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(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(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();