doc gen fails on 4.12.0-rc1

Stream: general

[Yaël Dillies]

I get strange CI errors in APAP that seem to mean that doc-gen wasn't updated to 4.12.0-rc1. @Bryan Gin-ge Chen, thoughts?

[Henrik Böving]

https://github.com/leanprover/doc-gen4/pull/217 it was indeed not updated because it fails to build due to dependency issues (among other things)

[Yaël Dillies]

Aha! Can I help?

[Bryan Gin-ge Chen]

I unfortunately have no experience with doc-gen4 or its CI (yet?) so I have nothing to contribute here...

[Henrik Böving]

The PR already exists: https://github.com/dupuisf/BibtexQuery/pull/10

[Yaël Dillies]

Sorry, I will erase the association between you and doc-gen4 from my brain :robot:

[Henrik Böving]

@Tobias Grosser would have to set the toolchain correct and then @Frédéric Dupuis would have to merge (I think Frederic can also change the content of that branch because he is the maintainer, it depends on how the PR was set up by Tobias).

[Henrik Böving]

There does also seem to be a small change necessary to doc-gen itself which I can make really quick

[Henrik Böving]

But yeah the main blocker is bibtex query so I guess waiting for Frederic and maybe Tobias is in order^^

[Julian Berman]

(#general > BibtexQuery CI is tangentially related)

[Henrik Böving]

doc-gen part is done

[Tobias Grosser]

https://github.com/dupuisf/BibtexQuery/pull/10 is done.

[Tobias Grosser]

Waiting for @Frédéric Dupuis to review and merge.

[Tobias Grosser]

Feel free to already do a review to catch any obvious errors I may have made.

[Frédéric Dupuis]

I just merged -- thanks Tobias, and sorry everyone for being slow here, this caught me on a very busy day.

[Tobias Grosser]

This was pretty quick.

[Tobias Grosser]

Thank you

[Henrik Böving]

on the update now!

[Henrik Böving]

done! @Yaël Dillies ping

[Kim Morrison]

Thanks all!

[Yaël Dillies]

All working good again on my end :smiley: