diff options
| author | Pierre Roux | 2020-03-24 16:05:42 +0100 |
|---|---|---|
| committer | Pierre Roux | 2020-03-25 11:19:41 +0100 |
| commit | 5e3e9507f890c01e1c48ce3b8014257ffd9a0931 (patch) | |
| tree | 344e6d3865f41964d4ab02617fe526ac085361d2 | |
| parent | 9f1f56e04fab689ab05339f8cddea4bd2935a554 (diff) | |
Add a specific opam file to build te docker image
The Docker image coqorg/coq:dev is currently built using the OPAM file
coq.opam. Since this file is used for develoment purpose, it would be
better to use a more stable one for building the docker images. The
OPAM option "--locked=docker" will then be used in the opam pin
command when building the docker image to use the new coq.opam.docker
file.
The new file builds Coq using make, this is temporary and could be
reverted to dune once it supports "-native-compiler yes".
| -rw-r--r-- | coq.opam.docker | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/coq.opam.docker b/coq.opam.docker new file mode 100644 index 0000000000..229a47a87b --- /dev/null +++ b/coq.opam.docker @@ -0,0 +1,38 @@ +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: "git+https://github.com/coq/coq.git" +license: "LGPL-2.1" + +version: "dev" + +depends: [ + "ocaml" { >= "4.05.0" } + "ocamlfind" { build } + "num" + "conf-findutils" {build} +] + +build: [ + [ "./configure" "-prefix" prefix "-coqide" "no" ] + [make "-j%{jobs}%"] + [make "-j%{jobs}%" "byte"] +] +install: [ + [make "install"] + [make "install-byte"] +] |
