leanprover / elan

The Lean version manager
Apache License 2.0
310 stars 35 forks source link

Don't prepend to LD_LIBRARY_PATH for Lean 4 #90

Closed iacore closed 1 year ago

iacore commented 1 year ago

elan shim prepends the toolchain lib path to LD_LIBRARY_PATH. It doesn't seem necessary. More importantly, it messes with lake exe progname (See here).

❯ echo '#eval IO.getEnv "LD_LIBRARY_PATH"' | lean --stdin
some "/home/user/.elan/toolchains/custom-stable/lib:/usr/lib:/usr/local/lib"

❯ echo '#eval IO.getEnv "LD_LIBRARY_PATH"' | ~/.elan/toolchains/leanprover--lean4---nightly/bin/lean --std
in
some "/usr/lib:/usr/local/lib"
iacore commented 1 year ago

tools like llvm-ar Need modified LD_LIBRARY_PATH to work, but lean programs themselves don't.

tage64 commented 1 year ago

I've ran into this issue as well. Tried to run clang as part of the build process when creating some c++ bindings. A minimal example can be found here: https://github.com/tage64/lean_subprocess_test.git