Automatic publication of dev.2025-03-03.0.df99b27e for...

Automatic publication of dev.2025-03-03.0.df99b27e for coq-caesium-config-no-align coq-lithium refinedc

packages/coq-caesium-config-no-align/coq-caesium-config-no-align.dev.2025-03-03.0.df99b27e/opam

+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" }

packages/coq-lithium/coq-lithium.dev.2025-03-03.0.df99b27e/opam

+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" }

packages/refinedc/refinedc.dev.2025-03-03.0.df99b27e/opam

+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" }