Documentation consolidation

[jeromesimeon]

The code documentation is scattered at the moment. The README now points to querycert.github.io for documentation. We should have a well understood process to produce documentation, and a clear entry point for both developers (in the code) and users (in the place where the README points to).

Some of the work items include:

• Document code documentation generation for developers (point to coq2html, Makefile target, etc)
• Provide a clean 'main page' for the code documentation produced by coq2html
• Consolidate existing documentation pieces (in ./doc, in querycert.github.io, etc)
• Switch compilation pipeline figure based on tikz, and corresponding removal of old versions of the figure
• Ensure the new documentation works properly from the webdemo

UPDATE:
Further edits of the code documentation in doc/doc.html should still happen so it looks more readable, and is more complete. Notably:

• Better document the utility modules in coq/Utils
• Better document the common components in coq/Common
• Better document the languages
  • cNNRC
  • NRA
  • cNRAEnv
  • All the rest
• Better document the translations in coq/Translations
• Better document the Compiler Driver in coq/Compiler

[jeromesimeon]

There is a now a small README in qcert/doc that documents how to re-generate the documentation and how to re-deploy it consistently to the external Web site. See a6ea8a5.

[jeromesimeon]

The 'main page' for the code documentation produced by coq2html is doc/doc.html. It is also available on querycert.github.io (the external Web site).

[jeromesimeon]

The main Web site is now produced from the qcert/doc directory, which is the single source for all the documentation. This ensures for consistency between the documentation and demo produced from the source, and the external Web site. A warning is that we should not edit the external Web site directly anymore.

[jeromesimeon]

The compilation pipeline figure in Tikz is in doc/figure and should be kept up to date there. Previous compilation pipeline figures in keynote have been removed from the source.

[jeromesimeon]

The Web demo and documentation are now both contained in the same directory, which facilitates consistent code browsing from the demo and should avoids inconsistent links from the demo to the correct documented Coq code.

[jeromesimeon]

Modules in Basic have now been split into two directories:

• Utils containing general purpose libraries, which have been added to the documentation
• Common containing common components such as data model, type system and operators, which still need further documentation

[jeromesimeon]

I've written a sort of "documentation template" for one of our languages (cNNRC). This includes a denotational semantics that closely aligns with the published papers, and I believe might be readable by a formal-leaning DB person, not just a Coq expert.

While this may not be the right approach for all languages, this can be used as a kind of guide for the other languages.