Ideal Technical Framework

[thomas-lamiaux]

At the beginning we are going to set up a interface using JsCoq and coqdoc similarly to what is done for Software Foundation.
However, it has a lot of issues and we would like something better on the long run.
Hence, I am starting this issue to gather idea about what the web interface could look like, and Zulip conversation to talk about it.

Ideally, we would have:

• An interactive web interface similar to what JsCoq can offer, that takes .v file and generate a page
• Using an expressive but standard format like github's version of md file (md + math + a few stuffs) rather than coqdoc
• Possibility to redefine a function or a lemma several time using the same name each time, in order not to have to write map, map', map''
• Possibility to have exercises and buttons to display the solutions
• Automatic generation of table contents like in Latex
• ?

Other criteria:

• If we put effort into that, we should think of users like teachers that need options like downloading the completed file / uploading a partially completed files etc...
• ?