Protect LD_LIBRARY_PATH environment variable for leanc

Stream: lean4 dev

[Xiyu Zhai]

Some terminals like alacritty, modifies LD_LIBRARY_PATH and running leanc directly will leads to problems like symbol lookup errors for clang. It took me an hour to trace this bug.

I suggest it would be good to set LD_LIBRARY_PATH to empty for the leanc process and then run clang so that whatever LD_LIBRARY_PATH is set in the environment doesn't affect the compilation process.

[Sebastian Ullrich]

You really should find out where LD_LIBRARY_PATH is set on your system, this is not normal and it's going to break much more than just Lean

[Xiyu Zhai]

This behavior is caused by the alacritty distribution by snap on ubuntu. The snapcrafters change LD_LIBRARY_PATH to something that will cause leanc to throw out symbol lookup errors.

In https://github.com/snapcrafters/alacritty/blob/candidate/snap/snapcraft.yaml
they set

      LD_LIBRARY_PATH: "$SNAP/usr/lib/$CRAFT_ARCH_TRIPLET:$SNAP/lib/$CRAFT_ARCH_TRIPLET"

It's community maintained, so not so professional, lol.
I just put it here so that if anyone encounters similar problems by using leanc in alacritty, they will solve it faster.

[Joachim Breitner]

I was curious since I am using alacritty, but not snap. On my system I have

~ $ echo $LD_LIBRARY_PATH
/etc/sane-libs

It’s a big relieve to see that that only sane libs are using LD_LIBRARY_PATH, it seems…

[Xiyu Zhai]

They just proposed a fix 2 hours ago.

[Xiyu Zhai]

https://github.com/snapcrafters/alacritty/pull/14