From fd3604cb2ff1657846a2bf358831e643b60f0f52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Mon, 3 Jul 2023 13:55:56 +0200 Subject: [PATCH] Auto-generate opam files using Dune. --- coq-core.opam | 10 ++++++---- coq-core.opam.template | 22 ++++++++++++++++++++++ coq-doc.opam | 6 ++++-- coq-stdlib.opam | 13 +++++++------ coq-stdlib.opam.template | 25 +++++++++++++++++++++++++ coq.opam | 5 ++++- coqide-server.opam | 6 ++++-- coqide.opam | 6 ++++-- dune-project | 3 +-- 9 files changed, 77 insertions(+), 19 deletions(-) create mode 100644 coq-core.opam.template create mode 100644 coq-stdlib.opam.template diff --git a/coq-core.opam b/coq-core.opam index 8b099cc827ab..17581cad9b22 100644 --- a/coq-core.opam +++ b/coq-core.opam @@ -32,10 +32,12 @@ depends: [ "ocamlfind" {>= "1.8.1"} "zarith" {>= "1.11"} "ounit2" {with-test} + "odoc" {with-doc} ] +depopts: ["coq-native"] +dev-repo: "git+https://github.com/coq/coq.git" build: [ - # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 - # ["dune" "subst"] {pinned} + ["dune" "subst"] {dev} [ "./configure" "-prefix" prefix "-mandir" man @@ -49,10 +51,10 @@ build: [ name "-j" jobs + "--promote-install-files=false" "@install" "@runtest" {with-test} "@doc" {with-doc} ] + ["dune" "install" "-p" name "--create-install-files" name] ] -dev-repo: "git+https://github.com/coq/coq.git" -depopts: ["coq-native"] diff --git a/coq-core.opam.template b/coq-core.opam.template new file mode 100644 index 000000000000..3484d4ce7366 --- /dev/null +++ b/coq-core.opam.template @@ -0,0 +1,22 @@ +build: [ + ["dune" "subst"] {dev} + [ "./configure" + "-prefix" prefix + "-mandir" man + "-libdir" "%{lib}%/coq" + "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + ] + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] diff --git a/coq-doc.opam b/coq-doc.opam index deec6ca199f2..88b9078fa223 100644 --- a/coq-doc.opam +++ b/coq-doc.opam @@ -19,10 +19,10 @@ depends: [ "dune" {>= "2.9"} "conf-python-3" {build} "coq" {build & = version} + "odoc" {with-doc} ] build: [ - # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 - # ["dune" "subst"] {pinned} + ["dune" "subst"] {dev} [ "dune" "build" @@ -30,9 +30,11 @@ build: [ name "-j" jobs + "--promote-install-files=false" "@install" "@runtest" {with-test} "@doc" {with-doc} ] + ["dune" "install" "-p" name "--create-install-files" name] ] dev-repo: "git+https://github.com/coq/coq.git" diff --git a/coq-stdlib.opam b/coq-stdlib.opam index e3b4006b1685..3cb83999c000 100644 --- a/coq-stdlib.opam +++ b/coq-stdlib.opam @@ -25,12 +25,13 @@ bug-reports: "https://github.com/coq/coq/issues" depends: [ "dune" {>= "2.9"} "coq-core" {= version} + "odoc" {with-doc} ] +depopts: ["coq-native"] +dev-repo: "git+https://github.com/coq/coq.git" build: [ - # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 - # ["dune" "subst"] {pinned} - # - # XXX need to run configure as in coq-core, or else dunestrap will + ["dune" "subst"] {dev} + # need to run configure as in coq-core, or else dunestrap will # use the default rule in config [ "./configure" "-prefix" prefix @@ -46,10 +47,10 @@ build: [ name "-j" jobs + "--promote-install-files=false" "@install" "@runtest" {with-test} "@doc" {with-doc} ] + ["dune" "install" "-p" name "--create-install-files" name] ] -dev-repo: "git+https://github.com/coq/coq.git" -depopts: ["coq-native"] diff --git a/coq-stdlib.opam.template b/coq-stdlib.opam.template new file mode 100644 index 000000000000..352d17b3038e --- /dev/null +++ b/coq-stdlib.opam.template @@ -0,0 +1,25 @@ +build: [ + ["dune" "subst"] {dev} + # need to run configure as in coq-core, or else dunestrap will + # use the default rule in config + [ "./configure" + "-prefix" prefix + "-mandir" man + "-libdir" "%{lib}%/coq" + "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + ] + [ make "dunestrap" "COQ_DUNE_EXTRA_OPT=-split" ] + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] diff --git a/coq.opam b/coq.opam index fe3d77ad6044..bc863fa11093 100644 --- a/coq.opam +++ b/coq.opam @@ -24,9 +24,10 @@ depends: [ "coq-core" {= version} "coq-stdlib" {= version} "coqide-server" {= version} + "odoc" {with-doc} ] build: [ - ["dune" "subst"] {pinned} + ["dune" "subst"] {dev} [ "dune" "build" @@ -34,9 +35,11 @@ build: [ name "-j" jobs + "--promote-install-files=false" "@install" "@runtest" {with-test} "@doc" {with-doc} ] + ["dune" "install" "-p" name "--create-install-files" name] ] dev-repo: "git+https://github.com/coq/coq.git" diff --git a/coqide-server.opam b/coqide-server.opam index ca03e2b9defc..ac90917064fe 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -21,10 +21,10 @@ bug-reports: "https://github.com/coq/coq/issues" depends: [ "dune" {>= "2.9"} "coq-core" {= version} + "odoc" {with-doc} ] build: [ - # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 - # ["dune" "subst"] {pinned} + ["dune" "subst"] {dev} [ "dune" "build" @@ -32,9 +32,11 @@ build: [ name "-j" jobs + "--promote-install-files=false" "@install" "@runtest" {with-test} "@doc" {with-doc} ] + ["dune" "install" "-p" name "--create-install-files" name] ] dev-repo: "git+https://github.com/coq/coq.git" diff --git a/coqide.opam b/coqide.opam index ae1270aa2fd1..6fd9e8d3ba00 100644 --- a/coqide.opam +++ b/coqide.opam @@ -24,10 +24,10 @@ depends: [ "coqide-server" {= version} "cairo2" {>= "0.6.4"} "lablgtk3-sourceview3" {>= "3.1.2"} + "odoc" {with-doc} ] build: [ - # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219 - # ["dune" "subst"] {pinned} + ["dune" "subst"] {dev} [ "dune" "build" @@ -35,9 +35,11 @@ build: [ name "-j" jobs + "--promote-install-files=false" "@install" "@runtest" {with-test} "@doc" {with-doc} ] + ["dune" "install" "-p" name "--create-install-files" name] ] dev-repo: "git+https://github.com/coq/coq.git" diff --git a/dune-project b/dune-project index e61b8472d545..92525b4cda8c 100644 --- a/dune-project +++ b/dune-project @@ -5,8 +5,7 @@ (formatting (enabled_for ocaml)) -; After Dune 2.8 we can use this, but let's wait for the build consolidation PR -; (generate_opam_files true) +(generate_opam_files true) (license LGPL-2.1-only) (maintainers "The Coq development team ")