From b5d6b7bbb416cc06745ea1c1e81de234050fcbd9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 20 Mar 2016 16:57:46 +0100
Subject: [PATCH] move some files around
---
README.md | 12 ++++++----
_CoqProject | 22 +++++++++----------
heap_lang/{ => lib}/assert.v | 0
{barrier => heap_lang/lib/barrier}/barrier.v | 0
{barrier => heap_lang/lib/barrier}/client.v | 2 +-
{barrier => heap_lang/lib/barrier}/proof.v | 4 ++--
{barrier => heap_lang/lib/barrier}/protocol.v | 0
.../lib/barrier}/specification.v | 4 ++--
heap_lang/{ => lib}/heap.v | 0
heap_lang/{ => lib}/par.v | 0
heap_lang/{ => lib}/spawn.v | 0
heap_lang/tests.v => tests/heap_lang.v | 0
.../tests.v => tests/program_logic.v | 0
13 files changed, 24 insertions(+), 20 deletions(-)
rename heap_lang/{ => lib}/assert.v (100%)
rename {barrier => heap_lang/lib/barrier}/barrier.v (100%)
rename {barrier => heap_lang/lib/barrier}/client.v (98%)
rename {barrier => heap_lang/lib/barrier}/proof.v (99%)
rename {barrier => heap_lang/lib/barrier}/protocol.v (100%)
rename {barrier => heap_lang/lib/barrier}/specification.v (92%)
rename heap_lang/{ => lib}/heap.v (100%)
rename heap_lang/{ => lib}/par.v (100%)
rename heap_lang/{ => lib}/spawn.v (100%)
rename heap_lang/tests.v => tests/heap_lang.v (100%)
rename program_logic/tests.v => tests/program_logic.v (100%)
diff --git a/README.md b/README.md
index 6e160a662..4b73aab77 100644
--- a/README.md
+++ b/README.md
@@ -35,10 +35,14 @@ running:
* The folder `program_logic` builds the semantic domain of Iris, defines and
verifies primitive view shifts and weakest preconditions, and builds some
language-independent derived constructions (e.g., STSs).
-* The folder `heap_lang` defines the ML-like concurrent heap language, and a
- few derived constructions (e.g., parallel composition).
-* The folder `barrier` contains the implementation and proof of the barrier
- <http://doi.acm.org/10.1145/2818638>.
+* The folder `heap_lang` defines the ML-like concurrent heap language
+ * The subfolder `lib` contains a few derived constructions within this
+ language, e.g., parallel composition.
+ Most notable here s `lib/barrier`, the implementation and proof of a barrier
+ as described in <http://doi.acm.org/10.1145/2818638>.
+* The folder `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.
## Documentation
diff --git a/_CoqProject b/_CoqProject
index 0cbaa47d1..e3074c433 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -69,7 +69,6 @@ program_logic/pviewshifts.v
program_logic/resources.v
program_logic/hoare.v
program_logic/language.v
-program_logic/tests.v
program_logic/ghost_ownership.v
program_logic/global_functor.v
program_logic/saved_prop.v
@@ -83,15 +82,16 @@ heap_lang/tactics.v
heap_lang/wp_tactics.v
heap_lang/lifting.v
heap_lang/derived.v
-heap_lang/heap.v
heap_lang/notation.v
-heap_lang/spawn.v
-heap_lang/par.v
-heap_lang/tests.v
heap_lang/substitution.v
-heap_lang/assert.v
-barrier/barrier.v
-barrier/specification.v
-barrier/protocol.v
-barrier/proof.v
-barrier/client.v
+heap_lang/lib/heap.v
+heap_lang/lib/spawn.v
+heap_lang/lib/par.v
+heap_lang/lib/assert.v
+heap_lang/lib/barrier/barrier.v
+heap_lang/lib/barrier/specification.v
+heap_lang/lib/barrier/protocol.v
+heap_lang/lib/barrier/proof.v
+heap_lang/lib/barrier/client.v
+tests/heap_lang.v
+tests/program_logic.v
diff --git a/heap_lang/assert.v b/heap_lang/lib/assert.v
similarity index 100%
rename from heap_lang/assert.v
rename to heap_lang/lib/assert.v
diff --git a/barrier/barrier.v b/heap_lang/lib/barrier/barrier.v
similarity index 100%
rename from barrier/barrier.v
rename to heap_lang/lib/barrier/barrier.v
diff --git a/barrier/client.v b/heap_lang/lib/barrier/client.v
similarity index 98%
rename from barrier/client.v
rename to heap_lang/lib/barrier/client.v
index e68492fb9..cf2bd60a3 100644
--- a/barrier/client.v
+++ b/heap_lang/lib/barrier/client.v
@@ -1,4 +1,4 @@
-From iris.barrier Require Import proof.
+From iris.heap_lang.lib.barrier Require Import proof.
From iris.heap_lang Require Import par.
From iris.program_logic Require Import auth sts saved_prop hoare ownership.
Import uPred.
diff --git a/barrier/proof.v b/heap_lang/lib/barrier/proof.v
similarity index 99%
rename from barrier/proof.v
rename to heap_lang/lib/barrier/proof.v
index b0c745823..6ca5d8372 100644
--- a/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -2,8 +2,8 @@ From iris.prelude Require Import functions.
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import sts saved_prop tactics.
From iris.heap_lang Require Export heap wp_tactics.
-From iris.barrier Require Export barrier.
-From iris.barrier Require Import protocol.
+From iris.heap_lang.lib.barrier Require Export barrier.
+From iris.heap_lang.lib.barrier Require Import protocol.
Import uPred.
(** The CMRAs we need. *)
diff --git a/barrier/protocol.v b/heap_lang/lib/barrier/protocol.v
similarity index 100%
rename from barrier/protocol.v
rename to heap_lang/lib/barrier/protocol.v
diff --git a/barrier/specification.v b/heap_lang/lib/barrier/specification.v
similarity index 92%
rename from barrier/specification.v
rename to heap_lang/lib/barrier/specification.v
index 68631962e..bfe830080 100644
--- a/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -1,6 +1,6 @@
From iris.program_logic Require Export hoare.
-From iris.barrier Require Export barrier.
-From iris.barrier Require Import proof.
+From iris.heap_lang.lib.barrier Require Export barrier.
+From iris.heap_lang.lib.barrier Require Import proof.
Import uPred.
Section spec.
diff --git a/heap_lang/heap.v b/heap_lang/lib/heap.v
similarity index 100%
rename from heap_lang/heap.v
rename to heap_lang/lib/heap.v
diff --git a/heap_lang/par.v b/heap_lang/lib/par.v
similarity index 100%
rename from heap_lang/par.v
rename to heap_lang/lib/par.v
diff --git a/heap_lang/spawn.v b/heap_lang/lib/spawn.v
similarity index 100%
rename from heap_lang/spawn.v
rename to heap_lang/lib/spawn.v
diff --git a/heap_lang/tests.v b/tests/heap_lang.v
similarity index 100%
rename from heap_lang/tests.v
rename to tests/heap_lang.v
diff --git a/program_logic/tests.v b/tests/program_logic.v
similarity index 100%
rename from program_logic/tests.v
rename to tests/program_logic.v
--
GitLab