From 99b78bcc23d759ed9af55a3cccae15da51c0730b Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 14 Sep 2023 14:26:22 -0400 Subject: [PATCH] fix: `stdin := .null` in `IO.Process.output` --- RELEASES.md | 1 + src/Init/System/IO.lean | 7 +++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index a4287e9d6d..215a8a0446 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -10,6 +10,7 @@ Please check the [releases](https://github.com/leanprover/lean4/releases) page f v4.3.0 (development in progress) --------- +* `IO.Process.output` no longer inherits the standard input of the caller. * The derive handler for `DecidableEq` [now handles](https://github.com/leanprover/lean4/pull/2591) mutual inductive types. * [Show path of failed import in Lake](https://github.com/leanprover/lean4/pull/2616). * [Fix linker warnings on macOS](https://github.com/leanprover/lean4/pull/2598). diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index fedc48dcd0..a204c1147f 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -638,9 +638,12 @@ structure Output where stdout : String stderr : String -/-- Run process to completion and capture output. -/ +/-- +Run process to completion and capture output. +The process does not inherit the standard input of the caller. +-/ def output (args : SpawnArgs) : IO Output := do - let child ← spawn { args with stdout := Stdio.piped, stderr := Stdio.piped } + let child ← spawn { args with stdout := .piped, stderr := .piped, stdin := .null } let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated let stderr ← child.stderr.readToEnd let exitCode ← child.wait