CI errors in "build pr-branch tools" step

Stream: mathlib4

[Bryan Gin-ge Chen]

Several PRs are now failing CI in the "build pr-branch tools" step, which was added in #26294:

• #PR reviews > #26060 Grassmannians @ 💬 (log)
• #26244 (log) was on the bors queue but is now blocked due to this.

Note that since the "Check {Mathlib, Tactic, Counterexamples, Archive}.lean" has if: always(), that seems to end up being the last step to fail when this occurs (probably we should do better error-handling there, since the error message doesn't always apply).

I won't be able to look at this in detail for a few hours, but if someone can figure out what's going on, I might be able to review+merge a fix quickly.

cc: @Johan Commelin

[Anatole Dedecker]

This is the same error as in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Failing.20CI/with/525466176, right?

[Bryan Gin-ge Chen]

I think they are distinct issues. That one has something to do with Cache and pops up in the "Post-Build Step" job.

[Vasilii Nesterov]

#26354 suffers from it too

[Damiano Testa]

Is the reason these tests fail that they are inside landrun? The analogous tests on the master branch work.

[Damiano Testa]

The error running lake build mathlib_test_executable appears to be

Building mathlib_test_executable...
info: plausible: cloning https://github.com/leanprover-community/plausible
error: external command 'git' exited with code 128

So, it looks like lake build is setting things up, but then git is unable to... download(?) and produces an error.

[Bryan Gin-ge Chen]

That's probably it... I'd forgotten about landrun. Is there any reasonable way to do the git clone in another step (mediated by e.g. actions/checkout) and then do the actual building in the sandbox?

[Damiano Testa]

There is a name: download dependencies step that has some version of landrun.

[Damiano Testa]

      - name: download dependencies
        # We need network access to download dependencies
        # We run this inside landrun, but restrict disk access.
        # Landrun argument notes:
        # - we give --rox access to `~/.elan` and `~/actions-runner/_work` (GitHub CI needs this)
        # - we give --unrestricted-network as we need this to download dependencies
        # - git needs read only access to `/etc`.
        shell: landrun --unrestricted-network --rox /etc --rox /usr --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT -- bash -euxo pipefail {0}
        run: |
          cd pr-branch
          lake env

[Damiano Testa]

Maybe we run name: build pr-branch tools (test) with the same setup?

[Damiano Testa]

Should we disable this step for now, while we think of a fix?

[Bryan Gin-ge Chen]

I think a separate step might work, but yes, let's disable the broken step for now: #26379

[Damiano Testa]

The workflow that was causing this issue has been reverted. If you had problems, try restarting CI and hopefully it should work.

[Robin Carlier]

Still broken in #26366, even after restarting and merging with master.

[Damiano Testa]

Isn't this the failure of the other thread?

[Sébastien Gouëzel]

It's not the same error. You're talking about the one from the thread of #mathlib4 > Failing CI @ 💬 (which is still not resolved), not the current one.

[Damiano Testa]

I have not had a chance to look at the other one, but it seems like it might require some lake modification, either in the code, or in the passed arguments.

[Damiano Testa]

Btw, a (good in my opinion) consequence of the new CI, is that merging master should not be necessary to get the "latest" CI actions.

[Robin Carlier]

Ah, my bad, sorry!