Zulip Chat Archive

Stream: CI

Topic: CI for 3rd party project


Riccardo Brasca (Apr 20 2022 at 08:47):

I use CI for 3rd party project in a small project with some students. Since today CI is failing with

/usr/bin/docker run --name b315d473a9926434fae944729100cfbba08_26e990 --label 294b31 --workdir /github/workspace --rm -e INPUT_REMOTE -e HOME -e GITHUB_JOB -e GITHUB_REF -e GITHUB_SHA -e GITHUB_REPOSITORY -e GITHUB_REPOSITORY_OWNER -e GITHUB_RUN_ID -e GITHUB_RUN_NUMBER -e GITHUB_RETENTION_DAYS -e GITHUB_RUN_ATTEMPT -e GITHUB_ACTOR -e GITHUB_WORKFLOW -e GITHUB_HEAD_REF -e GITHUB_BASE_REF -e GITHUB_EVENT_NAME -e GITHUB_SERVER_URL -e GITHUB_API_URL -e GITHUB_GRAPHQL_URL -e GITHUB_REF_NAME -e GITHUB_REF_PROTECTED -e GITHUB_REF_TYPE -e GITHUB_WORKSPACE -e GITHUB_ACTION -e GITHUB_EVENT_PATH -e GITHUB_ACTION_REPOSITORY -e GITHUB_ACTION_REF -e GITHUB_PATH -e GITHUB_ENV -e GITHUB_STEP_SUMMARY -e RUNNER_OS -e RUNNER_ARCH -e RUNNER_NAME -e RUNNER_TOOL_CACHE -e RUNNER_TEMP -e RUNNER_WORKSPACE -e ACTIONS_RUNTIME_URL -e ACTIONS_RUNTIME_TOKEN -e ACTIONS_CACHE_URL -e GITHUB_ACTIONS=true -e CI=true -v "/var/run/docker.sock":"/var/run/docker.sock" -v "/home/runner/work/_temp/_github_home":"/github/home" -v "/home/runner/work/_temp/_github_workflow":"/github/workflow" -v "/home/runner/work/_temp/_runner_file_commands":"/github/file_commands" -v "/home/runner/work/zsqrt2_eucl/zsqrt2_eucl":"/github/workspace" 294b31:5d473a9926434fae944729100cfbba08  "origin"
fatal: unsafe repository ('/github/workspace' is owned by someone else)
To add an exception for this directory, call:

    git config --global --add safe.directory /github/workspace
Updating mathlib branch lean-3.42.1 to match master
fatal: unsafe repository ('/github/workspace' is owned by someone else)
To add an exception for this directory, call:

    git config --global --add safe.directory /github/workspace

Is this my fault? Is there something I can do about it? Thanks!

Johan Commelin (Apr 20 2022 at 08:54):

@Riccardo Brasca Do the messages in this stream help?
https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/blueprint.20ci/near/279436983

Riccardo Brasca (Apr 20 2022 at 09:11):

It seems related, but I don't know exactly where to write these lines. It's not very important for my project, but we should maybe change the script in the doc page.

Mauricio Collares (Apr 20 2022 at 10:17):

This issue has the same root cause as the blueprint one, but since you're not using the TeX environment it might be enough to use the new (v3) checkout action

Mauricio Collares (Apr 20 2022 at 10:18):

At https://github.com/riccardobrasca/zsqrt2_eucl/blob/master/.github/workflows/lean_build.yml#L24

Riccardo Brasca (Apr 20 2022 at 11:39):

I get the same error with v3. Should I add

            git config --global --add safe.directory $GITHUB_WORKSPACE
            git config --global --add safe.directory `pwd`

somewhere? In any case thanks!

Mauricio Collares (Apr 20 2022 at 12:51):

Sorry, taking a look at it now!

Riccardo Brasca (Apr 20 2022 at 12:51):

I've tried like 40 random commits, don't be confused by my stupid tries

Mauricio Collares (Apr 20 2022 at 13:02):

It's a similar problem to the TeX environment, but slightly more annoying to fix downstream. The problem is that the update-versions-action action runs commands inside a Docker environment, so we need to add /github/workspace to the correct user's safe.directory, but there are no extension points for that. It might just be easier to fix the action.

Riccardo Brasca (Apr 20 2022 at 13:04):

I really have no idea how this works. Can you just confirm that the instructions given here are now wrong? If this is the case someone more skilled than me will hopefully fix them :D

Mauricio Collares (Apr 20 2022 at 13:09):

The instructions are correct in the sense that everything should go back to normal (with the same config) once https://github.com/leanprover-contrib/update-versions-action/pull/5 is merged.

Riccardo Brasca (Apr 20 2022 at 13:10):

Nice!

Mauricio Collares (Apr 20 2022 at 13:11):

If you want it working right now, you can change leanprover-contrib/update-versions-action@master to collares/update-versions-action@master in the "update branch" step, but please remember to change it back when the PR is merged :)

Riccardo Brasca (Apr 20 2022 at 14:07):

It now works, thanks!


Last updated: Dec 20 2023 at 11:08 UTC