`IO.appPath` fails when `/proc` belongs to another PID namespace
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, linux
- Domain
- operating-systems
Research direction
Start in src/runtime/io.cpp, in lean_io_app_path, where the executable path is read from /proc/<getpid()>/exe. Check the readlink call and the error path that produces 'failed to locate application'. Reproduce with unshare --user --map-root-user --pid --fork lean --version. Done when lean --version prints the version inside that PID namespace and the existing app-path behaviour still works outside it.
Written by the indexing model from the issue text.
Description
Prerequisites
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
On Linux, lean_io_app_path (src/runtime/io.cpp) reads /proc/<getpid()>/exe. In a PID namespace without its own /proc mount, getpid() returns the PID inside the namespace, while /proc lists the PIDs of the parent namespace. The path then names another process or none, readlink fails, and every tool that needs IO.appPath fails, including lean and lake.
Context
Sandboxes and rootless containers often run processes in a PID namespace without remounting /proc. In such a sandbox, lean --version fails while other tools work.
Steps to Reproduce
unshare --user --map-root-user --pid --fork lean --version
Expected behavior: Lean prints its version.
Actual behavior: error: failed to locate application
Versions
Lean (version 4.31.0, x86_64-unknown-linux-gnu, commit 68218e876d2a38b1985b8590fff244a83c321783, Release)
Linux 7.2.9
The code on master is unchanged.
Additional Information
/proc/self/exe resolves correctly in this setup, because the kernel resolves self in the namespace of the /proc mount. Reading it instead fixes the problem:
if (readlink("/proc/self/exe", dest, PATH_MAX - 1) == -1) {
As a workaround, an LD_PRELOAD shim can redirect readlink("/proc/<getpid()>/exe") to /proc/self/exe.
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
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupOpenbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15674 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
leanprover/lean4#15626 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
microsoft/azurelinux#19417 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
hermit-os/kernel#2747 · 1 comment ·
Maintainers usually reply within 1 day
-
base-files: 82_config_generate: regenerate /etc/board.json if 0-bytes / truncated after power cutOpen
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
openwrt/openwrt#25940 · 5 comments ·
Maintainers usually reply within 1 day
-
enhancement
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
Maintainers usually reply within 2 days
-
Difficulty 2/5 1-3 hours Newbie friendliness 70/100