Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Don't prepend to LD_LIBRARY_PATH for Lean 4 #90

Closed
iacore opened this issue Mar 12, 2023 · 2 comments · Fixed by #92
Closed

Don't prepend to LD_LIBRARY_PATH for Lean 4 #90

iacore opened this issue Mar 12, 2023 · 2 comments · Fixed by #92

Comments

@iacore
Copy link

iacore commented Mar 12, 2023

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
Copy link
Author

iacore commented Mar 19, 2023

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

@tage64
Copy link

tage64 commented Apr 12, 2023

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

Kha added a commit to Kha/elan that referenced this issue Apr 23, 2023
Our binaries are properly linked

Fixes leanprover#90
@Kha Kha closed this as completed in #92 Apr 23, 2023
Kha added a commit that referenced this issue Apr 23, 2023
Our binaries are properly linked

Fixes #90
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants