Stream: Coq devs & plugin devs

Topic: sudo broken on Coq CI docker images


view this post on Zulip Jason Gross (May 20 2021 at 23:26):

It seems like it's no longer possible to use Coq's CI docker images (such as registry.gitlab.com/coq/coq:bionic_coq-V2021-04-30-2b30c6dc00), since sudo is no longer found... What's up with this?
https://github.com/coq-community/run-coq-bug-minimizer/runs/2634834562?check_suite_focus=true#step:5:229

view this post on Zulip Théo Zimmermann (May 21 2021 at 10:09):

Did this use to work? I'm surprised because I don't think there was any change related to this in the Docker image and the base image is still the same (Ubuntu Bionic). Anyway, if this can be fixed by installing sudo in the Docker image, feel free to open a PR doing that on Coq's repo.

view this post on Zulip Théo Zimmermann (May 21 2021 at 12:48):

Did this issue appear simultaneously on Docker-Coq images (https://github.com/coq-community/docker-coq-action/issues/58) and on Coq's CI Docker images? If yes, that could have something to do with some other thing like GitHub Actions itself.

view this post on Zulip Jason Gross (May 21 2021 at 13:35):

Seems to be an issue only with Coq's CI docker images. I'll just install sudo myself on the bug minimizer script


Last updated: Oct 21 2021 at 21:03 UTC