coq-freespec-exec.opam

opam-version: "2.0"
maintainer: "Thomas Letan <lthms@soap.coffee>"
version: "dev"

homepage: "https://github.com/lthms/FreeSpec"
dev-repo: "git+https://github.com/lthms/FreeSpec.git"
bug-reports: "https://github.com/lthms/FreeSpec.git/issues"
doc: "https://lthms.github.io/FreeSpec"
license: "MPL-2.0"

synopsis: "A framework for implementing and certifying impure computations in Coq"
description: """
FreeSpec is a framework for the Coq proof assistant which allows to
implement and specify impure computations. This is the “exec” plugin,
which allows from executing impure computations from with Coq thanks
to a dedicated vernacular command.
"""

build: [
  ["patch" "-p1" "-i" "patches/opam-builds.patch"]
  ["dune" "build" "-p" name "-j" jobs]
]

depends: [
  "ocaml"
  "dune" {>= "2.5"}
  "coq" {>= "8.12" & < "8.14~" | = "dev"}
  "coq-freespec-core" {= "dev"}
  "coq-freespec-ffi" {= "dev"}
]

tags: [
  "keyword:plugin"
  "category:Miscellaneous/Coq Extensions"
  "logpath:FreeSpec.Exec"
]

authors: [
  "Thomas Letan"
  "Yann Régis-Gianas"
]

url {
  src: "git+https://github.com/lthms/FreeSpec.git#master"
}