Enable usage of github runner file commands

[JasonGross]

This should (hopefully) allow the use of things like >> $GITHUB_OUTPUT (when such variables are passed through via export:)

[erikmd]

Hi @JasonGross, thanks!

GITHUB_ENV wasn't available due to Docker's isolation, so the implementation of your PR looks sensible.

A few suggestions:

• Given GITHUB_* prefix is reserved, just to be on the safe side, maybe you could rename GITHUB_RUNNER_FILE_COMMANDS_DIR to DIR_GITHUB_RUNNER_FILE_COMMANDS (?)

• I believe you already did some tests, and I will be happy to merge the PR, but ideally, it would be very nice if you could add 1 integration test (involving GITHUB_ENV and export: 'GITHUB_ENV') in python-demo.yml or coq-demo.yml within the PR; could you take a look?

• Finally, do you believe the PR is enough for GITHUB_OUTPUT as well?
  or should we do something like DIR_GITHUB_RUNNER_FILE_COMMANDS_2="$(dirname "$GITHUB_OUTPUT")" along with some if [ "$DIR_GITHUB_RUNNER_FILE_COMMANDS_2" = "$DIR_GITHUB_RUNNER_FILE_COMMANDS" ]; then
Add (-v "$DIR_GITHUB_RUNNER_FILE_COMMANDS:$DIR_GITHUB_RUNNER_FILE_COMMANDS")
else Add (-v "$DIR_GITHUB_RUNNER_FILE_COMMANDS:$DIR_GITHUB_RUNNER_FILE_COMMANDS"
-v "$DIR_GITHUB_RUNNER_FILE_COMMANDS_2:$DIR_GITHUB_RUNNER_FILE_COMMANDS_2") ?

[JasonGross]

* Given `GITHUB_*` prefix is reserved, just to be on the safe side, maybe you could rename `GITHUB_RUNNER_FILE_COMMANDS_DIR` to `DIR_GITHUB_RUNNER_FILE_COMMANDS` (?)

Done, thanks for the suggestion

