[dune] [opam] Generate opam files automatically using Dune.

- closes #12376 : dune version is now consistent as suggested
- cc #12858 : coqide and coqide-server do no depend on ocamlfind
  when built this way.
- closes #13372 : more precision in the license identifier

7 files changed, 193 insertions, 87 deletions

diff --git a/coq-doc.opam b/coq-doc.opam
index 2f4072955f..67cdbd8bf0 100644
--- a/coq-doc.opam
+++ b/coq-doc.opam
@@ -1,3 +1,6 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
 synopsis: "The Coq Proof Assistant --- Reference Manual"
 description: """
 Coq is a formal proof management system. It provides
@@ -5,37 +8,29 @@ 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."
+This package provides the Coq Reference Manual."""
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "OPL-1.0"
 homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
-dev-repo: "https://github.com/coq/coq.git"
-license: "Open Publication License"
-
-version: "dev"
-
 depends: [
-  "dune"      { build }
-  "coq"       { build & = version }
+  "dune" {build & >= "2.5.0"}
+  "coq" {build & = version}
 ]
-
-build-env: [
-  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
-]
-
 build: [
-  [ "dune" "build" "-p" name "-j" jobs ]
-]
-
-# Would be better to have a *-conf package?
-depexts: [
-  [ "sphinx" ]
-  [ "sphinx_rtd_theme" ]
-  [ "beautifulsoup4" ]
-  [ "antlr4-python3-runtime"]
-  [ "pexpect" ]
-  [ "sphinxcontrib-bibtex" ]
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
+dev-repo: "git+https://github.com/coq/coq.git"
diff --git a/coq.opam b/coq.opam
index 77fdf14834..2f14b00238 100644
--- a/coq.opam
+++ b/coq.opam
@@ -1,33 +1,45 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
 synopsis: "The Coq Proof Assistant"
 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. Typical
-applications include the certification of properties of programming
-languages (e.g. the CompCert compiler certification project, or the
-Bedrock verified low-level programming library), the formalization of
-mathematics (e.g. the full formalization of the Feit-Thompson theorem
-or homotopy type theory) and teaching.
-"""
-opam-version: "2.0"
-maintainer: "The Coq development team <coqdev@inria.fr>"
-authors: "The Coq development team, INRIA, CNRS, and contributors."
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching."""
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
-dev-repo: "git+https://github.com/coq/coq.git"
-license: "LGPL-2.1"
-
-version: "dev"
-
 depends: [
-  "ocaml"     { >= "4.05.0" }
-  "dune"      { >= "2.5.0"  }
-  "ocamlfind" { build }
-  "zarith"    { >= "1.10" }
+  "ocaml" {>= "4.05.0"}
+  "dune" {>= "2.5.0"}
+  "ocamlfind" {>= "1.8.1"}
+  "zarith" {>= "1.10"}
 ]
-
 build: [
-  [ "./configure" "-prefix" prefix "-native-compiler" "no" ]
-  [ "dune" "build" "-p" name "-j" jobs ]
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
+build-env: [
+  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
 ]
diff --git a/coq.opam.template b/coq.opam.template
new file mode 100644
index 0000000000..c0efccdc0f
--- /dev/null
+++ b/coq.opam.template
@@ -0,0 +1,3 @@
+build-env: [
+  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
+]
diff --git a/coqide-server.opam b/coqide-server.opam
index 4cec409f78..101cd4ad78 100644
--- a/coqide-server.opam
+++ b/coqide-server.opam
@@ -1,4 +1,7 @@
-synopsis: "The Coq Proof Assistant"
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "The Coq Proof Assistant, XML protocol server"
 description: """
 Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable
@@ -8,21 +11,29 @@ semi-interactive development of machine-checked proofs.
 This package provides the `coqidetop` language server, an
 implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
 which allows clients, such as CoqIDE, to interact with Coq in a
-structured way.
-"""
-opam-version: "2.0"
-maintainer: "The Coq development team <coqdev@inria.fr>"
-authors: "The Coq development team, INRIA, CNRS, and contributors."
+structured way."""
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
-dev-repo: "git+https://github.com/coq/coq.git"
-license: "LGPL-2.1"
-
-version: "dev"
-
 depends: [
-  "dune"      { >= "2.0.0" }
-  "coq"       {  = version }
+  "dune" {>= "2.5.0"}
+  "coq" {= version}
 ]
-
-build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/coq/coq.git"
diff --git a/coqide.opam b/coqide.opam
index 54b8dca98b..3007200fe5 100644
--- a/coqide.opam
+++ b/coqide.opam
@@ -1,4 +1,7 @@
-synopsis: "The Coq Proof Assistant"
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "The Coq Proof Assistant --- GTK3 IDE"
 description: """
 Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable
@@ -6,26 +9,29 @@ algorithms and theorems together with an environment for
 semi-interactive development of machine-checked proofs.
 
 This package provides the CoqIDE, a graphical user interface for the
-development of interactive proofs.
-"""
-opam-version: "2.0"
-maintainer: "The Coq development team <coqdev@inria.fr>"
-authors: "The Coq development team, INRIA, CNRS, and contributors."
+development of interactive proofs."""
+maintainer: ["The Coq development team <coqdev@inria.fr>"]
+authors: ["The Coq development team, INRIA, CNRS, and contributors"]
+license: "LGPL-2.1-only"
 homepage: "https://coq.inria.fr/"
+doc: "https://coq.github.io/doc/"
 bug-reports: "https://github.com/coq/coq/issues"
-dev-repo: "git+https://github.com/coq/coq.git"
-license: "LGPL-2.1"
-
-version: "dev"
-
 depends: [
-  "dune"                 { >= "2.0.0" }
-  "coqide-server"        {  = version }
-  "lablgtk3"             { >= "3.0.beta5" }
-  "lablgtk3-sourceview3" { >= "3.0.beta5" }
+  "dune" {>= "2.5.0"}
+  "coqide-server" {= version}
 ]
-
-build-env: [
-  [ COQ_CONFIGURE_PREFIX = "%{prefix}" ]
+build: [
+  ["dune" "subst"] {pinned}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
-build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
+dev-repo: "git+https://github.com/coq/coq.git"
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 8b0bf216e3..de3d5a3d15 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -175,6 +175,12 @@ local copy of Coq. For this purpose, Dune supports the `-p` option, so
 version of Coq libs, and use a "release" profile that for example
 enables stronger compiler optimizations.
 
+## OPAM file generation
+
+`.opam` files are automatically generated by Dune from the package
+descriptions in the `dune-project` file; see Dune's manual for more
+details.
+
 ## Stanzas
 
 `dune` files contain the so-called "stanzas", that may declare:
diff --git a/dune-project b/dune-project
index 873d03e8dd..1265c993b7 100644
--- a/dune-project
+++ b/dune-project
@@ -5,6 +5,79 @@
 (formatting
  (enabled_for ocaml))
 
-; TODO
-;
-; (generate_opam_files true)
+(generate_opam_files true)
+
+(license LGPL-2.1-only)
+(maintainers "The Coq development team <coqdev@inria.fr>")
+(authors "The Coq development team, INRIA, CNRS, and contributors")
+; This generates bug-reports and dev-repo
+(source (github coq/coq))
+(homepage https://coq.inria.fr/)
+(documentation "https://coq.github.io/doc/")
+(version dev)
+
+; Note that we use coq.opam.template to have dune add the correct opam
+; prefix for configure
+(package
+ (name coq)
+ (depends
+  (ocaml (>= 4.05.0))
+  (dune  (>= 2.5.0))
+  (ocamlfind (>= 1.8.1))
+  (zarith (>= 1.10)))
+ (synopsis "The Coq Proof Assistant")
+ (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.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching."))
+
+(package
+ (name coqide-server)
+ (depends
+  (dune (>= 2.5.0))
+  (coq (= :version)))
+ (synopsis "The Coq Proof Assistant, XML protocol server")
+ (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 `coqidetop` language server, an
+implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md)
+which allows clients, such as CoqIDE, to interact with Coq in a
+structured way."))
+
+(package
+ (name coqide)
+ (depends
+  (dune (>= 2.5.0))
+  (coqide-server (= :version)))
+ (synopsis "The Coq Proof Assistant --- GTK3 IDE")
+ (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 CoqIDE, a graphical user interface for the
+development of interactive proofs."))
+
+(package
+ (name coq-doc)
+ (license "OPL-1.0")
+ (depends
+  (dune (and :build (>= 2.5.0)))
+  (coq (and :build (= :version))))
+ (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."))
+