Description
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))))
[1] https://github.com/coq/coq/pull/9649/files#diff-9ddcc18605a133c6234e2382ffb52a59R27
Metadata
Metadata
Assignees
Type
Projects
Status
Done