Auto-generate opam files using Dune.

SkySkimmer · Jul 6, 2023 · fd3604c · fd3604c
1 parent 6b2e87b
commit fd3604c
Show file tree

Hide file tree

Showing 9 changed files with 77 additions and 19 deletions.
diff --git 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
@@ -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
@@ -19,20 +19,22 @@ 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"
     "-p"
     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
@@ -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
@@ -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
@@ -24,19 +24,22 @@ depends: [
   "coq-core" {= version}
   "coq-stdlib" {= version}
   "coqide-server" {= version}
+  "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst"] {pinned}
+  ["dune" "subst"] {dev}
   [
     "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]
 ]
 dev-repo: "git+https://github.com/coq/coq.git"
diff --git a/coqide-server.opam b/coqide-server.opam
@@ -21,20 +21,22 @@ 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"
     "-p"
     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
@@ -24,20 +24,22 @@ 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"
     "-p"
     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
@@ -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 <[email protected]>")