From 1d454c7721a429490165d1147313c061164b0b66 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Nov 2019 19:57:02 +0100 Subject: [dune] Update to dune language version 2.0 This is the minimal set of changes requires for Coq to build under 2.0 mode. We may likely take advantage of some more new features. Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune in older versions as it will install a secondary compiler. --- .gitlab-ci.yml | 2 +- coq.opam | 4 ++-- coqide-server.opam | 4 ++-- coqide.opam | 8 ++++---- dev/build/windows/makecoq_mingw.sh | 19 ++++++++++++++++--- dev/ci/docker/bionic_coq/Dockerfile | 6 +++--- dev/dune-workspace.all | 2 +- doc/sphinx/dune | 8 +++++--- dune-project | 2 +- ide/dune | 2 ++ kernel/byterun/dune | 6 ++++-- topbin/dune | 1 + 12 files changed, 42 insertions(+), 22 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 49e1361407..6344b51702 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-11-25-V01" + CACHEKEY: "bionic_coq-V2019-12-03-V81" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/coq.opam b/coq.opam index 4399dafe7c..6aec0132be 100644 --- a/coq.opam +++ b/coq.opam @@ -21,8 +21,8 @@ license: "LGPL-2.1" version: "dev" depends: [ - "ocaml" { >= "4.05.0" } - "dune" { build & >= "1.10.0" } + "ocaml" { >= "4.05.0" } + "dune" { >= "2.0.0" } "ocamlfind" { build } "num" ] diff --git a/coqide-server.opam b/coqide-server.opam index 5da533ea6b..4cec409f78 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -21,8 +21,8 @@ license: "LGPL-2.1" version: "dev" depends: [ - "dune" { build & >= "1.10.0" } - "coq" { = version } + "dune" { >= "2.0.0" } + "coq" { = version } ] build: [ [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/coqide.opam b/coqide.opam index 3e588ed0cf..54b8dca98b 100644 --- a/coqide.opam +++ b/coqide.opam @@ -19,10 +19,10 @@ license: "LGPL-2.1" version: "dev" depends: [ - "dune" { build & >= "1.10.0" } - "coqide-server" { = version } - "lablgtk3" { >= "3.0.beta5" } - "lablgtk3-sourceview3" { >= "3.0.beta5" } + "dune" { >= "2.0.0" } + "coqide-server" { = version } + "lablgtk3" { >= "3.0.beta5" } + "lablgtk3-sourceview3" { >= "3.0.beta5" } ] build-env: [ diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 78c0b4b2c7..82cc7a7117 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1132,11 +1132,22 @@ function make_findlib { function make_dune { make_ocaml - if build_prep https://github.com/ocaml/dune/archive/ 1.10.0 tar.gz 1 dune-1.10.0 ; then + if build_prep https://github.com/ocaml/dune/archive/ 2.0.0 tar.gz 1 dune-2.0.0 ; then log2 make release log2 make install + # Dune support libs, we don't install glob and action-plugin as + # they are not needed by Coq + logn dune-private-build dune build -p dune-private-libs @install + logn dune-private-install dune install dune-private-libs + + logn dune-configurator-build dune build -p dune-configurator @install + logn dune-configurator-install dune install dune-configurator + + logn dune-build-info dune build -p dune-build-info @install + logn dune-build-info dune install dune-build-info + build_post fi } @@ -1191,7 +1202,8 @@ function make_ocaml_cairo2 { log2 dune build cairo2.install log2 dune install cairo2 - log2 dune clean + # See https://github.com/ocaml/dune/issues/2921 + # log2 dune clean build_post fi @@ -1216,7 +1228,8 @@ function make_lablgtk { log2 dune build -p lablgtk3-sourceview3 log2 dune install lablgtk3-sourceview3 - log2 dune clean + # See https://github.com/ocaml/dune/issues/2921 + # log2 dune clean build_post fi } diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index e80f96362b..8907843b12 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-11-25-V01" +# CACHEKEY: "bionic_coq-V2019-12-03-V81" # ^^ 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.1 dune.1.11.3 ounit.2.0.8 odoc.1.4.2" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.0 ounit.2.0.8 odoc.1.4.2" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.8.0" @@ -58,7 +58,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # EDGE switch ENV COMPILER_EDGE="4.09.0" \ COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \ - BASE_OPAM_EDGE="dune-release.1.3.2" + BASE_OPAM_EDGE="dune-release.1.3.3" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 28e8773e25..49e338d0a5 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -1,4 +1,4 @@ -(lang dune 1.10) +(lang dune 2.0) ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) diff --git a/doc/sphinx/dune b/doc/sphinx/dune index 353d58c676..b788fbbeed 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1,8 +1,10 @@ (dirs :standard _static) -(rule (targets README.gen.rst) +(rule + (targets README.gen.rst) (deps (source_tree ../tools/coqrst) README.template.rst) (action (run ../tools/coqrst/regen_readme.py %{targets}))) -(alias (name refman-html) - (action (diff README.rst README.gen.rst))) +(rule + (alias refman-html) + (action (diff README.rst README.gen.rst))) diff --git a/dune-project b/dune-project index 45d9d06314..1249c4af9f 100644 --- a/dune-project +++ b/dune-project @@ -1,4 +1,4 @@ -(lang dune 1.10) +(lang dune 2.0) (name coq) (using coq 0.1) diff --git a/ide/dune b/ide/dune index 7200915593..a599be9351 100644 --- a/ide/dune +++ b/ide/dune @@ -21,6 +21,7 @@ (package coqide-server) (modules idetop) (libraries coq.toplevel coqide-server.protocol) + (modes native byte) (link_flags -linkall)) (install @@ -45,6 +46,7 @@ (name coqide_main) (public_name coqide) (package coqide) + (optional) (modules coqide_main) (libraries coqide_gui)) diff --git a/kernel/byterun/dune b/kernel/byterun/dune index 8d8374a603..2998178be2 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -2,8 +2,10 @@ (name byterun) (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]") (public_name coq.vm) - (c_flags (:include %{project_root}/config/dune.c_flags)) - (c_names coq_fix_code coq_memory coq_values coq_interp)) + (foreign_stubs + (language c) + (names coq_fix_code coq_memory coq_values coq_interp) + (flags (:include %{project_root}/config/dune.c_flags)))) (rule (targets coq_instruct.h) diff --git a/topbin/dune b/topbin/dune index 7b77826216..46052c81e5 100644 --- a/topbin/dune +++ b/topbin/dune @@ -26,6 +26,7 @@ (package coq) (modules coqc_bin) (libraries coq.toplevel) + (modes native byte) ; Adding -ccopt -flto to links options could be interesting, however, ; it doesn't work on Windows (link_flags -linkall)) -- cgit v1.2.3