From eceb1506a3bde65fe99060756cb674ec1cd34753 Mon Sep 17 00:00:00 2001
From: Opam Update Bot <opam-update@botland>
Date: Mon, 3 Mar 2025 08:17:17 +0000
Subject: [PATCH] Automatic publication of dev.2025-03-03.0.df99b27e for
coq-caesium-config-no-align coq-lithium refinedc
---
.../opam | 23 ++++++++++
.../opam | 29 ++++++++++++
.../refinedc.dev.2025-03-03.0.df99b27e/opam | 44 +++++++++++++++++++
3 files changed, 96 insertions(+)
create mode 100644 packages/coq-caesium-config-no-align/coq-caesium-config-no-align.dev.2025-03-03.0.df99b27e/opam
create mode 100644 packages/coq-lithium/coq-lithium.dev.2025-03-03.0.df99b27e/opam
create mode 100644 packages/refinedc/refinedc.dev.2025-03-03.0.df99b27e/opam
diff --git a/packages/coq-caesium-config-no-align/coq-caesium-config-no-align.dev.2025-03-03.0.df99b27e/opam b/packages/coq-caesium-config-no-align/coq-caesium-config-no-align.dev.2025-03-03.0.df99b27e/opam
new file mode 100644
index 00000000..efe75878
--- /dev/null
+++ b/packages/coq-caesium-config-no-align/coq-caesium-config-no-align.dev.2025-03-03.0.df99b27e/opam
@@ -0,0 +1,23 @@
+opam-version: "2.0"
+name: "coq-caesium-config-no-align"
+synopsis: "Configuration package to configure Caesium to not use alignment"
+description: """
+Installing this package instructs the refinedc package to disable alignment in the Caesium C semantics.
+"""
+license: "BSD-3-Clause"
+
+maintainer: ["Michael Sammler <msammler@mpi-sws.org>"]
+authors: ["Michael Sammler" "Rodolphe Lepigre" "Kayvan Memarian"]
+
+homepage: "https://plv.mpi-sws.org/refinedc"
+bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
+
+conflict-class: [ "coq-caesium-config" ]
+
+depends: [
+]
+
+build: [
+]
+url { src: "git+https://gitlab.mpi-sws.org/iris/refinedc.git#df99b27eaf22f46a5230fa421072d1ce92a3673e" }
diff --git a/packages/coq-lithium/coq-lithium.dev.2025-03-03.0.df99b27e/opam b/packages/coq-lithium/coq-lithium.dev.2025-03-03.0.df99b27e/opam
new file mode 100644
index 00000000..9ecdb16a
--- /dev/null
+++ b/packages/coq-lithium/coq-lithium.dev.2025-03-03.0.df99b27e/opam
@@ -0,0 +1,29 @@
+opam-version: "2.0"
+name: "coq-lithium"
+synopsis: "Lithium proof automation for Iris"
+description: """
+Lithium proof automation for Iris
+"""
+license: "BSD-3-Clause"
+
+maintainer: ["Michael Sammler <msammler@mpi-sws.org>"
+ "Rodolphe Lepigre <lepigre@mpi-sws.org>"]
+authors: ["Michael Sammler" "Rodolphe Lepigre"]
+
+homepage: "https://plv.mpi-sws.org/refinedc"
+bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
+
+depends: [
+ "coq" { (= "8.20.0" ) }
+ "coq-iris" { (= "dev.2025-02-27.1.c773500a") | (= "dev") }
+ "coq-stdpp-unstable"
+ "dune" {>= "3.9.1"}
+ "coq-record-update" {= "0.3.4"}
+]
+
+build: [
+ ["dune" "subst"] {pinned}
+ ["dune" "build" "-p" name "-j" jobs]
+]
+url { src: "git+https://gitlab.mpi-sws.org/iris/refinedc.git#df99b27eaf22f46a5230fa421072d1ce92a3673e" }
diff --git a/packages/refinedc/refinedc.dev.2025-03-03.0.df99b27e/opam b/packages/refinedc/refinedc.dev.2025-03-03.0.df99b27e/opam
new file mode 100644
index 00000000..b4fec4d0
--- /dev/null
+++ b/packages/refinedc/refinedc.dev.2025-03-03.0.df99b27e/opam
@@ -0,0 +1,44 @@
+opam-version: "2.0"
+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.
+"""
+license: "BSD-3-Clause"
+
+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"
+bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
+
+depends: [
+ "coq-lithium" {= version | = "~dev"}
+ "cerberus" {= "dev" | = "~dev"} # I do not understand the difference between dev and ~dev and when opam uses which
+ "cmdliner" {>= "1.1.0"}
+ "sexplib0" {>= "v0.14.0"}
+ "earley" {= "3.0.0"}
+ "toml" {>= "6.0.0"}
+ "ubase" {>= "0.04"}
+]
+
+depopts: [
+ "coq-caesium-config-no-align"
+]
+
+build: [
+ [make "prepare-install-refinedc"]
+ [make "config"] {!coq-caesium-config-no-align:installed}
+ [make "config-no-align"] {coq-caesium-config-no-align:installed}
+ ["dune" "subst"] {pinned}
+ ["dune" "build" "-p" name "-j" jobs]
+]
+
+messages: [
+ "with default configuration" {!coq-caesium-config-no-align:installed}
+ "with no-align configuration" {coq-caesium-config-no-align:installed}
+]
+url { src: "git+https://gitlab.mpi-sws.org/iris/refinedc.git#df99b27eaf22f46a5230fa421072d1ce92a3673e" }
--
GitLab