From 03401366d06f9d9e858a4451ec957e9f98154120 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 24 Sep 2018 02:22:00 +0200 Subject: [dune] [opam] Move to OPAM 2.0 We need to update in Docker: - dune to 1.4.0: as it honors `-p` on test stanzas - dune-release to 1.1.0: support for OPAM 2.0 + fixes This makes `dune-release distrib` / `dune-release opam pkg` work. TODO: we need to figure out what is going on with the versioning. Should we do `dune subst` on `pinned`? --- coq.opam | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) (limited to 'coq.opam') diff --git a/coq.opam b/coq.opam index f5f553af2c..ab18119ac4 100644 --- a/coq.opam +++ b/coq.opam @@ -1,18 +1,28 @@ -opam-version: "1.2" +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 " authors: "The Coq development team, INRIA, CNRS, and contributors." homepage: "https://coq.inria.fr/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" +dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ ocaml-version >= "4.05.0" ] - depends: [ - "dune" { build & >= "1.2.0" } - "ocamlfind" { build } + "ocaml" { >= "4.05.0" } + "dune" { build & >= "1.4.0" } "num" - "camlp5" { >= "7.03" } + "camlp5" { >= "7.03" } ] build-env: [ -- cgit v1.2.3