Stream: Coq users

Topic: GitHub actions CI with make rather than opam


view this post on Zulip Tej Chajed (Nov 17 2020 at 18:08):

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

view this post on Zulip Tej Chajed (Nov 17 2020 at 18:09):

@Théo Zimmermann and @Erik Martin-Dorel if you can take a look I'd appreciate it

view this post on Zulip Théo Zimmermann (Nov 17 2020 at 18:15):

A minor note is the fact that opam_file is optional when you use a custom_script.

view this post on Zulip Théo Zimmermann (Nov 17 2020 at 18:17):

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.

view this post on Zulip Théo Zimmermann (Nov 17 2020 at 18:19):

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 .

view this post on Zulip Tej Chajed (Nov 17 2020 at 18:19):

ah that's what I concluded, too

view this post on Zulip Tej Chajed (Nov 17 2020 at 18:19):

we have something along those lines in the Travis config, sudo chown -R coq:coq /home/coq/demo

view this post on Zulip Tej Chajed (Nov 17 2020 at 18:23):

ok we have a build running, seems promising that it will work out - thanks for taking a look!

view this post on Zulip Erik Martin-Dorel (Nov 17 2020 at 23:56):

Hi @Tej Chajed, BTW you might want to revert the permission back with sudo chown …, like this:

https://github.com/erikmd/docker-run-github-workflow-example/blob/b30fbadb7a19078019791af76dcd8fdd06eb3a50/.github/workflows/test.yml#L35

in order to avoid a (minor) warning at cleanup time:

I will open an issue in docker-coq-action to better document this.

view this post on Zulip Erik Martin-Dorel (Nov 17 2020 at 23:57):

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

view this post on Zulip Tej Chajed (Nov 18 2020 at 00:33):

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.

view this post on Zulip Erik Martin-Dorel (Nov 25 2020 at 22:48):

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: Oct 13 2024 at 01:02 UTC