Zulip Chat Archive

Stream: general

Topic: install elan fails in CI

Sebastian Ullrich (May 03 2022 at 08:03):

fixed

Yaël Dillies (May 03 2022 at 08:25):

@Sebastian Ullrich, it still fails for me :sad:

Eric Wieser (May 03 2022 at 08:29):

mathlib seems to puse Kha/elan for one of its jobs which doesn't contain the fix and leanprover/elan for the other which does

Sebastian Ullrich (May 03 2022 at 08:33):

Yeah, looks like a lazy cache

Yaël Dillies (May 03 2022 at 08:34):

What can I do? Send an empty commit?

Scott Morrison (May 03 2022 at 08:34):

I've restarted lots of jobs.

Eric Wieser (May 03 2022 at 08:34):

Until those two links above contain the same content there might not be anything you can do

Eric Wieser (May 03 2022 at 08:34):

I've made #13906

Eric Wieser (May 03 2022 at 08:35):

Let's cancel the current bors batch to get both those CI changes in

Eric Wieser (May 03 2022 at 08:36):

I think probably it will fail anyway

Eric Wieser (May 03 2022 at 08:46):

~~Hmm, although I cancelled the batch our CI runner is still churning away on it (https://github.com/leanprover-community/mathlib/actions/runs/2262661349), and~~ no other runners are available to merge the fix

Eric Wieser (May 03 2022 at 08:47):

I guess every single open PR will have to merge master - so there's little point in restarting any jobs

Sebastien Gouezel (May 03 2022 at 10:17):

It seems that something is still broken: now, bors fails on the linting and testing stages (but it succeeds on building mathlib).

Eric Wieser (May 03 2022 at 10:40):

Yeah, I'll fix the PR

Eric Wieser (May 03 2022 at 10:42):

I did the edits by hand in browser, but should have used the build script to generate them. As a result I missed one. Fixed now

Eric Wieser (May 03 2022 at 10:42):

I guess we should cancel all the pending batches so that bors does them all at once again?

Last updated: Dec 20 2023 at 11:08 UTC