CI gets stuck

Stream: Brownian motion

[Rémy Degenne]

Half of our CI runs get stuck on the Lint project step, where we get those 3 lines printed, and then nothing for a very long time (I don't know how long, I stopped one after 50 minutes):

Run env LEAN_ABORT_ON_PANIC=1 ~/.elan/bin/lake exe runLinter BrownianMotion
  env LEAN_ABORT_ON_PANIC=1 ~/.elan/bin/lake exe runLinter BrownianMotion
  shell: /usr/bin/bash -e {0}

Example: this run https://github.com/RemyDegenne/brownian-motion/actions/runs/19140278725/job/54703144152?pr=199

When I cancel and then restart the job, I usually get a successful Lint project step which is less than a minute.

[Rémy Degenne]

There was no problem with CI yesterday, but today I had to restart many runs.

[Rémy Degenne]

Any idea of what could be the cause?

[Bryan Gin-ge Chen]

I took a brief look at the logs / commits and didn't notice anything suspicious. I was hoping there was maybe a command line option you could add to make runLinter spit out more info but I didn't see one. This is maybe worth posting in #general so someone with more knowledge about linters can see it.

[Bryan Gin-ge Chen]

(I have a wild theory which is that there's some non-deterministic linter which is sometimes causing the runner to run out of memory and not respond anymore, but I don't know enough about our linters to know if this even makes sense.)

[Rémy Degenne]

Thanks for looking into it. I posted here: #general > CI stuck at Lint project step

[Yongxi Lin (Aaron)]

The CI for https://github.com/RemyDegenne/brownian-motion/pull/301 and https://github.com/RemyDegenne/brownian-motion/pull/303 get stuck for several times on the Lint project step with the following warning message:

Run env LEAN_ABORT_ON_PANIC=1 ~/.elan/bin/lake exe runLinter BrownianMotion
warning: manifest out of date: git revision of dependency 'mathlib' changed; use `lake update mathlib` to update it
warning: manifest out of date: git revision of dependency 'subverso' changed; use `lake update subverso` to update it

I tried lake update subverso in my terminal with the following error message:

error: /Users/mac/Documents/GitHub/brownian-motion/.lake/packages/subverso: revision not found 'master'

What can I do to fix this issue?

[Rémy Degenne]

I think the warnings are not related to the CI issue. The only solution I have for now is to restart CI (by clicking the restart button, or if you don't have that button by making a new commit). Around half of the times it gets stuck, but half of the time linting succeeds (in < 10 s).

[Yongxi Lin (Aaron)]

Both of them passes all the checks after I made several meaningless commits. They are now ready to review.

[Rémy Degenne]

I restarted CI for the latest commit to master 10 times, and the latest attempt is still stuck. That CI issue is becoming really annoying. I don't want to remove the linting step, but it is getting too difficult to go around the issue.

[Pietro Monticone]

I'll take a look at it later today.