documentation is two days old

Stream: mathlib4

[Junyan Xu]

The current #docs is built at commit 4671780 93d4ae6635c0c755c9f7368f9b99483d4557b7a6 which is 2 days weeks old. What happened?

[Bryan Gin-ge Chen]

I don't know why the docs are 2 weeks old, but the builds have been failing since yesterday starting with this run: https://github.com/leanprover-community/mathlib4_docs/actions/runs/13332948246/job/37241331810

[Kyle Miller]

That's the commit for the current lean-toolchain for mathlib, and v4.17.0-rc1 came out two weeks ago

[Kyle Miller]

It looks like the docs are two days old

[Kyle Miller]

(It'd be nice to have the mathlib commit too. #general > Mathlib docs index page @ 💬 )

[Kyle Miller]

Maybe this is the error?

error: no such file or directory (error code: 2)
  file: ./././../mathlib4/././Cache.lean

[Kyle Miller]

Coincidentally, two days ago this was merged, and that added Cache to the list of things to build

[Kyle Miller]

(pinging @Michael Rothgang)

[Bryan Gin-ge Chen]

Should we try reverting that commit until it's fixed?

[Bryan Gin-ge Chen]

I've created https://github.com/leanprover-community/mathlib4_docs/pull/7 to add CI on PRs which should hopefully catch things like this in the future.

[Michael Rothgang]

It looks like my PR was the cause of the breakage; revert it for now sounds reasonable. (And investigating why that fails...)

[Bryan Gin-ge Chen]

I've reverted the commit and have triggered a redeploy :fingers_crossed:

[Bryan Gin-ge Chen]

The docs should be updated now. I also merged my CI PR.