doc-gen4 post 4.8.0-rc1

Stream: lean4 dev

[James Gallicchio]

Hey, I'm updating a project that uses doc-gen4 and am converting to a lakefile.toml -- there is a small bug (here) blocking this. But I am separately wondering if there's plans for the near future to change how projects generate docs.

[Kim Morrison]

Yes, lake install lean#3998 will hopefully land in either v4.9.0-rc1 (unlikely?) or v4.10.0-rc1 (likely!), and this will enable removing all the meta if require statements from lakefile.leans.

[James Gallicchio]

awesome!! looking forward to it :)