Subprocess function works unexpectedly

Stream: lean4

[Tage Johansson]

I discovered a potential bug when spawning a subprocess in IO.Process. The environment in which the process is running seems to be modified in some strange way. A description and (hopefully) reproducible example can be found here.

Hope someone can take a look at this, or explain why this is the expected behaviour.

Thanks,
Tage

[Sebastian Ullrich]

That sounds like https://github.com/leanprover/elan/issues/90, so it should be fine if you run it from build/ directly

[Tage Johansson]

Seems correct. I'm not really sure what you mean with running it from build/, what build/ directory?
But when I explicitly run lake from the bin folder in ~/.elan/toolchains/xxxx (I.E. without elan) it does work. So a solution to the issue you linked to would probably solve my problem as well.

[Sebastian Ullrich]

lake exe foo is roughly equal to lake build foo && ./build/bin/foo, except that you're running foo inside elan, which is the source of the issue

[Tage Johansson]

But for me even lake build is not working since I am running clang to build some c++ bindings as part of the build process. I temporarily solved it by creating a shell script run_clang.sh.