Zulip Chat Archive

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (d55a0757fac143156ac878cc289a7ff989126b2e).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Kim Morrison (Aug 27 2025 at 02:32):

This is still a work-in-progress; @Anne Baanen will let us know when we should start looking at the failure messages for real!

github mathlib4 bot (Aug 28 2025 at 02:35):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (7ac4458414b1b1f9a3727a7ff811d78c57a5b2db).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Aug 29 2025 at 02:18):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (d68f1d1f0a92f871b00c20ca469dcd683f7d4998).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Aug 30 2025 at 02:14):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (4a2112b923c565dea979f095339508883fc66b6d).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Aug 31 2025 at 02:22):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (59688f30ccd8be604a6058bb0734c2aca99dc464).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 01 2025 at 02:29):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (07fe84350fd82c7355766327fef3b9b8d284ef0a).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 02 2025 at 03:13):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (d055e8423fcfe976c3cac4c024cb82a3f9073d48).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Anne Baanen (Sep 02 2025 at 14:12):

I'm going to be debugging this workflow, please ignore the next few messages here!

github mathlib4 bot (Sep 02 2025 at 14:55):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (80361a9cd4821d68881759d2c4b45e0baba30cff).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 02 2025 at 16:11):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (b0b16e210ec91ba36e62da3ec71103d95e86697d).

Anne Baanen (Sep 02 2025 at 16:21):

Kim Morrison said:

This is still a work-in-progress; Anne Baanen will let us know when we should start looking at the failure messages for real!

Finally got it working! I'll keep monitoring this thread for failures for a few days, if we can make it consistently succeed then I declare the messages to actually have informative value :)

github mathlib4 bot (Sep 13 2025 at 02:08):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (de4a93e7adcf97696bba96e2cf6004985729504f).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 14 2025 at 02:18):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (16094030a086b1a28a32408a3aaa84ab99baffec).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Kim Morrison (Sep 14 2025 at 23:23):

Minor, I know how to fix this, I'll do it during the release of v4.24.0-rc1

github mathlib4 bot (Sep 15 2025 at 02:19):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (721a6355f2a7bab13b4cd13e67215fbbbd8b4ce8).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 16 2025 at 02:36):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (81d06f5195a74442763dcbc467354417fc3878aa).

github mathlib4 bot (Sep 17 2025 at 02:37):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (948ab23d2ea12963a1c4266aa6d4763993e1f7ae).

github mathlib4 bot (Sep 18 2025 at 02:37):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (eec514d532412569dbc0a968a940c99654801a70).

github mathlib4 bot (Sep 19 2025 at 02:47):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (e9ab2793e91dde3742f495b24f8d26d92a40a5de).

github mathlib4 bot (Sep 20 2025 at 02:40):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (c8e4e42213c636079e09e7ca0f883386d239fd34).

github mathlib4 bot (Sep 21 2025 at 02:48):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (0ab22dd232a7ba67285ba69e6b31cb621469ae46).

github mathlib4 bot (Sep 22 2025 at 02:20):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (6649a9bcb1f2845d26090da1412858c6c6c31321).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Kim Morrison (Sep 22 2025 at 03:50):

@Frédéric Dupuis, might you be able to take a look at this? BibtexQuery is broken on the latest Lean nightly due to changes in the definition of String.

Kim Morrison (Sep 22 2025 at 03:51):

If you'd be able to push a fix to the nightly-testing branch of BibtexQuery, we can then update the dependencies in doc-gen4, after which Mathlib's nightly-testing doc-gen4 should come good automatically.

github mathlib4 bot (Sep 23 2025 at 02:13):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (0179c7b76aee422113cf560285721b2f6259d8b6).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Frédéric Dupuis (Sep 23 2025 at 02:44):

Kim Morrison said:

Frédéric Dupuis, might you be able to take a look at this? BibtexQuery is broken on the latest Lean nightly due to changes in the definition of String.

I should be able to look at this in the next few days (I'm in a teaching blitz at the moment). How urgent is this?

github mathlib4 bot (Sep 24 2025 at 02:15):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (8326cdde318a88c96cfa9002ba7905cf3dc9d55d).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Kim Morrison (Sep 24 2025 at 03:08):

Next few days is fine, although I am about to go on holiday in about 60 hours, after which someone else will need to do the dependency bump inside doc-gen4's nightly testing branch (and then Mathlib's)

