coq-community / docker-coq-action

GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]
MIT License
12 stars 4 forks source link

Git issue with coqorg/coq:dev #86

Open erikmd opened 1 year ago

erikmd commented 1 year ago

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 https://github.com/coq-community/docker-coq-action/issues/85#issuecomment-1480816451

See also https://github.com/coq-community/docker-coq-action/pull/85#issuecomment-1481139961

(as well as https://github.com/actions/checkout/issues/766)

erikmd commented 1 year ago

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

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 commented 1 year ago

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 commented 1 year ago

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:

erikmd commented 1 year ago

@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 commented 1 year ago

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