mathlib docs are broken

Stream: general

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4_docs/actions/runs/8926938562/job/24519149843 since we moved to 4.8

CC @David Thrane Christiansen

[Henrik Böving]

I know they are, it will be fixed soon ish. (More precisely I'm waiting for Mac to wake up to give me lake help^^)

[Henrik Böving]

Okay the change is deploying to the mathlib4_docs page now, I'll ping here when its there.

I made a few changes in doc-gen to make everything compile again so please tell me if something is weird (er than usual^^), in particular around structures and reducibility attributes.

A note to the doc-gen users: Now that lake precomputes the build tasks it seems to spend quite some amount of time on thinking about the build tasks involved when building docs now so it might seem that it initially hangs for a while, it doesnt! It's just thinking hard^^

@Mac Malone is there possibly a way to speed this up as well? It's currently computing just the build tree for quite a time here: https://github.com/leanprover-community/mathlib4_docs/actions/runs/8945355312/job/24574182855

[Henrik Böving]

Bing! docs are up

[Bolton Bailey]

The "source" links are all still broken for me

[Utensil Song]

Bolton Bailey said:

The "source" links are all still broken for me

Same 404 here. (And I have cleared the browser cache.)

The link should begin with https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/ but it begins with https://github.com/leanprover-community/mathlib4/blob/mathlib4/Mathlib/, missing the branch spec and having an extra mathlib4.

[Henrik Böving]

Aha yes, I'll investigate

[Henrik Böving]

Okay so for me locally it computes: https://github.com/leanprover-community/mathlib4/blob/c1f040b7f1014c9eda2f5b9accb7dca9ed7ae097/docs/Conv/Introduction.lean

which means its a CI issue /o\ this is gonna be fun

[Kevin Buzzard]

What better way to spend a bank holiday weekend than thinking about CI

[Henrik Böving]

I think I got it, let's wait for a run and see

[Henrik Böving]

Kevin Buzzard said:

What better way to spend a bank holiday weekend than thinking about CI

indeed, I was planning on spending my day doing homework instead!

[Henrik Böving]

Utensil Song said:

Bolton Bailey said:

The "source" links are all still broken for me

Same 404 here. (And I have cleared the browser cache.)

The link should begin with https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/ but it begins with https://github.com/leanprover-community/mathlib4/blob/mathlib4/Mathlib/, missing the branch spec and having an extra mathlib4.

it worked !

[Utensil Song]

Many thanks, I can confirm that it works now. :tada: