Tracking Issue: pol doc documentation generator

[BinderDavid]

We want to add a documentation generator which can generate HTML documentation for polarity modules.
This issue is for tracking the discussion about features / anti-features that we want to or don't want to support.

Here are some starting questions that we have to answer:

• Should we follow the 1 module = 1 html file approach, or should we build a JS-based "single-page" documentation?
• We have to agree on some directory for build artefacts. Maybe target/docs/...?
• The invocation should probably be pol doc FILENAME at first, at least until we have some sort of project configuration files.
• @timsueberkrueb Is the annotation mechanism of our prettyprinting library ergonomic enough that we can also build a HTML backend which allows to create HTML with clickable links which lead to the definition site?

[timsueberkrueb]

Should we follow the 1 module = 1 html file approach, or should we build a JS-based "single-page" documentation?

I think there are pros and cons for both options, some that I can think of right now are:

1 module = 1 html file

• Easier to maintain (requires only limited web frontend knowledge)
• Works without JS enabled
• Easier to index by search engines

Single page app

• Supports more sophisticated interactive features (e.g. integrate LSP)

Note that frontend apps can also be written in Rust and wasm with (almost) no JavaScript required.

We have to agree on some directory for build artefacts. Maybe target/docs/...?

👍

The invocation should probably be pol doc FILENAME at first, at least until we have some sort of project configuration files.

Alternatively, accept a directory and document all files in the directory.

@timsueberkrueb Is the annotation mechanism of our prettyprinting library ergonomic enough that we can also build a HTML backend which allows to create HTML with clickable links which lead to the definition site?

I think it should be possible. The Anno type is entirely user-definable, so we can annotate nodes with anything we want. One thing we need to be careful with is to escape the strings in the pretty::Render implementation (write_str, write_str_all). E.g. see this library.
As long as all we want to do is to annotate syntax nodes and change the HTML output accordingly by wrapping the annotated spans in HTML tags, we should be good. Hover info and jump to definition can be achieved in this fashion. If we want to do anything beyond, we should look into other options.

[BinderDavid]

We should use target_pol instead of target, because target is already used by Rust, and we should avoid interference between the two tools.