github mathlib4 bot (Sep 25 2025 at 02:42):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (c1437285a5e1f7f19daf852142702ffbeaa1279d).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 26 2025 at 02:16):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (5afb2e8371acdf09593080cfa85dcc7cbd04be4b).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 27 2025 at 02:11):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (7d00b7f51de230e6fcb0159f413ed4241d9cc8d3).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 28 2025 at 02:22):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (6da53fa708b7196a725cefb032de88c4c47b4afd).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 29 2025 at 02:17):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (b20b7ed23f231f211900ad0c59c294b073b5dfd8).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Sep 30 2025 at 02:14):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (07dcec0ba6435e8c7a58571484a3573a16e52e0a).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Oct 01 2025 at 02:22):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (11fa7d4a8c6f4323a3259cb4d9617131c64d653a).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Oct 02 2025 at 02:14):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (43c1fdcc532a0143e92b4f0be3cec14f9e5a9207).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Oct 03 2025 at 02:13):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (e3a1ca33ee355432b57c5583a4997f39c70190b2).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Oct 04 2025 at 02:40):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (8e9a8409142b13a4dd0c531d49158057afc693d9).

github mathlib4 bot (Oct 05 2025 at 02:51):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (153004c946eb30180b50c062c13ddc488f3ea2c0).

github mathlib4 bot (Oct 06 2025 at 02:47):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (ac8a764b52b88ac588443dbd5adc5c7a4dd5b623).

github mathlib4 bot (Oct 07 2025 at 02:44):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (281600fbe3d8bbc04e67750842ed1d3d3e96306e).

github mathlib4 bot (Oct 08 2025 at 02:44):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (344943d97ed094c2eb259341ebdcdedc243cf1b4).

github mathlib4 bot (Oct 09 2025 at 02:55):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (1714afe17e0817825f737a705eb591291c79da7d).

github mathlib4 bot (Oct 10 2025 at 02:44):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (c1ecbec4f1c90e7af3049f855d1dadcb4641f1a1).

github mathlib4 bot (Oct 11 2025 at 02:12):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (ecda81f6b653e619a992d0cbfa83b88279d76789).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Oct 12 2025 at 02:17):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (556169194d932e268c0c157139eb62dcb4065b34).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Oct 13 2025 at 02:20):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (7160fdd0ecad9e45bd6db34976345b9a4b4ee1a4).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Oct 14 2025 at 02:44):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (aedff210c410968807e23fc4526b5daf5c2ae2eb).

github mathlib4 bot (Oct 15 2025 at 02:48):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (a87897fc37568b533d7f0319002d13e8701f9c34).

github mathlib4 bot (Oct 16 2025 at 02:51):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (6b832de385b24773084bf5e0afc077ef3818e85b).

github mathlib4 bot (Oct 17 2025 at 02:46):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (9da4d23e6d9f46c3cb9ebc3f81efa75c83e987b1).

github mathlib4 bot (Oct 18 2025 at 02:42):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (1b8918e9f7d6591414d0354289cec29fa1bab47d).

github mathlib4 bot (Oct 19 2025 at 02:56):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (3a09765e211bee40f7eebb7529a4b7dd90ba202a).

github mathlib4 bot (Oct 20 2025 at 02:53):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (30b020bbcb3b3e6c2b0c364f7725a7eafa8171c9).

github mathlib4 bot (Oct 21 2025 at 02:49):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (aaf0357a08613e4e21285c9f9af5129d45f47b99).

github mathlib4 bot (Oct 22 2025 at 02:50):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (ffba888159ff10e97faaa7c286f8ad212de952f4).

github mathlib4 bot (Oct 23 2025 at 02:47):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (cd6ddfd1969a31b2958625e8110b1c26e2c0b835).

github mathlib4 bot (Oct 24 2025 at 02:48):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (beab1c3f4292b46c3bc5fd6cedcc90fe59393b2e).

