can we avoid exporting LD_PRELOAD in set_env_vars.sh?

[cdisselkoen]

Category

DRT infrastructure

Describe the feature you'd like to request

Currently, set_env_vars.sh sets (exports) a number of environment variables, like LD_LIBRARY_PATH, JAVA_HOME, CLASSPATH. Most of these are sensible. However, it also sets (exports) LD_PRELOAD. This is less reasonable in my opinion, because it will cause that preload (Lean's libm) to be loaded for every future command in that shell, not just Lean-related ones. (Even worse, at the time of this writing, if you source set_env_vars.sh while not having lean on your PATH, the script will set LD_PRELOAD to a bogus path, which prints an error message every time you do anything subsequently in that shell. I'll have a PR shortly for the narrow issue of what happens when lean is not on your PATH.)

In my opinion it would be better if we could somehow set LD_PRELOAD only for the commands it is necessary, not globally in the shell.

Describe alternatives you've considered

Instead of a set_env_vars.sh meant for interactive use, we could have a runner script that sets all of these variables just locally (no export), and is responsible for calling cargo fuzz.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change

[cdisselkoen]

PR for the lean-not-on-PATH issue is #195. But the main issue discussed here remains.

[john-h-kastner-aws]

If there's nothing too expensive in setting the env vars, maybe something like

#!/bin/bash
cargo() (
  export LD_PRELOAD="..."
  command cargo "$@"
)