can docker-coq-action share a container throughout a multiple-step job? (`container: coqorg/coq`, `actions/checkout` can't) #88

JasonGross · 2023-12-25T09:06:35Z

When running actions/checking with container: coqorg/coq:dev, I see

/usr/bin/docker exec  d2f4cc80928d9913b66a607fd95b3abc47ed3b5a78234ed06151b3bcd6260342 sh -c "cat /etc/*release | grep ^ID"
node:internal/fs/sync:78
  return binding.openSync(
                 ^

Error: EACCES: permission denied, open '/__w/_temp/_runner_file_commands/save_state_e59de318-2ebd-4430-adee-f74fc8e00eb1'
    at Object.open (node:internal/fs/sync:78:18)
    at Object.openSync (node:fs:565:17)
    at Object.writeFileSync (node:fs:2288:35)
    at Object.appendFileSync (node:fs:2350:6)
    at Object.issueFileCommand (/__w/_actions/actions/checkout/v4/dist/index.js:2967:8)
    at Object.saveState (/__w/_actions/actions/checkout/v4/dist/index.js:2884:31)
    at 8647 (/__w/_actions/actions/checkout/v4/dist/index.js:2343:10)
    at __nccwpck_require__ (/__w/_actions/actions/checkout/v4/dist/index.js:18273:43)
    at 2565 (/__w/_actions/actions/checkout/v4/dist/index.js:146:34)
    at __nccwpck_require__ (/__w/_actions/actions/checkout/v4/dist/index.js:18273:43) {
  errno: -13,
  code: 'EACCES',
  syscall: 'open',
  path: '/__w/_temp/_runner_file_commands/save_state_e59de318-2ebd-4430-adee-f74fc8e00eb1'
}

Node.js v20.8.1

How do I get this image working?

The text was updated successfully, but these errors were encountered:

JasonGross · 2023-12-25T21:57:32Z

Would it be feasible to change the uid and gid to 1001 and 127 respectively to match github runners? Or at least to make docker run -it --user root coqorg/coq:dev /bin/bash work (rather than fail with [ERROR] Opam has not been initialised, please run `opam init') by symlinking /home/root/.opam and /home/root/.bashrc to the corresponding files in /home/coq?

JasonGross · 2023-12-25T23:39:29Z

See also actions/checkout#1576

erikmd · 2023-12-29T22:03:42Z

Thanks @JasonGross

Would it be feasible to change the uid and gid to 1001 and 127 respectively to match github runners? Or at least to make docker run -it --user root coqorg/coq:dev /bin/bash work (rather than fail with [ERROR] Opam has not been initialised, please run `opam init') by symlinking /home/root/.opam and /home/root/.bashrc to the corresponding files in /home/coq?

BTW where is documented this GID=127 ? IIRC, the github action workdir has GID=116

~~From the time being, I partly replied here:~~
~~actions/checkout#1576 (comment)~~

↓

Hi @JasonGross !
Thanks for opening these two issues! I'm in vacation now and away from keyboard this WE so I won't be able to commit much tonight (apart from pushing the release for the latest coq 8.19).
I'll be very happy to discuss what would be the proper fix-or-workaround with you after Jan 05.
Meanwhile, some comments:

I have no control over the set up of the docker file, so I cannot change the default userid (1000) to match the actions uid (1001)

Yes. But I disagree changing this , notably because:

it would be a non-trivial non-backwards-compatible change
the 1001 uid is specific to github actions,
1000:1000 is important for end users relying on Docker CLI (you know, to be able to do sudo docker run --rm -it -v "$PWD:$PWD" -w "$PWD" coqorg/coq:dev coq_makefile -f _CoqProject -o Makefile and so on; without a permission mismatch given 1000 is usually the uid of the first user in Linux distros)

cannot pass --user root because the root account on the docker image is broken in login mode,

Not exactly, there is an entrypoint, but you can certainly override it:

docker run -it --user root coqorg/coq:dev --entrypoint=/bin/sh

In any case, future steps need to be logged in as the coq (1000) user, not root, because opam is only set up for that user.

Sure, but TTBOMK, installing an opam switch for the root user is somewhat deprecated and would raise warnings.

Depending on your needs, you might be able to turn the /home/coq/.opam user switch into a system-wide switch by using $OPAMROOT

I have not found a way to change the host uid to 1000 (is there a way to tell github actions to do this?)

Not sure. If it's possible, I guess it should be documented…

I'd rather not pin to actions/checkout@v3.0.2, seems like bad practice and might open me to security issues

Sure. But just to have more insight:

what are the main use cases you aim at doing this? (maybe among these new use cases, some could be added to docker-coq-action)
do you know where is documented the "init script" of actions/checkout that requires USER root ?

JasonGross · 2023-12-30T02:11:18Z

Not exactly, there is an entrypoint, but you can certainly override it:

docker run -it --user root coqorg/coq:dev --entrypoint=/bin/sh

I see

$ docker run -it --user root coqorg/coq:dev --entrypoint=/bin/sh
[WARNING] Running as root is not recommended
[ERROR] Opam has not been initialised, please run `opam init'

Does this invocation actually work for you?

JasonGross · 2023-12-30T02:14:09Z

what are the main use cases you aim at doing this? (maybe among these new use cases, some could be added to docker-coq-action)

I'd like to have a single docker container running in the background that is shared between multiple steps of the same job, much like having container: coqorg/coq:dev or similar for the entire job would do.

Also, I would like to be able to share more code between testing on Docker coq, Alpine, Arch Linux, Debian, etc. If I can set it up so that the only difference between these platforms is

passing a different argument to container: in my workflow, and
invoking a different script to set up the system dependencies, etc, on the container

that would be ideal.

JasonGross · 2023-12-30T02:18:15Z

do you know where is documented the "init script" of actions/checkout that requires USER root ?

There's a "Detailed Summary" section of actions/checkout#956 that explains why having either USER root or uid 1001 results in success. Basically, the issue is that some parts of the checkout action run outside the docker container, while other parts run inside, and the parts that run inside avoid "permission denied" only if either uid matches the outside uid or the user is root. I personally think actions/checkout should fix this on their side and support the use of sudo to escalate privileges in the container.

erikmd · 2023-12-30T11:51:46Z

Does this invocation actually work for you?

Yes, but with the --entrypoint option earlier in the command line (sorry for the "typo" in my previous comment):

docker run -it --user root --entrypoint /bin/bash coqorg/coq:dev

erikmd · 2023-12-30T11:53:30Z

I'd like to have a single docker container running in the background that is shared between multiple steps of the same job, much like having container: coqorg/coq:dev or similar for the entire job would do.

OK, good point.

Also, I would like to be able to share more code between testing on Docker coq, Alpine, Arch Linux, Debian, etc. If I can set it up so that the only difference between these platforms is (…) invoking a different script to set up the system dependencies, etc, on the container

I'm not sure I understand what you mean! the Docker-Coq containers do have a Linux distro by themselves (Debian)

JasonGross · 2023-12-31T01:30:27Z

Hmmm, I'm not sure how to get the entry point working. According to stack overflow, it doesn't seem to be possible to override the entrypoint when specifying a container to use. Maybe I need to create a custom docker image here or something?

Also, I would like to be able to share more code between testing on Docker coq, Alpine, Arch Linux, Debian, etc. If I can set it up so that the only difference between these platforms is (…) invoking a different script to set up the system dependencies, etc, on the container

I'm not sure I understand what you mean! the Docker-Coq containers do have a Linux distro by themselves (Debian)

I mean that in addition to testing my code against coqorg/coq:dev, I also want to test my code against the system-packaged version of Coq on Debian, Alpine, ArchLinux, etc. It'd be nice to reuse workflow code between these platforms

erikmd · 2024-01-04T18:14:42Z

Hi!

it doesn't seem to be possible to override the entrypoint when specifying a container to use. Maybe I need to create a custom docker image here or something?

I don't think so (anyway, that would really look like some over-engineering to me… IMO, a default entrypoint such as the current one should never be a blocker, nor justify creating and maintaining custom images… just for removing the entrypoint; one should either fix the limitation of the platform, or find a good workaround)

can you test something like this?

docker run -it --user root -e OPAMROOT=/home/coq/.opam coqorg/coq:dev /bin/bash -c 'eval $(opam env); exec /bin/bash' bash

erikmd · 2024-01-04T18:16:26Z

I mean that in addition to testing my code against coqorg/coq:dev, I also want to test my code against the system-packaged version of Coq on Debian, Alpine, ArchLinux, etc. It'd be nice to reuse workflow code between these platforms

Ah OK, I understand better.

But IINM, regarding workflow code reuse, I guess you already have a bash script, compatible with both scenarios…
so isn't the custom_script: feature of docker-coq-action enough for your use case?
otherwise, what is missing/blocking?

JasonGross · 2024-01-06T14:10:25Z

just for removing the entrypoint; one should either fix the limitation of the platform

Yeah, I think that would be ideal, if I can convince GH Actions to support this...

can you test something like this?

docker run -it --user root -e OPAMROOT=/home/coq/.opam coqorg/coq:dev /bin/bash -c 'eval $(opam env); exec /bin/bash' bash

This works locally, at least, thanks!

But IINM, regarding workflow code reuse, I guess you already have a bash script, compatible with both scenarios…
so isn't the custom_script: feature of docker-coq-action enough for your use case?
otherwise, what is missing/blocking?

For workflow code reuse, yes. The main missing feature is not having to reinstall dependencies / set up the container at every job step, and still getting nice top-level grouping.

erikmd · 2024-01-09T00:39:48Z

The main missing feature is not having to reinstall dependencies / set up the container at every job step, and still getting nice top-level grouping.

Oh, I believe I see what you mean. You'd like to spin successively several docker-coq-actions with the same coq/ocaml, and only pull/setup the docker-coq-action container once. Right?

erikmd · 2024-01-09T00:45:03Z

AFAICT, currently, the image (not the container) is already reused: thanks to these lines:

docker-coq-action/entrypoint.sh

Lines 198 to 204 in 1c523ff

    
           docker image inspect "$COQ_IMAGE" --format="Reusing existing local image." || docker pull "$COQ_IMAGE" 
        
           endGroup 
        
           ## Note to docker-coq-action maintainers: Run ./helper.sh gen & Copy min.sh 
        
           # shellcheck disable=SC2046,SC2086 
        
           docker run --pull=never -i --init --rm --name=COQ $( [ -n "$INPUT_EXPORT" ] && printf -- "-e %s " $INPUT_EXPORT ) -e WORKDIR="$WORKDIR" -e PACKAGE="$PACKAGE" \

the pull of the same $COQ_IMAGE is only done once.

I don't know how easy it is to do more reuse… but anyway, I'm interested to discuss this. Cc @Zimmi48 FYI

All in all, docker-coq-action is just a GHA version of the Façade pattern, with a syntax à la Travis CI, for Docker containers in general (not limited to Coq). If we can find a nice extension that preserves backwards compatibility, I'm up for adding it.

JasonGross · 2024-01-09T09:25:09Z

The main missing feature is not having to reinstall dependencies / set up the container at every job step, and still getting nice top-level grouping.

Oh, I believe I see what you mean. You'd like to spin successively several docker-coq-actions with the same coq/ocaml, and only pull/setup the docker-coq-action container once. Right?

I know the pull is already shared, but it's still the case that if I have to, e.g., install 10 minutes worth of Coq dependencies via opam to run my job, I need to do this on every step, or I need to have just one step.

erikmd · 2024-01-15T09:57:53Z

Hi @JasonGross, Thanks for your feedback.

I believe it would be feasible to add some YAML Boolean in docker-coq-action's interface, e.g.:

steps:
  - uses: actions/checkout@v3
  - uses: coq-community/docker-coq-action@v1
    with:
      opam_file: 'folder/coq-proj.opam'
      coq_version: ${{ matrix.coq_version }}
      ocaml_version: ${{ matrix.ocaml_version }}
      non_ephemeral: true

Concretely, this would remove the docker run --rm CLI option and pass the -d option instead.

Questions (Cc @Zimmi48, feel free to react as well if ever you have comments):

does the non_ephemeral keyword looks good to you? or do you have other suggestions? (AFAIAC, I prefer keywords that suggest that this option is not the default recommended one, given for example that ephemeral containers are generally recommended in CI)
don't you think it would be a good invariant to require that two successive coq-community/docker-coq-action@v1 steps with non_ephemeral: true have the same Docker image name ?, e.g. so that the following raise an error:
```
- uses: coq-community/docker-coq-action@v1
  with:
    non_ephemeral: true
    custom_image: 'coqorg/coq:dev'
    custom_script: |
      …
- uses: coq-community/docker-coq-action@v1
  with:
    non_ephemeral: true
    custom_image: 'coqorg/coq:latest'
    custom_script: |
      …
```
after some quick test, this invariant could be checked using docker inspect -f '{{.Config.Image}}' COQ
Currently, the container name is fixed: "COQ" (implying only one container can run in the background);
would you be interested to run several different containers in the background?
If the answer to 3. is yes, we could restrict the "COQ" container name to ephemeral containers,
but we'd need to specify the container naming convention:
(4.1) either deduced from the image, replacing / with -- and : with .. for instance (but this is ugly),
(4.2) or specified by the user with a container_name: '…' keyword (with '…' ≠ 'COQ')
Finally, a post-processing step would be required to trigger docker rm -f at the end of the job.

Thoughts? other questions?

JasonGross · 2024-01-15T11:01:27Z

I like the direction this goes in, but I think the configuration could be simplified to just having a single container_name or non_ephemeral_container_name option.

The container is ephemeral iff the container_name is '', in which case the container is named COQ.
Error on container_name: COQ.
If container_name is given explicitly and the container already exists, maybe error if the image/version is explicitly given but does not match the existing container?

erikmd · 2024-01-15T15:04:57Z

Hi @JasonGross, thanks for your update! I agree with your suggestion.
Maybe it's unneeded to have a keyword that verbose such as non_ephemeral_container_name,
so let's stick to container_name for now.
I will prepare a PR in the upcoming days (not 100% sure that the feature is feasible but I'm confident enough).
Then, @Zimmi48 will be able review that PR (especially for the accompanying documentation and the container_name phrasing) before we obtain a new release.

erikmd · 2024-01-15T15:08:55Z

Meanwhile @JasonGross, feel free to think if you'd like that I put in the README.md documentation (later on) a hyperlink to a project/workflow you maintain where this feature could be useful: indeed that would be a useful, authentic example.
(There's no rush anyway.)

erikmd · 2024-01-16T15:08:25Z

Hi @JasonGross, given this issue led to a docker-coq-action wishlist, I'm migrating the issue now.

erikmd · 2024-03-06T21:38:08Z

Dear @JasonGross, sorry for the lag,

but I plan to start implementing it next week…

so question for you: will this feature still be useful from you side?

as in this case, you'll have the "privilege" to be the first tester ;)

Cheers

JasonGross · 2024-03-07T00:03:19Z

Yes, it will still be useful! (Though I won't have time to test this for a bit)

erikmd changed the title ~~image does not work with actions/checkout~~ can docker-coq-action share a container throughout a multiple-step job? (container: coqorg/coq, actions/checkout can't) Jan 16, 2024

erikmd transferred this issue from coq-community/docker-coq Jan 16, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

can docker-coq-action share a container throughout a multiple-step job? (`container: coqorg/coq`, `actions/checkout` can't) #88

can docker-coq-action share a container throughout a multiple-step job? (`container: coqorg/coq`, `actions/checkout` can't) #88

JasonGross commented Dec 25, 2023

JasonGross commented Dec 25, 2023

JasonGross commented Dec 25, 2023

erikmd commented Dec 29, 2023 •

edited

JasonGross commented Dec 30, 2023

JasonGross commented Dec 30, 2023

JasonGross commented Dec 30, 2023

erikmd commented Dec 30, 2023 •

edited

erikmd commented Dec 30, 2023 •

edited

JasonGross commented Dec 31, 2023

erikmd commented Jan 4, 2024 •

edited

erikmd commented Jan 4, 2024

JasonGross commented Jan 6, 2024

erikmd commented Jan 9, 2024 •

edited

erikmd commented Jan 9, 2024 •

edited

JasonGross commented Jan 9, 2024 •

edited

erikmd commented Jan 15, 2024

JasonGross commented Jan 15, 2024 •

edited

erikmd commented Jan 15, 2024 •

edited

erikmd commented Jan 15, 2024 •

edited

erikmd commented Jan 16, 2024

erikmd commented Mar 6, 2024

JasonGross commented Mar 7, 2024

can docker-coq-action share a container throughout a multiple-step job? (container: coqorg/coq, actions/checkout can't) #88

can docker-coq-action share a container throughout a multiple-step job? (container: coqorg/coq, actions/checkout can't) #88

Comments

JasonGross commented Dec 25, 2023

JasonGross commented Dec 25, 2023

JasonGross commented Dec 25, 2023

erikmd commented Dec 29, 2023 • edited

JasonGross commented Dec 30, 2023

JasonGross commented Dec 30, 2023

JasonGross commented Dec 30, 2023

erikmd commented Dec 30, 2023 • edited

erikmd commented Dec 30, 2023 • edited

JasonGross commented Dec 31, 2023

erikmd commented Jan 4, 2024 • edited

erikmd commented Jan 4, 2024

JasonGross commented Jan 6, 2024

erikmd commented Jan 9, 2024 • edited

erikmd commented Jan 9, 2024 • edited

JasonGross commented Jan 9, 2024 • edited

erikmd commented Jan 15, 2024

JasonGross commented Jan 15, 2024 • edited

erikmd commented Jan 15, 2024 • edited

erikmd commented Jan 15, 2024 • edited

erikmd commented Jan 16, 2024

erikmd commented Mar 6, 2024

JasonGross commented Mar 7, 2024

can docker-coq-action share a container throughout a multiple-step job? (`container: coqorg/coq`, `actions/checkout` can't) #88

can docker-coq-action share a container throughout a multiple-step job? (`container: coqorg/coq`, `actions/checkout` can't) #88

erikmd commented Dec 29, 2023 •

edited

erikmd commented Dec 30, 2023 •

edited

erikmd commented Dec 30, 2023 •

edited

erikmd commented Jan 4, 2024 •

edited

erikmd commented Jan 9, 2024 •

edited

erikmd commented Jan 9, 2024 •

edited

JasonGross commented Jan 9, 2024 •

edited

JasonGross commented Jan 15, 2024 •

edited

erikmd commented Jan 15, 2024 •

edited

erikmd commented Jan 15, 2024 •

edited