diff options
| -rw-r--r-- | .gitlab-ci.yml | 46 | ||||
| -rw-r--r-- | Makefile.dune | 35 | ||||
| -rw-r--r-- | config/dune | 2 | ||||
| -rw-r--r-- | coq-refman.opam | 39 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 4 | ||||
| -rw-r--r-- | dev/doc/build-system.dune.md | 15 | ||||
| -rw-r--r-- | doc/dune | 24 | ||||
| -rw-r--r-- | doc/sphinx/dune | 1 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 2 | ||||
| -rw-r--r-- | dune-project | 3 |
10 files changed, 137 insertions, 34 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b1a805b59e..de0de4cf83 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-11-08-V1" + CACHEKEY: "bionic_coq-V2018-12-05-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -89,18 +89,37 @@ after_script: - set +e +# Template for building Coq + stdlib, typical use: overload the switch .dune-template: &dune-template - dependencies: [] stage: build + dependencies: [] + script: + - set -e + - make -f Makefile.dune world + - set +e + variables: + OPAM_SWITCH: edge artifacts: name: "$CI_JOB_NAME" paths: - _build/ expire_in: 1 week + +.dune-ci-template: &dune-ci-template + stage: test + dependencies: + - build:egde:dune:dev script: - set -e + - echo 'start:coq.test' - make -f Makefile.dune "$DUNE_TARGET" + - echo 'end:coq.test' - set +e + variables: &dune-ci-template-vars + OPAM_SWITCH: edge + artifacts: &dune-ci-template-artifacts + name: "$CI_JOB_NAME" + expire_in: 1 month # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that @@ -221,9 +240,6 @@ build:edge+flambda: build:egde:dune:dev: <<: *dune-template - variables: - OPAM_SWITCH: edge - DUNE_TARGET: world build:base+async: <<: *build-template @@ -291,15 +307,23 @@ doc:refman: dependencies: - build:base +doc:refman:dune: + <<: *dune-ci-template + variables: + <<: *dune-ci-template-vars + DUNE_TARGET: refman-html + artifacts: + <<: *dune-ci-template-artifacts + paths: + - _build/default/doc/sphinx_build/html + doc:ml-api:odoc: - stage: test - dependencies: - - build:egde:dune:dev - script: make -f Makefile.dune apidoc + <<: *dune-ci-template variables: - OPAM_SWITCH: edge + <<: *dune-ci-template-vars + DUNE_TARGET: apidoc artifacts: - name: "$CI_JOB_NAME" + <<: *dune-ci-template-artifacts paths: - _build/default/_doc/ diff --git a/Makefile.dune b/Makefile.dune index 2293c69c38..4baf3402f1 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -1,7 +1,10 @@ # -*- mode: makefile -*- # Dune Makefile for Coq -.PHONY: help voboot states world watch check quickbyte quickopt test-suite release apidoc ocheck ireport clean +.PHONY: help voboot states world watch check # Main developer targets +.PHONY: quickbyte quickopt # Partial / quick developer targets +.PHONY: test-suite refman-html apidoc release # Accesory targets +.PHONY: ocheck ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build # DUNEOPT=--display=short @@ -10,15 +13,20 @@ BUILD_CONTEXT=_build/default help: @echo "Welcome to Coq's Dune-based build system. Targets are:" - @echo " - states: build a minimal functional coqtop" - @echo " - world: build all binaries and libraries" - @echo " - watch: build all binaries and libraries [continuous build]" - @echo " - check: build all ML files as fast as possible [requires Dune >= 1.5.0]" - @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" - @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" - @echo " - test-suite: run Coq's test suite" - @echo " - release: build Coq in release mode" - @echo " - apidoc: build ML API documentation" + @echo "" + @echo " - states: build a minimal functional coqtop" + @echo " - world: build all binaries and libraries" + @echo " - watch: build all binaries and libraries [continuous build]" + @echo " - check: build all ML files as fast as possible" + @echo "" + @echo " - quickbyte: build main ML files [coqtop + plugins + ide + printers] using the bytecode compiler" + @echo " - quickopt: build main ML files [coqtop + plugins + ide + printers] using the optimizing compiler" + @echo "" + @echo " - test-suite: run Coq's test suite" + @echo " - refman-html: build Coq's reference manual [HTML version]" + @echo " - apidoc: build ML API documentation" + @echo " - release: build Coq in release mode" + @echo "" @echo " - ocheck: build for all supported OCaml versions [requires OPAM]" @echo " - ireport: build with optimized flambda settings and emit an inline report" @echo " - clean: remove build directory and autogenerated files" @@ -55,12 +63,15 @@ quickopt: voboot test-suite: voboot dune runtest $(DUNEOPT) -release: voboot - dune build $(DUNEOPT) -p coq +refman-html: voboot + dune build @refman-html apidoc: voboot dune build $(DUNEOPT) @doc +release: voboot + dune build $(DUNEOPT) -p coq + ocheck: voboot dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all diff --git a/config/dune b/config/dune index cc993b97c9..c146e7df67 100644 --- a/config/dune +++ b/config/dune @@ -7,7 +7,7 @@ ; Dune doesn't use configure's output, but it is still necessary for ; some Coq files to work; will be fixed in the future. (rule - (targets coq_config.ml Makefile) + (targets coq_config.ml coq_config.py Makefile) (mode fallback) (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX)) (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no)))) diff --git a/coq-refman.opam b/coq-refman.opam new file mode 100644 index 0000000000..b9500243a3 --- /dev/null +++ b/coq-refman.opam @@ -0,0 +1,39 @@ +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 <coqdev@inria.fr>" +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" + +depends: [ + "dune" { build } + "coq" { build } +] + +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/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 diff --git a/doc/dune b/doc/dune new file mode 100644 index 0000000000..54ffa87205 --- /dev/null +++ b/doc/dune @@ -0,0 +1,24 @@ +(rule + (targets sphinx_build) + (deps + ; We could use finer dependencies here so the build is faster: + ; + ; - vo files: generated by sphinx after parsing the doc, promoted, + ; - Static files: + ; + %{bin:coqdoc} etc... + ; + config/coq_config.py + ; + tools/coqdoc/coqdoc.css + (package coq) + (source_tree sphinx) + (source_tree tools)) + (action (run sphinx-build -j4 -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + +(alias + (name refman-html) + (deps sphinx_build)) + +; The install target still needs more work. +; (install +; (section doc) +; (package coq-refman) +; (files sphinx_build)) diff --git a/doc/sphinx/dune b/doc/sphinx/dune new file mode 100644 index 0000000000..fff025c919 --- /dev/null +++ b/doc/sphinx/dune @@ -0,0 +1 @@ +(dirs :standard _static) diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index 57adcb287c..1de9890992 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -35,7 +35,7 @@ COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SY def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" - coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") + coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN", ""), "coqdoc") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") if platform.system().startswith("CYGWIN"): # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..." diff --git a/dune-project b/dune-project index 85238c70c5..f0ac11ba61 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,2 @@ -(lang dune 1.4) - +(lang dune 1.6) (name coq) |