Coqdoc support

[rgrinberg]

To match the functionality of coq_makefile, dune should support generating documentation for coq theories using coqdoc.

Coqdoc is documented here

Here's an example [1] of a coqdoc rule setup manually:

(rule
   (targets html)
   (deps
    ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
    (source_tree %{project_root}/theories)
    (source_tree %{project_root}/plugins)
    (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
    (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
    ; For .glob files, should be gone when Coq Dune is smarter.
    (package coq))
  (action
   (progn
    (run mkdir -p html)
    (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)")
    (run mv html/index.html html/genindex.html)
    (with-stdout-to
      _index.html
     (progn (cat %{header}) (cat index-list.html) (cat %{footer})))
    (run cp _index.html html/index.html))))

cc @Alizter @ejgallego

[1] https://github.com/coq/coq/pull/9649/files#diff-9ddcc18605a133c6234e2382ffb52a59R27

[Alizter]

This could very easily be implemented IMO, I already have some coqdoc rules in our test-suite PR.

The difference between these rules today vs. what coq_makefile is doing, is the location coqdoc is being run from, which can effect the names in the documentation. We also need to work out things about index files etc.

There are also two modes for coqdoc: html and latex. This is similar to support for odoc which is being added #5366

[rgrinberg]

Do you want to give this a try then?