Some steps toward easier inclusion of Platform Docs tutorials.

[Zimmi48]

The methodology followed thus far to include Alectryon-generated web content into rocq-prover.org (for the Tour of Rocq) was to include the generated HTML into the .md file for the corresponding page. This did not work well when the generated HTML had too much indentation, as this file would still be parsed as Markdown, and thus some blocks of HTML would be interpreted as blocks of code to be displayed as such.

Ideally, Alectryon should be able to produce Markdown output, where only the blocks of Rocq code use the final HTML tags, and the rest of the document is still pure Markdown syntax.

In the meantime, this PR takes some steps toward including the Platform Docs tutorials in the rocq-prover.org website by introducing a new YAML key to give the body of a tutorial in a separate HTML document. The markdown body is still used to generate the table of contents. The search bar on the website will probably only work for the table of contents and not the full text, because it is based on the markdown content as well.

Unfortunately, this document still has to be post-processed from what Alectryon produced:

• Alectryon only produces full web-pages. It would be better if we could tell it to only produce the body content.
• When using coqdoc as the source, generated identifiers are unrelated to the titles and need to be changed.
• Documents should start with a h2 or a p - some empty pre should be removed. coqdoc does not put paragraphs in p tags. And myst_parser only produce h1 tags for titles (so they have to be replaced by the appropriate level).
• Sometimes the generated HTML contains empty pre tags that will be visible, and thus should be removed.

I've only added two tutorials for now. Two more can be easily added (up to the post-processing described above), while some others do not seem to compile with versions of Coq and/or Equations that I tried them with.

Preview (top of the page):

Preview (bottom of the page, with a link to the Platform Docs repo):

[Zimmi48]

Switching to draft because following the meeting from yesterday and the discussion about the version switcher for Platform Docs, it is not so clear if we want such a tight integration on the website or to host static files through the doc repo as for the refman instead.