opam-version: "2.0"
maintainer: "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-only"
synopsis: "Formal proof management system"
description: """
The Coq proof assistant 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 and the
Bedrock verified low-level programming library), the formalization of
mathematics (e.g., the full formalization of the Feit-Thompson theorem
and homotopy type theory) and teaching.
"""

depends: [
  "ocaml" {>= "4.05.0" & < "4.12"}
  "ocamlfind" {build}
  "num"
  "conf-findutils" {build}
]
depopts: [
  "coq-native"
]
build: [
  [
    "./configure"
    "-configdir" "%{lib}%/coq/config"
    "-prefix" prefix
    "-mandir" man
    "-docdir" doc
    "-libdir" "%{lib}%/coq"
    "-datadir" "%{share}%/coq"
    "-coqide" "no"
    "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed}
  ]
  [make "COQ_USE_DUNE=" "-j%{jobs}%"]
  [make "COQ_USE_DUNE=" "-j%{jobs}%" "byte"]
]
install: [
  [make "COQ_USE_DUNE=" "install"]
  [make "COQ_USE_DUNE=" "install-byte"]
]

url {
  src: "https://github.com/coq/coq/releases/download/V8.12.1/coq-8.12.1.tar.gz"
  checksum: "sha512=39452c86a35403b4ca7427c1973b93bc4d1e0052f12a53608ca94bbd2a4f902b9fc0f58b550b7eba03c2d346e06989104e92eee0d842ec267ce69200b8aa37a6"
}
extra-source "coq.install" {
  src:
    "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/coq/coq.install.8.12.1"
  checksum:
    "sha512=b501737b4dbd22adc1c0377d744448056fb1dc493caf72c05f57c8463cf23f758373605ab3a50b9f505e4c856c41039d0bd7f81f96ed62adc6a674179523e7d2"
}