setenv shouldn't add /usr/bin to PATH

[tothtamas28]

Related:

• Kompile executes post-processing command in modified environment #2974
• Cannot install K on ubuntu-latest GitHub Actions runner #4059

For example, on a Debian package installation, the script prepends /usr/lib/kframework/../../bin to PATH:

k/k-distribution/src/main/scripts/lib/setenv

Line 12 in ab78f57

export PATH="$K_LIB_DIR/../../bin:$PATH"

As a consequence, the user cannot override a dependency in /usr/bin by updating the PATH, although that might be necessary in certain cases:

• Switch from system python3 to a virtual environment Kompile executes post-processing command in modified environment #2974
• Switch from system java to a more recent version Cannot install K on ubuntu-latest GitHub Actions runner #4059

Instead of prepending /usr/bin to PATH, the script should prepend a directory that only contains K executables: #2974 (comment).

Also, to make replacing the java dependency easier, consider increasing the priority of JAVA_HOME:

k/k-distribution/src/main/scripts/lib/checkJava

Line 8 in 83f6df4

_java="$JAVA_HOME/bin/java"

[Baltoli]

Currently, the K packaging workflow installs executables by directly copying them into the target directory from where they're built by Maven:

k/package/package

Line 6 in 67ef71b

cp -R k-distribution/target/release/k/bin/* $DESTDIR$PREFIX/bin

k/nix/k.nix

Line 59 in 67ef71b

cp -r k-distribution/target/release/k/bin/* $out/bin-unwrapped/

We can probably implement the fix suggested here by instead copying all the binaries to an isolated directory, and symlinking them into the output binary directory. Then, setenv can prepend the isolated directory instead of the global install location.

NB. I think this only actually applies to the non-Nix configuration as Nix takes care of paths for us via wrapper scripts.

[Baltoli]

There may be a way to do this without PATH tinkering; all the binaries live near each other on disk so maybe they can know where their siblings are somehow.