Upstreaming dashboard

Stream: FLT

[Kevin Buzzard]

I just merged FLT#673, if we now have a new URL to look at then great.

[Yaël Dillies]

http://imperialcollegelondon.github.io/FLT/upstreaming (will start working in a few minutes)

[Matthew Jasper]

Or it would if the build didn't fail

[Ruben Van de Velde]

Error: Creating Pages deployment failed

Error: HttpError: Deployment request failed for d4d53cd1b6db8169e99c67fced54a69bd72a24bf due to in progress deployment. Please cancel 1d4371152a784f394094bd1ff7a7ceffcc6874a2 first or wait for it to complete.

[Ruben Van de Velde]

@Kevin Buzzard I think you can just restart the build at https://github.com/ImperialCollegeLondon/FLT/actions/runs/16598632967/job/46951764778

[Kevin Buzzard]

I clicked restart failed jobs

[Ruben Van de Velde]

Huh, that didn't work, but it seems to be a known issue: https://github.com/orgs/community/discussions/111260#discussioncomment-9102466

[Kevin Buzzard]

Feel free to tell me what to do next

[Ruben Van de Velde]

I hope the next time you push something it'll solve itself

[Kevin Buzzard]

You have anything in mind?

[Matthew Jasper]

It's finally up: https://imperialcollegelondon.github.io/FLT/upstreaming

[Matthew Jasper]

The assumptions files probably shouldn't be included though

[Ruben Van de Velde]

Yes, probably we should disallow axiom

[Kevin Buzzard]

Yes I had another go at FLT today. I'm sorry things are so slow at the minute, I had two weeks out of action and then a week picking up the pieces and fighting off emails. Some PRs to mathlib got merged and I've bumped today so at least that's progress.

[Kevin Buzzard]

My next goal is to review all the PRs which are ready.