From 0fe3d627957d53dfd0a5ddd27ebb40353d5ee77f Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sat, 26 Aug 2017 14:26:25 +0200
Subject: [PATCH] move to a standard directory layout

---
 .gitignore                                    |  2 +-
 coq/ra/Makefile => Makefile                   |  6 +-
 _CoqProject                                   | 73 +++++++++++++++++++
 coq/ra/awk.Makefile => awk.Makefile           |  0
 {coq/build => build}/opam-ci.sh               |  0
 {coq/build => build}/opam-pins.sh             |  0
 coq/ra/_CoqProject                            | 73 -------------------
 coq/ra/base/atomic.v                          |  1 -
 coq/ra/base/base.v                            |  1 -
 coq/ra/gps/raw.v                              |  1 -
 opam                                          |  8 +-
 {coq/ra => theories}/abs_view.v               |  4 +-
 {coq/ra => theories}/adequacy.v               |  4 +-
 {coq/ra => theories}/arith.v                  |  0
 {coq/ra => theories}/base/accessors.v         |  4 +-
 {coq/ra => theories}/base/alloc.v             |  4 +-
 {coq/ra => theories}/base/at_cas.v            |  2 +-
 {coq/ra => theories}/base/at_fai.v            |  2 +-
 {coq/ra => theories}/base/at_read.v           |  2 +-
 {coq/ra => theories}/base/at_shared.v         |  4 +-
 {coq/ra => theories}/base/at_write.v          |  2 +-
 theories/base/atomic.v                        |  1 +
 theories/base/base.v                          |  1 +
 {coq/ra => theories}/base/dealloc.v           |  2 +-
 {coq/ra => theories}/base/fork.v              |  2 +-
 {coq/ra => theories}/base/ghosts.v            |  2 +-
 {coq/ra => theories}/base/helpers.v           |  4 +-
 {coq/ra => theories}/base/na_read.v           |  2 +-
 {coq/ra => theories}/base/na_shared.v         |  4 +-
 {coq/ra => theories}/base/na_write.v          |  2 +-
 {coq/ra => theories}/bigop.v                  |  2 +-
 {coq/ra => theories}/blocks.v                 |  4 +-
 {coq/ra => theories}/blocks_generic.v         |  2 +-
 {coq/ra => theories}/derived.v                |  2 +-
 {coq/ra => theories}/escrows.v                |  6 +-
 {coq/ra => theories}/examples/circ_buffer.v   |  8 +-
 .../examples/message_passing.v                | 10 +--
 .../examples/message_passing_base.v           |  6 +-
 {coq/ra => theories}/examples/msqueue.v       |  6 +-
 {coq/ra => theories}/examples/nat_tokens.v    |  2 +-
 {coq/ra => theories}/examples/protocols.v     |  2 +-
 {coq/ra => theories}/examples/rcu.v           |  6 +-
 {coq/ra => theories}/examples/rcu_data.v      |  2 +-
 {coq/ra => theories}/examples/repeat.v        |  2 +-
 {coq/ra => theories}/examples/sc_stack.v      |  2 +-
 {coq/ra => theories}/examples/spin_lock.v     |  6 +-
 {coq/ra => theories}/examples/ticket_lock.v   |  8 +-
 {coq/ra => theories}/examples/tstack.v        |  4 +-
 {coq/ra => theories}/examples/unit_token.v    |  2 +-
 {coq/ra => theories}/fractor.v                |  4 +-
 {coq/ra => theories}/gps/cas.v                |  4 +-
 {coq/ra => theories}/gps/fai.v                |  4 +-
 {coq/ra => theories}/gps/fractional.v         |  4 +-
 {coq/ra => theories}/gps/init.v               |  4 +-
 {coq/ra => theories}/gps/inst_shared.v        |  6 +-
 {coq/ra => theories}/gps/plain.v              |  2 +-
 theories/gps/raw.v                            |  1 +
 {coq/ra => theories}/gps/read.v               |  4 +-
 {coq/ra => theories}/gps/recursive.v          |  6 +-
 {coq/ra => theories}/gps/shared.v             |  6 +-
 {coq/ra => theories}/gps/singlewriter.v       |  4 +-
 {coq/ra => theories}/gps/write.v              |  4 +-
 {coq/ra => theories}/history.v                |  2 +-
 {coq/ra => theories}/infrastructure.v         |  0
 {coq/ra => theories}/iris_lemmas.v            |  0
 {coq/ra => theories}/lang.v                   |  2 +-
 {coq/ra => theories}/lifting.v                |  4 +-
 {coq/ra => theories}/machine.v                |  2 +-
 {coq/ra => theories}/malloc.v                 |  8 +-
 {coq/ra => theories}/na.v                     |  6 +-
 {coq/ra => theories}/notation.v               |  2 +-
 {coq/ra => theories}/persistor.v              |  6 +-
 {coq/ra => theories}/proofmode.v              |  2 +-
 {coq/ra => theories}/rsl.v                    |  6 +-
 {coq/ra => theories}/rsl_instances.v          |  4 +-
 {coq/ra => theories}/rsl_sts.v                |  4 +-
 {coq/ra => theories}/tactics.v                |  2 +-
 {coq/ra => theories}/tests/message_passing.v  |  6 +-
 {coq/ra => theories}/types.v                  |  2 +-
 {coq/ra => theories}/viewpred.v               |  2 +-
 {coq/ra => theories}/weakestpre.v             |  4 +-
 {coq/ra => theories}/wp_tactics.v             |  2 +-
 82 files changed, 206 insertions(+), 208 deletions(-)
 rename coq/ra/Makefile => Makefile (82%)
 create mode 100644 _CoqProject
 rename coq/ra/awk.Makefile => awk.Makefile (100%)
 rename {coq/build => build}/opam-ci.sh (100%)
 rename {coq/build => build}/opam-pins.sh (100%)
 delete mode 100644 coq/ra/_CoqProject
 delete mode 100644 coq/ra/base/atomic.v
 delete mode 100644 coq/ra/base/base.v
 delete mode 100644 coq/ra/gps/raw.v
 rename {coq/ra => theories}/abs_view.v (97%)
 rename {coq/ra => theories}/adequacy.v (99%)
 rename {coq/ra => theories}/arith.v (100%)
 rename {coq/ra => theories}/base/accessors.v (98%)
 rename {coq/ra => theories}/base/alloc.v (98%)
 rename {coq/ra => theories}/base/at_cas.v (99%)
 rename {coq/ra => theories}/base/at_fai.v (99%)
 rename {coq/ra => theories}/base/at_read.v (98%)
 rename {coq/ra => theories}/base/at_shared.v (97%)
 rename {coq/ra => theories}/base/at_write.v (98%)
 create mode 100644 theories/base/atomic.v
 create mode 100644 theories/base/base.v
 rename {coq/ra => theories}/base/dealloc.v (98%)
 rename {coq/ra => theories}/base/fork.v (97%)
 rename {coq/ra => theories}/base/ghosts.v (99%)
 rename {coq/ra => theories}/base/helpers.v (98%)
 rename {coq/ra => theories}/base/na_read.v (99%)
 rename {coq/ra => theories}/base/na_shared.v (95%)
 rename {coq/ra => theories}/base/na_write.v (98%)
 rename {coq/ra => theories}/bigop.v (98%)
 rename {coq/ra => theories}/blocks.v (98%)
 rename {coq/ra => theories}/blocks_generic.v (99%)
 rename {coq/ra => theories}/derived.v (98%)
 rename {coq/ra => theories}/escrows.v (98%)
 rename {coq/ra => theories}/examples/circ_buffer.v (98%)
 rename {coq/ra => theories}/examples/message_passing.v (95%)
 rename {coq/ra => theories}/examples/message_passing_base.v (97%)
 rename {coq/ra => theories}/examples/msqueue.v (99%)
 rename {coq/ra => theories}/examples/nat_tokens.v (98%)
 rename {coq/ra => theories}/examples/protocols.v (93%)
 rename {coq/ra => theories}/examples/rcu.v (99%)
 rename {coq/ra => theories}/examples/rcu_data.v (99%)
 rename {coq/ra => theories}/examples/repeat.v (97%)
 rename {coq/ra => theories}/examples/sc_stack.v (99%)
 rename {coq/ra => theories}/examples/spin_lock.v (95%)
 rename {coq/ra => theories}/examples/ticket_lock.v (99%)
 rename {coq/ra => theories}/examples/tstack.v (99%)
 rename {coq/ra => theories}/examples/unit_token.v (95%)
 rename {coq/ra => theories}/fractor.v (99%)
 rename {coq/ra => theories}/gps/cas.v (99%)
 rename {coq/ra => theories}/gps/fai.v (99%)
 rename {coq/ra => theories}/gps/fractional.v (99%)
 rename {coq/ra => theories}/gps/init.v (98%)
 rename {coq/ra => theories}/gps/inst_shared.v (81%)
 rename {coq/ra => theories}/gps/plain.v (99%)
 create mode 100644 theories/gps/raw.v
 rename {coq/ra => theories}/gps/read.v (98%)
 rename {coq/ra => theories}/gps/recursive.v (98%)
 rename {coq/ra => theories}/gps/shared.v (98%)
 rename {coq/ra => theories}/gps/singlewriter.v (99%)
 rename {coq/ra => theories}/gps/write.v (99%)
 rename {coq/ra => theories}/history.v (99%)
 rename {coq/ra => theories}/infrastructure.v (100%)
 rename {coq/ra => theories}/iris_lemmas.v (100%)
 rename {coq/ra => theories}/lang.v (99%)
 rename {coq/ra => theories}/lifting.v (99%)
 rename {coq/ra => theories}/machine.v (99%)
 rename {coq/ra => theories}/malloc.v (97%)
 rename {coq/ra => theories}/na.v (98%)
 rename {coq/ra => theories}/notation.v (99%)
 rename {coq/ra => theories}/persistor.v (98%)
 rename {coq/ra => theories}/proofmode.v (98%)
 rename {coq/ra => theories}/rsl.v (99%)
 rename {coq/ra => theories}/rsl_instances.v (99%)
 rename {coq/ra => theories}/rsl_sts.v (99%)
 rename {coq/ra => theories}/tactics.v (99%)
 rename {coq/ra => theories}/tests/message_passing.v (87%)
 rename {coq/ra => theories}/types.v (98%)
 rename {coq/ra => theories}/viewpred.v (99%)
 rename {coq/ra => theories}/weakestpre.v (99%)
 rename {coq/ra => theories}/wp_tactics.v (99%)

