Panic in doc-gen4

Stream: general

[Anne Baanen]

FYI, the Mathlib docs are experiencing some panics while building: search for PANIC here. This means we're missing some declarations. I'm looking into it right now.

Update: this seems to be related to some of the recent cache issues. Hopefully this will pass in a moment.

[Anne Baanen]

(Also, the action appears to succeed despite the panics, we only noticed because the website started failing to build when docs#Field failed to appear in the list of declarations. We should fix the action so it actually fails upon failure...)

[Anne Baanen]

Hmm. On the Mathlib master branch, #eval findDeclarationRanges? ``RatCast returns none, even though it does return some ... if I try to run this in Batteries...

[Damiano Testa]

Ah, the missing Field is also the source of failure of the website PRs.

[Anne Baanen]

Ooh, is this because Batteries switched to the module system and now doc-gen4 can't access the declarations? If I link to the file defining RatCast we get an empty page.

[Sebastian Ullrich]

For #eval in a module this is true. For docgen it depends on how the environment is set up, a bare importModules should give access to everything

[Anne Baanen]

The relevant code in doc-gen4 is:

def envOfImports (imports : Array Name) : IO Environment := do
  -- needed for modules which use syntax registered with `initialize add_parser_alias ..`
  unsafe Lean.enableInitializersExecution
  importModules (imports.map (Import.mk · false true false)) Options.empty (leakEnv := true) (loadExts := true)

[Damiano Testa]

Could something related to the module system also be an explanation for #mathlib4 > Build error in Tactic file?

[Anne Baanen]

I guess Import.mk · (importAll := true) true false could be a fix here?

[Anne Baanen]

I made a branch in mathlib4_docs with that change, let's see how it goes... https://github.com/leanprover-community/mathlib4_docs/actions/runs/18712722825

[Anne Baanen]

Aww, we're still getting panics :(

[Sebastian Ullrich]

Yes, this is likely a cache failure as well

[Anne Baanen]

You're right, removing .lake/package/batteries/.lake and building again does return ranges again.

[Bryan Gin-ge Chen]

The cache issues in mathlib master are now fixed (I think?), but I guess the docs won't work unless we make mathlib4_docs use an older version of doc-gen4?

cf. the latest build errors which are from v4.25.0 changes, as far as I can tell: https://github.com/leanprover-community/mathlib4_docs/actions/runs/18729477389/job/53422622333#step:9:49

[Anne Baanen]

Oh yes, that looks like a lean version mismatch.

[Bryan Gin-ge Chen]

The latest builds of mathlib4_docs seem to have succeeded :tada: