Kompile executes post-processing command in modified environment

[tothtamas28]

When running kompile with --post-process <command>, one would expect that command is executed in the caller's environment (extended perhaps with a few variables that do not clash with existing ones).

This is not the case however. Consider e.g. script.sh:

env
false

Then

% docker run -it --rm -v $(pwd):$(pwd) -w $(pwd) -u $(id -u):$(id -g) runtimeverificationinc/kframework-k:ubuntu-focal-5.4.26 sh script.sh

produces

HOSTNAME=11b5112cca9a
HOME=/
TERM=xterm
PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
PWD=<working directory>
TZ=America/Chicago

whereas

% docker run -it --rm -v $(pwd):$(pwd) -w $(pwd) -u $(id -u):$(id -g) runtimeverificationinc/kframework-k:ubuntu-focal-5.4.26 kompile imp.k --post-process 'sh script.sh'

produces

[Error] Critical: Post-processing returned a non-zero exit code: 1
Stdout:
K_COLOR_SUPPORT=8
HOSTNAME=16538a1e94af
LD_LIBRARY_PATH=:/usr/lib/kframework/native/linux64
SHLVL=1
HOME=/
_=/usr/lib/kframework/../../bin/java
TERM=xterm
K_OPTS=-Xms64m -Xmx4096m -Xss32m -XX:+TieredCompilation
PATH=/usr/lib/kframework/native/linux64:/usr/lib/kframework/../../bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
LC_ALL=C
PWD=<working directory>
TZ=America/Chicago

Stderr:

Notably, $PATH is extended with new directories, so command names might resolve to different files.

[radumereuta]

This comes from here: https://github.com/runtimeverification/k/blob/master/k-distribution/src/main/scripts/lib/setenv#L12

[radumereuta]

@dwightguth are we still using the extra path added to $PATH added to the K environment?
It seems that Tamash is running into some issue because of that.

[dwightguth]

This particular behavior is necessary so that k will always call its own version of any tools that exist even if the tool being run isn't the version on the path. For example, if I say krun --parser kast but k isn't on the path, without this line that will be an error.

We can probably remove the native directory from the path though as I believe that was specifically to deal with windows particularities, and we don't support windows natively anymore.
Note that if we restrict the path change to that one bin directory, the only difference in the path will be if you invoke a tool that is part of the k framework, in which case you are guaranteed to get a version of k consistent with the version you originally invoked, which is, I think, actually desirable.

[tothtamas28]

It seems that Tamash is running into some issue because of that.

The particular issue I have is the following. Consider the following dummy post-processing script:

# ./script
echo VIRTUAL_ENV=$VIRTUAL_ENV
echo PATH=$PATH
which python3
python3 -c 'from pyk.kast import KVariable ; print(KVariable("hello"))'

(Obviously, this is not a proper post-processing script, as its output is not well formed KAST JSON.)

In order to have the pyk module available, we can run it from the pyk project folder using Poetry (I ran it in a pyk CI docker container):

% poetry install --quiet && poetry run sh ./script

and the output, as expected, will be something like

VIRTUAL_ENV=/root/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.8
PATH=/root/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.8/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
/root/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.8/bin/python3
KVariable(name='hello', att=KAtt(atts=FrozenDict({})))

However, when ran as a post-process script like

% poetry install --quiet && poetry run kompile k-files/imp.k --post-process 'sh ./script'

the output becomes

[Error] Critical: Post-processing returned a non-zero exit code: 1
Stdout:
VIRTUAL_ENV=/root/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.8
PATH=/usr/lib/kframework/native/linux64:/usr/lib/kframework/../../bin:/root/.cache/pypoetry/virtualenvs/pyk-YghnWhM2-py3.8/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
/usr/lib/kframework/../../bin/python3

Stderr:
Traceback (most recent call last):
  File "<string>", line 1, in <module>
ModuleNotFoundError: No module named 'pyk'

That is, the pyk module cannot be imported, even though Poetry ensures the script is executed in a virtual environment where pyk is installed. My strong suspicion is that this is because in this case python3 resolves to /usr/lib/kframework/../../bin/python3 (i.e. /usr/bin/python3) due to the paths prepended to $PATH, and not to $VIRTUAL_ENV/bin/python3 as one would expect.

My opinion is the post-process scripts should be executed in the caller's environment (with perhaps a few documented additions that do not interfere with it), even if kompile itself needs to set up its own environment to work properly.

[dwightguth]

What you describe may be possible but it might be simpler simply to add a directory that only contains k binaries to the path instead.