Text on root API documentation page

[joelberkeley]

I'd like to be able to show text on the root page of the --mkdoc API reference. I might use this to add an introduction to the library.

[gallais]

Thinking about this: what's the principled solution? A template index.html with magic anchors to substitute for the list of modules? We could start by adding that & then it should not be too much work to add an extra command line option to allow to override the default template.

[joelberkeley]

python sphinx has two ways to do (something like) this. First is in the root __init__.py, where that module docstring becomes the library root doc. Without such a file in Idris, I'm not sure if there's anywhere in the source code to replace that. The other place is in an index.rst.

[joelberkeley]

i'm so used to sphinx and all the pre-processing it does i'm finding it a little difficult to decouple myself from that way of thinking

[gallais]

We could use the description in the .ipkg file if we don't want to go down the template route.

[joelberkeley]

Do you mean brief? I think that would do well for now. Sounds simpler too. Is it simpler? And is it used anywhere yet? I'm just thinking that we don't want to give it multiple uses if one use would require some contents and the other use some different contents.

[joelberkeley]

On second thoughts, I'm on the fence. If it's about the same amount of effort, the index.html route sounds better, because it could easily swamp the .ipkg file

[joelberkeley]

I'd also like to be able to add arbitrary html pages to the docs. For example, compiling a literate Idris file to html and including that. I'm not suggesting we change the scope of this work, but thought I'd mention it in case it's relevant for how we approach the index.html