fix: correct markdown header processing by jcreedcmu · Pull Request #539 · leanprover/verso

jcreedcmu · 2025-09-29T21:51:38Z

Previously, parts generated by addPartFromMarkdown were at wrong nesting depth for nontrivial structures. Error explanations (for which this code was originally written) did not exercise this but because they have fairly simple structure, without many children of the same header, or decreases of header depth.

This PR simplifies the verso-nesting-depth-to-markdown-nesting-depth state, to a list of Nat rather than a list of pair of Nats. I think without sacrificing correctness.

jcreedcmu · 2025-09-29T21:52:19Z

I added some incidental comments to some Verso code as well based on my current understanding of it, let me know if I said anything wrong.

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

david-christiansen · 2025-10-01T14:57:27Z

Apart from nitpicky docstring stuff, I think this is a nice simplification and I think the docs were all correct.

Did you have set_option doc.verso true in the file? If not, then Verso docstrings probably shouldn't be used quite yet :)

david-christiansen · 2025-10-01T14:57:37Z

(or, alternatively, make sure to enable it)

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

Make the type `HeaderMapping` an abbreviation instead of a definition. This change was intended as part of leanprover#539 and will make leanprover/reference-manual#599 easier to land. There's still [one place remaining](https://github.com/leanprover/reference-manual/blob/main/Manual/Meta/ErrorExplanation.lean#L639-L640) in `Manual/Meta/ErrorExplanation.lean` where it's relying on the implementation of this type, which breaks if typeclass resolution doesn't see the `ForIn` instance on `List`. Of course, we could also expose `ForIn` on `HeaderMapping`, or expose a "close all sections for this `HeaderMapping` but I'd rather decouple that decision from [the present PR](leanprover/reference-manual#599).

Make the type `HeaderMapping` an abbreviation instead of a definition. This change was intended as part of #539 and will make leanprover/reference-manual#599 easier to land. There's still [one place remaining](https://github.com/leanprover/reference-manual/blob/main/Manual/Meta/ErrorExplanation.lean#L639-L640) in `Manual/Meta/ErrorExplanation.lean` where it's relying on the implementation of this type, which breaks if typeclass resolution doesn't see the `ForIn` instance on `List`. Of course, we could also expose `ForIn` on `HeaderMapping`, or expose a "close all sections for this `HeaderMapping` but I'd rather decouple that decision from [the present PR](leanprover/reference-manual#599).

Previously, parts generated by `addPartFromMarkdown` were at wrong nesting depth for nontrivial structures. Error explanations (for which this code was originally written) did not exercise this but because they have fairly simple structure, without many children of the same header, or decreases of header depth. This PR simplifies the verso-nesting-depth-to-markdown-nesting-depth state, to a list of `Nat` rather than a list of pair of `Nat`s. I think without sacrificing correctness.

Make the type `HeaderMapping` an abbreviation instead of a definition. This change was intended as part of leanprover#539 and will make leanprover/reference-manual#599 easier to land. There's still [one place remaining](https://github.com/leanprover/reference-manual/blob/main/Manual/Meta/ErrorExplanation.lean#L639-L640) in `Manual/Meta/ErrorExplanation.lean` where it's relying on the implementation of this type, which breaks if typeclass resolution doesn't see the `ForIn` instance on `List`. Of course, we could also expose `ForIn` on `HeaderMapping`, or expose a "close all sections for this `HeaderMapping` but I'd rather decouple that decision from [the present PR](leanprover/reference-manual#599).

jcreedcmu · 2025-10-02T12:51:25Z

Verso docstrings were later enabled in #547

jcreedcmu added 4 commits September 29, 2025 17:46

Fix broken mardown parsing

c99d0e2

Simplify markdown parsing

d0f72b8

Some more comments

046bba6

Add guard_msgs test

df133f4

jcreedcmu requested a review from david-christiansen September 29, 2025 21:51

jcreedcmu mentioned this pull request Sep 29, 2025

feat: make release notes insert parts from markdown leanprover/reference-manual#599

Merged

jcreedcmu added a commit to jcreedcmu/reference-manual that referenced this pull request Sep 29, 2025

Adapt to leanprover/verso#539

2f50097