aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Roux2020-03-24 16:05:42 +0100
committerPierre Roux2020-03-25 11:19:41 +0100
commit5e3e9507f890c01e1c48ce3b8014257ffd9a0931 (patch)
tree344e6d3865f41964d4ab02617fe526ac085361d2
parent9f1f56e04fab689ab05339f8cddea4bd2935a554 (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.docker38
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"]
+]