Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process group

Open Beginner friendly
  • Is something wrong?
#15,674 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
2/5
Estimated time
1-3 hours
Newbie friendliness
72/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
cpp
Domain
operating-systems

Research direction

The bug is in src/runtime/process.cpp: spawn writes the setsid byte at scalar offset 3 * sizeof(object *) + sizeof(pid_t), kill reads it, and takeStdin allocates only sizeof(pid_t) and copies only the pid. Start by reading those three spots, then add the byte copy to takeStdin as the issue suggests. Done means the repro prints grandchild survived kill: without takeStdin = false, after takeStdin = false, and the process-group kill behaviour is unchanged for the non-take path.

Written by the indexing model from the issue text.

Description

bug
Prerequisites
Description

Child.kill's docstring promises to kill the child's entire process group when it was started with
SpawnArgs.setsid. After Child.takeStdin it does not: the returned Child has a scalar area of only
sizeof(pid_t) and just the pid is copied, so setsid is lost and grandchildren survive — even though
takeStdin's docstring presents take-stdin-then-kill/wait as the intended flow.

Context

Supervising a spawned process tree: setsid := true, then takeStdin, then kill, expecting the whole
group to die.

Steps to Reproduce
  1. Repro.lean:
def round (take : Bool) : IO Bool := do
  let child ← IO.Process.spawn
    { cmd := "sh", args := #["-c", "sleep 30 & echo $!; wait"],
      stdin := .piped, stdout := .piped, setsid := true }
  let grandchild := (← child.stdout.getLine).trimAscii.toString
  IO.sleep 100
  if take then
    let (_, child2) ← child.takeStdin
    child2.kill
    let _ ← child2.wait
  else
    child.kill
    let _ ← child.wait
  IO.sleep 300
  let alive := (← IO.Process.output { cmd := "kill", args := #["-0", grandchild] }).exitCode == 0
  let _ ← IO.Process.output { cmd := "kill", args := #["-KILL", grandchild] }
  return alive

def main : IO Unit := do
  let ctl ← round false
  let take ← round true
  IO.println s!"grandchild survived kill: without takeStdin = {ctl}, after takeStdin = {take}"
  1. lean --run Repro.lean (or compile: lean Repro.lean -c Repro.c && leanc -O1 -o Repro Repro.c && ./Repro).

Expected behavior: grandchild survived kill: without takeStdin = false, after takeStdin = false —
the sleep is in the child's process group in both rounds.

Actual behavior:

grandchild survived kill: without takeStdin = false, after takeStdin = true
Versions
Lean (version 4.36.0-nightly-2026-10-13, x86_64-unknown-linux-gnu, commit b7725c34da98e6e2f6323d7f382448ddf31477fb, Release)
Linux 7.0.0-38-generic (x86_64)
Additional Information

spawn writes the setsid byte at scalar offset 3 * sizeof(object *) + sizeof(pid_t) (process.cpp:543,546); kill reads it there (process.cpp:395); takeStdin allocates only sizeof(pid_t) and copies only the pid (process.cpp:550-553) — so the kill path reads zeroed padding.

Fix — copy the byte too:

object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2),
                             sizeof(pid_t) + sizeof(uint8_t));
cnstr_set_uint32(child2.raw(), 3 * sizeof(object *), cnstr_get_uint32(child.raw(), 3 * sizeof(object *)));
cnstr_set_uint8(child2.raw(), 3 * sizeof(object *) + sizeof(pid_t), cnstr_get_uint8(child.raw(), 3 * sizeof(object *) + sizeof(pid_t)));
Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Dominant language
Lean
Stars
9.5k
Forks
1k
Avg merge
23h 14m
Merged PRs (30d)
273

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from leanprover/lean4

All issues in leanprover/lean4

Similar issues

More Operating Systems issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.