; This is an ad-hoc rule to ease the migration, it should be handled
; natively by Dune in the future.
(rule
 (targets index-list.html)
 (deps
   make-library-index index-list.html.template hidden-files
   (source_tree %{project_root}/theories)
   (source_tree %{project_root}/user-contrib))
 (action
  (chdir %{project_root}
   ; On windows run will fail
   (bash "doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files"))))

(rule
  (targets html)
  (alias stdlib-html)
  (package coq-doc)
  (deps
   ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg
   (source_tree %{project_root}/theories)
   (source_tree %{project_root}/user-contrib)
   (: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 -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/user-contrib -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))))

; Installable directories are not yet fully supported by Dune.  See
; ocaml/dune#1868.  Yet, this makes coq-doc.install a valid target to
; generate the whole Coq documentation.  And the result under
; _build/install/default/doc/coq-doc looks just right!

(install
 (files (html as html/stdlib))
 (section doc)
 (package coq-doc))