Expose output configuration via CLI arguments

[shonfeder]

• Followup to ADR on Apalache output files #1025
• Required for [BUG] Benchmark tests are broken #1059

This plumbs configuration of the OutputManager's settings
for the out-dir and write-intermediate fields through to the CLI.

This is needed for us to control the location and kind of output for the
benchmark tests, and was planned in #1025

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entry added to UNRELEASED.md for any new functionality

[shonfeder]

There's an issue with the docker container interacting with the file system in integration tests, but it doesn't have any impact on the core functionality added here, so I think this is ready for review, even while I figure out how to account for that detail.

[shonfeder]

Oof. The docker CI job has been given me hell here. Been trapped for hours now trying to reconciling between broken permissions on generated output files and broken users home/dir for creation of the config directory. :(

[shonfeder]

I have no idea why these new tests are failing. It seems clear it's a docker issue (cause the other integration tests are working as expected), and 2/3 aren't related to anything added in this pr.

I may need to try to re-engineer the way we're testing the docker images, but maybe it's a good idea to stop testing the docker container in our CI for now (it introduces a lot of IO/system-level complexity, and nearly doubles our longest CI time), until we can budget time to re-architect the dockerization? (And maybe just depricate this docker support in favor of some proper packaging?).

I'll thing about it a bit tomorrow after some rest.

[konnov]

Looking at the logs, I think the problem is in find -type f. Should not it be find -type d instead?

[shonfeder]

Looking at the logs, I think the problem is in find -type f. Should not it be find -type d instead?

Thanks for looking! I don’t think that’s the problem, however. I’m only meaning to list the files, not the dirs (since the dir names are different every run). Note that the same tests are passing on the non-docker integration tests, and there are like 3 other tests using the same find command that are passing even in the docker container.

[shonfeder]

My main conclusion after 2 days of fighting with the docerized integration tests, is there is way too much ad hoc complexity in the current way we are dockerization (and then testing) the application. I think it's taken me 3 times as long to debug the IO and environment interaction between the dockerized app and the tests as it took to add the feature introduced here. (This is mostly my own fault, as the complexity has gradually piled on over the last year+).

To illustrate, here's a brief summary of what we currently have to do to get the IO and environment threaded through correctly:

• in test/.envrc, we look for an envvar USE_DOCKER, which will then shadow the path to apalache-mc with an alias to script/run-docker.sh. This enables using the dockerized version of the app in the integration tests.

• in run-docker.sh, we are hard-coding in all environment variables that have to preserved inside of the docker container:

  cmd="docker run \
      -e OUT_DIR -e WRITE_INTERMEDIATE -e SMT_ENCODING \
      -e TLA_PATH -e JVM_ARGS \
      -e USER_ID=$(id -u) -e GROUP_ID=$(id -g) \
      --rm -v $(pwd):/var/apalache ${img} ${*}"
  

  without passing exposing these environment variables, we lose the functionality which these are meant to provide whenever the app is run in the container.

  Except the story is different with USER_ID and GROUP_ID...

• we are also dynamically fetching the user id and group id of the user who invokes the script. This has to be threaded through the container for reasons described shortly.

• the entrypoint of the docker container is bin/run-in-docker-container, where we are creating a new user and and group dynamically inside the container:

  # Create a user and group matching the invoking user
  # this is critical to avoid generating files with bad permissions
  USER_ID=${USER_ID:-1000}
  GROUP_ID=${GROUP_ID:-1000}
  groupadd --gid "$GROUP_ID" --non-unique apalache
  useradd --create-home --shell /bin/bash --uid "$USER_ID" --non-unique --gid "$GROUP_ID" apalache
  

  And then invoking the contained apalache with the new user:

  exec sudo --preserve-env=PATH --set-home -u apalache env /opt/apalache/bin/apalache-mc $@
  

  Without this crap, the files that are created by apalache inside of the docker container end up belonging to the user inside of the docker container, along with whatever permissions and groups they belong to. This means they can (and were before) ending up not being readable/writeable by the actual user running the docker container (without running as root, in the worst case).

• Note that we now have to pass the environment that holds in the docker container on to the new user. this is what is currently causing the few docker tests to fail! We are only forwarding the PATH here, so the JVM envvars and the apalache-specific envvars are getting stripped out of the environment.

There must be a better way!

However, I think getting to that better way will require some thought and reworking the architecture for this whole chain of nested environments.

(Note that these complications are not arising from anything particular added in this PR, they are entailed by the way our dockerization currently is configured and by the nature of docker itself, coming into conflict with the desire to test our new file outputting design. Moreover, these complications are not introduced by the new design for output files! Rather, afaict, we just weren't testing anything about the output files before, so we weren't hitting the permissions errors. I think this has always been a problem, tho I haven't confirmed by checking log file permissions produced by an older container image.)

So my current plan is:

• Get this PR fixed by patching up the missing environment vars.
• Merge in this PR, which will allow me to fix the benchmark tests.
• Then we can consider prioritization of a rewrite of the whole container story and maybe of the integration test harness.

[shonfeder]

Wow. I can't believe it finally worked... lol 😅

[shonfeder]

Just cleaning up some remnants from the move from dockerhub to github container registry.

[shonfeder]

The change here is removing the caveat about parent dirs needing to exist. I changed it so that qualification is not needed.

[shonfeder]

This is just due to an update of depss in our nix dev-shell (only used in integration test currently).

[shonfeder]

This just fixes a problem I was hitting on my machine, but would likely impact other OCaml users

[rodrigo7491]

LGTM