Repository navigation
Build failure in LeanPlot.ToFloat due to incorrect markdown header nesting #7
Description
Description
When building the project with Lake, the build fails at LeanPlot.ToFloat because of a strict Markdown validation error in the documentation comments.
It seems there is a skipped header level (using ### without a preceding ##), which causes documentation tools like Verso/Subverso to crash the build.
Error Log
error: LeanPlot/ToFloat.lean:50:4: Incorrect header nesting: expected at most `##` but got `###`
error: Lean exited with code 1
Environment
Lean version: 4.31.0, x86_64-w64-windows-gnu
(Note: Written with the assistance of an AI assistant.)
Activity
alok commentedon Jul 10, 2026
Thanks for the precise report. This was a real Verso/SubVerso validation failure:
LeanPlot.ToFloatjumped from a level-one heading directly to### Rat. PR #5 merged the minimal###to##correction as55d17d2, preserving the contributor fix separately. Follow-up PR #8 updatedmainto Leanv4.32.0-rc1, ProofWidgetsv0.0.104, and Versov4.32.0-rc1, including the small docs-generator API adjustment required by current Verso.lake build LeanPlot.ToFloat, the fulllake build, the 498-job docs build, and both Lean Action CI runs pass. Closing as fixed onmain.