CI for 3rd party project

Stream: CI

[Riccardo Brasca]

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]

@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]

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]

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]

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

[Riccardo Brasca]

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]

Sorry, taking a look at it now!

[Riccardo Brasca]

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

[Mauricio Collares]

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]

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]

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]

Nice!

[Mauricio Collares]

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]

It now works, thanks!