max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: IO.Process.spawn empty env var on Windows (#12220)

Browse source 
This PR fixes a bug on Windows with `IO.Process.spawn` where setting an
environment variable to the empty string would not set the environment
variable on the subprocess.
This commit is contained in:
Mac Malone 2026-01-31 14:17:26 -05:00 • committed by GitHub
parent 6c5de545f9
commit ce980895b2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 25 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/runtime/process.cpp
View file

@ -235,9 +235,9 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
char *new_envp = new_env.get();
if (env.size()) {
std::unordered_map<std::string, std::string> new_env_vars; // C++17 gives us no-copy std::string_view for this, much better!
std::unordered_map<std::string, option_ref<string_ref>> new_env_vars; // C++17 gives us no-copy std::string_view for this, much better!
for (auto & entry : env) {
new_env_vars[entry.fst().data()] = entry.snd() ? entry.snd().get()->data() : std::string{};
new_env_vars[entry.fst().data()] = entry.snd();
}
// First copy old evars not in new evars.
@ -257,12 +257,13 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
// Then copy new evars if nonempty
for(const auto & ev : new_env_vars) {
if (ev.second.empty()) continue;
if (!ev.second) continue;
std::string val = ev.second.get()->data();
// Check if the destination buffer has enough room.
if (new_envp + ev.first.length() + 1 + ev.second.length() + 1 > new_env.get() + env_buf_size - 1) break;
if (new_envp + ev.first.length() + 1 + val.length() + 1 > new_env.get() + env_buf_size - 1) break;
new_envp = std::copy(ev.first.cbegin(), ev.first.cend(), new_envp);
*new_envp++ = '=';
new_envp = std::copy(ev.second.cbegin(), ev.second.cend(), new_envp);
new_envp = std::copy(val.cbegin(), val.cend(), new_envp);
*new_envp++ = '\0';
}
}

4
tests/lake/tests/env/test.sh vendored
View file

@ -45,9 +45,7 @@ LEAN_CC=foo test_eq "foo" env printenv LEAN_CC
# Test `LAKE_ARTIFACT_CACHE` setting and default
LAKE_ARTIFACT_CACHE=true test_eq "true" env printenv LAKE_ARTIFACT_CACHE
LAKE_ARTIFACT_CACHE=false test_eq "false" env printenv LAKE_ARTIFACT_CACHE
# FIXME: Currently fails on Windows due to a platform inconsistency in how
# Lean configures the environments of spawned processes
# LAKE_ARTIFACT_CACHE= test_eq "" env printenv LAKE_ARTIFACT_CACHE
LAKE_ARTIFACT_CACHE= test_eq "" env printenv LAKE_ARTIFACT_CACHE
LAKE_ARTIFACT_CACHE= test_eq "false" -d ../../examples/hello env printenv LAKE_ARTIFACT_CACHE
LAKE_ARTIFACT_CACHE= test_eq "true" -f enableArtifactCache.toml env printenv LAKE_ARTIFACT_CACHE
test_cmd rm lake-manifest.json

18
tests/lean/run/emptyEnvVar.lean Normal file
View file

@ -0,0 +1,18 @@
/--
Tests that spawning a process with a environment variable configured to the
empty string correctly sets the environment variable on the subprocess on
all platforms. Previously, this was broken on Windows.
-/
def test : IO String := do
let var := "TEST_VAR"
let out ← IO.Process.output {
cmd := "printenv"
args := #[var]
env := #[(var, some "")]
}
unless out.exitCode == 0 do
throw <| .userError "environment variable not set"
return out.stdout.trimAsciiEnd.copy -- trim ending newline
/-- info: "" -/
#guard_msgs in #eval test