diff --git a/Makefile.coq.local b/Makefile.coq.local
index e34123a3222d82f633ba4516694c9c30e581ee2d..edb097cd69488c1de48bebd795082ed2677ba7fd 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -15,8 +15,10 @@ test: $(TESTFILES:.v=.vo)
 # Make sure everything imports the options, and all Instance/Argument/Hint are qualified.
 	$(HIDE)for FILE in $(VFILES); do \
 	  if ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
-	  if egrep '^\s*(Instance|Arguments|Remove|Hint (Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold))\s' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint'."; echo; exit 1; fi \
+	  if egrep '^\s*(Instance|Arguments|Remove|Hint (Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold))\s' "$$FILE"; then echo "ERROR: $$FILE contains unqualified 'Instance'/'Arguments'/'Hint' (see above)."; echo; exit 1; fi \
 	done
+# Make sure main Iris does not import other Iris packages.
+	$(HIDE)if egrep 'iris\.(heap_lang|deprecated|staging)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
diff --git a/README.md b/README.md
index c4ee8b22e6229d9e9ccc72772dd6dfa506001f64..65241467b8bf9c3df0b464a30d4a3813147b5b67 100644
--- a/README.md
+++ b/README.md
@@ -65,7 +65,8 @@ We do not guarantee backwards-compatibility, so upgrading Iris may break your
 Iris-using developments.  If you want to be notified of breaking changes, please
 let us know your account name on the
 [MPI-SWS GitLab](https://gitlab.mpi-sws.org/) so we can add you to the
-notification group.
+notification group.  Note that this excludes the "staging" and "deprecated"
+packages (see below).
 
 #### Use of Iris in submitted artifacts
 
@@ -85,39 +86,57 @@ the Iris development itself.
 
 ## Directory Structure
 
-* The folder [prelude](iris/prelude) contains modules imported everywhere in
-  Iris.
-* The folder [algebra](iris/algebra) contains the COFE and CMRA
-  constructions as well as the solver for recursive domain equations.
-* The folder [base_logic](iris/base_logic) defines the Iris base logic and
-  the primitive connectives.  It also contains derived constructions that are
-  entirely independent of the choice of resources.
-  * The subfolder [lib](iris/base_logic/lib) contains some generally useful
-    derived constructions.  Most importantly, it defines composable
-    dynamic resources and ownership of them; the other constructions depend
-    on this setup.
-* The folder [program_logic](iris/program_logic) specializes the base logic
-  to build Iris, the program logic.   This includes weakest preconditions that
-  are defined for any language satisfying some generic axioms, and some derived
-  constructions that work for any such language.
-* The folder [bi](iris/bi) contains the BI++ laws, as well as derived
-  connectives, laws and constructions that are applicable for general BIS.
-* The folder [proofmode](iris/proofmode) contains
-  [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
-  intuitionistic and spatial BI++ assertions. It also contains tactics for
-  interactive proofs. Documentation can be found in
-  [proof_mode.md](docs/proof_mode.md).
-* The folder [heap_lang](iris_heap_lang) defines the ML-like concurrent heap
-  language
-  * The subfolder [lib](iris_heap_lang/lib) contains a few derived
+Iris is structured into multiple *packages*, some of which contain multiple
+modules in separate folders.
+
+* The [iris](iris) package contains the language-independent parts of Iris.
+  + The folder [prelude](iris/prelude) contains modules imported everywhere in
+    Iris.
+  + The folder [algebra](iris/algebra) contains the COFE and CMRA
+    constructions as well as the solver for recursive domain equations.
+    - The subfolder [lib](iris/algebra/lib) contains some general derived RA
+      constructions.
+  + The folder [bi](iris/bi) contains the BI++ laws, as well as derived
+    connectives, laws and constructions that are applicable for general BIs.
+    - The subfolder [lib](iris/bi/lib) contains some general derived logical
+      constructions.
+  + The folder [proofmode](iris/proofmode) contains
+    [MoSeL](http://iris-project.org/mosel/), which extends Coq with contexts for
+    intuitionistic and spatial BI++ assertions. It also contains tactics for
+    interactive proofs. Documentation can be found in
+    [proof_mode.md](docs/proof_mode.md).
+  + The folder [base_logic](iris/base_logic) defines the Iris base logic and
+    the primitive connectives.  It also contains derived constructions that are
+    entirely independent of the choice of resources.
+    - The subfolder [lib](iris/base_logic/lib) contains some generally useful
+      derived constructions.  Most importantly, it defines composable
+      dynamic resources and ownership of them; the other constructions depend
+      on this setup.
+  + The folder [program_logic](iris/program_logic) specializes the base logic
+    to build Iris, the program logic.   This includes weakest preconditions that
+    are defined for any language satisfying some generic axioms, and some derived
+    constructions that work for any such language.
+  + The folder [si_logic](iris/si_logic) defines a "plain" step-indexed logic
+    and shows that it is an instance of the BI interface.
+* The [iris_heap_lang](iris_heap_lang) package defines the ML-like concurrent
+  language HeapLang and provides tactic support and proof mode integration.
+  + The subfolder [lib](iris_heap_lang/lib) contains a few derived
     constructions within this language, e.g., parallel composition.
     For more examples of using Iris and heap_lang, have a look at the
     [Iris Examples](https://gitlab.mpi-sws.org/iris/examples).
+* The [iris_staging](iris_staging) package contains libraries that are not yet
+  ready for inclusion in Iris proper. For each library, there is a corresponding
+  "tracking issue" in the Iris issue tracker (also linked from the library
+  itself) which tracks the work that still needs to be done before moving the
+  library to Iris. No stability guarantees whatsoever are made for this package.
+* The [iris_deprecated](iris_deprecated) package contains libraries that have been
+  removed from Iris proper, but are kept around to give users some more time to
+  switch to their intended replacements. The individual libraries come with comments
+  explaining the deprecation and making recommendations for what to use
+  instead. No stability guarantees whatsoever are made for this package.
 * The folder [tests](tests) contains modules we use to test our
-  infrastructure. Users of the Iris Coq library should *not* depend on these
-  modules; they may change or disappear without any notice.
-* The folder [si_logic](iris/si_logic) defines a "plain" step-indexed logic
-  and shows that it is an instance of the BI interface.
+  infrastructure. These modules are not installed by `make install`, and should
+  not be imported.
 
 ## Case Studies
 
diff --git a/_CoqProject b/_CoqProject
index 30b03d9dfcaf8c481dae9fcaa91cf34135045165..16023029e1d0e19517db9a3ded38ab5b80dfcb9e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,6 +8,8 @@
 -Q iris/base_logic iris.base_logic
 -Q iris/program_logic iris.program_logic
 -Q iris_heap_lang iris.heap_lang
+-Q iris_staging iris.staging
+-Q iris_deprecated iris.deprecated
 # 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
@@ -88,9 +90,6 @@ iris/base_logic/lib/saved_prop.v
 iris/base_logic/lib/wsat.v
 iris/base_logic/lib/invariants.v
 iris/base_logic/lib/fancy_updates.v
-iris/base_logic/lib/viewshifts.v
-iris/base_logic/lib/auth.v
-iris/base_logic/lib/sts.v
 iris/base_logic/lib/boxes.v
 iris/base_logic/lib/na_invariants.v
 iris/base_logic/lib/cancelable_invariants.v
@@ -106,7 +105,6 @@ iris/program_logic/lifting.v
 iris/program_logic/weakestpre.v
 iris/program_logic/total_weakestpre.v
 iris/program_logic/total_adequacy.v
-iris/program_logic/hoare.v
 iris/program_logic/language.v
 iris/program_logic/ectx_language.v
 iris/program_logic/ectxi_language.v
@@ -166,3 +164,8 @@ iris_heap_lang/lib/increment.v
 iris_heap_lang/lib/diverge.v
 iris_heap_lang/lib/arith.v
 iris_heap_lang/lib/array.v
+
+iris_deprecated/base_logic/auth.v
+iris_deprecated/base_logic/sts.v
+iris_deprecated/base_logic/viewshifts.v
+iris_deprecated/program_logic/hoare.v
diff --git a/coq-iris-deprecated.opam b/coq-iris-deprecated.opam
new file mode 100644
index 0000000000000000000000000000000000000000..8f26f10b81d42b2290352668d853a3ef45cd27a4
--- /dev/null
+++ b/coq-iris-deprecated.opam
@@ -0,0 +1,20 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+
+synopsis: "Deprecated Iris libraries"
+description: """
+This package contains libraries that have been deprecated from Iris, and are planned to be
+entirely removed at some point.
+"""
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_deprecated" "-j%{jobs}%"]
+install: ["./make-package" "iris_deprecated" "install"]
diff --git a/coq-iris-staging.opam b/coq-iris-staging.opam
new file mode 100644
index 0000000000000000000000000000000000000000..49bff7b518358aff61470f111c7fae14061ca7b9
--- /dev/null
+++ b/coq-iris-staging.opam
@@ -0,0 +1,20 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+
+synopsis: "Unfinished Iris libraries"
+description: """
+This package contains libraries that have been proposed for inclusion in Iris, but more
+work is needed before they are ready for this.
+"""
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_staging" "-j%{jobs}%"]
+install: ["./make-package" "iris_staging" "install"]
diff --git a/iris_deprecated/.keep b/iris_deprecated/.keep
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/iris/base_logic/lib/auth.v b/iris_deprecated/base_logic/auth.v
similarity index 97%
rename from iris/base_logic/lib/auth.v
rename to iris_deprecated/base_logic/auth.v
index 5a3e4a0bd735f0db8c1cbc6b9ecd369ff6b127dd..64b121384150410f226f6460242e15faa0b26647 100644
--- a/iris/base_logic/lib/auth.v
+++ b/iris_deprecated/base_logic/auth.v
@@ -1,3 +1,7 @@
+(** This logic-level wrapper on top of the [auth] RA turns out to be much harder
+to use than just directly using the RA, hence it is deprecated and will be
+removed entirely after some grace period. *)
+
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics.
diff --git a/iris/base_logic/lib/sts.v b/iris_deprecated/base_logic/sts.v
similarity index 97%
rename from iris/base_logic/lib/sts.v
rename to iris_deprecated/base_logic/sts.v
index 0ed4b13905ed20f040f4cdd26f27acd8d278e3ad..de1785235f3711ae78c2b1bb4f46319c8e5da3b2 100644
--- a/iris/base_logic/lib/sts.v
+++ b/iris_deprecated/base_logic/sts.v
@@ -1,3 +1,7 @@
+(** This logic-level wrapper on top of the [sts] RA turns out to be much harder
+to use than just directly using the RA, hence it is deprecated and will be
+removed entirely after some grace period. *)
+
 From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
diff --git a/iris/base_logic/lib/viewshifts.v b/iris_deprecated/base_logic/viewshifts.v
similarity index 90%
rename from iris/base_logic/lib/viewshifts.v
rename to iris_deprecated/base_logic/viewshifts.v
index 6dce544643dc147d5f1b722bfedbbce550b55d5f..c2a571e9475161ee4796114a9dff904181a2d843 100644
--- a/iris/base_logic/lib/viewshifts.v
+++ b/iris_deprecated/base_logic/viewshifts.v
@@ -1,3 +1,10 @@
+(** The binary (implicitly persistent) view shift connective is rarely ever
+useful in Coq.  This module only exists to verify that the proof rules we give
+on paper hold true.  Use the non-persistent connective [={E}=∗] wrapped in a [□]
+modality if needed.
+This file will be removed when we find a good way to have a [Definition] with
+telescopes for Texan triples. *)
+
 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
diff --git a/iris/program_logic/hoare.v b/iris_deprecated/program_logic/hoare.v
similarity index 95%
rename from iris/program_logic/hoare.v
rename to iris_deprecated/program_logic/hoare.v
index 42ec5962628a1317f8927e2d4b5b8e89654fa45c..c40fa8df9cb6ad01771ee4fdbe5119856d680cfc 100644
--- a/iris/program_logic/hoare.v
+++ b/iris_deprecated/program_logic/hoare.v
@@ -1,5 +1,11 @@
+(** Hoare triples are rarely ever useful in Coq.  This module only exists to
+verify that the proof rules we give on paper hold true.  Use Texan triples or
+[WP] instead.
+This file will be removed when we find a good way to have a [Definition] with
+telescopes for Texan triples. *)
+
 From iris.proofmode Require Import tactics.
-From iris.base_logic.lib Require Export viewshifts.
+From iris.deprecated.base_logic Require Export viewshifts.
 From iris.program_logic Require Export weakestpre.
 From iris.prelude Require Import options.
 
diff --git a/iris_staging/.keep b/iris_staging/.keep
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 6c7517d51380043fcd47bfe197708acce07000f7..b1a5d2d6167432abba4bd0e5fb3a85ab00d84b20 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -5,7 +5,7 @@ Robbert Krebbers, Amin Timany and Lars Birkedal
 POPL 2017 *)
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import base_logic.
-From iris.program_logic Require Export hoare.
+From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
diff --git a/tests/one_shot.v b/tests/one_shot.v
index b6dd81209482ff9714b715bbe886fdb9f613be0c..59df90b7596d3333726de26427c80a90a5380db4 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Import excl agree csum.
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre hoare.
+From iris.program_logic Require Export weakestpre.
+From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.heap_lang.lib Require Import par.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index e51a877c192fee7dd1d4cc724783a616b057efe5..65a617639548268aa212b511e8106e8fb2ef029c 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -1,6 +1,7 @@
 From iris.algebra Require Import frac agree csum.
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Export weakestpre hoare.
+From iris.program_logic Require Export weakestpre.
+From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import assert proofmode notation adequacy.
 From iris.heap_lang.lib Require Import par.