Skip to content
Snippets Groups Projects
Commit dd8067c5 authored by Opam Update Bot's avatar Opam Update Bot
Browse files

Automatic publication of dev.2025-03-11.0.415e1d8c for coq-iris-deprecated...

Automatic publication of dev.2025-03-11.0.415e1d8c for coq-iris-deprecated coq-iris-heap-lang coq-iris-unstable coq-iris
parent eceb1506
No related branches found
No related tags found
No related merge requests found
opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The Iris Team"
license: "BSD-3-Clause"
homepage: "https://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
version: "dev"
synopsis: "Deprecated Iris libraries"
description: """
This package contains libraries that have been deprecated from Iris, and are planned to be
entirely removed at some point.
"""
depends: [
"coq-iris" {= version}
]
build: ["./make-package" "iris_deprecated" "-j%{jobs}%"]
install: ["./make-package" "iris_deprecated" "install"]
url { src: "git+https://gitlab.mpi-sws.org/iris/iris.git#415e1d8cf53d0005a82b0f22ac73445a8047d67b" }
opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The Iris Team"
license: "BSD-3-Clause"
homepage: "https://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
version: "dev"
synopsis: "The canonical example language for Iris"
description: """
This package defines HeapLang, a concurrent lambda calculus with references, and
uses Iris to build a program logic for HeapLang programs.
"""
tags: [
"logpath:iris.heap_lang"
]
depends: [
"coq-iris" {= version}
]
build: ["./make-package" "iris_heap_lang" "-j%{jobs}%"]
install: ["./make-package" "iris_heap_lang" "install"]
url { src: "git+https://gitlab.mpi-sws.org/iris/iris.git#415e1d8cf53d0005a82b0f22ac73445a8047d67b" }
opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The Iris Team"
license: "BSD-3-Clause"
homepage: "https://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
version: "dev"
synopsis: "Unfinished Iris libraries"
description: """
This package contains libraries that have been proposed for inclusion in Iris, but more
work is needed before they are ready for this.
"""
depends: [
"coq-iris" {= version}
"coq-iris-heap-lang" {= version}
]
build: ["./make-package" "iris_unstable" "-j%{jobs}%"]
install: ["./make-package" "iris_unstable" "install"]
url { src: "git+https://gitlab.mpi-sws.org/iris/iris.git#415e1d8cf53d0005a82b0f22ac73445a8047d67b" }
opam-version: "2.0"
maintainer: "Ralf Jung <jung@mpi-sws.org>"
authors: "The Iris Team"
license: "BSD-3-Clause"
homepage: "https://iris-project.org/"
bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
version: "dev"
synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
description: """
Iris is a framework for reasoning about the safety of concurrent programs using
concurrent separation logic. It can be used to develop a program logic, for
defining logical relations, and for reasoning about type systems, among other
applications. This package includes the base logic, Iris Proof Mode (IPM) /
MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
for an instantiation of the program logic to a particular programming language.
"""
tags: [
"logpath:iris.prelude"
"logpath:iris.algebra"
"logpath:iris.si_logic"
"logpath:iris.bi"
"logpath:iris.proofmode"
"logpath:iris.base_logic"
"logpath:iris.program_logic"
]
depends: [
"coq" { (>= "8.19" & < "9.1~") | (= "dev") }
"coq-stdpp" { (= "dev.2025-02-26.0.d2e8771d") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
install: ["./make-package" "iris" "install"]
url { src: "git+https://gitlab.mpi-sws.org/iris/iris.git#415e1d8cf53d0005a82b0f22ac73445a8047d67b" }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment