From a5c2dd2779184caab8b03260d4374cdb9c8f678e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 1 Feb 2021 13:04:21 +0100
Subject: [PATCH] create iris-deprecated and iris-staging packages, and
deprecate some hard-to-use logic-level wrappers as well as view shift and
Hoare triple notation
---
Makefile.coq.local | 4 +-
README.md | 79 ++++++++++++-------
_CoqProject | 11 ++-
coq-iris-deprecated.opam | 20 +++++
coq-iris-staging.opam | 20 +++++
iris_deprecated/.keep | 0
.../lib => iris_deprecated/base_logic}/auth.v | 4 +
.../lib => iris_deprecated/base_logic}/sts.v | 4 +
.../base_logic}/viewshifts.v | 7 ++
.../program_logic/hoare.v | 8 +-
iris_staging/.keep | 0
tests/ipm_paper.v | 2 +-
tests/one_shot.v | 3 +-
tests/one_shot_once.v | 3 +-
14 files changed, 126 insertions(+), 39 deletions(-)
create mode 100644 coq-iris-deprecated.opam
create mode 100644 coq-iris-staging.opam
create mode 100644 iris_deprecated/.keep
rename {iris/base_logic/lib => iris_deprecated/base_logic}/auth.v (97%)
rename {iris/base_logic/lib => iris_deprecated/base_logic}/sts.v (97%)
rename {iris/base_logic/lib => iris_deprecated/base_logic}/viewshifts.v (90%)
rename {iris => iris_deprecated}/program_logic/hoare.v (95%)
create mode 100644 iris_staging/.keep
diff --git a/Makefile.coq.local b/Makefile.coq.local
index e34123a32..edb097cd6 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 c4ee8b22e..65241467b 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 30b03d9df..16023029e 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 000000000..8f26f10b8
--- /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 000000000..49bff7b51
--- /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 000000000..e69de29bb
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 5a3e4a0bd..64b121384 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 0ed4b1390..de1785235 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 6dce54464..c2a571e94 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 42ec59626..c40fa8df9 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 000000000..e69de29bb
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 6c7517d51..b1a5d2d61 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 b6dd81209..59df90b75 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 e51a877c1..65a617639 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.
--
GitLab