Environment leaks between spawned processes (on Windows)

[tydeu]

trafficstars

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

On Windows, spawning a process using IO.Process.spawn with one environment in one thread will affect the environment of another spawned process in another thread. This is a major problem for Lake which often wishes to spawn processes in different build threads with different environments.

This is due to this section of code (which specifically states that its manner of setting environment variables is thread-unsafe):

https://github.com/leanprover/lean4/blob/2061c9bbea847afd6cd301381c5fb239fb21062f/src/runtime/process.cpp#L163-L176

Based on the comment, I assume this may be an issue for @gebner?

Steps to Reproduce

def printenv (var : String) (env : Array (String × Option String) := #[]) : IO String :=
  IO.Process.output {cmd := "printenv", args :=  #[var], env} <&> (·.stdout)

def singleTest : IO PUnit := do
  IO.println s!"Initial: {repr (← printenv "LEAN_CC").trim}"

def jointSyncTest : IO PUnit := do
  let a ← printenv "LEAN_CC" #[("LEAN_CC", "cc")]
  let b ← printenv "LEAN_CC" #[]
  IO.print s!"1st: {repr a.trim}; "
  IO.println s!"2nd: {repr b.trim}"

def jointAsyncTest : IO PUnit := do
  let t1 ← IO.asTask <| printenv "LEAN_CC" #[("LEAN_CC", "cc")]
  let t2 ← IO.asTask <| printenv "LEAN_CC" #[]
  IO.print s!"Task 1: {repr (← IO.ofExcept (← IO.wait t1)).trim}; "
  IO.println s!"Task 2: {repr (← IO.ofExcept (← IO.wait t2)).trim}"

#eval singleTest -- Initial: ""
#eval jointSyncTest -- 1st: "cc"; 2nd: ""
#eval jointAsyncTest -- Task 1: "cc"; Task 2: "cc"

Expected behavior:

Environment does not leak between separately spawned process (even those spawned in parallel).

Actual behavior:

Environment leaks between processes spawned in parallel.

Reproduces how often:

Always (on Windows).

Versions

Windows 20H2 Lean (version 4.0.0-nightly-2022-07-03, commit 7326c817d22e, Release)

Additional Information

This bug can exacerbate the issue in #1281. If one process has LEAN_CC set and leanc is run in separate, parallel process, leanc breaks. I discovered this when attempting to get Alloy to work with the new build features of Lake. The environment set for the alloy executable (which included a set LEAN_CC) would break parallel runs of leanc.

[gebner]

Based on the comment, I assume this may be an issue for @gebner?

The comment just means that this has been on (the end of) my todo list for five years. :smile:

From what I can tell, the windows CreateProcess function actually takes an argument for the environment variables. We'd just need to pass the right thing there. I don't have a windows machine, so I can't easily debug this.