refinedc.opam 898 Bytes
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1
opam-version: "2.0"
2
3
4
5
6
7
name: "refinedc"
synopsis: "RefinedC verification framework"
description: """
RefinedC is a framework for verifying idiomatic, low-level C code using a
combination of refinement types and ownership types.
"""
Michael Sammler's avatar
Michael Sammler committed
8
license: "BSD"
9
10
11
12
13
14

maintainer: ["Michael Sammler <msammler@mpi-sws.org>"
             "Rodolphe Lepigre <lepigre@mpi-sws.org>"]
authors: ["Michael Sammler" "Rodolphe Lepigre" "Kayvan Memarian"]

homepage: "https://plv.mpi-sws.org/refinedc"
Michael Sammler's avatar
Michael Sammler committed
15
16
17
18
bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"

depends: [
Michael Sammler's avatar
Michael Sammler committed
19
  "coq" { (>= "8.13.2" & < "8.14~") }
Michael Sammler's avatar
Michael Sammler committed
20
  "coq-iris" { (= "dev.2021-07-29.2.bfccb2a2") | (= "dev") }
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
21
  "dune" {>= "2.7.0"}
22
23
  "cerberus" {= "~dev"}
  "cmdliner" {>= "1.0.4"}
Rodolphe Lepigre's avatar
Rodolphe Lepigre committed
24
  "earley" {= "3.0.0"}
25
  "toml" {= "5.0.0"}
Michael Sammler's avatar
Michael Sammler committed
26
27
]

28
29
30
31
build: [
  ["dune" "subst"] {pinned}
  ["dune" "build" "-p" name "-j" jobs]
]