Commit 3a92dab3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Reorder Requires so that we do not depend of Export bugs.

The general idea is to first import/export modules which are further
than the current one, and then import/export modules which are close
dependencies.

This commit tries to use the same order of imports for every file, and
describes the convention in ProofGuide.md. There are two exceptions,
where we do not follow said convention:

   - In program_logic/weakestpre.v. This would break printing of texan
     triples (??)
   - In program_logic/adequacy.v. This is to give priority of our
     nsteps definition over stdpp's.
parent 0236daec
......@@ -6,6 +6,24 @@ This complements the tactic documentation for the [proof mode](ProofMode.md) and
[HeapLang](HeapLang.md) as well as the documentation of syntactic conventions in
the [style guide](StyleGuide.md).
## Order of `Requires`
In Coq, declarations in modules imported later may override the
previous definition. Therefore, in order to make sure the most
relevant declarations and notations always take priority, we recommend
importing dependencies from the furthest to the closest.
In particular, when importing Iris, Stdpp and Coq stdlib modules, we
recommend importing in the following order:
Coq
stdpp
iris.bi
iris.algebra
iris.base_logic
iris.program_logic
iris.proofmode
iris.heap_lang
## Combinators for functors
In Iris, the type of propositions [iProp] is described by the solution to the
......
......@@ -12,5 +12,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-08-29.0.75435486") | (= "dev") }
"coq-stdpp" { (= "dev.2019-09-05.0.c579b46c") | (= "dev") }
]
From iris.algebra Require Export monoid.
From stdpp Require Export functions gmap gmultiset.
From iris.algebra Require Export monoid.
Set Default Proof Using "Type*".
Local Existing Instances monoid_ne monoid_assoc monoid_comm
monoid_left_id monoid_right_id monoid_proper
......
From iris.algebra Require Export ofe monoid.
From stdpp Require Import finite.
From iris.algebra Require Export ofe monoid.
Set Default Proof Using "Type".
Class PCore (A : Type) := pcore : A option A.
......
From iris.algebra Require Export big_op cmra.
From stdpp Require Import gmap gmultiset.
From iris.algebra Require Export big_op cmra.
Set Default Proof Using "Type*".
(** Option *)
......@@ -33,4 +33,4 @@ Proof.
{ rewrite big_opMS_empty. set_solver. }
rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
set_solver.
Qed.
\ No newline at end of file
Qed.
From stdpp Require Export sets coPset.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From stdpp Require Export sets coPset.
Set Default Proof Using "Type".
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
......
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import local_updates.
From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type".
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
......
From iris.algebra Require Export frac auth.
From iris.algebra Require Export updates local_updates.
From iris.algebra Require Export frac auth updates local_updates.
From iris.algebra Require Import proofmode_classes.
(** Authoritative CMRA where the NON-authoritative parts can be fractional.
......
From stdpp Require Import finite.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From stdpp Require Import finite.
Set Default Proof Using "Type".
Definition discrete_fun_insert `{EqDecision A} {B : A ofeT}
......
From iris.algebra Require Export cmra.
From stdpp Require Export list gmap.
From iris.algebra Require Import updates local_updates.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates proofmode_classes.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
Section cofe.
......
From stdpp Require Export sets gmultiset countable.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From stdpp Require Export sets gmultiset countable.
Set Default Proof Using "Type".
(* The multiset union CMRA *)
......
From stdpp Require Export sets gmap mapset.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From stdpp Require Export sets gmap mapset.
Set Default Proof Using "Type".
(* The union CMRA *)
......
From iris.algebra Require Export cmra.
From stdpp Require Export list.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type".
Section cofe.
......
From iris.algebra Require Export gmap coPset local_updates.
From stdpp Require Import namespaces.
From iris.algebra Require Import updates.
From iris.algebra Require Import proofmode_classes.
From iris.algebra Require Export gmap coPset local_updates.
From iris.algebra Require Import updates proofmode_classes.
Set Default Proof Using "Type".
(** The camera [namespace_map A] over a camera [A] provides the connectives
......
From iris.proofmode Require Export classes.
From iris.algebra Require Export cmra.
From iris.proofmode Require Export classes.
(* There are various versions of [IsOp] with different modes:
......@@ -51,4 +51,4 @@ Proof. by constructor. Qed.
(* This one has a higher precendence than [is_op_op] so we get a [+] instead of
an [⋅]. *)
Global Instance is_op_plus (n1 n2 : nat) : IsOp (n1 + n2) n1 n2.
Proof. done. Qed.
\ No newline at end of file
Proof. done. Qed.
......@@ -16,11 +16,9 @@ difference:
- We no longer have the [◯U{1} a] is the exclusive fragmental element (cf.
[frac_auth_frag_validN_op_1_l]).
*)
From iris.algebra Require Export auth frac.
From iris.algebra Require Import ufrac.
From iris.algebra Require Export updates local_updates.
From iris.algebra Require Import proofmode_classes.
From Coq Require Import QArith Qcanon.
From iris.algebra Require Export auth frac updates local_updates.
From iris.algebra Require Import ufrac proofmode_classes.
Definition ufrac_authR (A : cmraT) : cmraT :=
authR (optionUR (prodR ufracR A)).
......
From iris.base_logic Require Export derived proofmode.
From iris.bi Require Export bi.
From iris.base_logic Require Export derived proofmode.
Set Default Proof Using "Type".
(* The trick of having multiple [uPred] modules, which are all exported in
......
......@@ -43,7 +43,7 @@ Proof.
- exact: @exist_intro.
- exact: @exist_elim.
- exact: sep_mono.
- exact: True_sep_1.
- exact: True_sep_1.
- exact: True_sep_2.
- exact: sep_comm'.
- exact: sep_assoc'.
......
From iris.base_logic Require Export bi.
From iris.bi Require Export bi.
From iris.base_logic Require Export bi.
Set Default Proof Using "Type".
Import bi base_logic.bi.uPred.
Import bi.bi base_logic.bi.uPred.
(** Derived laws for Iris-specific primitive connectives (own, valid).
This file does NOT unseal! *)
......
From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Export auth.
From iris.algebra Require Import gmap.
From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Import excl auth gmap agree.
From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
From iris.base_logic.lib Require Export invariants.
From iris.bi.lib Require Import fractional.
From iris.algebra Require Export frac.
From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
From iris.base_logic.lib Require Export own.
From stdpp Require Export coPset.
From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import wsat.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Export invG.
......
(* This file shows that the fancy update can be encoded in terms of the
view shift, and that the laws of the fancy update can be derived from the
laws of the view shift. *)
From stdpp Require Export coPset.
From iris.base_logic Require Export base_logic.
From iris.proofmode Require Import tactics.
From stdpp Require Export coPset.
Set Default Proof Using "Type*".
Section fupd.
......
From iris.algebra Require Import auth gmap frac agree namespace_map.
From stdpp Require Export namespaces.
From iris.base_logic.lib Require Export own.
From iris.bi.lib Require Import fractional.
From iris.algebra Require Import auth gmap frac agree namespace_map.
From iris.base_logic.lib Require Export own.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
From iris.base_logic.lib Require Export fancy_updates.
From stdpp Require Export namespaces.
From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap.
From iris.base_logic.lib Require Export fancy_updates.
From iris.base_logic.lib Require Import wsat.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
From iris.base_logic Require Export base_logic.
From iris.algebra Require Import gmap.
From iris.algebra Require cofe_solver.
From iris.base_logic Require Export base_logic.
Set Default Proof Using "Type".
(** In this file we construct the type [iProp] of propositions of the Iris
......
From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Import gset coPset.
From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
From iris.algebra Require Import functions gmap.
From iris.algebra Require Import functions gmap proofmode_classes.
From iris.base_logic.lib Require Export iprop.
From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
Import uPred.
......
From iris.base_logic Require Export own.
From iris.algebra Require Import agree.
From stdpp Require Import gmap.
From iris.algebra Require Import agree.
From iris.base_logic Require Export own.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Export sts.
From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
From iris.base_logic.lib Require Export own.
From stdpp Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic.lib Require Export own.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
......
From iris.base_logic Require Export derived.
From iris.algebra Require Import proofmode_classes.
From iris.base_logic Require Export derived.
Import base_logic.bi.uPred.
......
From iris.algebra Require Export cmra updates.
From iris.bi Require Import notation.
From stdpp Require Import finite.
From Coq.Init Require Import Nat.
From iris.bi Require Import notation.
From iris.algebra Require Export cmra updates.
Set Default Proof Using "Type".
Local Hint Extern 1 (_ _) => etrans; [eassumption|] : core.
Local Hint Extern 1 (_ _) => etrans; [|eassumption] : core.
......
From iris.algebra Require Export big_op.
From iris.bi Require Import derived_laws_sbi.
From stdpp Require Import countable fin_sets functions.
From iris.bi Require Import derived_laws_sbi.
From iris.algebra Require Export big_op.
Set Default Proof Using "Type".
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
......
From iris.algebra Require Import monoid.
From iris.bi Require Import interface derived_laws_sbi big_op plainly updates.
From iris.algebra Require Import monoid.
Class Embed (A B : Type) := embed : A B.
Arguments embed {_ _ _} _%I : simpl never.
......
From iris.algebra Require Export ofe.
From iris.bi Require Export notation.
From iris.algebra Require Export ofe.
Set Primitive Projections.
Section bi_mixin.
......
From stdpp Require Import coPset namespaces.
From iris.bi Require Export bi updates laterable.
From iris.bi.lib Require Import fixpoint.
From stdpp Require Import coPset namespaces.
From iris.proofmode Require Import coq_tactics tactics reduction.
Set Default Proof Using "Type".
......
From stdpp Require Export coPset.
From iris.program_logic Require Import language.
From iris.bi Require Import interface derived_connectives.
From iris.program_logic Require Import language.
Inductive stuckness := NotStuck | MaybeStuck.
......
From iris.program_logic Require Export weakestpre adequacy.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.base_logic.lib Require Import proph_map.
From iris.program_logic Require Export weakestpre adequacy.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Class heapPreG Σ := HeapPreG {
......
From stdpp Require Import fin_maps.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lifting.
From iris.heap_lang Require Import tactics notation.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
(** This file defines the [array] connective, a version of [mapsto] that works
......
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.heap_lang Require Export locations.
From iris.algebra Require Export ofe.
From stdpp Require Export binders strings.
From stdpp Require Import gmap.
From iris.algebra Require Export ofe.
From iris.program_logic Require Export language ectx_language ectxi_language.
From iris.heap_lang Require Export locations.
Set Default Proof Using "Type".
(** heap_lang. A fairly simple language used for common Iris examples.
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.heap_lang Require Export lifting notation.
From iris.bi.lib Require Import fractional.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.bi.lib Require Import fractional.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode.
Set Default Proof Using "Type".
(** A general logically atomic interface for a heap. *)
......
From iris.program_logic Require Export weakestpre.
From iris.algebra Require Import frac_auth auth.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth auth.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation atomic_heap par.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".
(** Show that implementing fetch-and-add on top of CAS preserves logical
......
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lifting notation.
Set Default Proof Using "Type".
Structure lock Σ `{!heapG Σ} := Lock {
......@@ -36,4 +36,3 @@ Existing Instances is_lock_ne is_lock_persistent locked_timeless.
Instance is_lock_proper Σ `{!heapG Σ} (L: lock Σ) N γ lk:
Proper (() ==> ()) (is_lock L N γ lk) := ne_proper _.
From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang Require Export spawn.
Set Default Proof Using "Type".
Import uPred.
......
From iris.program_logic Require Export weakestpre.
From iris.algebra Require Import excl.
From iris.base_logic.lib Require Export invariants.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
Set Default Proof Using "Type".
Definition spawn : val :=
......
From iris.algebra Require Import excl.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
From iris.heap_lang.lib Require Import lock.
Set Default Proof Using "Type".
......
From iris.algebra Require Import excl auth gset.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl auth gset.
From iris.heap_lang.lib Require Export lock.
Set Default Proof Using "Type".
Import uPred.
......
From stdpp Require Import fin_maps.
From iris.algebra Require Import auth gmap.
From iris.base_logic Require Export gen_heap.
From iris.base_logic.lib Require Export proph_map.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics notation.
From iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps.
Set Default Proof Using "Type".
Class heapG Σ := HeapG {
......
From iris.algebra Require Import base.
From stdpp Require Import countable numbers gmap.
From iris.algebra Require Import base.
Record loc := { loc_car : Z }.
......
From iris.heap_lang Require Export lang.
From stdpp Require Import gmap.
From iris.heap_lang Require Export lang.
(* This file contains some metatheory about the heap_lang language,
which is not needed for verifying programs. *)
......
From iris.program_logic Require Export total_adequacy.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export adequacy.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
......
From iris.program_logic Require Export weakestpre.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic.lib Require Import wsat.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
Set Default Proof Using "Type".
Import uPred.
......
From stdpp Require Import namespaces.
From iris.bi Require Import telescopes.
From iris.bi.lib Require Export atomic.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics classes.
From iris.bi.lib Require Export atomic.
From iris.bi Require Import telescopes.
Set Default Proof Using "Type".
(* This hard-codes the inner mask to be empty, because we have yet to find an
......
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export viewshifts.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
......
From iris.algebra Require Import excl auth.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language.
From iris.algebra Require Import excl auth.
From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type".
......
From iris.program_logic Require Export total_weakestpre adequacy.
From iris.algebra Require Import gmap auth agree gset coPset list.
From iris.bi Require Import big_op fixpoint.
From iris.algebra Require Import gmap auth agree gset coPset list.
From iris.program_logic Require Export total_weakestpre adequacy.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......
(** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language.
From iris.program_logic Require Export total_weakestpre total_lifting.
From iris.program_logic Require Export ectx_language total_weakestpre total_lifting.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
......
From iris.program_logic Require Export total_weakestpre.
From iris.bi Require Export big_op.
From iris.program_logic Require Export total_weakestpre.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
......
From iris.bi Require Import fixpoint big_op.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import tactics.
From iris.bi Require Import fixpoint big_op.
Set Default Proof Using "Type".
Import uPred.
......
From Coq Require Export Ascii.
From stdpp Require Export strings.
From iris.algebra Require Export base.
From Coq Require Export Ascii.
Set Default Proof Using "Type".
(** * Utility definitions used by the proofmode *)
......
From stdpp Require Import namespaces.