Document the source code

[HuStmpHrrr]

related to #145

There is a particular way in which we should write the docs in the source files so that it generates more reasonable and readable outputs. This can wait, until we need to submit some artifact.

[HuStmpHrrr]

consider https://github.com/coq-community/proviola and https://github.com/cpitclaudel/alectryon

[Ailrun]

I think both have some issues.

1. https://github.com/coq-community/proviola seems dead, and it is not even clear whether it is compatible with Coq 8.17.1. Also, there is no clear installation/execution doc.
2. https://github.com/cpitclaudel/alectryon works fine, but the output has one (critical, IMO) issue. There is no "go-to-definition" links.

[HuStmpHrrr]

2. https://github.com/cpitclaudel/alectryon works fine, but the output has one (critical, IMO) issue. There is no "go-to-definition" links.

what? that's deadly! really sad that this basic stuff is not working.

[Ailrun]

I guess the only reasonable solution is coqdoc.

[HuStmpHrrr]

ok, make sense to me. I have a template, if you want to save some time, this template works: https://hustmphrrr.github.io/popl20-artifact/

otherwise, I am also open to other options.

[HuStmpHrrr]

I think we can first change all (* to (**. A sed command should do the trick.

[HuStmpHrrr]

I think we should use a different star as the coqdoc renders something less expected: https://beluga-lang.github.io/McLTT/toc.html

[Ailrun]

@HuStmpHrrr We can move them to h3.

[Ailrun]

But I hate how the format ignores a basic recommendation for html: "Do not use multiple h1s". That formatting assumes the use of multiple h1s as items.