split the lifetime logic into its own package

_CoqProject

--Q theories lrust
+# Search paths for all packages. They must all match the regex
+# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
+-Q lifetime lrust.lifetime
+-Q lambda-rust/lang lrust.lang
+-Q lambda-rust/typing lrust.typing
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures
 # (https://github.com/coq/coq/issues/6294).
 -arg -w -arg -redundant-canonical-projection
 
-theories/lifetime/model/definitions.v
-theories/lifetime/model/faking.v
-theories/lifetime/model/creation.v
-theories/lifetime/model/primitive.v
-theories/lifetime/model/accessors.v
-theories/lifetime/model/borrow.v
-theories/lifetime/model/borrow_sep.v
-theories/lifetime/model/reborrow.v
-theories/lifetime/lifetime_sig.v
-theories/lifetime/lifetime.v
-theories/lifetime/at_borrow.v
-theories/lifetime/na_borrow.v
-theories/lifetime/frac_borrow.v
-theories/lifetime/meta.v
-theories/lang/adequacy.v
-theories/lang/heap.v
-theories/lang/lang.v
-theories/lang/lifting.v
-theories/lang/notation.v
-theories/lang/proofmode.v
-theories/lang/races.v
-theories/lang/tactics.v
-theories/lang/lib/memcpy.v
-theories/lang/lib/swap.v
-theories/lang/lib/new_delete.v
-theories/lang/lib/spawn.v
-theories/lang/lib/lock.v
-theories/lang/lib/arc.v
-theories/lang/lib/tests.v
-theories/typing/base.v
-theories/typing/type.v
-theories/typing/util.v
-theories/typing/lft_contexts.v
-theories/typing/type_context.v
-theories/typing/cont_context.v
-theories/typing/uninit.v
-theories/typing/own.v
-theories/typing/uniq_bor.v
-theories/typing/shr_bor.v
-theories/typing/product.v
-theories/typing/product_split.v
-theories/typing/sum.v
-theories/typing/bool.v
-theories/typing/int.v
-theories/typing/function.v
-theories/typing/programs.v
-theories/typing/borrow.v
-theories/typing/cont.v
-theories/typing/fixpoint.v
-theories/typing/type_sum.v
-theories/typing/typing.v
-theories/typing/soundness.v
-theories/typing/lib/panic.v
-theories/typing/lib/option.v
-theories/typing/lib/fake_shared.v
-theories/typing/lib/cell.v
-theories/typing/lib/spawn.v
-theories/typing/lib/join.v
-theories/typing/lib/take_mut.v
-theories/typing/lib/rc/rc.v
-theories/typing/lib/rc/weak.v
-theories/typing/lib/arc.v
-theories/typing/lib/swap.v
-theories/typing/lib/diverging_static.v
-theories/typing/lib/brandedvec.v
-theories/typing/lib/ghostcell.v
-theories/typing/lib/mutex/mutex.v
-theories/typing/lib/mutex/mutexguard.v
-theories/typing/lib/refcell/refcell.v
-theories/typing/lib/refcell/ref.v
-theories/typing/lib/refcell/refmut.v
-theories/typing/lib/refcell/refcell_code.v
-theories/typing/lib/refcell/ref_code.v
-theories/typing/lib/refcell/refmut_code.v
-theories/typing/lib/rwlock/rwlock.v
-theories/typing/lib/rwlock/rwlockreadguard.v
-theories/typing/lib/rwlock/rwlockwriteguard.v
-theories/typing/lib/rwlock/rwlock_code.v
-theories/typing/lib/rwlock/rwlockreadguard_code.v
-theories/typing/lib/rwlock/rwlockwriteguard_code.v
-theories/typing/examples/fixpoint.v
-theories/typing/examples/get_x.v
-theories/typing/examples/rebor.v
-theories/typing/examples/unbox.v
-theories/typing/examples/init_prod.v
-theories/typing/examples/lazy_lft.v
-theories/typing/examples/nonlexical.v
+lifetime/model/definitions.v
+lifetime/model/faking.v
+lifetime/model/creation.v
+lifetime/model/primitive.v
+lifetime/model/accessors.v
+lifetime/model/borrow.v
+lifetime/model/borrow_sep.v
+lifetime/model/reborrow.v
+lifetime/lifetime_sig.v
+lifetime/lifetime.v
+lifetime/at_borrow.v
+lifetime/na_borrow.v
+lifetime/frac_borrow.v
+lifetime/meta.v
+lambda-rust/lang/adequacy.v
+lambda-rust/lang/heap.v
+lambda-rust/lang/lang.v
+lambda-rust/lang/lifting.v
+lambda-rust/lang/notation.v
+lambda-rust/lang/proofmode.v
+lambda-rust/lang/races.v
+lambda-rust/lang/tactics.v
+lambda-rust/lang/lib/memcpy.v
+lambda-rust/lang/lib/swap.v
+lambda-rust/lang/lib/new_delete.v
+lambda-rust/lang/lib/spawn.v
+lambda-rust/lang/lib/lock.v
+lambda-rust/lang/lib/arc.v
+lambda-rust/lang/lib/tests.v
+lambda-rust/typing/base.v
+lambda-rust/typing/type.v
+lambda-rust/typing/util.v
+lambda-rust/typing/lft_contexts.v
+lambda-rust/typing/type_context.v
+lambda-rust/typing/cont_context.v
+lambda-rust/typing/uninit.v
+lambda-rust/typing/own.v
+lambda-rust/typing/uniq_bor.v
+lambda-rust/typing/shr_bor.v
+lambda-rust/typing/product.v
+lambda-rust/typing/product_split.v
+lambda-rust/typing/sum.v
+lambda-rust/typing/bool.v
+lambda-rust/typing/int.v
+lambda-rust/typing/function.v
+lambda-rust/typing/programs.v
+lambda-rust/typing/borrow.v
+lambda-rust/typing/cont.v
+lambda-rust/typing/fixpoint.v
+lambda-rust/typing/type_sum.v
+lambda-rust/typing/typing.v
+lambda-rust/typing/soundness.v
+lambda-rust/typing/lib/panic.v
+lambda-rust/typing/lib/option.v
+lambda-rust/typing/lib/fake_shared.v
+lambda-rust/typing/lib/cell.v
+lambda-rust/typing/lib/spawn.v
+lambda-rust/typing/lib/join.v
+lambda-rust/typing/lib/take_mut.v
+lambda-rust/typing/lib/rc/rc.v
+lambda-rust/typing/lib/rc/weak.v
+lambda-rust/typing/lib/arc.v
+lambda-rust/typing/lib/swap.v
+lambda-rust/typing/lib/diverging_static.v
+lambda-rust/typing/lib/brandedvec.v
+lambda-rust/typing/lib/ghostcell.v
+lambda-rust/typing/lib/mutex/mutex.v
+lambda-rust/typing/lib/mutex/mutexguard.v
+lambda-rust/typing/lib/refcell/refcell.v
+lambda-rust/typing/lib/refcell/ref.v
+lambda-rust/typing/lib/refcell/refmut.v
+lambda-rust/typing/lib/refcell/refcell_code.v
+lambda-rust/typing/lib/refcell/ref_code.v
+lambda-rust/typing/lib/refcell/refmut_code.v
+lambda-rust/typing/lib/rwlock/rwlock.v
+lambda-rust/typing/lib/rwlock/rwlockreadguard.v
+lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
+lambda-rust/typing/lib/rwlock/rwlock_code.v
+lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
+lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
+lambda-rust/typing/examples/fixpoint.v
+lambda-rust/typing/examples/get_x.v
+lambda-rust/typing/examples/rebor.v
+lambda-rust/typing/examples/unbox.v
+lambda-rust/typing/examples/init_prod.v
+lambda-rust/typing/examples/lazy_lft.v
+lambda-rust/typing/examples/nonlexical.v

coq-lambda-rust.opam

@@ -13,8 +13,8 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2024-02-16.1.06f499e0") | (= "dev") }
+  "coq-lifetime-logic" { = version }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "lambda-rust" "-j%{jobs}%"]
+install: ["./make-package" "lambda-rust" "install"]

coq-lifetime-logic.opam

+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.2024-03-05.0.d71f4877") | (= "dev") }
+]
+
+build: ["./make-package" "lambda-rust" "-j%{jobs}%"]
+install: ["./make-package" "lambda-rust" "install"]