Pretty exports buttons on vscode

Stream: general

[Arthur Paulino]

@Gabriel Ebner I suggested a feature on the vscode plugin repo about adding a button export the lean code to some formatted extensions like md and html. Do you think it can be useful? I thought about having it centralized in one plugin because the syntax json is already being maintained there. This is the issue link: https://github.com/leanprover/vscode-lean4/issues/60

[Eric Wieser]

I'm not sure I see the point in exporting to md, isn't that literally just surrounding the text in ``` ? I assume the idea in the HTML export would be to output static syntax-highlighted code, rather than just surrounding the text in <code>?

[Eric Wieser]

Sorry, I should have read the link first.

[Scott Morrison]

Replied on the PR:

This doesn't really belong in the vscode-lean4 extension. Instead there should be a generic tool to translate a .lean file to a .md file. However this is hard to do on a single file basis, because of course imports and definitions should be linkified to their declarations in other files. Really the tool should take a whole project (e.g. with a leanpkg.toml file, or looking to the future lakefile.lean) and output a directory full of .md files. So at this point you're not so far off the documentation generation that supports https://leanprover-community.github.io/mathlib_docs/. Maybe it's better start working on improving that?

I agree, however, that the VSCode extension should eventually provide a Generate documentation command in the command palette. But this is a one-line change to the extension once lake doc or whatever is ready.