1 files changed, 54 insertions, 0 deletions
diff --git a/coq-core.opam b/coq-core.opam
new file mode 100644
index 0000000000..8b8c43f66e
--- /dev/null
+++ b/coq-core.opam
@@ -0,0 +1,54 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "dev"
+synopsis: "The Coq Proof Assistant -- Core Binaries and Tools"
+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.
+
+This package includes the Coq core binaries, plugins, and tools, but
+not the vernacular standard library.
+
+Note that in this setup, Coq needs to be started with the -boot and
+-noinit options, as will otherwise fail to find the regular Coq
+prelude, now living in the coq-stdlib package."""
+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"
+depends: [
+  "dune" {>= "2.5"}
+  "ocaml" {>= "4.05.0"}
+  "ocamlfind" {>= "1.8.1"}
+  "zarith" {>= "1.10"}
+  "ounit2" {with-test}
+]
+build: [
+  # Requires dune 2.8 due to https://github.com/ocaml/dune/issues/3219
+  # ["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}" ]
+]