From 80ad6e5ce4f08db4ba3089e89c691bacc741c992 Mon Sep 17 00:00:00 2001
From: Opam Update Bot <opam-update@botland>
Date: Mon, 31 Mar 2025 08:12:58 +0000
Subject: [PATCH] Automatic publication of dev.2025-03-31.0.017605dd for
coq-iris-deprecated coq-iris-heap-lang coq-iris-unstable coq-iris
---
.../opam | 22 ++++++++++++
.../opam | 25 +++++++++++++
.../opam | 23 ++++++++++++
.../coq-iris.dev.2025-03-31.0.017605dd/opam | 36 +++++++++++++++++++
4 files changed, 106 insertions(+)
create mode 100644 packages/coq-iris-deprecated/coq-iris-deprecated.dev.2025-03-31.0.017605dd/opam
create mode 100644 packages/coq-iris-heap-lang/coq-iris-heap-lang.dev.2025-03-31.0.017605dd/opam
create mode 100644 packages/coq-iris-unstable/coq-iris-unstable.dev.2025-03-31.0.017605dd/opam
create mode 100644 packages/coq-iris/coq-iris.dev.2025-03-31.0.017605dd/opam
diff --git a/packages/coq-iris-deprecated/coq-iris-deprecated.dev.2025-03-31.0.017605dd/opam b/packages/coq-iris-deprecated/coq-iris-deprecated.dev.2025-03-31.0.017605dd/opam
new file mode 100644
index 00000000..c05d8e21
--- /dev/null
+++ b/packages/coq-iris-deprecated/coq-iris-deprecated.dev.2025-03-31.0.017605dd/opam
@@ -0,0 +1,22 @@
+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#017605dd82eff44ab2bad79a9b404ca617adcc27" }
diff --git a/packages/coq-iris-heap-lang/coq-iris-heap-lang.dev.2025-03-31.0.017605dd/opam b/packages/coq-iris-heap-lang/coq-iris-heap-lang.dev.2025-03-31.0.017605dd/opam
new file mode 100644
index 00000000..5038641f
--- /dev/null
+++ b/packages/coq-iris-heap-lang/coq-iris-heap-lang.dev.2025-03-31.0.017605dd/opam
@@ -0,0 +1,25 @@
+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#017605dd82eff44ab2bad79a9b404ca617adcc27" }
diff --git a/packages/coq-iris-unstable/coq-iris-unstable.dev.2025-03-31.0.017605dd/opam b/packages/coq-iris-unstable/coq-iris-unstable.dev.2025-03-31.0.017605dd/opam
new file mode 100644
index 00000000..04f2680d
--- /dev/null
+++ b/packages/coq-iris-unstable/coq-iris-unstable.dev.2025-03-31.0.017605dd/opam
@@ -0,0 +1,23 @@
+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#017605dd82eff44ab2bad79a9b404ca617adcc27" }
diff --git a/packages/coq-iris/coq-iris.dev.2025-03-31.0.017605dd/opam b/packages/coq-iris/coq-iris.dev.2025-03-31.0.017605dd/opam
new file mode 100644
index 00000000..40019337
--- /dev/null
+++ b/packages/coq-iris/coq-iris.dev.2025-03-31.0.017605dd/opam
@@ -0,0 +1,36 @@
+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-03-30.0.9274984b") | (= "dev") }
+]
+
+build: ["./make-package" "iris" "-j%{jobs}%"]
+install: ["./make-package" "iris" "install"]
+url { src: "git+https://gitlab.mpi-sws.org/iris/iris.git#017605dd82eff44ab2bad79a9b404ca617adcc27" }
--
GitLab