github mathlib4 bot (Oct 25 2025 at 02:46):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (7db953b1c5d3fdef287052f1cc71200abdb32fb3).

github mathlib4 bot (Oct 26 2025 at 02:52):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (036f813c9eca605191c202a4c57ab273dc1d4c55).

github mathlib4 bot (Oct 27 2025 at 02:58):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (510cbb2ce097c4dc39fe834d187b1ff395c41946).

github mathlib4 bot (Oct 28 2025 at 02:49):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (cff302c2007733e8f9b951ab5d3f6bfb183b466c).

github mathlib4 bot (Oct 29 2025 at 02:54):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (ba2341b0a2cd84eafefc43ee7c87dd10dd3211d8).

github mathlib4 bot (Oct 30 2025 at 02:53):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (35fa5127109e68931467c618e595d58c5269849f).

github mathlib4 bot (Oct 31 2025 at 02:57):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (1549eab285285e8070358e992655979560cbe2a8).

github mathlib4 bot (Nov 01 2025 at 02:55):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (11edabcd45544c04649d9ee6b58b58199d47ae5d).

github mathlib4 bot (Nov 02 2025 at 02:56):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (318efa2722d9da2d9de6dfae77c32d4e2531c83a).

github mathlib4 bot (Nov 03 2025 at 02:57):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (768853f0f3097af2b2d5594fbfbd804d98eaa9cf).

github mathlib4 bot (Nov 04 2025 at 02:52):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (8aa7c1209959ca21b1a807d2f032175a02bb0ac9).

github mathlib4 bot (Nov 05 2025 at 02:55):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (10fc4a72e170e247cf5ec196beb484e0b6cb9bdf).

github mathlib4 bot (Nov 12 2025 at 03:04):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (e66a7c98a6871ae2719ce08aeb613f2b45d4119d).

github mathlib4 bot (Nov 13 2025 at 02:23):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (69b30f6081061f8153765afc8388abc311884e58).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 14 2025 at 02:22):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (6ab3440a00cd34ee8da16d2352506f84e59dff93).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 15 2025 at 02:19):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (83359cd6f034232379715c2c70ac5a59a9ea8847).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 16 2025 at 02:26):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (22f65ecb8d8277c06aa54e12efa281e803ed1ac4).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 17 2025 at 02:22):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (95f13e57fc48ad261601c11726c1b7d964a2e679).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 18 2025 at 02:21):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (780cbe2da5302ccce8e15061c51f458e969c92dc).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 19 2025 at 02:54):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (c292560fc11278dc4ee8a0d967523615e5919264).

github mathlib4 bot (Nov 20 2025 at 02:56):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (8068277c3ab280502aecf3c5100d7dd55806c53a).

github mathlib4 bot (Nov 21 2025 at 02:25):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (1978c4df79b318f01a66d0bbe19151885f450659).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 22 2025 at 02:23):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (a8fd4cfae81b8bba48e8efba21ba8cb398fe3bbe).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 23 2025 at 02:36):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (7dafbfd9df6544ec16d3b4b89d83d7b407277dd1).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 24 2025 at 02:32):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (b02313854c5766832e4a4f822f9dddd9d5c96717).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 25 2025 at 02:28):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (93c47f1843e4cabe08e69dbb110b90dcf2cbf6f8).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Robin Arnez (Nov 25 2025 at 07:32):

There is some adaptation for the string API changes necessary to make this one work again

Markus Himmel (Nov 25 2025 at 09:08):

github mathlib4 bot (Nov 26 2025 at 02:23):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (5e416f69da92a1d2b369c5481a741ec78c6d0bc7).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Kim Morrison (Nov 26 2025 at 04:31):

Markus Himmel said:

https://github.com/fgdorais/lean4-unicode-basic/pull/101

https://github.com/dupuisf/BibtexQuery/pull/28

https://github.com/leanprover/doc-gen4/pull/332

I ran the requisite lake updates and did the merges.

github mathlib4 bot (Nov 27 2025 at 02:21):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (9ce81b10927d4c9c4126c6b5c985064f147a6e30).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 27 2025 at 03:24):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (9ce81b10927d4c9c4126c6b5c985064f147a6e30).

