fix(docs): resolve doc-gen4 before docs build (lets Pages deploy)

[Robby955]

First lake command runs with -Kenv=dev so doc-gen4's docs facet registers before the build. Validated on run 28635186013 — build-docs green, full mathlib doc closure built in ~57m, artifact uploaded; deploy waited on the main-only branch policy. Merging publishes.

Summary by CodeRabbit

• Documentation
  • Improved the docs publishing workflow so documentation builds are more reliable.
  • Updated the caching and build steps used for generating and deploying the site, helping avoid missing documentation errors during the process.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

Run ID: 902e40c8-cd77-4862-8361-27e39522ff33

📥 Commits

Reviewing files that changed from the base of the PR and between 26be272 and 19dca78.

📒 Files selected for processing (1)

• .github/workflows/docs.yml

---

📝 Walkthrough

Walkthrough

The GitHub Actions docs workflow's cache retrieval step was renamed and modified to run lake -Kenv=dev exe cache get instead of lake exe cache get, with added comments explaining that this ensures doc-gen4 dev dependency elaboration for later docs facet resolution.

Changes

Docs Workflow Cache Update

Layer / File(s)	Summary
Update Lake cache step for doc-gen4 resolution .github/workflows/docs.yml	The cache step is renamed to "Get Mathlib cache and resolve doc-gen4," its command now uses -Kenv=dev, and comments explain the dev environment requirement for facet resolution.

Estimated code review effort: 1 (Trivial) | ~3 minutes

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly summarizes the main fix: resolving doc-gen4 before the docs build to unblock Pages deployment.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch formalslt/docs-ci-fix-2026-07-02

---

_{Comment @coderabbitai help to get the list of available commands.}