Build artifacts not cleaned when regenerating documentation

[justincasher]

Build artifacts not cleaned when regenerating documentation

I'm developing LeanExplore, a search engine that wraps doc-gen4 to provide more frequent documentation updates aligned with Lean FRO releases. While integrating doc-gen4 into the pipeline, I discovered that stale build artifacts are not automatically cleaned between documentation regeneration runs.

Issue

When upgrading from Lean v4.23.0 to v4.24.0 and rebuilding documentation, the previous version's .json and .bmp files in lean/.lake/build/doc-data/ persist alongside the newly generated files. This results in mixed artifacts from different Lean versions in the same output directory.

Expected behavior

When running lake build <library>:docs, the build system should either:

1. Clean the doc and doc-data directories before regeneration, or
2. Document that users should manually clean these directories when switching Lean versions

Actual behavior

Old artifacts remain in place, potentially causing version conflicts when parsing the generated documentation files. In particular, the file declaration-data.Batteries.Data.ByteSubarray.bmp remains.

Question

Is this intentional behavior, or should doc-gen4 automatically clean these directories before building?