diff --git a/.gitignore b/.gitignore
index 8c0aeb80..c9a7505f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,5 +17,5 @@
 .#*
 auto
 *.fmt
-coq/*/Makefile.coq
+Makefile.coq*
 *~
diff --git a/coq/ra/Makefile b/Makefile
similarity index 82%
rename from coq/ra/Makefile
rename to Makefile
index 5971295f..7bfa06f8 100644
--- a/coq/ra/Makefile
+++ b/Makefile
@@ -12,7 +12,7 @@ all: Makefile.coq
 
 clean: Makefile.coq
 	+@make -f Makefile.coq clean
-	find \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
+	find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
 	rm -f Makefile.coq
 
 # Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real filename, so we do some file gymnastics.
@@ -22,9 +22,9 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
 
 # Install build-dependencies
 build-dep:
-	../build/opam-pins.sh < ../../opam.pins
+	build/opam-pins.sh < opam.pins
 	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add opam-builddep-temp "$$(pwd)/../..#HEAD" -k git -n -y
+	opam pin add opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
 	opam install opam-builddep-temp --deps-only $(YFLAG)
 	opam pin remove opam-builddep-temp
 
diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 00000000..1f56b6dd
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,73 @@
+-Q theories igps
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+theories/iris_lemmas.v
+theories/arith.v
+theories/infrastructure.v
+theories/types.v
+theories/proofmode.v
+theories/machine.v
+theories/history.v
+theories/lifting.v
+theories/lang.v
+theories/tactics.v
+theories/wp_tactics.v
+theories/derived.v
+theories/notation.v
+theories/blocks_generic.v
+theories/blocks.v
+theories/malloc.v
+theories/persistor.v
+theories/fractor.v
+theories/viewpred.v
+theories/weakestpre.v
+theories/bigop.v
+theories/abs_view.v
+theories/escrows.v
+theories/rsl_sts.v
+theories/rsl.v
+theories/rsl_instances.v
+theories/base/ghosts.v
+theories/base/helpers.v
+theories/base/accessors.v
+theories/base/at_shared.v
+theories/base/na_shared.v
+theories/base/fork.v
+theories/base/alloc.v
+theories/base/dealloc.v
+theories/base/na_read.v
+theories/base/na_write.v
+theories/na.v
+theories/base/at_read.v
+theories/base/at_write.v
+theories/base/at_cas.v
+theories/base/at_fai.v
+theories/base/atomic.v
+theories/base/base.v
+theories/adequacy.v
+theories/gps/shared.v
+theories/gps/init.v
+theories/gps/read.v
+theories/gps/write.v
+theories/gps/cas.v
+theories/gps/fai.v
+theories/gps/raw.v
+theories/gps/inst_shared.v
+theories/gps/plain.v
+theories/gps/singlewriter.v
+theories/gps/fractional.v
+theories/gps/recursive.v
+theories/examples/repeat.v
+theories/examples/nat_tokens.v
+theories/examples/unit_token.v
+theories/examples/message_passing_base.v
+theories/examples/protocols.v
+theories/examples/message_passing.v
+theories/examples/spin_lock.v
+theories/examples/circ_buffer.v
+theories/examples/ticket_lock.v
+theories/examples/tstack.v
+theories/examples/msqueue.v
+theories/examples/sc_stack.v
+theories/examples/rcu_data.v
+theories/examples/rcu.v
+theories/tests/message_passing.v
diff --git a/coq/ra/awk.Makefile b/awk.Makefile
similarity index 100%
rename from coq/ra/awk.Makefile
rename to awk.Makefile
diff --git a/coq/build/opam-ci.sh b/build/opam-ci.sh
similarity index 100%
rename from coq/build/opam-ci.sh
rename to build/opam-ci.sh
diff --git a/coq/build/opam-pins.sh b/build/opam-pins.sh
similarity index 100%
rename from coq/build/opam-pins.sh
rename to build/opam-pins.sh
diff --git a/coq/ra/_CoqProject b/coq/ra/_CoqProject
deleted file mode 100644
index b2daa558..00000000
--- a/coq/ra/_CoqProject
+++ /dev/null
@@ -1,73 +0,0 @@
--R . ra
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-./iris_lemmas.v
-./arith.v
-./infrastructure.v
-./types.v
-./proofmode.v
-./machine.v
-./history.v
-./lifting.v
-./lang.v
-./tactics.v
-./wp_tactics.v
-./derived.v
-./notation.v
-./blocks_generic.v
-./blocks.v
-./malloc.v
-./persistor.v
-./fractor.v
-./viewpred.v
-./weakestpre.v
-./bigop.v
-./abs_view.v
-./escrows.v
-./rsl_sts.v
-./rsl.v
-./rsl_instances.v
-base/ghosts.v
-base/helpers.v
-base/accessors.v
-base/at_shared.v
-base/na_shared.v
-base/fork.v
-base/alloc.v
-base/dealloc.v
-base/na_read.v
-base/na_write.v
-na.v
-base/at_read.v
-base/at_write.v
-base/at_cas.v
-base/at_fai.v
-base/atomic.v
-base/base.v
-adequacy.v
-gps/shared.v
-gps/init.v
-gps/read.v
-gps/write.v
-gps/cas.v
-gps/fai.v
-gps/raw.v
-gps/inst_shared.v
-gps/plain.v
-gps/singlewriter.v
-gps/fractional.v
-gps/recursive.v
-examples/repeat.v
-examples/nat_tokens.v
-examples/unit_token.v
-examples/message_passing_base.v
-examples/protocols.v
-examples/message_passing.v
-examples/spin_lock.v
-examples/circ_buffer.v
-examples/ticket_lock.v
-examples/tstack.v
-examples/msqueue.v
-examples/sc_stack.v
-examples/rcu_data.v
-examples/rcu.v
-tests/message_passing.v
diff --git a/coq/ra/base/atomic.v b/coq/ra/base/atomic.v
deleted file mode 100644
index 56e2be03..00000000
--- a/coq/ra/base/atomic.v
+++ /dev/null
@@ -1 +0,0 @@
-From ra.base Require Export at_read at_write at_cas at_fai.
\ No newline at end of file
diff --git a/coq/ra/base/base.v b/coq/ra/base/base.v
deleted file mode 100644
index e1023b43..00000000
--- a/coq/ra/base/base.v
+++ /dev/null
@@ -1 +0,0 @@
-From ra.base Require Export atomic alloc dealloc accessors fork.
\ No newline at end of file
diff --git a/coq/ra/gps/raw.v b/coq/ra/gps/raw.v
deleted file mode 100644
index 9c41a656..00000000
--- a/coq/ra/gps/raw.v
+++ /dev/null
@@ -1 +0,0 @@
-From ra.gps Require Export shared init read write cas fai.
\ No newline at end of file
diff --git a/opam b/opam
index 8d6cdca9..b3dba1e7 100644
--- a/opam
+++ b/opam
@@ -1,5 +1,5 @@
 opam-version: "1.2"
-name: "coq-gps"
+name: "coq-igps"
 version: "dev"
 maintainer: "Jan-Oliver Kaiser, Hoang-Hai Dang"
 authors: "Jan-Oliver Kaiser, Hoang-Hai Dang"
@@ -10,9 +10,7 @@ build: [
   [make "-j%{jobs}%"]
 ]
 install: [make "install"]
-# TODO: probably we want to install things to a different folder, "ra" is rather undescriptive
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/ra" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris" #{ = "3.0.0" }
-  "coq-stdpp"
+  "coq-iris"
 ]
diff --git a/coq/ra/abs_view.v b/theories/abs_view.v
similarity index 97%
rename from coq/ra/abs_view.v
rename to theories/abs_view.v
index 19805a0e..67aa5d5b 100644
--- a/coq/ra/abs_view.v
+++ b/theories/abs_view.v
@@ -3,8 +3,8 @@ From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import viewpred proofmode.
-From ra.base Require Import ghosts.
+From igps Require Import viewpred proofmode.
+From igps.base Require Import ghosts.
 
 
 Class absViewG Σ := AbsViewG {
diff --git a/coq/ra/adequacy.v b/theories/adequacy.v
similarity index 99%
rename from coq/ra/adequacy.v
rename to theories/adequacy.v
index b1d2c547..5ce53a9d 100644
--- a/coq/ra/adequacy.v
+++ b/theories/adequacy.v
@@ -3,8 +3,8 @@ From iris.base_logic Require Import lib.invariants big_op.
 From iris.algebra Require Import auth.
 Set Default Proof Using "Type".
 
-From ra Require Import lang weakestpre proofmode.
-From ra.base Require Import ghosts.
+From igps Require Import lang weakestpre proofmode.
+From igps.base Require Import ghosts.
 
 Class basePreG Σ := BasePreG {
   base_preG_iris :> ownPPreG (ra_lang) Σ;
diff --git a/coq/ra/arith.v b/theories/arith.v
similarity index 100%
rename from coq/ra/arith.v
rename to theories/arith.v
diff --git a/coq/ra/base/accessors.v b/theories/base/accessors.v
similarity index 98%
rename from coq/ra/base/accessors.v
rename to theories/base/accessors.v
index 49b349ad..4f188fe9 100644
--- a/coq/ra/base/accessors.v
+++ b/theories/base/accessors.v
@@ -2,8 +2,8 @@ From iris.base_logic Require Export lib.invariants lib.viewshifts.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth excl gmap.
 
-From ra Require Import infrastructure machine lang history.
-From ra Require Export ghosts.
+From igps Require Import infrastructure machine lang history.
+From igps Require Export ghosts.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/base/alloc.v b/theories/base/alloc.v
similarity index 98%
rename from coq/ra/base/alloc.v
rename to theories/base/alloc.v
index f18e163e..a8aa56cf 100644
--- a/coq/ra/base/alloc.v
+++ b/theories/base/alloc.v
@@ -1,6 +1,6 @@
-From ra Require Import lang.
+From igps Require Import lang.
 From iris.proofmode Require Import tactics.
-From ra.base Require Import ghosts at_shared.
+From igps.base Require Import ghosts at_shared.
 
 Section Alloc.
   Context `{fG : !foundationG Σ}.
diff --git a/coq/ra/base/at_cas.v b/theories/base/at_cas.v
similarity index 99%
rename from coq/ra/base/at_cas.v
rename to theories/base/at_cas.v
index 305d7939..197acd7e 100644
--- a/coq/ra/base/at_cas.v
+++ b/theories/base/at_cas.v
@@ -1,4 +1,4 @@
-From ra.base Require Import at_shared.
+From igps.base Require Import at_shared.
 
 Lemma f_CAS `{fG : !foundationG Σ} π V l h (v_r v_w: Z):
   {{{ PSCtx ∗ ▷ Seen π V ∗ ▷ Hist l h ∗ ⌜init_local h V⌝ }}}
diff --git a/coq/ra/base/at_fai.v b/theories/base/at_fai.v
similarity index 99%
rename from coq/ra/base/at_fai.v
rename to theories/base/at_fai.v
index 076b4024..7c63dfe9 100644
--- a/coq/ra/base/at_fai.v
+++ b/theories/base/at_fai.v
@@ -1,4 +1,4 @@
-From ra.base Require Import at_shared.
+From igps.base Require Import at_shared.
 
 Lemma f_FAI `{fG : !foundationG Σ} C π V l h:
   {{{ PSCtx ∗ ▷ Seen π V ∗ ▷ Hist l h ∗ ⌜init_local h V⌝ }}}
diff --git a/coq/ra/base/at_read.v b/theories/base/at_read.v
similarity index 98%
rename from coq/ra/base/at_read.v
rename to theories/base/at_read.v
index 2d09f3df..bb8e4ad2 100644
--- a/coq/ra/base/at_read.v
+++ b/theories/base/at_read.v
@@ -1,4 +1,4 @@
-From ra.base Require Import at_shared.
+From igps.base Require Import at_shared.
 
 Lemma f_read_at `{fG : !foundationG Σ} π V_l l h :
   {{{ PSCtx
diff --git a/coq/ra/base/at_shared.v b/theories/base/at_shared.v
similarity index 97%
rename from coq/ra/base/at_shared.v
rename to theories/base/at_shared.v
index d09b4485..64a15eed 100644
--- a/coq/ra/base/at_shared.v
+++ b/theories/base/at_shared.v
@@ -5,8 +5,8 @@ From iris.algebra Require Export auth frac excl gmap.
 
 Import uPred.
 
-From ra Require Export notation.
-From ra.base Require Export accessors helpers ghosts.
+From igps Require Export notation.
+From igps.base Require Export accessors helpers ghosts.
 
 Lemma write_at_update_hist Ï‚ Ï‚' V h t l v (m: message)
   (HOld: h ≡ map_vt (hist_from (mem ς) l t))
diff --git a/coq/ra/base/at_write.v b/theories/base/at_write.v
similarity index 98%
rename from coq/ra/base/at_write.v
rename to theories/base/at_write.v
index d2b1ad49..217c227a 100644
--- a/coq/ra/base/at_write.v
+++ b/theories/base/at_write.v
@@ -1,4 +1,4 @@
-From ra.base Require Import at_shared.
+From igps.base Require Import at_shared.
 
 Lemma f_write_at `{fG : !foundationG Σ} π V_l l h v:
   {{{ PSCtx 
diff --git a/theories/base/atomic.v b/theories/base/atomic.v
new file mode 100644
index 00000000..d8a02a7d
--- /dev/null
+++ b/theories/base/atomic.v
@@ -0,0 +1 @@
+From igps.base Require Export at_read at_write at_cas at_fai.
\ No newline at end of file
diff --git a/theories/base/base.v b/theories/base/base.v
new file mode 100644
index 00000000..f1742508
--- /dev/null
+++ b/theories/base/base.v
@@ -0,0 +1 @@
+From igps.base Require Export atomic alloc dealloc accessors fork.
\ No newline at end of file
diff --git a/coq/ra/base/dealloc.v b/theories/base/dealloc.v
similarity index 98%
rename from coq/ra/base/dealloc.v
rename to theories/base/dealloc.v
index 0307287c..6ab0f0c3 100644
--- a/coq/ra/base/dealloc.v
+++ b/theories/base/dealloc.v
@@ -1,4 +1,4 @@
-From ra.base Require Import na_shared.
+From igps.base Require Import na_shared.
 
 Lemma f_dealloc `{fG : !foundationG Σ} π V_l l h v :
   {{{ PSCtx ∗ ▷ Seen π V_l 
diff --git a/coq/ra/base/fork.v b/theories/base/fork.v
similarity index 97%
rename from coq/ra/base/fork.v
rename to theories/base/fork.v
index 49c7a69a..a0697deb 100644
--- a/coq/ra/base/fork.v
+++ b/theories/base/fork.v
@@ -1,4 +1,4 @@
-From ra.base Require Import na_shared.
+From igps.base Require Import na_shared.
 
 Lemma f_fork `{fG : foundationG Σ} (Φ : val ra_lang → iProp _) (P: iProp _) π V e:
     PSCtx
diff --git a/coq/ra/base/ghosts.v b/theories/base/ghosts.v
similarity index 99%
rename from coq/ra/base/ghosts.v
rename to theories/base/ghosts.v
index 875c6831..1ed9991f 100644
--- a/coq/ra/base/ghosts.v
+++ b/theories/base/ghosts.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Export ownp.
 From iris.algebra Require Import deprecated.
 Export deprecated.dec_agree.
 From iris.base_logic Require Import big_op lib.invariants.
-From ra Require Import lang history.
+From igps Require Import lang history.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/base/helpers.v b/theories/base/helpers.v
similarity index 98%
rename from coq/ra/base/helpers.v
rename to theories/base/helpers.v
index 51e411b2..39a60f0b 100644
--- a/coq/ra/base/helpers.v
+++ b/theories/base/helpers.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Import excl.
 
-From ra Require Import infrastructure machine history lifting.
-From ra Require Export ghosts.
+From igps Require Import infrastructure machine history lifting.
+From igps Require Export ghosts.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/base/na_read.v b/theories/base/na_read.v
similarity index 99%
rename from coq/ra/base/na_read.v
rename to theories/base/na_read.v
index 7552c034..95a71e28 100644
--- a/coq/ra/base/na_read.v
+++ b/theories/base/na_read.v
@@ -1,4 +1,4 @@
-From ra.base Require Import na_shared.
+From igps.base Require Import na_shared.
 
 Lemma f_read_na `{fG : foundationG Σ} π V_l l h :
   {{{ PSCtx ∗ ▷ Seen π V_l ∗ ▷ Hist l h
diff --git a/coq/ra/base/na_shared.v b/theories/base/na_shared.v
similarity index 95%
rename from coq/ra/base/na_shared.v
rename to theories/base/na_shared.v
index b9e1b635..25776422 100644
--- a/coq/ra/base/na_shared.v
+++ b/theories/base/na_shared.v
@@ -5,8 +5,8 @@ From iris.algebra Require Export auth frac excl gmap.
 
 Import uPred.
 
-From ra Require Export notation history proofmode.
-From ra.base Require Export ghosts accessors helpers.
+From igps Require Export notation history proofmode.
+From igps.base Require Export ghosts accessors helpers.
 
 Lemma write_na_update_HInv `{fG : !foundationG Σ}
   Ï‚ Ï‚' (h  h2: History) (l : loc) (m: message) HIST
diff --git a/coq/ra/base/na_write.v b/theories/base/na_write.v
similarity index 98%
rename from coq/ra/base/na_write.v
rename to theories/base/na_write.v
index c006cdbd..dc259ad9 100644
--- a/coq/ra/base/na_write.v
+++ b/theories/base/na_write.v
@@ -1,4 +1,4 @@
-From ra.base Require Import na_shared.
+From igps.base Require Import na_shared.
 
 Lemma f_write_na `{fG : !foundationG Σ} π V_l l h v:
   {{{ PSCtx
diff --git a/coq/ra/bigop.v b/theories/bigop.v
similarity index 98%
rename from coq/ra/bigop.v
rename to theories/bigop.v
index 8fef0b9b..b9ed8ee6 100644
--- a/coq/ra/bigop.v
+++ b/theories/bigop.v
@@ -1,6 +1,6 @@
 From iris.base_logic Require Import big_op lib.iprop lib.fractional.
 From iris.proofmode Require Import tactics.
-From ra Require Import viewpred proofmode.
+From igps Require Import viewpred proofmode.
 
 
 Program Definition Pos2Qp (n: positive) : Qp := mk_Qp (Zpos n) _.
diff --git a/coq/ra/blocks.v b/theories/blocks.v
similarity index 98%
rename from coq/ra/blocks.v
rename to theories/blocks.v
index 6d1fa708..f73ab8fa 100644
--- a/coq/ra/blocks.v
+++ b/theories/blocks.v
@@ -1,5 +1,5 @@
-From ra Require Import blocks_generic types lang.
-From ra.base Require Import ghosts.
+From igps Require Import blocks_generic types lang.
+From igps.base Require Import ghosts.
 
 Section MHist.
   Implicit Type (M : gset message).
diff --git a/coq/ra/blocks_generic.v b/theories/blocks_generic.v
similarity index 99%
rename from coq/ra/blocks_generic.v
rename to theories/blocks_generic.v
index 42da9964..e5cd1e1e 100644
--- a/coq/ra/blocks_generic.v
+++ b/theories/blocks_generic.v
@@ -3,7 +3,7 @@ From mathcomp Require Import ssreflect.
 From stdpp Require Import gmap.
 From iris.base_logic Require Import big_op lib.iprop.
 From iris.proofmode Require Import tactics.
-From ra Require Import infrastructure.
+From igps Require Import infrastructure.
 
 Section Blocks.
   Context `{Count : Countable A} {R : relation A}
diff --git a/coq/ra/derived.v b/theories/derived.v
similarity index 98%
rename from coq/ra/derived.v
rename to theories/derived.v
index 558daca6..799b0999 100644
--- a/coq/ra/derived.v
+++ b/theories/derived.v
@@ -1,4 +1,4 @@
-From ra Require Export lifting.
+From igps Require Export lifting.
 
 Import uPred.
 
diff --git a/coq/ra/escrows.v b/theories/escrows.v
similarity index 98%
rename from coq/ra/escrows.v
rename to theories/escrows.v
index bbc32025..9ee7d5e9 100644
--- a/coq/ra/escrows.v
+++ b/theories/escrows.v
@@ -3,9 +3,9 @@ From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import viewpred proofmode.
-From ra.base Require Import ghosts.
-From ra Require Export abs_view.
+From igps Require Import viewpred proofmode.
+From igps.base Require Import ghosts.
+From igps Require Export abs_view.
 
 Definition escrowN : namespace := nroot .@ "escrow".
 
diff --git a/coq/ra/examples/circ_buffer.v b/theories/examples/circ_buffer.v
similarity index 98%
rename from coq/ra/examples/circ_buffer.v
rename to theories/examples/circ_buffer.v
index 56f595c3..e2984ec2 100644
--- a/coq/ra/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -2,10 +2,10 @@ From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import coPset.
 
-From ra Require Export notation malloc escrows bigop.
-From ra Require Import persistor viewpred weakestpre proofmode arith.
-From ra.examples Require Import nat_tokens protocols.
-From ra.gps Require Import singlewriter.
+From igps Require Export notation malloc escrows bigop.
+From igps Require Import persistor viewpred weakestpre proofmode arith.
+From igps.examples Require Import nat_tokens protocols.
+From igps.gps Require Import singlewriter.
 
 Import uPred.
 
diff --git a/coq/ra/examples/message_passing.v b/theories/examples/message_passing.v
similarity index 95%
rename from coq/ra/examples/message_passing.v
rename to theories/examples/message_passing.v
index 361b85d1..7710100e 100644
--- a/coq/ra/examples/message_passing.v
+++ b/theories/examples/message_passing.v
@@ -2,11 +2,11 @@ From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 
-From ra Require Export malloc repeat notation wp_tactics escrows.
-From ra Require Import persistor viewpred proofmode weakestpre protocols.
-From ra.base Require Import fork.
-From ra.gps Require Import plain.
-From ra.examples Require Import unit_token.
+From igps Require Export malloc repeat notation wp_tactics escrows.
+From igps Require Import persistor viewpred proofmode weakestpre protocols.
+From igps.base Require Import fork.
+From igps.gps Require Import plain.
+From igps.examples Require Import unit_token.
 
 Import uPred.
 
diff --git a/coq/ra/examples/message_passing_base.v b/theories/examples/message_passing_base.v
similarity index 97%
rename from coq/ra/examples/message_passing_base.v
rename to theories/examples/message_passing_base.v
index f32ae78f..9e402149 100644
--- a/coq/ra/examples/message_passing_base.v
+++ b/theories/examples/message_passing_base.v
@@ -3,9 +3,9 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 From iris.base_logic.lib Require Import invariants.
 
-From ra.base Require Import ghosts alloc fork na_write na_read at_write at_read.
-From ra.examples Require Import unit_token.
-From ra Require Export repeat notation wp_tactics proofmode.
+From igps.base Require Import ghosts alloc fork na_write na_read at_write at_read.
+From igps.examples Require Import unit_token.
+From igps Require Export repeat notation wp_tactics proofmode.
 Import uPred.
 
 Definition message_passing : base.expr :=
diff --git a/coq/ra/examples/msqueue.v b/theories/examples/msqueue.v
similarity index 99%
rename from coq/ra/examples/msqueue.v
rename to theories/examples/msqueue.v
index b244e123..f21480b2 100644
--- a/coq/ra/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -1,9 +1,9 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import notation malloc escrows repeat protocols.
-From ra.gps Require Import shared plain recursive.
-From ra.examples Require Import unit_token.
+From igps Require Import notation malloc escrows repeat protocols.
+From igps.gps Require Import shared plain recursive.
+From igps.examples Require Import unit_token.
 Import uPred.
 
 (** Simplified formalization of Michael-Scott queue
diff --git a/coq/ra/examples/nat_tokens.v b/theories/examples/nat_tokens.v
similarity index 98%
rename from coq/ra/examples/nat_tokens.v
rename to theories/examples/nat_tokens.v
index d871e679..39cd4f0f 100644
--- a/coq/ra/examples/nat_tokens.v
+++ b/theories/examples/nat_tokens.v
@@ -1,7 +1,7 @@
 From Coq Require Import Psatz.
 From iris.algebra Require Import coPset.
 
-From ra Require Import arith infrastructure.
+From igps Require Import arith infrastructure.
 
 (** Tokens with infinite number to be used in various examples **)
 
diff --git a/coq/ra/examples/protocols.v b/theories/examples/protocols.v
similarity index 93%
rename from coq/ra/examples/protocols.v
rename to theories/examples/protocols.v
index a1a49fc8..56320748 100644
--- a/coq/ra/examples/protocols.v
+++ b/theories/examples/protocols.v
@@ -1,4 +1,4 @@
-From ra.gps Require Export shared.
+From igps.gps Require Export shared.
 
 Canonical Structure natProtocol : protocolT := ProtocolT _ le.
 
diff --git a/coq/ra/examples/rcu.v b/theories/examples/rcu.v
similarity index 99%
rename from coq/ra/examples/rcu.v
rename to theories/examples/rcu.v
index 1dc85fdf..72ea64f0 100644
--- a/coq/ra/examples/rcu.v
+++ b/theories/examples/rcu.v
@@ -3,9 +3,9 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth coPset.
 From iris.base_logic Require Import big_op.
 
-From ra Require Import notation malloc escrows repeat protocols bigop.
-From ra.gps Require Import shared plain fractional singlewriter recursive.
-From ra.examples Require Import sc_stack nat_tokens rcu_data.
+From igps Require Import notation malloc escrows repeat protocols bigop.
+From igps.gps Require Import shared plain fractional singlewriter recursive.
+From igps.examples Require Import sc_stack nat_tokens rcu_data.
 
 Import uPred.
 
diff --git a/coq/ra/examples/rcu_data.v b/theories/examples/rcu_data.v
similarity index 99%
rename from coq/ra/examples/rcu_data.v
rename to theories/examples/rcu_data.v
index 17008d78..484b398d 100644
--- a/coq/ra/examples/rcu_data.v
+++ b/theories/examples/rcu_data.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Import iprop own.
 From iris.algebra Require Import auth gmap coPset.
-From ra Require Import infrastructure machine.
+From igps Require Import infrastructure machine.
 
 (** Logical data structure needed for the RCU proof,
       see rcu.v for more info about the original paper *)
diff --git a/coq/ra/examples/repeat.v b/theories/examples/repeat.v
similarity index 97%
rename from coq/ra/examples/repeat.v
rename to theories/examples/repeat.v
index c679a690..6907be7a 100644
--- a/coq/ra/examples/repeat.v
+++ b/theories/examples/repeat.v
@@ -1,7 +1,7 @@
 From iris.base_logic Require Import upred primitive derived.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
-From ra Require Export notation wp_tactics.
+From igps Require Export notation wp_tactics.
 Import uPred.
 
 (* Definition repeat (e: base.expr): base.expr := *)
diff --git a/coq/ra/examples/sc_stack.v b/theories/examples/sc_stack.v
similarity index 99%
rename from coq/ra/examples/sc_stack.v
rename to theories/examples/sc_stack.v
index d686b5b1..546dbe13 100644
--- a/coq/ra/examples/sc_stack.v
+++ b/theories/examples/sc_stack.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import notation malloc na proofmode weakestpre.
+From igps Require Import notation malloc na proofmode weakestpre.
 
 Import uPred.
 
diff --git a/coq/ra/examples/spin_lock.v b/theories/examples/spin_lock.v
similarity index 95%
rename from coq/ra/examples/spin_lock.v
rename to theories/examples/spin_lock.v
index 60fa6b88..8a749599 100644
--- a/coq/ra/examples/spin_lock.v
+++ b/theories/examples/spin_lock.v
@@ -2,9 +2,9 @@ From iris.program_logic Require Export weakestpre.
 From iris.base_logic.lib Require Import cancelable_invariants.
 From iris.proofmode Require Import tactics.
 
-From ra Require Export notation malloc repeat wp_tactics viewpred rsl_instances.
-From ra Require Import rsl persistor proofmode weakestpre.
-From ra.base Require Import base.
+From igps Require Export notation malloc repeat wp_tactics viewpred rsl_instances.
+From igps Require Import rsl persistor proofmode weakestpre.
+From igps.base Require Import base.
 Import uPred.
 
 (** Basic spin-lock proven with iRSL *)
diff --git a/coq/ra/examples/ticket_lock.v b/theories/examples/ticket_lock.v
similarity index 99%
rename from coq/ra/examples/ticket_lock.v
rename to theories/examples/ticket_lock.v
index adbb44a0..7d4822e8 100644
--- a/coq/ra/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -3,10 +3,10 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import coPset gmap auth excl.
 From iris.base_logic Require Import big_op.
 
-From ra Require Import escrows notation malloc repeat.
-From ra Require Import persistor viewpred weakestpre proofmode bigop arith.
-From ra.examples Require Import nat_tokens protocols.
-From ra.gps Require Import singlewriter plain recursive.
+From igps Require Import escrows notation malloc repeat.
+From igps Require Import persistor viewpred weakestpre proofmode bigop arith.
+From igps.examples Require Import nat_tokens protocols.
+From igps.gps Require Import singlewriter plain recursive.
 
 (** Formalization of bounded ticket-lock examples.
     The proof is simplified by using single-writer protocols and 
diff --git a/coq/ra/examples/tstack.v b/theories/examples/tstack.v
similarity index 99%
rename from coq/ra/examples/tstack.v
rename to theories/examples/tstack.v
index 5fcbbe75..a6f287f7 100644
--- a/coq/ra/examples/tstack.v
+++ b/theories/examples/tstack.v
@@ -1,8 +1,8 @@
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import notation malloc repeat protocols.
-From ra.gps Require Import shared plain.
+From igps Require Import notation malloc repeat protocols.
+From igps.gps Require Import shared plain.
 
 Import uPred.
 
diff --git a/coq/ra/examples/unit_token.v b/theories/examples/unit_token.v
similarity index 95%
rename from coq/ra/examples/unit_token.v
rename to theories/examples/unit_token.v
index 0f206b89..b8aa3392 100644
--- a/coq/ra/examples/unit_token.v
+++ b/theories/examples/unit_token.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
 From iris.base_logic.lib Require Import own.
 
-From ra Require Import viewpred.
+From igps Require Import viewpred.
 
 Class uTokG Σ := UnitTokG { init_tokG :> inG Σ (exclR unitC) }.
 Definition uTokΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
diff --git a/coq/ra/fractor.v b/theories/fractor.v
similarity index 99%
rename from coq/ra/fractor.v
rename to theories/fractor.v
index 868eaac8..26684736 100644
--- a/coq/ra/fractor.v
+++ b/theories/fractor.v
@@ -5,8 +5,8 @@ From iris.base_logic.lib Require Export cancelable_invariants.
 
 Import uPred.
 
-From ra Require Import lang.
-From ra.base Require Import accessors.
+From igps Require Import lang.
+From igps.base Require Import accessors.
 
 Definition fracN : namespace := nroot .@ "fractor".
 
diff --git a/coq/ra/gps/cas.v b/theories/gps/cas.v
similarity index 99%
rename from coq/ra/gps/cas.v
rename to theories/gps/cas.v
index 08754e44..6b4abe19 100644
--- a/coq/ra/gps/cas.v
+++ b/theories/gps/cas.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import at_cas.
+From igps.gps Require Import shared.
+From igps.base Require Import at_cas.
 
 Section CAS.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
diff --git a/coq/ra/gps/fai.v b/theories/gps/fai.v
similarity index 99%
rename from coq/ra/gps/fai.v
rename to theories/gps/fai.v
index ad5500cc..6d8d5045 100644
--- a/coq/ra/gps/fai.v
+++ b/theories/gps/fai.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import at_fai.
+From igps.gps Require Import shared.
+From igps.base Require Import at_fai.
 
 Section FAI.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
diff --git a/coq/ra/gps/fractional.v b/theories/gps/fractional.v
similarity index 99%
rename from coq/ra/gps/fractional.v
rename to theories/gps/fractional.v
index e121c2ca..a476af30 100644
--- a/coq/ra/gps/fractional.v
+++ b/theories/gps/fractional.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
-From ra.gps Require Export inst_shared.
-From ra Require Import abs_view.
+From igps.gps Require Export inst_shared.
+From igps Require Import abs_view.
 
 Section Fractional.
   Context `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF}
diff --git a/coq/ra/gps/init.v b/theories/gps/init.v
similarity index 98%
rename from coq/ra/gps/init.v
rename to theories/gps/init.v
index c2f4fdb0..f7c0eded 100644
--- a/coq/ra/gps/init.v
+++ b/theories/gps/init.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import na_write.
+From igps.gps Require Import shared.
+From igps.base Require Import na_write.
 
 Section Init_Strong.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} 
diff --git a/coq/ra/gps/inst_shared.v b/theories/gps/inst_shared.v
similarity index 81%
rename from coq/ra/gps/inst_shared.v
rename to theories/gps/inst_shared.v
index 56d4ba1c..fbe5623a 100644
--- a/coq/ra/gps/inst_shared.v
+++ b/theories/gps/inst_shared.v
@@ -3,9 +3,9 @@ From iris.algebra Require Export auth.
 
 Import uPred.
 
-From ra Require Export persistor fractor proofmode weakestpre viewpred.
-From ra Require Export notation na.
-From ra.gps Require Export raw.
+From igps Require Export persistor fractor proofmode weakestpre viewpred.
+From igps Require Export notation na.
+From igps.gps Require Export raw.
 
 Definition state_sort_eqdec Prtcl {PF : protocol_facts Prtcl} : EqDecision (state_sort Prtcl) := _.
 Notation gps_agreeG Σ Prtcl := (inG Σ (dec_agreeR (EqDecision0 := state_sort_eqdec Prtcl%type) (state_sort Prtcl))).
diff --git a/coq/ra/gps/plain.v b/theories/gps/plain.v
similarity index 99%
rename from coq/ra/gps/plain.v
rename to theories/gps/plain.v
index 81de484c..13de7c35 100644
--- a/coq/ra/gps/plain.v
+++ b/theories/gps/plain.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From ra.gps Require Export inst_shared.
+From igps.gps Require Export inst_shared.
 
 Section Plain.
   Context {Σ : gFunctors} {Prtcl : protocolT} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF}
diff --git a/theories/gps/raw.v b/theories/gps/raw.v
new file mode 100644
index 00000000..c2b4a38c
--- /dev/null
+++ b/theories/gps/raw.v
@@ -0,0 +1 @@
+From igps.gps Require Export shared init read write cas fai.
\ No newline at end of file
diff --git a/coq/ra/gps/read.v b/theories/gps/read.v
similarity index 98%
rename from coq/ra/gps/read.v
rename to theories/gps/read.v
index ec61e0e1..837cb6b1 100644
--- a/coq/ra/gps/read.v
+++ b/theories/gps/read.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import at_read.
+From igps.gps Require Import shared.
+From igps.base Require Import at_read.
 
 Section Read.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
diff --git a/coq/ra/gps/recursive.v b/theories/gps/recursive.v
similarity index 98%
rename from coq/ra/gps/recursive.v
rename to theories/gps/recursive.v
index 3a9692d6..68b2f5b2 100644
--- a/coq/ra/gps/recursive.v
+++ b/theories/gps/recursive.v
@@ -5,9 +5,9 @@ From iris.algebra Require Export cmra_big_op ofe.
 
 Import uPred.
 
-From ra Require Import persistor fractor proofmode weakestpre.
-From ra Require Export notation na.
-From ra.gps Require Import shared inst_shared plain fractional singlewriter.
+From igps Require Import persistor fractor proofmode weakestpre.
+From igps Require Export notation na.
+From igps.gps Require Import shared inst_shared plain fractional singlewriter.
 
 Section RecInterp.
   Context {Σ : gFunctors} (Prtcl : protocolT). 
diff --git a/coq/ra/gps/shared.v b/theories/gps/shared.v
similarity index 98%
rename from coq/ra/gps/shared.v
rename to theories/gps/shared.v
index 2cdd4f2e..6acb1bc9 100644
--- a/coq/ra/gps/shared.v
+++ b/theories/gps/shared.v
@@ -2,9 +2,9 @@ From iris.algebra Require Export auth frac excl gmap gset local_updates.
 From iris.program_logic Require Import ectx_lifting.
 From iris.base_logic Require Import lib.sts big_op.
 
-From ra Require Export viewpred tactics notation.
-From ra Require Export blocks_generic blocks proofmode viewpred.
-From ra.base Require Export ghosts.
+From igps Require Export viewpred tactics notation.
+From igps Require Export blocks_generic blocks proofmode viewpred.
+From igps.base Require Export ghosts.
 
 Structure protocolT :=
    ProtocolT {
diff --git a/coq/ra/gps/singlewriter.v b/theories/gps/singlewriter.v
similarity index 99%
rename from coq/ra/gps/singlewriter.v
rename to theories/gps/singlewriter.v
index e1bed844..0412ef6e 100644
--- a/coq/ra/gps/singlewriter.v
+++ b/theories/gps/singlewriter.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
-From ra.gps Require Export inst_shared.
-From ra Require Import bigop abs_view.
+From igps.gps Require Export inst_shared.
+From igps Require Import bigop abs_view.
 
 
 Section Gname_StrongSW.
diff --git a/coq/ra/gps/write.v b/theories/gps/write.v
similarity index 99%
rename from coq/ra/gps/write.v
rename to theories/gps/write.v
index b26c3ca6..c6b1e701 100644
--- a/coq/ra/gps/write.v
+++ b/theories/gps/write.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export weakestpre.
-From ra.gps Require Import shared.
-From ra.base Require Import at_write.
+From igps.gps Require Import shared.
+From igps.base Require Import at_write.
 
 Section Write.
   Context {Σ} `{fG : !foundationG Σ} `{GPSG : !gpsG Σ Prtcl PF} (IP : interpC Σ Prtcl) (l : loc).
diff --git a/coq/ra/history.v b/theories/history.v
similarity index 99%
rename from coq/ra/history.v
rename to theories/history.v
index d3e8fb80..ca5b84f4 100644
--- a/coq/ra/history.v
+++ b/theories/history.v
@@ -7,7 +7,7 @@ Global Set Asymmetric Patterns.
 Global Set Bullet Behavior "Strict Subproofs".
 From Coq Require Export Utf8.
 
-From ra Require Import infrastructure types machine.
+From igps Require Import infrastructure types machine.
 
 Section History.
   Notation MessageSet := (gset message).
diff --git a/coq/ra/infrastructure.v b/theories/infrastructure.v
similarity index 100%
rename from coq/ra/infrastructure.v
rename to theories/infrastructure.v
diff --git a/coq/ra/iris_lemmas.v b/theories/iris_lemmas.v
similarity index 100%
rename from coq/ra/iris_lemmas.v
rename to theories/iris_lemmas.v
diff --git a/coq/ra/lang.v b/theories/lang.v
similarity index 99%
rename from coq/ra/lang.v
rename to theories/lang.v
index fedfbeae..9a2f3b7f 100644
--- a/coq/ra/lang.v
+++ b/theories/lang.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export ectx_language ectxi_language.
 From stdpp Require Export strings gmap.
 From iris.algebra Require Import ofe.
 
-From ra Require Export machine.
+From igps Require Export machine.
 
 Module base.
   Open Scope Z_scope.
diff --git a/coq/ra/lifting.v b/theories/lifting.v
similarity index 99%
rename from coq/ra/lifting.v
rename to theories/lifting.v
index 3000bb88..fec1dc98 100644
--- a/coq/ra/lifting.v
+++ b/theories/lifting.v
@@ -4,8 +4,8 @@ From iris.proofmode Require Import tactics.
 
 Import uPred.
 
-From ra Require Import types.
-From ra Require Export lang history tactics.
+From igps Require Import types.
+From igps Require Export lang history tactics.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/machine.v b/theories/machine.v
similarity index 99%
rename from coq/ra/machine.v
rename to theories/machine.v
index e15203d6..bef65df3 100644
--- a/coq/ra/machine.v
+++ b/theories/machine.v
@@ -9,7 +9,7 @@ From Coq Require Export Utf8.
 
 Open Scope positive.
 
-From ra Require Export infrastructure types.
+From igps Require Export infrastructure types.
 
 Notation loc := (positive) (only parsing).
 Section RAMachine.
diff --git a/coq/ra/malloc.v b/theories/malloc.v
similarity index 97%
rename from coq/ra/malloc.v
rename to theories/malloc.v
index c2b48916..8383cb56 100644
--- a/coq/ra/malloc.v
+++ b/theories/malloc.v
@@ -3,10 +3,10 @@ From iris.base_logic Require Export lib.invariants.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import gmap.
 
-From ra Require Import weakestpre proofmode.
-From ra Require Export viewpred wp_tactics.
-From ra Require Import notation bigop na.
-From ra.base Require Import ghosts alloc dealloc.
+From igps Require Import weakestpre proofmode.
+From igps Require Export viewpred wp_tactics.
+From igps Require Import notation bigop na.
+From igps.base Require Import ghosts alloc dealloc.
 
 Definition mdealloc : base.val :=
   (λ: "l" "n",
diff --git a/coq/ra/na.v b/theories/na.v
similarity index 98%
rename from coq/ra/na.v
rename to theories/na.v
index f32f133d..96474c05 100644
--- a/coq/ra/na.v
+++ b/theories/na.v
@@ -2,9 +2,9 @@ From iris.program_logic Require Import weakestpre.
 From iris.base_logic Require Import lib.invariants.
 From iris.proofmode Require Import tactics.
 
-From ra Require Import viewpred proofmode weakestpre fractor abs_view.
-From ra Require Export notation bigop.
-From ra.base Require Export ghosts na_read na_write.
+From igps Require Import viewpred proofmode weakestpre fractor abs_view.
+From igps Require Export notation bigop.
+From igps.base Require Export ghosts na_read na_write.
 
 Section Helpers.
   Context {Σ : gFunctors}.
diff --git a/coq/ra/notation.v b/theories/notation.v
similarity index 99%
rename from coq/ra/notation.v
rename to theories/notation.v
index 6de027a5..3cc4be4e 100644
--- a/coq/ra/notation.v
+++ b/theories/notation.v
@@ -1,4 +1,4 @@
-From ra Require Export derived.
+From igps Require Export derived.
 Export ra_lang.
 
 Coercion LitInt : Z >-> base_lit.
diff --git a/coq/ra/persistor.v b/theories/persistor.v
similarity index 98%
rename from coq/ra/persistor.v
rename to theories/persistor.v
index c4921547..39c66a71 100644
--- a/coq/ra/persistor.v
+++ b/theories/persistor.v
@@ -4,9 +4,9 @@ From iris.algebra Require Import auth frac excl gmap.
 
 Import uPred.
 
-From ra Require Import iris_lemmas.
-From ra Require Export lang.
-From ra.base Require Import accessors.
+From igps Require Import iris_lemmas.
+From igps Require Export lang.
+From igps.base Require Import accessors.
 
 Definition persistN : namespace := nroot .@ "persistor".
 Notation persist_invN := (persistN .@ "inv").
diff --git a/coq/ra/proofmode.v b/theories/proofmode.v
similarity index 98%
rename from coq/ra/proofmode.v
rename to theories/proofmode.v
index de307ea8..c9223d2a 100644
--- a/coq/ra/proofmode.v
+++ b/theories/proofmode.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Import iprop.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Export tactics.
-From ra Require Import viewpred.
+From igps Require Import viewpred.
 
 Section Instances.
   Context {Σ : gFunctors}.
diff --git a/coq/ra/rsl.v b/theories/rsl.v
similarity index 99%
rename from coq/ra/rsl.v
rename to theories/rsl.v
index 4913a719..b1c18933 100644
--- a/coq/ra/rsl.v
+++ b/theories/rsl.v
@@ -8,9 +8,9 @@ From iris.proofmode Require Import tactics.
 
 Import uPred.
 
-From ra Require Export lang blocks iris_lemmas.
-From ra Require Import rsl_sts notation viewpred na.
-From ra.base Require Import base.
+From igps Require Export lang blocks iris_lemmas.
+From igps Require Import rsl_sts notation viewpred na.
+From igps.base Require Import base.
 
 Set Bullet Behavior "Strict Subproofs".
 
diff --git a/coq/ra/rsl_instances.v b/theories/rsl_instances.v
similarity index 99%
rename from coq/ra/rsl_instances.v
rename to theories/rsl_instances.v
index 8f3b532e..59bea7cf 100644
--- a/coq/ra/rsl_instances.v
+++ b/theories/rsl_instances.v
@@ -7,8 +7,8 @@ From iris.proofmode Require Import tactics.
 
 Import uPred.
 
-From ra Require Export notation viewpred.
-From ra Require Import rsl fractor persistor na proofmode weakestpre.
+From igps Require Export notation viewpred.
+From igps Require Import rsl fractor persistor na proofmode weakestpre.
 
 Section proof.
 
diff --git a/coq/ra/rsl_sts.v b/theories/rsl_sts.v
similarity index 99%
rename from coq/ra/rsl_sts.v
rename to theories/rsl_sts.v
index 4c538956..572aed9a 100644
--- a/coq/ra/rsl_sts.v
+++ b/theories/rsl_sts.v
@@ -2,8 +2,8 @@ From iris.algebra Require Import sts.
 From iris.base_logic.lib Require Import own.
 From stdpp Require Export gmap.
 
-From ra Require Import types infrastructure.
-From ra.base Require Export ghosts.
+From igps Require Import types infrastructure.
+From igps.base Require Export ghosts.
 
 Implicit Types (I : gset gname) (h: History) (i: gname).
 
diff --git a/coq/ra/tactics.v b/theories/tactics.v
similarity index 99%
rename from coq/ra/tactics.v
rename to theories/tactics.v
index 7d4f6912..84c47f9d 100644
--- a/coq/ra/tactics.v
+++ b/theories/tactics.v
@@ -1,4 +1,4 @@
-From ra Require Export lang.
+From igps Require Export lang.
 From stdpp Require Import fin_maps.
 Import base ra_lang.
 
diff --git a/coq/ra/tests/message_passing.v b/theories/tests/message_passing.v
similarity index 87%
rename from coq/ra/tests/message_passing.v
rename to theories/tests/message_passing.v
index 31e61ee4..1b440aac 100644
--- a/coq/ra/tests/message_passing.v
+++ b/theories/tests/message_passing.v
@@ -1,6 +1,6 @@
-From ra.examples Require Import message_passing unit_token.
-From ra.gps Require Import shared inst_shared.
-From ra Require Import adequacy.
+From igps.examples Require Import message_passing unit_token.
+From igps.gps Require Import shared inst_shared.
+From igps Require Import adequacy.
 
 Let Σ : gFunctors := #[ baseΣ;
                         gpsΣ protocols.boolProtocol _ ;
diff --git a/coq/ra/types.v b/theories/types.v
similarity index 98%
rename from coq/ra/types.v
rename to theories/types.v
index 10276756..0bdeeb54 100644
--- a/coq/ra/types.v
+++ b/theories/types.v
@@ -1,6 +1,6 @@
 From Coq Require Export Utf8.
 From stdpp Require Export gmap finite.
-From ra Require Import infrastructure.
+From igps Require Import infrastructure.
 
 Reserved Notation "'<' x → v @ t , R >" (at level 20, format "< x → v @ t , R >",
                                          x at level 21, v at level 21, t at level 21, R at level 21).
diff --git a/coq/ra/viewpred.v b/theories/viewpred.v
similarity index 99%
rename from coq/ra/viewpred.v
rename to theories/viewpred.v
index 1b899b49..79dad232 100644
--- a/coq/ra/viewpred.v
+++ b/theories/viewpred.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base.
 From iris.base_logic.lib Require Import viewshifts.
 From iris.proofmode Require Import tactics.
-From ra Require Export infrastructure types.
+From igps Require Export infrastructure types.
 
 Canonical Structure View_ofe : ofeT := leibnizC View.
 
diff --git a/coq/ra/weakestpre.v b/theories/weakestpre.v
similarity index 99%
rename from coq/ra/weakestpre.v
rename to theories/weakestpre.v
index 368bf27c..e6a67d88 100644
--- a/coq/ra/weakestpre.v
+++ b/theories/weakestpre.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Import weakestpre.
-From ra Require Import lang viewpred.
-From ra.base Require Import ghosts.
+From igps Require Import lang viewpred.
+From igps.base Require Import ghosts.
 
 (* Section WeakestPre. *)
 (*   Context `{foundationG Σ}. *)
diff --git a/coq/ra/wp_tactics.v b/theories/wp_tactics.v
similarity index 99%
rename from coq/ra/wp_tactics.v
rename to theories/wp_tactics.v
index 8608952d..40d81b81 100644
--- a/coq/ra/wp_tactics.v
+++ b/theories/wp_tactics.v
@@ -1,4 +1,4 @@
-From ra Require Export tactics derived.
+From igps Require Export tactics derived.
 Import uPred.
 
 (** wp-specific helper tactics *)
-- 
GitLab