diff options
| author | Théo Zimmermann | 2018-12-14 12:53:29 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-14 12:53:29 +0100 |
| commit | 40aac459c94b9a8696e4d23dfdc0ce9279e63616 (patch) | |
| tree | c6fd34efea1f0ca2638bc9aa68809a2d3640ed46 /dev | |
| parent | 7e3603069cf591c6c70ef25d4cfc72f62aa44058 (diff) | |
| parent | ca4e25215144503f1dd42903421a61baee22b73e (diff) | |
Merge PR #9147: [dune] [doc] Support for building the reference manual with Dune.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 4 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 15 |
2 files changed, 12 insertions, 7 deletions
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 3fc6dce4e5..f1020e5f8e 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-11-08-V1" +# CACHEKEY: "bionic_coq-V2018-12-05-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.1 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 3609171b82..01c32041d2 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -10,9 +10,9 @@ Coq can now be built using [Dune](https://github.com/ocaml/dune). ## Quick Start -Dune >= 1.5.0 is recommended, see `dune-project` for the minimum -required version; type `dune build` to build the base Coq -libraries. No call to `./configure` is needed. +Usually, using the latest version of Dune is recommended, see +`dune-project` for the minimum required version; type `dune build` to +build the base Coq libraries. No call to `./configure` is needed. Dune will get confused if it finds leftovers of in-tree compilation, so please be sure your tree is clean from objects files generated by @@ -63,11 +63,16 @@ ml files in quick mode. Dune also provides targets for documentation, testing, and release builds, please see below. -## Documentation and test targets +## Documentation and testing targets Coq's test-suite can be run with `dune runtest`. -The documentation target is not implemented in Dune yet. +There is preliminary support to build the API documentation and +reference manual in HTML format, use `dune build {@doc,@refman-html}` +to generate them. + +So far these targets will build the documentation artifacts, however +no install rules are generated yet. ## Developer shell |