I'm trying to set up GitHub Actions for Perennial, which builds with
make rather than using opam. In theory docker-coq-action should have no problem with that but I run into permissions issues that I don't really understand: https://github.com/mit-pdos/perennial/runs/1413709206?check_suite_focus=true
@Théo Zimmermann and @Erik Martin-Dorel if you can take a look I'd appreciate it
A minor note is the fact that
opam_file is optional when you use a
There's this note in the README though:
if you use the docker-coq images, the container user has UID=GID=1000 while the GitHub action workdir has (UID=1001, GID=116). This is not an issue when relying on opam to build the Coq project. Otherwise, you may want to use sudo in the container to change the permissions. You may also install additional Debian packages.
And this page completes this answer: If this UID does not match that of your CI provider environment, you may want to change the permissions of the cloned working directory at the beginning of the script, e.g. by doing
sudo chown -R coq:coq .
ah that's what I concluded, too
we have something along those lines in the Travis config,
sudo chown -R coq:coq /home/coq/demo
ok we have a build running, seems promising that it will work out - thanks for taking a look!
Hi @Tej Chajed, BTW you might want to revert the permission back with
sudo chown …, like this:
in order to avoid a (minor) warning at cleanup time:
I will open an issue in docker-coq-action to better document this.
also for completeness, note that GitHub actions generate a report for each run here: https://github.com/mit-pdos/perennial/actions/runs/368746310 - and these annotations (i.e., warnings) would be directly incorporated in the diff the case of a PR, see e.g. https://github.com/erikmd/docker-coq-github-action-demo/pull/5/files#diff-e46a037bd57fa9f651b2cdb547fde6605d7f7d7ce5c321c7872668e16c2c9f51
Cool, thanks Erik! I was so close to having this setup from when I was experimenting with self-hosted runners; I wish we had just switched over then. Documenting the permissions change for the GitHub action would indeed help.
Tej Chajed said:
Documenting the permissions change for the GitHub action would indeed help.
I've just opened a PR that we'll integrate soon: https://github.com/coq-community/docker-coq-action/pull/30 (Cc @Théo Zimmermann)
Last updated: Jan 27 2023 at 00:03 UTC