Git issue with coqorg/coq:dev

[erikmd]

As discussed on Zulip, at least for MetaCoq we need to fix permissions already before the installation, otherwise installing dependencies via opam fails.

The sentence This is not an issue when relying on opam to build the Coq project. in the README might be incorrect with the newest git version. To me, it might be reasonable to run the chown by default in before_install.

Originally posted by @yforster in #85 (comment)

See also #85 (comment)

(as well as actions/checkout#766)

[erikmd]

FTR I noticed in https://tracker.debian.org/pkg/git that

• the fix for CVE-2022-24765 was released upstream in April 2022 (git 2.30.3)
• and was incorporated in Debian 11, bullseye-security in January 2023 (git 1:2.30.2-1+deb11u2),
• which explains that the issue showed up a bit later in Docker-Coq.

I'm busy upto tomorrow Friday but I'll push a new release of docker-coq-action by the end of the week to ensure no manual workaround is needed anymore.

Cc @JasonGross @mattam82 @proux01 FYI

[JasonGross]

Instead of running chown, it might be better to run

sudo chmod -R a=u .
git config --global --add safe.directory "*"

because chown might mess up future non-docker steps (I think chown gave me some issues with uploading artifacts?). Even better would be if the docker images could be configured to have a user (the default user?) have the same user and group ids as used on GitHub

[erikmd]

Even better would be if the docker images could be configured to have a user (the default user?) have the same user and group ids as used on GitHub.

I believe this is the other way around:

• the UID/GID of the default coq account in coqorg/coq images' filesystem is 1000:1000, which looks standard w.r.t. the ID of the main user in GNU/Linux distros.
• the UID/GID of the workspace in a GitHub container action is (UID=1001, GID=116), and it does not look like a good idea to pick this pair as default for Docker-Coq…

[erikmd]

@JasonGross

Instead of running chown, it might be better to run

sudo chmod -R a=u .
git config --global --add safe.directory "*"

Why not. This needs to be discussed. The git config won't be enough anyway, because as mentioned in our current README, compiling the projects with custom_script: … make … won't work given the permissions forbid writing in the current folder.

because chown might mess up future non-docker steps

Yes but I only see one possible such case, and I was precisely planning to cope with this issue by running:

  - name: Revert permissions
    # to avoid a warning at cleanup time
    if: ${{ always() }}
    run: sudo chown -R 1001:116 .  # <--

automatically with a post-entrypoint.

[JasonGross]

Yes but I only see one possible such case, and I was precisely planning to cope with this issue by running:

  - name: Revert permissions
    # to avoid a warning at cleanup time
    if: ${{ always() }}
    run: sudo chown -R 1001:116 .  # <--

automatically with a post-entrypoint.

This seems good to me