diff options
| -rw-r--r-- | .gitlab-ci.yml | 14 | ||||
| -rw-r--r-- | Makefile.dune | 7 | ||||
| -rw-r--r-- | doc/stdlib/dune | 36 |
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)) |