github mathlib4 bot (Nov 28 2025 at 02:54):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (a9faeaabfed78e92b3e47f6c2f2b3995c3a0b0f2).

github mathlib4 bot (Nov 29 2025 at 03:04):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (b3687cde5b3ccbaf04e5c3b772a97465ff3949b3).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Nov 30 2025 at 02:30):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (ae8e7b63aea6f3181e3a76e98a859aaf27843c3f).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 01 2025 at 02:30):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (2bd1b8fc87246c6ddcbef2e414aad2c558edb3e4).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 02 2025 at 02:24):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (871f8b1529fd5062d298a8265545464f2257ca20).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 03 2025 at 02:24):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (4c7a6b2ec6b6cfebf6521848b0ee53796a2b66dc).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 04 2025 at 02:24):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (453cce856d41bd2715d9055ecdc877015033095f).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 05 2025 at 02:24):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (96d98dd8f37a7723fdb3f43a766a7fea4580b92b).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 06 2025 at 02:20):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (beb1a1dc8899a9b31359eb461c1562bbced8ec2a).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 07 2025 at 02:30):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (f7826d333e7f78a0636e6353ac61dd003abeb484).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 08 2025 at 02:25):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (5fa4f5c7207be9360643fe42987bcbb7c4d7b48d).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 09 2025 at 02:24):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (7ce3f2693854a9dfacf1633fbc1ab62fc2b9a5cc).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Kim Morrison (Dec 09 2025 at 23:16):

Sorry about this one falling by the wayside, should be fixed again now.

github mathlib4 bot (Dec 10 2025 at 03:05):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (03d33bda9f269145a3e31ef1971e4f7d8e922a4f).

github mathlib4 bot (Dec 11 2025 at 02:27):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (249f247c0a329a8940058cdfe4dfca0afeeacd55).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 12 2025 at 03:06):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (0e01e942cf77712b3c312afb0bace9fd6fc540a9).

github mathlib4 bot (Dec 13 2025 at 03:01):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (b62a16dd533561fd54375ccb4570e56df88a2063).

github mathlib4 bot (Dec 14 2025 at 03:01):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (e0e4b3764f55ff95f4c6fb9dc2178cb528baafa3).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 15 2025 at 02:29):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (6cda3b4ae49ccfb8af631b143404895d3637bdf7).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

github mathlib4 bot (Dec 16 2025 at 02:27):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (819c9e30c119428cfd1a078fb77b44597e02e24f).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Kim Morrison (Dec 16 2025 at 05:42):

info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4
info: leanprover/doc-gen4: checking out revision '785274dce3aa6677ba23026b881c80ffb7713b46'
info: toolchain not updated; already up-to-date
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic
info: UnicodeBasic: checking out revision 'b7f6be0ccc4216c8af5de6fe0ff3d063fe1d223d'
error: external command 'git' exited with code 128

Could someone please investigate this? I'd like to not have this one on my plate. :-)

Ruben Van de Velde (Dec 16 2025 at 07:50):

#lean4 > UnicodeBasic: 'git' exited with code 128 ? CC @Markus Himmel

Markus Himmel (Dec 16 2025 at 09:48):

This was due to the doc-gen4 lake manifest on nightly-testing referring to a nonexistent commit in UnicodeBasic. I have lake updated doc-gen4 which should hopefully fix it. Not sure how the nonexistent commit found its way into the lake manifest; the most likely reason is a force-push to UnicodeBasic's nightly-testing branch.

Kim Morrison (Dec 16 2025 at 21:44):

I'm really confused -- I have fixed exactly this issue on the nightly-testing branch of doc-gen4 at least once, I think twice, previously. Is there some mystery job re-breaking it for us?

github mathlib4 bot (Dec 17 2025 at 03:03):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (1d00b4d59cb464d6d4bcb213b54f4328b743a32d).

Markus Himmel (Dec 17 2025 at 06:53):

Just to rule out the simplest explanation: @François G. Dorais, you haven't been force-pushing the nightly-testing branch of UnicodeBasic by any chance, have you?

François G. Dorais (Dec 17 2025 at 07:36):

No, but why are you using nightly-testing in the first place? It's always been just for private use.

