1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
; 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-core)
(package coq-stdlib))
(action
(progn
(run mkdir -p html)
(bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -coqlib %{project_root} -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))
|
