feat: make release notes insert parts from markdown

[jcreedcmu]

Resolves #542.

Previously, we turned all headers into emphasized text regardless of level. With this change, we insert nested parts into the current verso document corresponding to the markdown structure.

[jcreedcmu]

This isn't right yet; it inserts consecutive parts more deeply nested than they ought to be, e.g. release note markdown

## foo
## bar
## baz

becomes rendered as if it was

## foo
### bar
#### baz

[jcreedcmu]

I think I see what I'm supposed to do instead from addPartsFromMarkdown's docstring...

[jcreedcmu]

This is now, I think, correct, unless we expect permalink icons to appear while hovering over section headers in the release notes. I tentatively expected that, and I observe that they do not appear.

I think traversal is still correctly assigning fresh ids to sections arising from markdown in the release notes, because the sections appear in the TOC sidebar, and clicking on them still correctly goes to the right url-with-fragment. I think this is where permalinks get created.

[jcreedcmu]

There was another Parallel Elaboration section in the release notes with which this one was redundant. The other one contained #7084 with identical description, and many more items.

[nomeata]

One subsection is a subsection of Highlights and the other one in the full list. Don't delete @eyihluyc's work 😅

[jcreedcmu]

Perish the thought! Thanks for catching my mistake. Trying to determine now why the two sections were rendered in my testing as siblings, which I now see is clearly wrong.

[jcreedcmu]

There was another Lake section in the release notes with which this one was redundant. The other one contained #7909 with almost identical description, (except it misspelled server as sever) and many more items.

[nomeata]

One subsection is a subsection of Highlights and the other one in the full list. Don't delete @eyihluyc's work 😅

[jcreedcmu]

I'm interested in ignoring the prose checks for now as they are numerous and orthogonal to this change.

[david-christiansen]

If you stick class="no-vale" on the resulting HTML, the prose linter will ignore these.

[david-christiansen]

This is matching the literal identifier markdown, which means that it won't react correctly to the user's open statements or their own shadowing definitions. Similarly, it's better to accept arguments here, then either ignore or reject them, so that the pattern doesn't stop matching as soon as someone provides an argument.

You should instead do something like:

Suggested change

	| `(Lean.Doc.Syntax.codeblock| ``` markdown | $txt ``` ) => do
	| `(Lean.Doc.Syntax.codeblock| ``` $markdown:ident $args*| $txt ``` ) => do
	let x <- realizeGlobalConstNoOverloadsWithInfo markdown -- This actually resolves the name
	if x != ``markdown then Elab.throwUnsupportedSyntax -- If it's some other `markdown`, defer to it
	-- Now we commit to our function and can reject arguments
	for arg in args do
	let h <- m!"Remove it:" #[""] (ref? := arg)
	logErrorAt arg m!"No arguments expected{h}"

[jcreedcmu]

Thanks, makes sense, will do!

[david-christiansen]

This is now, I think, correct, unless we expect permalink icons to appear while hovering over section headers in the release notes. I tentatively expected that, and I observe that they do not appear.

I think traversal is still correctly assigning fresh ids to sections arising from markdown in the release notes, because the sections appear in the TOC sidebar, and clicking on them still correctly goes to the right url-with-fragment. I think this is where permalinks get created.

To get a permalink, the section has to have a stable identifier. That represents our commitment to keeping it around and keeping that name. Because release notes are basically immutable, this is easy - some mangling of the title and version will suffice. You do this by assigning the tag field of each section's PartMetadata, which will also result in them appearing in the quickjump.

[jcreedcmu]

To get a permalink, the section has to have a stable identifier. That represents our commitment to keeping it around and keeping that name. Because release notes are basically immutable, this is easy - some mangling of the title and version will suffice. You do this by assigning the tag field of each section's PartMetadata, which will also result in them appearing in the quickjump.

Perfect, that's exactly the information I was interested in.

[jcreedcmu]

This PR now depends on leanprover/verso#539 to fix markdown header processing to be actually correct. @jrr6 's original implementation was good enough for the typical error explanations markdown, but had iiuc a slightly subtle bug for repeating headers at the same depth, which my PR aims to fix.

[jcreedcmu]

Is this (by exact decl_name%) tactic invocation appropriate here? As I understand it, I'm not able to literally write ``markdown because I want to refer to the very def markdown defined on line 32, right? So this is what I guessed would work instead, having seem decl_name% many places elsewhere. It does in fact seem to work, and using MessageData.hint below works to get argument deletion hints as well.