* I believe you already did some tests, and I will be happy to merge the PR, but **ideally**, it would be very nice if you could add 1 integration test (involving `GITHUB_ENV` and `export: 'GITHUB_ENV'`) in [python-demo.yml](https://github.com/coq-community/docker-coq-action/blob/master/.github/workflows/python-demo.yml) or [coq-demo.yml](https://github.com/coq-community/docker-coq-action/blob/master/.github/workflows/coq-demo.yml) within the PR; could you take a look?

I haven't really tested this, so I extended the env test in the Coq demo to write to GitHub step summary (this should be the easiest one to observe the effect of), let's see if it works here

* Finally, do you believe the PR is enough for `GITHUB_OUTPUT` as well?
  **or** should we do something like `DIR_GITHUB_RUNNER_FILE_COMMANDS_2="$(dirname "$GITHUB_OUTPUT")"` along with some `if [ "$DIR_GITHUB_RUNNER_FILE_COMMANDS_2" = "$DIR_GITHUB_RUNNER_FILE_COMMANDS" ]; then`
  `Add (-v "$DIR_GITHUB_RUNNER_FILE_COMMANDS:$DIR_GITHUB_RUNNER_FILE_COMMANDS")`
  `else Add (-v "$DIR_GITHUB_RUNNER_FILE_COMMANDS:$DIR_GITHUB_RUNNER_FILE_COMMANDS"`
  `-v "$DIR_GITHUB_RUNNER_FILE_COMMANDS_2:$DIR_GITHUB_RUNNER_FILE_COMMANDS_2")`  ?

I think all the runner file commands should be based in the same directory. Currently this seems to be the case, and if this changes, we can either add a couple more dirnames to get to higher ancestors or we can add the other variables as needed.

[JasonGross]

Hm, I guess by default we have ownership issues:

tee: /github/file_commands/step_summary_dd7ed627-2f9d-45dc-99d8-0cf3861b9e4f: Permission denied

Should we chmod the relevant files?

[JasonGross]

Hm, chmod a=u fails at https://github.com/coq-community/docker-coq-action/actions/runs/9035969091/job/24831820394?pr=90, let's try a+rw at https://github.com/coq-community/docker-coq-action/actions/runs/9036006653/job/24831950493

[JasonGross]

Current test at https://github.com/coq-community/docker-coq-action/actions/runs/9036006653/job/24831950493 fails with
tee: /github/file_commands/step_summary_f4dc0b5a-cefc-48ac-8907-26c585553ed1: Permission denied
Not sure what's going on

[JasonGross]

I am thoroughly confused by https://github.com/coq-community/docker-coq-action/actions/runs/9036191567/job/24832574488?pr=90#step:4:614
tee: /github/file_commands/step_summary_1a978c3f-c1ac-4779-804e-e39da1477cd2: Permission denied

https://github.com/coq-community/docker-coq-action/actions/runs/9036191567/job/24832574488?pr=90#step:4:391
$ ls -la /github/file_commands
total 16
drwxrwxrwx 2 1001 127 4096 May 10 18:03 .
drwxrwxrwx 6 root root 4096 May 10 18:03 ..
-rw-rw-rw- 1 1001 127 0 May 10 18:03 step_summary_1a978c3f-c1ac-4779-804e-e39da1477cd2
-rw-rw-rw- 1 1001 127 0 May 10 18:03 step_summary_491fb03e-fd5c-481f-bd5c-566962b3d076
-rw-rw-rw- 1 1001 127 0 May 10 18:03 step_summary_d03ec76f-0fb3-4d14-ad1e-f237c1a49825

So the file seems to exist and is writable...

Any ideas @erikmd

[JasonGross]

I see

• (script @ line 15) $ ls -la /github/file_commands/step_summary_8257a3b8-4aea-4b08-87e9-4967aeaf2803
  ls: cannot access '/github/file_commands/step_summary_8257a3b8-4aea-4b08-87e9-4967aeaf2803': No such file or directory
  From inside the docker image. Is the -v argument somehow not getting passed, or is it getting ignored? Or do I have to bind /github if I want to bind a subdirectory of it?

[erikmd]

Hi Jason, thanks for your experiments! I'll take a look tonight and let you know...

[JasonGross]

Latest results: the directory exists but looks empty from inside docker (according to find). No idea why tee wouldn't be able to create a file, though. I've run out of time to debug this, I hope you can figure out what's going on easily.

[JasonGross]

A little bit more debugging:
Outside docker, ls -la /github/file_commands says

  total 16
  drwxrwxrwx    2 1001     127           4096 May 10 20:25 .
  drwxrwxrwx    6 root     root          4096 May 10 20:25 ..
  -rw-rw-rw-    1 1001     127              0 May 10 20:25 add_path_02228d2c-c168-4d89-9304-b95e600b9dbc
[...]

and ls -la /github/file_commands/.. says

  total 24
  drwxrwxrwx    6 root     root          4096 May 10 20:25 .
  drwxr-xr-x    1 root     root          4096 May 10 20:25 ..
  drwxrwxrwx    2 1001     127           4096 May 10 20:25 file_commands
[...]

Docker is invoked with docker run --pull=never -i --init --rm --name=COQ -e ex_var -e OPAMWITHTEST -e GITHUB_STEP_SUMMARY -e WORKDIR=. -e PACKAGE=coq-demo -v /home/runner/work/docker-coq-action/docker-coq-action:/github/workspace -w /github/workspace -v /github/file_commands:/github/file_commands coqorg/coq:latest /bin/bash --login -c [...] and then insider docker, ls -la /github says

  total 16
  drwxr-xr-x 4 root root 4096 May 10 20:26 .
  drwxr-xr-x 1 root root 4096 May 10 20:26 ..
  drwxr-xr-x 2 root root 4096 May 10 20:26 file_commands
  drwxr-xr-x 7 1001  127 4096 May 10 20:25 workspace

(why is the total 16 if there are only four things?) and ls -la /github/file_commands says

  total 8
  drwxr-xr-x 2 root root 4096 May 10 20:26 .
  drwxr-xr-x 4 root root 4096 May 10 20:26 ..

(why 8 if there is nothing but . and ..?) So it seems that somehow the permissions are getting reset or something?

[erikmd]

Hi @JasonGross, sorry for replying in-depth just now.

I think you are facing an issue directly related to a double-embedding of Docker.

I had already fixed something similar in e3df63e.

To be more precise:

1. GHA starts a build, using Docker. The complete command is available at the start of the job:

Details from this job

/usr/bin/docker run --name a37585f135444204c5f9a40cb2da24bd67470_dac428 --label 0a3758 --workdir /github/workspace --rm -e "INPUT_OPAM_FILE" -e "INPUT_CUSTOM_IMAGE" -e "INPUT_AFTER_SCRIPT" -e "INPUT_COQ_VERSION" -e "INPUT_OCAML_VERSION" -e "INPUT_BEFORE_INSTALL" -e "INPUT_INSTALL" -e "INPUT_AFTER_INSTALL" -e "INPUT_BEFORE_SCRIPT" -e "INPUT_SCRIPT" -e "INPUT_UNINSTALL" -e "INPUT_CUSTOM_SCRIPT" -e "INPUT_EXPORT" -e "HOME" -e "GITHUB_JOB" -e "GITHUB_REF" -e "GITHUB_SHA" -e "GITHUB_REPOSITORY" -e "GITHUB_REPOSITORY_OWNER" -e "GITHUB_REPOSITORY_OWNER_ID" -e "GITHUB_RUN_ID" -e "GITHUB_RUN_NUMBER" -e "GITHUB_RETENTION_DAYS" -e "GITHUB_RUN_ATTEMPT" -e "GITHUB_REPOSITORY_ID" -e "GITHUB_ACTOR_ID" -e "GITHUB_ACTOR" -e "GITHUB_TRIGGERING_ACTOR" -e "GITHUB_WORKFLOW" -e "GITHUB_HEAD_REF" -e "GITHUB_BASE_REF" -e "GITHUB_EVENT_NAME" -e "GITHUB_SERVER_URL" -e "GITHUB_API_URL" -e "GITHUB_GRAPHQL_URL" -e "GITHUB_REF_NAME" -e "GITHUB_REF_PROTECTED" -e "GITHUB_REF_TYPE" -e "GITHUB_WORKFLOW_REF" -e "GITHUB_WORKFLOW_SHA" -e "GITHUB_WORKSPACE" -e "GITHUB_ACTION" -e "GITHUB_EVENT_PATH" -e "GITHUB_ACTION_REPOSITORY" -e "GITHUB_ACTION_REF" -e "GITHUB_PATH" -e "GITHUB_ENV" -e "GITHUB_STEP_SUMMARY" -e "GITHUB_STATE" -e "GITHUB_OUTPUT" -e "RUNNER_OS" -e "RUNNER_ARCH" -e "RUNNER_NAME" -e "RUNNER_ENVIRONMENT" -e "RUNNER_TOOL_CACHE" -e "RUNNER_TEMP" -e "RUNNER_WORKSPACE" -e "ACTIONS_RUNTIME_URL" -e "ACTIONS_RUNTIME_TOKEN" -e "ACTIONS_CACHE_URL" -e "ACTIONS_RESULTS_URL" -e GITHUB_ACTIONS=true -e CI=true -v "/var/run/docker.sock":"/var/run/docker.sock" -v "/home/runner/work/_temp/_github_home":"/github/home" -v "/home/runner/work/_temp/_github_workflow":"/github/workflow" -v "/home/runner/work/_temp/_runner_file_commands":"/github/file_commands" -v "/home/runner/work/docker-coq-action/docker-coq-action":"/github/workspace" 0a3758:5f135444204c5f9a40cb2da24bd67470

2. The container's entrypoint.sh then runs an embedded Docker container.

But, the pwd command for instance, returns /github/… while this is a path only valid in the intermediate container, not a proper path from the host itself.

That's it for the logical explanation. Now I'll take a look at your latest commits.

[JasonGross]

Ah, I see, yes, that would fully explain the issue. So I guess just that path needs fixing somehow? And then one of us can just strip off all of my debugging commits / drop the extraneous stuff in the test file

[erikmd]

Yes, exactly! I'm going to push soonish

[erikmd]

Good news! the latest commit succeeded in this log:

https://github.com/coq-community/docker-coq-action/actions/runs/9039122047/job/24841442923?pr=90

I propose to keep the PR as-is for now, polish the test ASAP and do a release on Monday or so…

Thanks again @JasonGross for suggesting this feature!

[JasonGross]

New version looks good to me! Is there anything else to do before merging?

[erikmd]

I'll just polish the test, add some documentation (README.md), and squash-merge.

[erikmd]

@JasonGross Also contrarily to COQ_IMAGE, the variables GITHUB_OUTPUT / GITHUB_ENV are fairly standard... so unless you strongly object, I believe we should export them by default, without requiring the export: 'GITHUB_ENV' invocation...

[erikmd]

@JasonGross: the 2 PRs now go live in v1.5.0 & v1