François G. Dorais (Dec 17 2025 at 07:37):

This issue will happen every day if you keep using nightly-testing.

Markus Himmel (Dec 17 2025 at 07:56):

Okay, the way I understand the situation is as follows:

You are using the nightly-testing branch of UnicodeBasic in some way that regularly loses commits. This makes it unsuitable to appear in a lakefile, because the commits that end up in a lake-manifest need to continue existing.
The FRO's mathlib nightly-testing infrastructure needs a branch that is regularly updated to the latest nightly and that doesn't lose commits because it will appear, for example, in doc-gen4's lakefile. In all other repositories this branch is called nightly-testing.
Here I'm not sure whether I'm misremembering: you were previously using the branch nightly for your private use, but Kim, believing that that nightly branch would serve our purposes for nightly-testing, requested it to be renamed to nightly-testing to be consistent with the rest of the ecosystem
This might have been a mistake; it would have been better to keep nightly as it is, and create a FRO-maintained nightly-testing branch downstream that regularly merges nightly, but doesn't lose commits so that it is safe to use as a target branch in a lakefile.

Does that sound right?

François G. Dorais (Dec 17 2025 at 08:10):

Or, I could switch to a testing model with linear history. Nobody asked about that nor mentioned that this would be desirable.

Markus Himmel (Dec 17 2025 at 08:25):

Yes, we should have communicated more clearly there. If you were to switch to a linear model, that would be great for us of course, but it's your repository; we're not in a position to tell you what to do. If you prefer to continue your curent workflow, that's perfectly fine (though in that case you could make our life much easier by releasing the nightly-testing branch name to us so that we can maintain our linear-history branch with a uniform name across the entire ecosystem).

François G. Dorais (Dec 17 2025 at 21:01):

I made the change to a linear nightly-testing. Time will tell whether I messed up some options and settings, but it's been tested once and it worked as intended.

François G. Dorais (Dec 17 2025 at 22:19):

I plan to release UnicodeBasic v2.0.0 in January. A small part of that plan was to arrange CI so that UnicodeBasic would have ready-made PRs that could be merged when needed. Does using nightly-testing make that obsolete?

Kim Morrison (Dec 17 2025 at 23:11):

I would like some branch that I can push changes to, without any coordination with others, that enables me to get UnicodeBasic working on a new nightly. Apologies that there seems to have been a communication failure, almost surely my fault, around this! To the extent that you (or anyone else!) can reduce the need for me to have this branch by speedily providing some version of UnicodeBasic that works on nightlies, that is incredibly appreciated and welcome. :-)

François G. Dorais (Dec 17 2025 at 23:52):

Thanks Kim! The current nightly-testing should do what you want.

I'm sorry about the lack of communication. I was confused about what you were doing but I was too busy to ask for details. It's my fault too!

Anyway, I'm always happy to work with you (Kim and Markus) to make the whole ecosystem work as smoothly as it can.

github mathlib4 bot (Dec 18 2025 at 02:24):

:cross_mark: The docgen run for Mathlib's nightly-testing branch has failed (41366a77a05165b3313523d07b2e4710142426c2).
This likely indicates an issue with the nightly Lean build, or a required update in doc-gen4.

Kim Morrison (Dec 18 2025 at 04:33):

Same problem. I've run lake update on doc-gen4's nightly-testing branch yet again.

François G. Dorais (Dec 18 2025 at 05:37):

But maybe for the last time?

François G. Dorais (Dec 18 2025 at 05:38):

What are the shas?

François G. Dorais (Dec 18 2025 at 21:32):

The updated sha has survived the last nightly update of UnicodeBasic. Yay!

github mathlib4 bot (Dec 19 2025 at 04:04):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (581e65392b3f3c7490f7c659ed743b2fa4a669d2).

github mathlib4 bot (Dec 20 2025 at 03:07):

:check: The docgen run for Mathlib's nightly-testing branch has succeeded (2eb6d9e4a3b89acd9b81c67012c8b4ef27b55d4c).

Last updated: Dec 20 2025 at 21:32 UTC

Stream: nightly-testing

Topic: Docgen status updates

github mathlib4 bot (Aug 27 2025 at 02:18):