Commit a5c2dd27 authored by Ralf Jung's avatar Ralf Jung
Browse files

create iris-deprecated and iris-staging packages, and deprecate some...

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
parent 4c96a504
......@@ -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
......
......@@ -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
......
......@@ -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
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"]
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"]
(** 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.
......
(** 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.
......
(** 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.
......
(** 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.
......
......@@ -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".
......
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.
......
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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment