[dune] Simple rule to generate Stdlib's documentation.

Ideally this will be handled by Dune's native library support, but
this could be useful for the likes of #9648.

I am not sure what should be done w.r.t. style files.

3 files changed, 54 insertions, 3 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 668f0f50f4..a1da9be20b 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -346,6 +346,16 @@ doc:refman:dune:
     paths:
       - _build/default/doc/sphinx_build/html
 
+doc:stdlib:dune:
+  <<: *dune-ci-template
+  variables:
+    <<: *dune-ci-template-vars
+    DUNE_TARGET: stdlib-html
+  artifacts:
+    <<: *dune-ci-template-artifacts
+    paths:
+      - _build/default/doc/stdlib/html
+
 doc:refman:deploy:
   stage: deploy
   environment:
@@ -357,7 +367,7 @@ doc:refman:deploy:
   dependencies:
     - doc:ml-api:odoc
     - doc:refman:dune
-    - doc:refman
+    - doc:stdlib:dune
   before_script:
     - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y )
     - eval $(ssh-agent -s)
@@ -375,7 +385,7 @@ doc:refman:deploy:
     - mkdir -p _deploy/$CI_COMMIT_REF_NAME
     - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api
     - cp -rv _build/default/doc/sphinx_build/html _deploy/$CI_COMMIT_REF_NAME/refman
-    - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib
+    - cp -rv _build/default/doc/stdlib/html _deploy/$CI_COMMIT_REF_NAME/stdlib
     - cd _deploy/$CI_COMMIT_REF_NAME/
     - git add api refman stdlib
     - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"
diff --git a/Makefile.dune b/Makefile.dune
index 29f6fed974..da4c59af75 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -4,7 +4,8 @@
 .PHONY: help voboot states world watch check          # Main developer targets
 .PHONY: coq coqide coqide-server                      # Package targets
 .PHONY: quickbyte quickopt                            # Partial / quick developer targets
-.PHONY: test-suite refman-html apidoc release         # Accesory targets
+.PHONY: refman-html stdlib-html apidoc                # Documentation targets
+.PHONY: test-suite release                            # Accesory targets
 .PHONY: ocheck trunk ireport clean                    # Maintenance targets
 
 # use DUNEOPT=--display=short for a more verbose build
@@ -29,6 +30,7 @@ help:
 	@echo ""
 	@echo "  - test-suite:  run Coq's test suite"
 	@echo "  - refman-html: build Coq's reference manual [HTML version]"
+	@echo "  - stdlib-html: build Coq's Stdlib documentation [HTML version]"
 	@echo "  - apidoc:      build ML API documentation"
 	@echo "  - release:     build Coq in release mode"
 	@echo ""
@@ -81,6 +83,9 @@ test-suite: voboot
 refman-html: voboot
 	dune build @refman-html
 
+stdlib-html: voboot
+	dune build @stdlib-html
+
 apidoc: voboot
 	dune build $(DUNEOPT) @doc
 
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))