Add documentation

[Columbus240]

I created a branch 'doc' in my repo with some notes about the structure of the code.

I’m beginning to decipher Primitives.v and would like to add my notes about it to this repo, so that other people can understand it more easily. I’d like to discuss how the documentation shall be added to the repo. Should it be in coqdoc format (adding a new target to the makefile) or in files separate to src/? Should it, if read front-to-back, touch on every aspect of the repo or only highlight major parts?

The documentation of the stdlib of Coq is relatively sparse, consisting mostly of headings and a sometimes a few lines of text. I don’t think this style would be completely adequate, because the stdlib contains well-known math, while the structure and content of this repo is unfamiliar to a new reader. But for files like Utility/Monads.v the style of the stdlib seems okay to me.

[samuelgruetter]

Thanks for starting this, see also my comment at https://github.com/Columbus240/riscv-coq/commit/0387c87f8ed0aa57d09fa3ab395364f68412d320#r33765552

Primitives.v is just an alternative interface to the spec which is more suitable for the bedrock2 compiler.

I think .md files for a general overview are good, and coqdoc comments for noteworthy points about certain code features as well. I personally never read coqdoc-generated html files, but if a .v file contains good coqdoc comments, I appreciate it.

[Columbus240]

I rebased my branch, put in your paragraph and added a few words about PrimitivesParams. I believe now, a general overview like this should be fine for an interested reader of this project. The rest should be possible to find out by studying the code.

If I come up with something relevant for the docs, I’ll add it. After finishing the doc branch, merging it and nothing new coming up, I consider this issue closed.