# This file is generated by dune, edit dune-project instead

opam-version: "2.0"

version: "dev"

synopsis: "The Rocq Prover with its prelude"

description: """

The Rocq Prover is an interactive theorem prover, or proof assistant. 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 Rocq development team <coqdev@inria.fr>"]

authors: ["The Rocq 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}

]

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]

]