Zulip Chat Archive

Stream: nightly-testing

Topic: mathlib4_docs failure

leanprover-community Monitor Runners Bot (Jan 24 2026 at 03:58):

:cross_mark: mathlib4_docs http:// on d4c01cba1d7432e0616e43fd4e454ac6c2b33d1c

Kim Morrison (Jan 24 2026 at 04:00):

This is new!

Bryan Gin-ge Chen (Jan 24 2026 at 04:02):

Yes! I happened to get a notification that the build was broken so I decided that it was time we had a bot for this as well. PR still in progress at mathlib4_docs#10

leanprover-community Monitor Runners Bot (Jan 24 2026 at 04:02):

:cross_mark: mathlib4_docs failure on e8c83fdcccf9766cc2cd540af5c7ac8e65601bbf

Bryan Gin-ge Chen (Jan 24 2026 at 04:05):

OK, I think this is working now (the SHA is not likely to be useful in diagnosing failures, but I left it in anyways). I think the current failure is expected since mathlib4 hasn't quite made it to v4.27.0, so I'll merge the above PR after #34346 lands.

Kim Morrison (Jan 24 2026 at 04:10):

Note the URL is empty.

Bryan Gin-ge Chen (Jan 24 2026 at 04:11):

I think the URL in the second run was OK?

leanprover-community Monitor Runners Bot said:

:cross_mark: mathlib4_docs failure on e8c83fdcccf9766cc2cd540af5c7ac8e65601bbf

leanprover-community Monitor Runners Bot (Jan 26 2026 at 08:07):

:cross_mark: mathlib4_docs failure on 2c62b348276f71ca1a0b5956c40ae0c8393b1c26

leanprover-community Monitor Runners Bot (Feb 02 2026 at 16:23):

:cross_mark: mathlib4_docs cancelled on 2c62b348276f71ca1a0b5956c40ae0c8393b1c26

leanprover-community Monitor Runners Bot (Feb 09 2026 at 16:21):

:cross_mark: mathlib4_docs failure on 2c62b348276f71ca1a0b5956c40ae0c8393b1c26

leanprover-community Monitor Runners Bot (Feb 19 2026 at 00:21):

:cross_mark: mathlib4_docs failure on 2c62b348276f71ca1a0b5956c40ae0c8393b1c26

leanprover-community Monitor Runners Bot (Feb 19 2026 at 08:14):

:cross_mark: mathlib4_docs failure on 2c62b348276f71ca1a0b5956c40ae0c8393b1c26

Bryan Gin-ge Chen (Feb 19 2026 at 16:44):

Should be fixed by #35542.

leanprover-community Monitor Runners Bot (Feb 24 2026 at 08:59):

:cross_mark: mathlib4_docs cancelled on 2c62b348276f71ca1a0b5956c40ae0c8393b1c26

leanprover-community Monitor Runners Bot (Feb 24 2026 at 16:24):

:cross_mark: mathlib4_docs failure on 2c62b348276f71ca1a0b5956c40ae0c8393b1c26

Bryan Gin-ge Chen (Feb 24 2026 at 16:26):

@Henrik Böving any idea what might be causing this?

error: DocGen4/Process/Attributes.lean:85:6: Unknown constant `Lean.ReducibilityStatus.instanceReducible`

Note: Inferred this name from the expected resulting type of `.instanceReducible`:
  ReducibilityStatus
error: DocGen4/Process/Attributes.lean:172:4: Unknown constant `Lean.ReducibilityStatus.instanceReducible`

Note: Inferred this name from the expected resulting type of `.instanceReducible`:
  ReducibilityStatus
error: Lean exited with code 1

Henrik Böving (Feb 24 2026 at 16:27):

That constant was recently renamed on master https://github.com/leanprover/lean4/blob/master/src/Lean/ReducibilityAttrs.lean#L34

Last updated: Feb 28 2026 at 14:05 UTC