coq-eventstruct.opam

opam-version: "2.0"
maintainer: "Vladimir Gladstein <vovaglad00@gmail.com>"
version: "dev"

homepage: "https://github.com/event-structures/event-struct"
dev-repo: "git+https://github.com/event-structures/event-struct.git"
bug-reports: "https://github.com/event-structures/event-struct/issues"
doc: "https://event-structures.github.io/event-struct/"
license: "MIT"

synopsis: "Formalization of event structures in Coq"
description: """
A Coq library of formalized theory of event structures with applications to
concurrency semantics. Includes a theory of prime event structures and
operational small-step semantics for their incremental construction.
"""

build: [make "-j%{jobs}%" ]
install: [make "install"]
depends: [
  "coq" {(>= "8.13" & < "8.15~") | (= "dev")}
  "coq-mathcomp-ssreflect" {(>= "1.13.0" & < "1.15.0~") | (= "dev")}
  "coq-mathcomp-finmap" {(>= "1.5.1") | (= "dev")}
  "coq-mathcomp-tarjan" {(= "dev")}
  "coq-mathcomp-zify" {(>= "1.0.0") | (= "dev")}
  "coq-relation-algebra" {(>= "1.7.4") | (= "dev")}
  "coq-equations" {(>= "1.2") | (= "dev")}
]
# we pin dev version, because 1.0.0 and dev 
# use different module names (Kosaraju.v vs kosaraju.v)
pin-depends: [
  [ "coq-mathcomp-tarjan.dev" "git+https://github.com/math-comp/tarjan/"]
]
conflicts: [
  "coq-equations" {(= "dev+HoTT")}
]
tags: [
  "keyword:concurrency"
  "keyword:event structures"
  "keyword:weak memory models"
  "keyword:operational semantics"
  "category:Computer Science/Concurrency/Weak Memory Models"
  "logpath:eventstruct"
]
authors: [
  "Vladimir Gladstein <vovaglad00@gmail.com>"
  "Dmitrii Mikhailovskii <mikhaylovskiy.dmitriy@gmail.com>"
  "Evgenii Moiseenko <evg.moiseenko94@gmail.com>"
  "Anton Trunov <anton.a.trunov@gmail.com>"
]