coq-vst-iris.opam

opam-version: "2.0"
version: "dev"
synopsis: "Verified Software Toolchain with Iris"
description: "VST with support for Iris tactics, definitions, and notation. Especially useful for reasoning about fine-grained concurrent programs and logical atomicity."
authors: [
  "William Mansky"
  "Shengyi Wang"
]
maintainer: "VST team"
homepage: "http://vst.cs.princeton.edu/"
dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"

build: [
  [make "-j%{jobs}%" "build-iris" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
install: [
  [make "install-iris" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
run-test: [
  [make "-j%{jobs}%" "atomics" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
]
depends: [
  "coq-vst" { = version }
  "coq-iris" {>= "4.0.0"}
]
url {
  src: "git+https://github.com/PrincetonUniversity/VST.git#master"
}