The documentation page breaks?

Stream: mathlib4

[Gian Cordana Sanjaya]

Hello, it seems that the documentation page (https://leanprover-community.github.io/mathlib4_docs/index.html) breaks; I do not see the Mathlib folder. Could someone look into this issue? Thank you.

[David Renshaw]

Looks broken to me too.

[Eric Wieser]

I would guess this is a caching issue

[Bryan Gin-ge Chen]

Nothing is jumping out at me in the latest build log. For reference, here's a build log from 17 hours ago when presumably things were OK (?)

[Gian Cordana Sanjaya]

It was OK before, it just suddenly breaks in the last hour :sweat_smile:

[Bryan Gin-ge Chen]

I've triggered another run. When this finishes, hopefully things will be magically fixed?

[Aaron Liu]

Seems to have finished, but I still get a 404. Maybe I should wait a few minutes?

[Bryan Gin-ge Chen]

Unfortunately I think something is broken. It does look like a fairly beefy PR was merged into doc-gen4 about 10 hours ago so maybe there's something we need to update in our workflow?

cc: @David Thrane Christiansen

[David Thrane Christiansen]

A cursory glance looks like it worked. I'll investigate. Thanks for the ping!

[David Thrane Christiansen]

I figured it out. Sorry for the mistake, fix underway.

[Matt Diamond]

this fix may have been unfixed...

edit: sorry, never mind! misread the date of the thread and thought the discussion was from last night, not from an hour ago

thanks David Thrane Christiansen! (looks like this is the fix PR)

[David Thrane Christiansen]

Yes, I'm doing one more API cleanup before reporting success here :)

[David Thrane Christiansen]

All right, I'm running everything locally to make sure it's fixed. I'll let you know.

[David Thrane Christiansen]

They all worked locally too.

[Henrik Böving]

Fixed!

[Miyahara Kō]

Thank you very much, @David Thrane Christiansen!

[David Thrane Christiansen]

My apologies for the oversight, thank you for your understanding :)

This big PR causes doc-gen to create a SQLite database as an intermediate step towards the HTML, which will unlock lots of nice things going forwards.

[Miyahara Kō]

No problem at all. Also, through this, I learned that SQL is being used practically in Lean for the first time (at least to my knowledge). Database functionality is a major milestone towards becoming a practical programming language, so I'm very excited about this.