diff options
Diffstat (limited to 'doc/stdlib')
| -rw-r--r-- | doc/stdlib/dune | 36 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 |
2 files changed, 37 insertions, 0 deletions
diff --git a/doc/stdlib/dune b/doc/stdlib/dune new file mode 100644 index 0000000000..7fe2493fbf --- /dev/null +++ b/doc/stdlib/dune @@ -0,0 +1,36 @@ +; 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}/plugins)) + (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) + (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)))) + +(alias + (name stdlib-html) + (deps html)) diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7b21b67eea..fd79996bb7 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -33,6 +33,7 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Logic/SetIsType.v + theories/Logic/StrictProp.v theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.v (theories/Logic/Classical.v) |