Add `lean4+md` and `lean3+md` as frontends

[utensil]

When following the pattern of --frontend coq+rst, using --frontend lean4+md gives:

alectryon: error: argument --frontend: invalid choice: 'lean4+md' (choose from 'coq', 'coq+rst', 'coq.io.json', 'coq.json', 'coqdoc', 'json', 'lean3', 'lean3+rst', 'lean3.io.json', 'lean3.json', 'lean4', 'lean4+rst', 'lean4.io.json', 'lean4.json', 'md', 'rst')

It's reasonable to expect such a combination because most lean 4 sources are written with comments in Markdown.

After a little digging, it seems not too difficult to add lean4+md:

Registration

Add

"lean3+md": ("alectryon.myst", "MDLean3Parser"),
"lean4+md": ("alectryon.myst", "MDLean4Parser"),

to

PARSERS = {
    "coq+rst": (__name__, "RSTCoqParser"),
    "lean3+rst": (__name__, "RSTLean3Parser"),
    "lean4+rst": (__name__, "RSTLean4Parser"),
    "rst": ("docutils.parsers.rst", "Parser"),
    "md": ("alectryon.myst", "Parser"),
}

in https://github.com/cpitclaudel/alectryon/blob/e1dae3133710e9f4ebbaa0da465b12bd97e77b3c/alectryon/docutils.py#L1441

Add code for +md pipelines like

    pipelines[lang + '+rst'] = {
        'webpage':
        (read_plain, register_docutils, gen_docutils, copy_assets,
         write_file(".html", strip=(*exts, ".rst"))),
        'latex':
        (read_plain, register_docutils, gen_docutils, copy_assets,
         write_file(".tex", strip=(*exts, ".rst"))),
        'lint':
        (read_plain, register_docutils, gen_docutils,
         write_file(".lint.json", strip=(*exts, ".rst"))),
    }

in

https://github.com/cpitclaudel/alectryon/blob/master/alectryon/cli.py#L444

Implementation

Implement MDLeanXParser using almost identical code from RSTLiterateParser but inherit it from the parser in https://github.com/cpitclaudel/alectryon/blob/master/alectryon/myst.py which also inherited from docutils.parsers.rst.Parser so there's no major technical obstacle.

[cpitclaudel]

I believe this is implemented on the next branch at https://github.com/cpitclaudel/alectryon/tree/next ; could you give it a try nd see how well it works for your use case?

[utensil]

Thank you for pointing me to the next branch, is it the main development branch and PRs should be based on it?

I've given it a try:

1. it supports writing Lean 4 in Markdown (there's no recipe for it, but I've created one here satisfying the expectation of etc/regen_makefile.py: https://github.com/utensil-contrib/alectryon/commit/8584b33fefc2f92ec5c170b7ba81a0c8df4dddcb )
2. it still doesn't support writing Markdown comments in Lean 4

For 2, the rabbit hole is deeper than I thought, I've managed to make it partially work here: https://github.com/cpitclaudel/alectryon/commit/4f99f7323f4c61f31d6208c235d8adf1907505fc

literate: POC for MyST in Lean 4
Results:
- MyST in Lean 4 renders to HTML
Problems:
- Annotations are not working
- Flags are not working
- Hard dependency on MyST
- messy code organization

It can now consume a Lean 4 file with Markdown comments in it and generate HTML output, but the annotations are gone.

Trying to make annotation work by eval-rst will trigger the following error:

  File "/opt/homebrew/anaconda3/lib/python3.9/site-packages/docutils/nodes.py", line 2021, in dispatch_visit
    return method(node)
    method = <bound method NodeVisitor.unknown_visit of <alectryon.docutils.make_HtmlTranslator.<locals>.Translator object at 0x10654b8e0>>
    node = <alectryon_pending: >
    node_name = 'alectryon_pending'
    self = <alectryon.docutils.make_HtmlTranslator.<locals>.Translator object at 0x10654b8e0>

  File "/opt/homebrew/anaconda3/lib/python3.9/site-packages/docutils/nodes.py", line 2044, in unknown_visit
    raise NotImplementedError(
    node = <alectryon_pending: >
    self = <alectryon.docutils.make_HtmlTranslator.<locals>.Translator object at 0x10654b8e0>

NotImplementedError: <class 'alectryon.docutils.make_HtmlTranslator.<locals>.Translator'> visiting unknown node type: alectryon_pending

which I have no clue how to solve.

[utensil]

It turns out that this is indeed implemented, but in https://github.com/Kha/alectryon/tree/typeid and as 'lean4+markup' which used a "passing through markup as is" approach that's way better than my attempt.

The branch of alectryon is already used in Lean 4 Manual rendering:

https://github.com/Vtec234/lean4/blob/master/doc/flake.nix#L80

and some literate Lean 4 in Markdown can be found here: https://github.com/Vtec234/lean4/blob/widget-doc/doc/widgets.lean .

I'll close this issue. Thanks!

[Kha]

Hm, "passing through markup as is" is just a quick hack I implemented because we didn't want to move on from mdbook! A true markdown frontend that can be used to produce equivalent output to the ReST frontend would still be nice to have I think.