Commit 43a1a90f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

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 is one exception,
where we do not follow said convention: in program_logic/weakestpre.v,
using that order would break printing of texan triples (??).
parent 5d4caebb
......@@ -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.proofmode
- iris.algebra
- iris.base_logic
- iris.program_logic
- iris.heap_lang
## Combinators for functors
In Iris, the type of propositions [iProp] is described by the solution to the
......
From iris.heap_lang Require Export lifting notation.
From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation atomic_heap.
Set Default Proof Using "Type".
......
(* Test yet another way of importing heap_lang modules that used to break
printing *)
From iris.heap_lang Require Export lifting notation.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
......@@ -3,8 +3,8 @@
Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert Krebbers, Amin Timany and Lars Birkedal
POPL 2017 *)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import base_logic.
From iris.program_logic Require Export hoare.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
(** Correctness of in-place list reversal *)
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export total_weakestpre weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
......@@ -5,8 +5,8 @@ Separation Logic
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti,
Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
ICFP 2018 *)
From iris.proofmode Require Import tactics monpred.
From iris.bi Require Import monpred.
From iris.proofmode Require Import tactics monpred.
Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A PROP) :
P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a).
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl agree csum.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import excl agree csum.
From iris.heap_lang Require Import assert proofmode notation adequacy.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import par.
Set Default Proof Using "Type".
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac agree csum.
From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang.
From iris.algebra Require Import frac agree csum.
From iris.heap_lang Require Import assert proofmode notation adequacy.
From iris.proofmode Require Import tactics.
From iris.heap_lang.lib Require Import par.
Set Default Proof Using "Type".
......
From iris.proofmode Require Export tactics.
From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Export frac agree local_updates.
From iris.algebra Require Import proofmode_classes.
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
(** Authoritative CMRA with fractional authoritative parts. [auth] has 3 types
......
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 *)
......
Markdown is supported
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