lake sometimes hangs on NetBSD

[0-wiz-0]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

After packaging lean 4.32.1, I've been building it repeatedly in a clean environment. Sometimes (1 out of 3? 5? times) during a build, lake will hang.

I've attached a debugger once, reading the backtrace there is a process hanging in pthread_join, one in fread, the others are idle in pthread_cond_timedwait.

I can only see one fread() in the code, in src/runtime/io.cpp - perhaps this code should have a timeout (i.e. use select or poll and non-blocking reads.

Context

n/a

Steps to Reproduce

1. Build lean4 4.32.1 repeatedly.
2. be unlucky

Expected behavior: [Clear and concise description of what you expect to happen]

lake should not hang.

Actual behavior: [Clear and concise description of what actually happens]

lake sometimes does hang.

Versions

4.32.1
NetBSD 11.99.7/x86_64

Additional Information

n/a

Impact

[hargoniX]

We regularly build Lean hundreds of times per week on several platforms and it does not exhibit this behavior. Whatever is going on here is a NetBSD specific issue.

[0-wiz-0]

Here is the full backtrace with symbols for a hang I saw today when updating the package to 4.32.2.

https://gist.github.com/0-wiz-0/5840923a09abac1c2099b492ba7fea2f

[0-wiz-0]

I've asked Claude Sonnet 5 for an analysis, here's the result:

Lake fork()-hang analysis

Symptom

Lake occasionally hangs during lake build. A GDB backtrace of a hung
process shows the monitor thread blocked forever in IO.Process.output,
reading the child process's stdout pipe to EOF:

#0  read () from /usr/lib/libc.so.12
...
#6  lean::lean_io_prim_handle_read (...) at .../stage0/src/runtime/io.cpp:594
#7  l___private_Init_System_IO_0__IO_FS_Handle_readBinToEndInto_loop ()
#8  l_IO_FS_Handle_readToEnd ()
#9  l_IO_Process_output___lam__0 ()
...
#15 lean::task_manager::run_task (...) at .../stage0/src/runtime/object.cpp:864

Meanwhile thread apply all bt shows ~30+ other threads: the main
thread joined on the runtime, the libuv event loop thread, the Lake
monitor thread (in nanosleep), and a large number of Lean
task_manager worker threads parked in pthread_cond_timedwait
(task_manager::spawn_worker). This is typical of a Lean/Lake process
doing a parallel build with many dedicated task-manager threads alive.

Code path

• IO.Process.output (src/Init/System/IO.lean:1544) spawns a child
  with piped stdout/stderr, then does a blocking readToEnd on stdout.
• The actual process creation is spawn() in
  stage0/src/runtime/process.cpp:440, which uses plain fork()
  followed by, in the child (before execvp):
  • clearenv() / setenv() / unsetenv() (lines 458-471)
  • dup2()/close() on the pipe fds (lines 473-495)
  • on chdir() failure, std::cerr << ... (line 499)

Root cause

fork() only duplicates the calling thread. Any mutex held by another
thread at the moment of fork() (glibc/BSD libc malloc arena locks,
C++ iostream locks, locale locks, etc.) is copied into the child
already locked, and no thread remains in the child that will ever
unlock it.

None of clearenv, setenv, unsetenv, strdup (used to build argv
before the fork, but preserved across it), or std::cerr are
async-signal-safe / fork-safe. If the child calls any of these and
happens to need a lock that some other thread in the multi-threaded
parent held at fork time, the child deadlocks before ever reaching
execvp.

Because Lake/Lean processes routinely run with many live threads
(task-manager workers, the libuv loop thread, etc.), the odds of a
malloc/stdio lock being held at the instant of fork() are
non-negligible under load, explaining why the hang is intermittent.

Consequence: if the forked child deadlocks before execvp/_exit,
it never closes its inherited copy of the pipe's write end. The
parent's read end therefore never sees EOF, and the blocking
read() in IO.Process.output's readToEnd hangs forever — exactly
what the backtrace shows.

Conclusion

This is a classic "unsafe fork() from a multi-threaded process" bug,
not NetBSD-specific in principle, though NetBSD's libc/pthread malloc
locking around fork() may make it easier to trigger.

Fix direction

Replace the fork() + child-side clearenv/setenv/dup2/std::cerr
sequence with posix_spawn() (using
posix_spawn_file_actions_t for the dup2/close pipe setup and
posix_spawnattr_t as needed), and build the target environment array
in the parent (fork-safe/allocation-free constraints don't apply there)
before calling posix_spawn, rather than mutating environment state in
the child after fork(). This avoids running non-async-signal-safe
code in a freshly forked, single-threaded child, and eliminates the
possibility of the child deadlocking on a lock it can never release.

[0-wiz-0]

Would a patch using posix_spawn be acceptable?

[hargoniX]

Would be welcome if it doesn't change too much of the runtime yes!

[Kha]

There were plans for revamping Process, so it might not be a good time for such a nontrivial change to it. /cc @TwoFX

[0-wiz-0]

I made a minor step on the way: when I create the environment for the child process in the main process before the fork (thus saving the mallocs/frees of clearenv/setenv), this already seems to work better. We will need this for a possible posix_spawn version as well. Please consider including (a version of) this patch:

$NetBSD: patch-src_runtime_process.cpp,v 1.2 2026/07/24 21:26:20 wiz Exp $

Set proper thread id on NetBSD.
clearenv() does not exist on NetBSD.
https://github.com/leanprover/lean4/pull/14543

--- src/runtime/process.cpp.orig	2026-08-15 19:18:21.000000000 +0000
+++ src/runtime/process.cpp
@@ -8,7 +8,9 @@ Author: Jared Roesch
 #include <fstream>
 #include <iostream>
 #include <iomanip>
+#include <map>
 #include <utility>
+#include <vector>
 #include <system_error>
 
 #if defined(LEAN_WINDOWS)
@@ -431,10 +435,52 @@ static optional<pipe> setup_stdio(stdio cfg) {
     lean_unreachable();
 }
 
-#ifdef __APPLE__
+#if defined(__APPLE__) || defined(__NetBSD__)
 extern "C" char **environ;
 #endif
 
+static std::vector<char*> build_environ(bool inherit_env, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env) {
+    std::map<std::string, std::string> current;
+    if (inherit_env) {
+	/* Build a lookup map from current environ */
+	for (char** env = environ; *env; ++env) {
+	    auto sep = std::strstr(*env, "=");
+	    if (sep) {
+		std::string key(*env, sep - *env);
+		current[std::move(key)] = sep + 1;
+	    }
+	}
+    }
+
+    /* Apply overrides */
+    for (auto & entry : env) {
+	if (entry.snd()) {
+	    current[entry.fst().data()] = entry.snd().get()->data();
+	} else {
+	    current.erase(entry.fst().data());
+	}
+    }
+
+    /* Create the new environ array */
+    std::vector<char*> result;
+    result.reserve(current.size() + 1);
+
+    for (auto & [key, val] : current) {
+        size_t key_len = key.size();
+        size_t val_len = val.size();
+        size_t total = key_len + 1 + val_len + 1;
+        char* entry = new char[total];
+        std::memcpy(entry, key.data(), key_len);
+        entry[key_len] = '=';
+        std::memcpy(entry + key_len + 1, val.data(), val_len);
+        entry[key_len + 1 + val_len] = '\0';
+        result.push_back(entry);
+    }
+
+    result.push_back(nullptr);
+    return result;
+}
+
 static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const & args, stdio stdin_mode, stdio stdout_mode,
   stdio stderr_mode, option_ref<string_ref> const & cwd, array_ref<pair_ref<string_ref, option_ref<string_ref>>> const & env,
   bool inherit_env, bool do_setsid) {
@@ -450,24 +496,11 @@ static obj_res spawn(string_ref const & proc_name, arr
         pargs.push_back(strdup(arg.data()));
     pargs.push_back(NULL);
 
+    std::vector<char*> new_env =  build_environ(inherit_env, env);
+
     int pid = fork();
 
     if (pid == 0) {
-        if (!inherit_env) {
-#ifdef __APPLE__
-            environ = NULL;
-#else
-            clearenv();
-#endif
-        }
-        for (auto & entry : env) {
-            if (entry.snd()) {
-                setenv(entry.fst().data(), entry.snd().get()->data(), true);
-            } else {
-                unsetenv(entry.fst().data());
-            }
-        }
-
         if (stdin_pipe) {
             dup2(stdin_pipe->m_read_fd, STDIN_FILENO);
             close(stdin_pipe->m_write_fd);
@@ -507,7 +540,7 @@ static obj_res spawn(string_ref const & proc_name, arr
             lean_always_assert(setsid() >= 0);
         }
 
-        if (execvp(pargs[0], pargs.data()) < 0) {
+        if (execvpe(pargs[0], pargs.data(), new_env.data()) < 0) {
             std::cerr << "could not execute external process '" << pargs[0] << "'" << std::endl;
             // See the comment above about `_exit` vs `exit`.
             _exit(-1);
@@ -520,6 +553,11 @@ static obj_res spawn(string_ref const & proc_name, arr
         if (parg != NULL) {
             free(parg);
         }
+    }
+    for (char* entry : new_env) {
+        if (entry != NULL) {
+	    free(entry);
+	}
     }
 
     object * parent_stdin  = box(0);