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

`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)

Open Beginner friendly
  • Is something wrong?
#15,681 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
70/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
cpp
Domain
operating-systems

Research direction

The binding is Child.pid in src/Init/System/IO.lean near line 1524, and the C side is lean_io_process_child_pid in src/runtime/process.cpp around lines 402-406. Compare it with the @& borrowed annotations on Child.tryWait and Child.kill in the same file. Run the repro with lean --run Repro.lean and check that the open-fd count stays flat after the change. Done means the borrow annotation (or a release in the runtime function) makes the Child.pid rounds leave no extra fds open.

Written by the indexing model from the issue text.

Description

bug
Prerequisites
Description

Child.pid's binding is opaque Child.pid {cfg : @& StdioConfig} : Child cfg → UInt32: only cfg is
borrowed, so the Child cfg argument is owned and the callee must release it. The runtime function
takes it as b_obj_arg (borrowed) and never releases it, so each child.pid leaks the Child and the
Handles it holds — one pipe fd per call with stdout := .piped.

Context

A long-running supervisor that polls child.pid leaks one Child (and its piped stdout fd) per call.

Steps to Reproduce
  1. Repro.lean:
def fds : IO Nat := return (← (System.FilePath.mk "/proc/self/fd").readDir).size

def rounds (usePid : Bool) : IO UInt32 := do
  let mut acc : UInt32 := 0
  for _ in List.range 40 do
    let child ← IO.Process.spawn { cmd := "true", stdout := .piped }
    if usePid then acc := acc + child.pid
    let _ ← child.wait
  return acc

def main : IO UInt32 := do
  let b0 ← fds
  let _ ← rounds false
  let b1 ← fds
  let _ ← rounds true
  let b2 ← fds
  IO.println s!"open fds: 40 spawns without Child.pid: +{b1 - b0}; with Child.pid: +{b2 - b1}"
  return 0
  1. lean Repro.lean -c Repro.c && leanc -O1 -o Repro Repro.c && ./Repro. (lean --run Repro.lean
    reproduces it in the interpreter too.)

Expected behavior: both rounds release what they open, leaving the fd count unchanged:
open fds: 40 spawns without Child.pid: +0; with Child.pid: +0.

Actual behavior:

$ ./Repro
open fds: 40 spawns without Child.pid: +0; with Child.pid: +40
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

lean_io_process_child_pid (process.cpp:402-406) only reads the pid from b_obj_arg child; the binding (Init/System/IO.lean:1524) is what passes it owned. Child.tryWait/Child.kill declare the child @&, matching the borrowed runtime argument.

Fix — mark the argument borrowed, as tryWait/kill do (or lean_dec(child) in the runtime function):

@[extern "lean_io_process_child_pid"] opaque Child.pid {cfg : @& StdioConfig} : @& Child cfg → UInt32
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
1d 4h
Merged PRs (30d)
270

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.