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
|
; 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/corelib/make-library-index doc/corelib/index-list.html doc/corelib/hidden-files"))))
(rule
(targets (dir html))
(alias corelib-html)
(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 rocq-runtime)
(package coq-core)
(package rocq-core))
(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/Corelib Corelib -Q %{project_root}/theories/Ltac2 Ltac2 $(find %{project_root}/theories -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))))
|
