From fa3550d6519dc2724d6cce033d2ca8bdff7e695c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 8 Mar 2024 15:51:13 +0100
Subject: [PATCH] split the lifetime logic into its own package
---
_CoqProject | 180 +++++++++---------
coq-lambda-rust.opam | 6 +-
coq-lifetime-logic.opam | 19 ++
{theories => lambda-rust}/lang/adequacy.v | 0
{theories => lambda-rust}/lang/heap.v | 0
{theories => lambda-rust}/lang/lang.v | 0
{theories => lambda-rust}/lang/lib/arc.v | 0
{theories => lambda-rust}/lang/lib/lock.v | 0
{theories => lambda-rust}/lang/lib/memcpy.v | 0
.../lang/lib/new_delete.v | 0
{theories => lambda-rust}/lang/lib/spawn.v | 0
{theories => lambda-rust}/lang/lib/swap.v | 0
{theories => lambda-rust}/lang/lib/tests.v | 0
{theories => lambda-rust}/lang/lifting.v | 0
{theories => lambda-rust}/lang/notation.v | 0
{theories => lambda-rust}/lang/proofmode.v | 0
{theories => lambda-rust}/lang/races.v | 0
{theories => lambda-rust}/lang/tactics.v | 0
{theories => lambda-rust}/typing/base.v | 0
{theories => lambda-rust}/typing/bool.v | 0
{theories => lambda-rust}/typing/borrow.v | 0
{theories => lambda-rust}/typing/cont.v | 0
.../typing/cont_context.v | 0
.../typing/examples/fixpoint.v | 0
.../typing/examples/get_x.v | 0
.../typing/examples/init_prod.v | 0
.../typing/examples/lazy_lft.v | 0
.../typing/examples/nonlexical.v | 0
.../typing/examples/rebor.v | 0
.../typing/examples/unbox.v | 0
{theories => lambda-rust}/typing/fixpoint.v | 0
{theories => lambda-rust}/typing/function.v | 0
{theories => lambda-rust}/typing/int.v | 0
.../typing/lft_contexts.v | 0
{theories => lambda-rust}/typing/lib/arc.v | 0
.../typing/lib/brandedvec.v | 0
{theories => lambda-rust}/typing/lib/cell.v | 0
.../typing/lib/diverging_static.v | 0
.../typing/lib/fake_shared.v | 0
.../typing/lib/ghostcell.v | 0
{theories => lambda-rust}/typing/lib/join.v | 0
.../typing/lib/mutex/mutex.v | 0
.../typing/lib/mutex/mutexguard.v | 0
{theories => lambda-rust}/typing/lib/option.v | 0
{theories => lambda-rust}/typing/lib/panic.v | 0
{theories => lambda-rust}/typing/lib/rc/rc.v | 0
.../typing/lib/rc/weak.v | 0
.../typing/lib/refcell/ref.v | 0
.../typing/lib/refcell/ref_code.v | 0
.../typing/lib/refcell/refcell.v | 0
.../typing/lib/refcell/refcell_code.v | 0
.../typing/lib/refcell/refmut.v | 0
.../typing/lib/refcell/refmut_code.v | 0
.../typing/lib/rwlock/rwlock.v | 0
.../typing/lib/rwlock/rwlock_code.v | 0
.../typing/lib/rwlock/rwlockreadguard.v | 0
.../typing/lib/rwlock/rwlockreadguard_code.v | 0
.../typing/lib/rwlock/rwlockwriteguard.v | 0
.../typing/lib/rwlock/rwlockwriteguard_code.v | 0
{theories => lambda-rust}/typing/lib/spawn.v | 0
{theories => lambda-rust}/typing/lib/swap.v | 0
.../typing/lib/take_mut.v | 0
{theories => lambda-rust}/typing/own.v | 0
{theories => lambda-rust}/typing/product.v | 0
.../typing/product_split.v | 0
{theories => lambda-rust}/typing/programs.v | 0
{theories => lambda-rust}/typing/shr_bor.v | 0
{theories => lambda-rust}/typing/soundness.v | 0
{theories => lambda-rust}/typing/sum.v | 0
{theories => lambda-rust}/typing/type.v | 0
.../typing/type_context.v | 0
{theories => lambda-rust}/typing/type_sum.v | 0
{theories => lambda-rust}/typing/typing.v | 0
{theories => lambda-rust}/typing/uninit.v | 0
{theories => lambda-rust}/typing/uniq_bor.v | 0
{theories => lambda-rust}/typing/util.v | 0
{theories/lifetime => lifetime}/at_borrow.v | 0
{theories/lifetime => lifetime}/frac_borrow.v | 0
{theories/lifetime => lifetime}/lifetime.v | 0
.../lifetime => lifetime}/lifetime_sig.v | 0
{theories/lifetime => lifetime}/meta.v | 0
.../lifetime => lifetime}/model/accessors.v | 0
.../lifetime => lifetime}/model/borrow.v | 0
.../lifetime => lifetime}/model/borrow_sep.v | 0
.../lifetime => lifetime}/model/creation.v | 0
.../lifetime => lifetime}/model/definitions.v | 0
.../lifetime => lifetime}/model/faking.v | 0
.../lifetime => lifetime}/model/primitive.v | 0
.../lifetime => lifetime}/model/reborrow.v | 0
{theories/lifetime => lifetime}/na_borrow.v | 0
make-package | 32 ++++
91 files changed, 146 insertions(+), 91 deletions(-)
create mode 100644 coq-lifetime-logic.opam
rename {theories => lambda-rust}/lang/adequacy.v (100%)
rename {theories => lambda-rust}/lang/heap.v (100%)
rename {theories => lambda-rust}/lang/lang.v (100%)
rename {theories => lambda-rust}/lang/lib/arc.v (100%)
rename {theories => lambda-rust}/lang/lib/lock.v (100%)
rename {theories => lambda-rust}/lang/lib/memcpy.v (100%)
rename {theories => lambda-rust}/lang/lib/new_delete.v (100%)
rename {theories => lambda-rust}/lang/lib/spawn.v (100%)
rename {theories => lambda-rust}/lang/lib/swap.v (100%)
rename {theories => lambda-rust}/lang/lib/tests.v (100%)
rename {theories => lambda-rust}/lang/lifting.v (100%)
rename {theories => lambda-rust}/lang/notation.v (100%)
rename {theories => lambda-rust}/lang/proofmode.v (100%)
rename {theories => lambda-rust}/lang/races.v (100%)
rename {theories => lambda-rust}/lang/tactics.v (100%)
rename {theories => lambda-rust}/typing/base.v (100%)
rename {theories => lambda-rust}/typing/bool.v (100%)
rename {theories => lambda-rust}/typing/borrow.v (100%)
rename {theories => lambda-rust}/typing/cont.v (100%)
rename {theories => lambda-rust}/typing/cont_context.v (100%)
rename {theories => lambda-rust}/typing/examples/fixpoint.v (100%)
rename {theories => lambda-rust}/typing/examples/get_x.v (100%)
rename {theories => lambda-rust}/typing/examples/init_prod.v (100%)
rename {theories => lambda-rust}/typing/examples/lazy_lft.v (100%)
rename {theories => lambda-rust}/typing/examples/nonlexical.v (100%)
rename {theories => lambda-rust}/typing/examples/rebor.v (100%)
rename {theories => lambda-rust}/typing/examples/unbox.v (100%)
rename {theories => lambda-rust}/typing/fixpoint.v (100%)
rename {theories => lambda-rust}/typing/function.v (100%)
rename {theories => lambda-rust}/typing/int.v (100%)
rename {theories => lambda-rust}/typing/lft_contexts.v (100%)
rename {theories => lambda-rust}/typing/lib/arc.v (100%)
rename {theories => lambda-rust}/typing/lib/brandedvec.v (100%)
rename {theories => lambda-rust}/typing/lib/cell.v (100%)
rename {theories => lambda-rust}/typing/lib/diverging_static.v (100%)
rename {theories => lambda-rust}/typing/lib/fake_shared.v (100%)
rename {theories => lambda-rust}/typing/lib/ghostcell.v (100%)
rename {theories => lambda-rust}/typing/lib/join.v (100%)
rename {theories => lambda-rust}/typing/lib/mutex/mutex.v (100%)
rename {theories => lambda-rust}/typing/lib/mutex/mutexguard.v (100%)
rename {theories => lambda-rust}/typing/lib/option.v (100%)
rename {theories => lambda-rust}/typing/lib/panic.v (100%)
rename {theories => lambda-rust}/typing/lib/rc/rc.v (100%)
rename {theories => lambda-rust}/typing/lib/rc/weak.v (100%)
rename {theories => lambda-rust}/typing/lib/refcell/ref.v (100%)
rename {theories => lambda-rust}/typing/lib/refcell/ref_code.v (100%)
rename {theories => lambda-rust}/typing/lib/refcell/refcell.v (100%)
rename {theories => lambda-rust}/typing/lib/refcell/refcell_code.v (100%)
rename {theories => lambda-rust}/typing/lib/refcell/refmut.v (100%)
rename {theories => lambda-rust}/typing/lib/refcell/refmut_code.v (100%)
rename {theories => lambda-rust}/typing/lib/rwlock/rwlock.v (100%)
rename {theories => lambda-rust}/typing/lib/rwlock/rwlock_code.v (100%)
rename {theories => lambda-rust}/typing/lib/rwlock/rwlockreadguard.v (100%)
rename {theories => lambda-rust}/typing/lib/rwlock/rwlockreadguard_code.v (100%)
rename {theories => lambda-rust}/typing/lib/rwlock/rwlockwriteguard.v (100%)
rename {theories => lambda-rust}/typing/lib/rwlock/rwlockwriteguard_code.v (100%)
rename {theories => lambda-rust}/typing/lib/spawn.v (100%)
rename {theories => lambda-rust}/typing/lib/swap.v (100%)
rename {theories => lambda-rust}/typing/lib/take_mut.v (100%)
rename {theories => lambda-rust}/typing/own.v (100%)
rename {theories => lambda-rust}/typing/product.v (100%)
rename {theories => lambda-rust}/typing/product_split.v (100%)
rename {theories => lambda-rust}/typing/programs.v (100%)
rename {theories => lambda-rust}/typing/shr_bor.v (100%)
rename {theories => lambda-rust}/typing/soundness.v (100%)
rename {theories => lambda-rust}/typing/sum.v (100%)
rename {theories => lambda-rust}/typing/type.v (100%)
rename {theories => lambda-rust}/typing/type_context.v (100%)
rename {theories => lambda-rust}/typing/type_sum.v (100%)
rename {theories => lambda-rust}/typing/typing.v (100%)
rename {theories => lambda-rust}/typing/uninit.v (100%)
rename {theories => lambda-rust}/typing/uniq_bor.v (100%)
rename {theories => lambda-rust}/typing/util.v (100%)
rename {theories/lifetime => lifetime}/at_borrow.v (100%)
rename {theories/lifetime => lifetime}/frac_borrow.v (100%)
rename {theories/lifetime => lifetime}/lifetime.v (100%)
rename {theories/lifetime => lifetime}/lifetime_sig.v (100%)
rename {theories/lifetime => lifetime}/meta.v (100%)
rename {theories/lifetime => lifetime}/model/accessors.v (100%)
rename {theories/lifetime => lifetime}/model/borrow.v (100%)
rename {theories/lifetime => lifetime}/model/borrow_sep.v (100%)
rename {theories/lifetime => lifetime}/model/creation.v (100%)
rename {theories/lifetime => lifetime}/model/definitions.v (100%)
rename {theories/lifetime => lifetime}/model/faking.v (100%)
rename {theories/lifetime => lifetime}/model/primitive.v (100%)
rename {theories/lifetime => lifetime}/model/reborrow.v (100%)
rename {theories/lifetime => lifetime}/na_borrow.v (100%)
create mode 100755 make-package
diff --git a/_CoqProject b/_CoqProject
index 388e1c67..8a8ef0b0 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,94 +1,98 @@
--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
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 1120df37..cb1a9b4d 100644
--- a/coq-lambda-rust.opam
+++ b/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"]
diff --git a/coq-lifetime-logic.opam b/coq-lifetime-logic.opam
new file mode 100644
index 00000000..accb10e8
--- /dev/null
+++ b/coq-lifetime-logic.opam
@@ -0,0 +1,19 @@
+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"]
diff --git a/theories/lang/adequacy.v b/lambda-rust/lang/adequacy.v
similarity index 100%
rename from theories/lang/adequacy.v
rename to lambda-rust/lang/adequacy.v
diff --git a/theories/lang/heap.v b/lambda-rust/lang/heap.v
similarity index 100%
rename from theories/lang/heap.v
rename to lambda-rust/lang/heap.v
diff --git a/theories/lang/lang.v b/lambda-rust/lang/lang.v
similarity index 100%
rename from theories/lang/lang.v
rename to lambda-rust/lang/lang.v
diff --git a/theories/lang/lib/arc.v b/lambda-rust/lang/lib/arc.v
similarity index 100%
rename from theories/lang/lib/arc.v
rename to lambda-rust/lang/lib/arc.v
diff --git a/theories/lang/lib/lock.v b/lambda-rust/lang/lib/lock.v
similarity index 100%
rename from theories/lang/lib/lock.v
rename to lambda-rust/lang/lib/lock.v
diff --git a/theories/lang/lib/memcpy.v b/lambda-rust/lang/lib/memcpy.v
similarity index 100%
rename from theories/lang/lib/memcpy.v
rename to lambda-rust/lang/lib/memcpy.v
diff --git a/theories/lang/lib/new_delete.v b/lambda-rust/lang/lib/new_delete.v
similarity index 100%
rename from theories/lang/lib/new_delete.v
rename to lambda-rust/lang/lib/new_delete.v
diff --git a/theories/lang/lib/spawn.v b/lambda-rust/lang/lib/spawn.v
similarity index 100%
rename from theories/lang/lib/spawn.v
rename to lambda-rust/lang/lib/spawn.v
diff --git a/theories/lang/lib/swap.v b/lambda-rust/lang/lib/swap.v
similarity index 100%
rename from theories/lang/lib/swap.v
rename to lambda-rust/lang/lib/swap.v
diff --git a/theories/lang/lib/tests.v b/lambda-rust/lang/lib/tests.v
similarity index 100%
rename from theories/lang/lib/tests.v
rename to lambda-rust/lang/lib/tests.v
diff --git a/theories/lang/lifting.v b/lambda-rust/lang/lifting.v
similarity index 100%
rename from theories/lang/lifting.v
rename to lambda-rust/lang/lifting.v
diff --git a/theories/lang/notation.v b/lambda-rust/lang/notation.v
similarity index 100%
rename from theories/lang/notation.v
rename to lambda-rust/lang/notation.v
diff --git a/theories/lang/proofmode.v b/lambda-rust/lang/proofmode.v
similarity index 100%
rename from theories/lang/proofmode.v
rename to lambda-rust/lang/proofmode.v
diff --git a/theories/lang/races.v b/lambda-rust/lang/races.v
similarity index 100%
rename from theories/lang/races.v
rename to lambda-rust/lang/races.v
diff --git a/theories/lang/tactics.v b/lambda-rust/lang/tactics.v
similarity index 100%
rename from theories/lang/tactics.v
rename to lambda-rust/lang/tactics.v
diff --git a/theories/typing/base.v b/lambda-rust/typing/base.v
similarity index 100%
rename from theories/typing/base.v
rename to lambda-rust/typing/base.v
diff --git a/theories/typing/bool.v b/lambda-rust/typing/bool.v
similarity index 100%
rename from theories/typing/bool.v
rename to lambda-rust/typing/bool.v
diff --git a/theories/typing/borrow.v b/lambda-rust/typing/borrow.v
similarity index 100%
rename from theories/typing/borrow.v
rename to lambda-rust/typing/borrow.v
diff --git a/theories/typing/cont.v b/lambda-rust/typing/cont.v
similarity index 100%
rename from theories/typing/cont.v
rename to lambda-rust/typing/cont.v
diff --git a/theories/typing/cont_context.v b/lambda-rust/typing/cont_context.v
similarity index 100%
rename from theories/typing/cont_context.v
rename to lambda-rust/typing/cont_context.v
diff --git a/theories/typing/examples/fixpoint.v b/lambda-rust/typing/examples/fixpoint.v
similarity index 100%
rename from theories/typing/examples/fixpoint.v
rename to lambda-rust/typing/examples/fixpoint.v
diff --git a/theories/typing/examples/get_x.v b/lambda-rust/typing/examples/get_x.v
similarity index 100%
rename from theories/typing/examples/get_x.v
rename to lambda-rust/typing/examples/get_x.v
diff --git a/theories/typing/examples/init_prod.v b/lambda-rust/typing/examples/init_prod.v
similarity index 100%
rename from theories/typing/examples/init_prod.v
rename to lambda-rust/typing/examples/init_prod.v
diff --git a/theories/typing/examples/lazy_lft.v b/lambda-rust/typing/examples/lazy_lft.v
similarity index 100%
rename from theories/typing/examples/lazy_lft.v
rename to lambda-rust/typing/examples/lazy_lft.v
diff --git a/theories/typing/examples/nonlexical.v b/lambda-rust/typing/examples/nonlexical.v
similarity index 100%
rename from theories/typing/examples/nonlexical.v
rename to lambda-rust/typing/examples/nonlexical.v
diff --git a/theories/typing/examples/rebor.v b/lambda-rust/typing/examples/rebor.v
similarity index 100%
rename from theories/typing/examples/rebor.v
rename to lambda-rust/typing/examples/rebor.v
diff --git a/theories/typing/examples/unbox.v b/lambda-rust/typing/examples/unbox.v
similarity index 100%
rename from theories/typing/examples/unbox.v
rename to lambda-rust/typing/examples/unbox.v
diff --git a/theories/typing/fixpoint.v b/lambda-rust/typing/fixpoint.v
similarity index 100%
rename from theories/typing/fixpoint.v
rename to lambda-rust/typing/fixpoint.v
diff --git a/theories/typing/function.v b/lambda-rust/typing/function.v
similarity index 100%
rename from theories/typing/function.v
rename to lambda-rust/typing/function.v
diff --git a/theories/typing/int.v b/lambda-rust/typing/int.v
similarity index 100%
rename from theories/typing/int.v
rename to lambda-rust/typing/int.v
diff --git a/theories/typing/lft_contexts.v b/lambda-rust/typing/lft_contexts.v
similarity index 100%
rename from theories/typing/lft_contexts.v
rename to lambda-rust/typing/lft_contexts.v
diff --git a/theories/typing/lib/arc.v b/lambda-rust/typing/lib/arc.v
similarity index 100%
rename from theories/typing/lib/arc.v
rename to lambda-rust/typing/lib/arc.v
diff --git a/theories/typing/lib/brandedvec.v b/lambda-rust/typing/lib/brandedvec.v
similarity index 100%
rename from theories/typing/lib/brandedvec.v
rename to lambda-rust/typing/lib/brandedvec.v
diff --git a/theories/typing/lib/cell.v b/lambda-rust/typing/lib/cell.v
similarity index 100%
rename from theories/typing/lib/cell.v
rename to lambda-rust/typing/lib/cell.v
diff --git a/theories/typing/lib/diverging_static.v b/lambda-rust/typing/lib/diverging_static.v
similarity index 100%
rename from theories/typing/lib/diverging_static.v
rename to lambda-rust/typing/lib/diverging_static.v
diff --git a/theories/typing/lib/fake_shared.v b/lambda-rust/typing/lib/fake_shared.v
similarity index 100%
rename from theories/typing/lib/fake_shared.v
rename to lambda-rust/typing/lib/fake_shared.v
diff --git a/theories/typing/lib/ghostcell.v b/lambda-rust/typing/lib/ghostcell.v
similarity index 100%
rename from theories/typing/lib/ghostcell.v
rename to lambda-rust/typing/lib/ghostcell.v
diff --git a/theories/typing/lib/join.v b/lambda-rust/typing/lib/join.v
similarity index 100%
rename from theories/typing/lib/join.v
rename to lambda-rust/typing/lib/join.v
diff --git a/theories/typing/lib/mutex/mutex.v b/lambda-rust/typing/lib/mutex/mutex.v
similarity index 100%
rename from theories/typing/lib/mutex/mutex.v
rename to lambda-rust/typing/lib/mutex/mutex.v
diff --git a/theories/typing/lib/mutex/mutexguard.v b/lambda-rust/typing/lib/mutex/mutexguard.v
similarity index 100%
rename from theories/typing/lib/mutex/mutexguard.v
rename to lambda-rust/typing/lib/mutex/mutexguard.v
diff --git a/theories/typing/lib/option.v b/lambda-rust/typing/lib/option.v
similarity index 100%
rename from theories/typing/lib/option.v
rename to lambda-rust/typing/lib/option.v
diff --git a/theories/typing/lib/panic.v b/lambda-rust/typing/lib/panic.v
similarity index 100%
rename from theories/typing/lib/panic.v
rename to lambda-rust/typing/lib/panic.v
diff --git a/theories/typing/lib/rc/rc.v b/lambda-rust/typing/lib/rc/rc.v
similarity index 100%
rename from theories/typing/lib/rc/rc.v
rename to lambda-rust/typing/lib/rc/rc.v
diff --git a/theories/typing/lib/rc/weak.v b/lambda-rust/typing/lib/rc/weak.v
similarity index 100%
rename from theories/typing/lib/rc/weak.v
rename to lambda-rust/typing/lib/rc/weak.v
diff --git a/theories/typing/lib/refcell/ref.v b/lambda-rust/typing/lib/refcell/ref.v
similarity index 100%
rename from theories/typing/lib/refcell/ref.v
rename to lambda-rust/typing/lib/refcell/ref.v
diff --git a/theories/typing/lib/refcell/ref_code.v b/lambda-rust/typing/lib/refcell/ref_code.v
similarity index 100%
rename from theories/typing/lib/refcell/ref_code.v
rename to lambda-rust/typing/lib/refcell/ref_code.v
diff --git a/theories/typing/lib/refcell/refcell.v b/lambda-rust/typing/lib/refcell/refcell.v
similarity index 100%
rename from theories/typing/lib/refcell/refcell.v
rename to lambda-rust/typing/lib/refcell/refcell.v
diff --git a/theories/typing/lib/refcell/refcell_code.v b/lambda-rust/typing/lib/refcell/refcell_code.v
similarity index 100%
rename from theories/typing/lib/refcell/refcell_code.v
rename to lambda-rust/typing/lib/refcell/refcell_code.v
diff --git a/theories/typing/lib/refcell/refmut.v b/lambda-rust/typing/lib/refcell/refmut.v
similarity index 100%
rename from theories/typing/lib/refcell/refmut.v
rename to lambda-rust/typing/lib/refcell/refmut.v
diff --git a/theories/typing/lib/refcell/refmut_code.v b/lambda-rust/typing/lib/refcell/refmut_code.v
similarity index 100%
rename from theories/typing/lib/refcell/refmut_code.v
rename to lambda-rust/typing/lib/refcell/refmut_code.v
diff --git a/theories/typing/lib/rwlock/rwlock.v b/lambda-rust/typing/lib/rwlock/rwlock.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlock.v
rename to lambda-rust/typing/lib/rwlock/rwlock.v
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/lambda-rust/typing/lib/rwlock/rwlock_code.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlock_code.v
rename to lambda-rust/typing/lib/rwlock/rwlock_code.v
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/lambda-rust/typing/lib/rwlock/rwlockreadguard.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlockreadguard.v
rename to lambda-rust/typing/lib/rwlock/rwlockreadguard.v
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlockreadguard_code.v
rename to lambda-rust/typing/lib/rwlock/rwlockreadguard_code.v
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlockwriteguard.v
rename to lambda-rust/typing/lib/rwlock/rwlockwriteguard.v
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
similarity index 100%
rename from theories/typing/lib/rwlock/rwlockwriteguard_code.v
rename to lambda-rust/typing/lib/rwlock/rwlockwriteguard_code.v
diff --git a/theories/typing/lib/spawn.v b/lambda-rust/typing/lib/spawn.v
similarity index 100%
rename from theories/typing/lib/spawn.v
rename to lambda-rust/typing/lib/spawn.v
diff --git a/theories/typing/lib/swap.v b/lambda-rust/typing/lib/swap.v
similarity index 100%
rename from theories/typing/lib/swap.v
rename to lambda-rust/typing/lib/swap.v
diff --git a/theories/typing/lib/take_mut.v b/lambda-rust/typing/lib/take_mut.v
similarity index 100%
rename from theories/typing/lib/take_mut.v
rename to lambda-rust/typing/lib/take_mut.v
diff --git a/theories/typing/own.v b/lambda-rust/typing/own.v
similarity index 100%
rename from theories/typing/own.v
rename to lambda-rust/typing/own.v
diff --git a/theories/typing/product.v b/lambda-rust/typing/product.v
similarity index 100%
rename from theories/typing/product.v
rename to lambda-rust/typing/product.v
diff --git a/theories/typing/product_split.v b/lambda-rust/typing/product_split.v
similarity index 100%
rename from theories/typing/product_split.v
rename to lambda-rust/typing/product_split.v
diff --git a/theories/typing/programs.v b/lambda-rust/typing/programs.v
similarity index 100%
rename from theories/typing/programs.v
rename to lambda-rust/typing/programs.v
diff --git a/theories/typing/shr_bor.v b/lambda-rust/typing/shr_bor.v
similarity index 100%
rename from theories/typing/shr_bor.v
rename to lambda-rust/typing/shr_bor.v
diff --git a/theories/typing/soundness.v b/lambda-rust/typing/soundness.v
similarity index 100%
rename from theories/typing/soundness.v
rename to lambda-rust/typing/soundness.v
diff --git a/theories/typing/sum.v b/lambda-rust/typing/sum.v
similarity index 100%
rename from theories/typing/sum.v
rename to lambda-rust/typing/sum.v
diff --git a/theories/typing/type.v b/lambda-rust/typing/type.v
similarity index 100%
rename from theories/typing/type.v
rename to lambda-rust/typing/type.v
diff --git a/theories/typing/type_context.v b/lambda-rust/typing/type_context.v
similarity index 100%
rename from theories/typing/type_context.v
rename to lambda-rust/typing/type_context.v
diff --git a/theories/typing/type_sum.v b/lambda-rust/typing/type_sum.v
similarity index 100%
rename from theories/typing/type_sum.v
rename to lambda-rust/typing/type_sum.v
diff --git a/theories/typing/typing.v b/lambda-rust/typing/typing.v
similarity index 100%
rename from theories/typing/typing.v
rename to lambda-rust/typing/typing.v
diff --git a/theories/typing/uninit.v b/lambda-rust/typing/uninit.v
similarity index 100%
rename from theories/typing/uninit.v
rename to lambda-rust/typing/uninit.v
diff --git a/theories/typing/uniq_bor.v b/lambda-rust/typing/uniq_bor.v
similarity index 100%
rename from theories/typing/uniq_bor.v
rename to lambda-rust/typing/uniq_bor.v
diff --git a/theories/typing/util.v b/lambda-rust/typing/util.v
similarity index 100%
rename from theories/typing/util.v
rename to lambda-rust/typing/util.v
diff --git a/theories/lifetime/at_borrow.v b/lifetime/at_borrow.v
similarity index 100%
rename from theories/lifetime/at_borrow.v
rename to lifetime/at_borrow.v
diff --git a/theories/lifetime/frac_borrow.v b/lifetime/frac_borrow.v
similarity index 100%
rename from theories/lifetime/frac_borrow.v
rename to lifetime/frac_borrow.v
diff --git a/theories/lifetime/lifetime.v b/lifetime/lifetime.v
similarity index 100%
rename from theories/lifetime/lifetime.v
rename to lifetime/lifetime.v
diff --git a/theories/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v
similarity index 100%
rename from theories/lifetime/lifetime_sig.v
rename to lifetime/lifetime_sig.v
diff --git a/theories/lifetime/meta.v b/lifetime/meta.v
similarity index 100%
rename from theories/lifetime/meta.v
rename to lifetime/meta.v
diff --git a/theories/lifetime/model/accessors.v b/lifetime/model/accessors.v
similarity index 100%
rename from theories/lifetime/model/accessors.v
rename to lifetime/model/accessors.v
diff --git a/theories/lifetime/model/borrow.v b/lifetime/model/borrow.v
similarity index 100%
rename from theories/lifetime/model/borrow.v
rename to lifetime/model/borrow.v
diff --git a/theories/lifetime/model/borrow_sep.v b/lifetime/model/borrow_sep.v
similarity index 100%
rename from theories/lifetime/model/borrow_sep.v
rename to lifetime/model/borrow_sep.v
diff --git a/theories/lifetime/model/creation.v b/lifetime/model/creation.v
similarity index 100%
rename from theories/lifetime/model/creation.v
rename to lifetime/model/creation.v
diff --git a/theories/lifetime/model/definitions.v b/lifetime/model/definitions.v
similarity index 100%
rename from theories/lifetime/model/definitions.v
rename to lifetime/model/definitions.v
diff --git a/theories/lifetime/model/faking.v b/lifetime/model/faking.v
similarity index 100%
rename from theories/lifetime/model/faking.v
rename to lifetime/model/faking.v
diff --git a/theories/lifetime/model/primitive.v b/lifetime/model/primitive.v
similarity index 100%
rename from theories/lifetime/model/primitive.v
rename to lifetime/model/primitive.v
diff --git a/theories/lifetime/model/reborrow.v b/lifetime/model/reborrow.v
similarity index 100%
rename from theories/lifetime/model/reborrow.v
rename to lifetime/model/reborrow.v
diff --git a/theories/lifetime/na_borrow.v b/lifetime/na_borrow.v
similarity index 100%
rename from theories/lifetime/na_borrow.v
rename to lifetime/na_borrow.v
diff --git a/make-package b/make-package
new file mode 100755
index 00000000..5bf541bc
--- /dev/null
+++ b/make-package
@@ -0,0 +1,32 @@
+#!/bin/bash
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
+ echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+ exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+make -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*
--
GitLab