Lean executable can only be run inside its directory

Stream: lean4

[Leni Aniva]

I have a very simple lean project compiling an executable:

lean-examples
|- build
   |- bin
      |- lean-examples

However if the pwd is outside of lean-examples, and I run e.g. from ../lean-examples the command lean-examples/build/bin/lean-examples, lean crashes:

uncaught exception: process 'lean' exited with code 1

The problem is solved by moving the toolchain file "outside" or set the default toolchain

cp lean-examples/lean-toolchain .

Is there a way to bundle this information along with the executable or will the executable always be dependent on this toolchain file or the default toolchain?

[Sebastian Ullrich]

I'm assuming your executable calls lean? Are you okay with the executable running correctly only on your current machine? Then you could bake the path to lean into the executable (manually or via some metaprogramming if you want)

[Leni Aniva]

Sebastian Ullrich said:

I'm assuming your executable calls lean? Are you okay with the executable running correctly only on your current machine? Then you could bake the path to lean into the executable (manually or via some metaprogramming if you want)

How can I bake the path into the executable?