Jason Gross (May 20 2021 at 23:26): 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
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.
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.
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: Jun 09 2023 at 08:01 UTC