rocq-core.opam

# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
version: "dev"
synopsis: "The Coq Proof Assistant with its prelude"
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.

This package includes the Rocq prelude, that is loaded automatically
by Rocq in every .v file, as well as other modules bound to the
Corelib.* and Ltac2.* namespaces."""
maintainer: ["The Coq development team <coqdev@inria.fr>"]
authors: ["The Coq development team, INRIA, CNRS, and contributors"]
license: "LGPL-2.1-only"
homepage: "https://coq.inria.fr/"
doc: "https://coq.github.io/doc/"
bug-reports: "https://github.com/coq/coq/issues"
depends: [
  "dune" {>= "3.8"}
  "rocq-runtime" {= version}
  "odoc" {with-doc}
]
depopts: ["coq-native"]
dev-repo: "git+https://github.com/coq/coq.git"
build: [
  ["dune" "subst"] {dev}
  # We tell dunestrap to use coq-config from rocq-runtime
  [ make "dunestrap" "COQ_SPLIT=1" "DUNESTRAPOPT=-p rocq-core"]
  [
    "dune"
    "build"
    "-p"
    name
    "-j"
    jobs
    "--promote-install-files=false"
    "@install"
    "@runtest" {with-test}
    "@doc" {with-doc}
  ]
  ["dune" "install" "-p" name "--create-install-files" name]
]