You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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):
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.
The text was updated successfully, but these errors were encountered:
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. 😄
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.
Prerequisites
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):
lean4/src/runtime/process.cpp
Lines 163 to 176 in 2061c9b
Based on the comment, I assume this may be an issue for @gebner?
Steps to Reproduce
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 andleanc
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 thealloy
executable (which included a setLEAN_CC
) would break parallel runs ofleanc
.The text was updated successfully, but these errors were encountered: