From 80f3011eb5ca479b9b1f059c0f04e131028d5312 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 18 Mar 2020 16:07:19 +0100 Subject: Build and install refman with Dune. --- .gitlab-ci.yml | 11 ++++++++++- Makefile.dune | 6 +++++- coq-doc.opam | 41 +++++++++++++++++++++++++++++++++++++++++ coq-refman.opam | 41 ----------------------------------------- doc/dune | 48 ++++++++++++++++++++++++++++++++---------------- doc/stdlib/dune | 14 +++++++++++--- 6 files changed, 99 insertions(+), 62 deletions(-) create mode 100644 coq-doc.opam delete mode 100644 coq-refman.opam diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5e6c380f4b..9fd7b7d53d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -425,7 +425,16 @@ doc:refman:dune: artifacts: paths: - _build/log - - _build/default/doc/sphinx_build/html + - _build/default/doc/refman-html + +doc:refman-pdf:dune: + extends: .dune-ci-template + variables: + DUNE_TARGET: refman-pdf + artifacts: + paths: + - _build/log + - _build/default/doc/refman-pdf doc:stdlib:dune: extends: .dune-ci-template diff --git a/Makefile.dune b/Makefile.dune index b433ed1b94..ec10568a30 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -4,7 +4,7 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets .PHONY: quickbyte quickopt quickide # Partial / quick developer targets -.PHONY: refman-html stdlib-html apidoc # Documentation targets +.PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets .PHONY: test-suite release # Accessory targets .PHONY: fmt ocheck ireport clean # Maintenance targets @@ -32,6 +32,7 @@ help: @echo "" @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" + @echo " - refman-pdf: build Coq's reference manual [PDF version]" @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" @echo " - release: build Coq in release mode" @@ -92,6 +93,9 @@ test-suite: voboot refman-html: voboot dune build @refman-html +refman-pdf: voboot + dune build @refman-pdf + stdlib-html: voboot dune build @stdlib-html diff --git a/coq-doc.opam b/coq-doc.opam new file mode 100644 index 0000000000..2f4072955f --- /dev/null +++ b/coq-doc.opam @@ -0,0 +1,41 @@ +synopsis: "The Coq Proof Assistant --- Reference Manual" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the Coq Reference Manual. +""" +opam-version: "2.0" +maintainer: "The Coq development team " +authors: "The Coq development team, INRIA, CNRS, and contributors." +homepage: "https://coq.inria.fr/" +bug-reports: "https://github.com/coq/coq/issues" +dev-repo: "https://github.com/coq/coq.git" +license: "Open Publication License" + +version: "dev" + +depends: [ + "dune" { build } + "coq" { build & = version } +] + +build-env: [ + [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] +] + +build: [ + [ "dune" "build" "-p" name "-j" jobs ] +] + +# Would be better to have a *-conf package? +depexts: [ + [ "sphinx" ] + [ "sphinx_rtd_theme" ] + [ "beautifulsoup4" ] + [ "antlr4-python3-runtime"] + [ "pexpect" ] + [ "sphinxcontrib-bibtex" ] +] diff --git a/coq-refman.opam b/coq-refman.opam deleted file mode 100644 index 937c4b08d3..0000000000 --- a/coq-refman.opam +++ /dev/null @@ -1,41 +0,0 @@ -synopsis: "The Coq Proof Assistant --- Reference Manual" -description: """ -Coq is a formal proof management system. It provides -a formal language to write mathematical definitions, executable -algorithms and theorems together with an environment for -semi-interactive development of machine-checked proofs. - -This package provides the Coq Reference Manual. -""" -opam-version: "2.0" -maintainer: "The Coq development team " -authors: "The Coq development team, INRIA, CNRS, and contributors." -homepage: "https://coq.inria.fr/" -bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" -license: "Open Publication License" - -version: "dev" - -depends: [ - "dune" { build } - "coq" { build & = version } -] - -build-env: [ - [ COQ_CONFIGURE_PREFIX = "%{prefix}" ] -] - -build: [ - [ "dune" "build" "@refman" "-j" jobs ] -] - -# Would be better to have a *-conf package? -depexts: [ - [ "sphinx" ] - [ "sphinx_rtd_theme" ] - [ "beautifulsoup4" ] - [ "antlr4-python3-runtime"] - [ "pexpect" ] - [ "sphinxcontrib-bibtex" ] -] diff --git a/doc/dune b/doc/dune index 02ca33b682..4210c0a482 100644 --- a/doc/dune +++ b/doc/dune @@ -1,5 +1,10 @@ (rule - (targets sphinx_build) + (targets unreleased.rst) + (deps (source_tree changelog)) + (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) + +(alias + (name refman-deps) (deps ; We could use finer dependencies here so the build is faster: ; @@ -10,23 +15,34 @@ ; + tools/coqdoc/coqdoc.css (package coq) (source_tree sphinx) - (source_tree tools) + (source_tree tools/coqrst) unreleased.rst - (env_var SPHINXWARNOPT)) - (action - (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (env_var SPHINXWARNOPT))) -(alias - (name refman-html) - (deps sphinx_build)) +(rule + (targets refman-html) + (alias refman-html) + (package coq-doc) + (deps (alias refman-deps)) + (action + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets}))) (rule - (targets unreleased.rst) - (deps (source_tree changelog)) - (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) + (targets refman-pdf) + (alias refman-pdf) + (package coq-doc) + (deps (alias refman-deps)) + (action + (progn + (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets}) + (chdir %{targets} (run make))))) + +; 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! -; The install target still needs more work. -; (install -; (section doc) -; (package coq-refman) -; (files sphinx_build)) +(install + (files (refman-html as html/refman) (refman-pdf as pdf/refman)) + (section doc) + (package coq-doc)) diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 093c7a62b2..0b6ca5f178 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -13,6 +13,8 @@ (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) @@ -31,6 +33,12 @@ (progn (cat %{header}) (cat index-list.html) (cat %{footer}))) (run cp _index.html html/index.html)))) -(alias - (name stdlib-html) - (deps 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)) -- cgit v1.2.3