diff --git a/packages/coq-lambda-rust/coq-lambda-rust.dev.2025-03-28.1.fca004c4/opam b/packages/coq-lambda-rust/coq-lambda-rust.dev.2025-03-28.1.fca004c4/opam new file mode 100644 index 0000000000000000000000000000000000000000..ba38b8134d9691a9cd64fdb9bae29691c6e10447 --- /dev/null +++ b/packages/coq-lambda-rust/coq-lambda-rust.dev.2025-03-28.1.fca004c4/opam @@ -0,0 +1,21 @@ +opam-version: "2.0" +maintainer: "Ralf Jung <jung@mpi-sws.org>" +authors: "The RustBelt Team" +license: "BSD-3-Clause" +homepage: "https://plv.mpi-sws.org/rustbelt/" +bug-reports: "https://gitlab.mpi-sws.org/iris/lambda-rust/issues" +dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git" + +synopsis: "LambdaRust Coq formalization" +description: """ +A formal model of a Rust core language and type system, a logical relation for +the type system, and safety proof for some Rust libraries. +""" + +depends: [ + "coq-lifetime-logic" { = version } +] + +build: ["./make-package" "lambda-rust" "-j%{jobs}%"] +install: ["./make-package" "lambda-rust" "install"] +url { src: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git#fca004c458e411ebea790e4f86089c22ebe2a643" } diff --git a/packages/coq-lifetime-logic/coq-lifetime-logic.dev.2025-03-28.1.fca004c4/opam b/packages/coq-lifetime-logic/coq-lifetime-logic.dev.2025-03-28.1.fca004c4/opam new file mode 100644 index 0000000000000000000000000000000000000000..a7caacae3bcf7ce8aeebb109c338313eb2d8893c --- /dev/null +++ b/packages/coq-lifetime-logic/coq-lifetime-logic.dev.2025-03-28.1.fca004c4/opam @@ -0,0 +1,20 @@ +opam-version: "2.0" +maintainer: "Ralf Jung <jung@mpi-sws.org>" +authors: "The RustBelt Team" +license: "BSD-3-Clause" +homepage: "https://plv.mpi-sws.org/rustbelt/" +bug-reports: "https://gitlab.mpi-sws.org/iris/lambda-rust/issues" +dev-repo: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git" + +synopsis: "Lifetime Logic Coq formalization" +description: """ +The lifetime logic extends Iris with a notion of "borrowing". +""" + +depends: [ + "coq-iris" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") } +] + +build: ["./make-package" "lifetime" "-j%{jobs}%"] +install: ["./make-package" "lifetime" "install"] +url { src: "git+https://gitlab.mpi-sws.org/iris/lambda-rust.git#fca004c458e411ebea790e4f86089c22ebe2a643" }