diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | coq.opam | 24 | ||||
| -rw-r--r-- | coqide-server.opam | 20 | ||||
| -rw-r--r-- | coqide.opam | 19 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 6 | ||||
| -rw-r--r-- | dev/dune-workspace.all | 2 | ||||
| -rw-r--r-- | dune | 1 | ||||
| -rw-r--r-- | dune-project | 2 |
8 files changed, 52 insertions, 24 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index bb1aa81a73..01931fd7ef 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-10-22-V1" + CACHEKEY: "bionic_coq-V2018-10-23-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -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 <coqdev@inria.fr>" 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: [ diff --git a/coqide-server.opam b/coqide-server.opam index 546ce75dbd..ed6f3d98d8 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -1,15 +1,25 @@ -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. + +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." 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" } + "dune" { build & >= "1.4.0" } "coq" ] diff --git a/coqide.opam b/coqide.opam index 17fb5dbbe2..314943a881 100644 --- a/coqide.opam +++ b/coqide.opam @@ -1,16 +1,23 @@ -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. + +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." 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" } - "coq" + "dune" { build & >= "1.4.0" } "coqide-server" "conf-gtksourceview" "lablgtk" { >= "2.18.5" } diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 41e1d1a937..098c950b32 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-22-V1" +# CACHEKEY: "bionic_coq-V2018-10-23-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.3.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. @@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="dune-release.0.3.0" + BASE_OPAM_EDGE="dune-release.1.1.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 93b807d5e3..f45f6de529 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -1,4 +1,4 @@ -(lang dune 1.2) +(lang dune 1.4) ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) @@ -38,4 +38,5 @@ ; Use summary.log as the target (alias (name runtest) + (package coqide-server) (deps test-suite/summary.log)) diff --git a/dune-project b/dune-project index 607e5a68a5..85238c70c5 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 1.2) +(lang dune 1.4) (name coq) |