Merge branch 'ralf/extra' into 'master'

add "deprecated" and "staging" packages and deprecate some modules

See merge request iris/iris!602

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

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
 

_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

coq-iris-deprecated.opam

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

coq-iris-staging.opam

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

iris/base_logic/lib/auth.v → iris_deprecated/base_logic/auth.v

+(** 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.

iris/base_logic/lib/sts.v → iris_deprecated/base_logic/sts.v

+(** 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.

iris/base_logic/lib/viewshifts.v → iris_deprecated/base_logic/viewshifts.v

+(** 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.

iris/program_logic/hoare.v → iris_deprecated/program_logic/hoare.v

+(** 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.
 

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".
 

tests/one_shot.v

 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.

tests/one_shot_once.v

 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.