From dd483d31c60b4d07eae50ddd68ea2e8e324897a0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 7 Oct 2024 11:17:22 +0200
Subject: [PATCH] merge orc11 into gpfsl package to get rid of the diamond
 dependency

---
 _CoqProject                        | 21 ++++++++++-----------
 coq-gpfsl.opam                     |  3 +--
 coq-orc11.opam                     | 17 -----------------
 gpfsl-examples/list_helper.v       |  2 +-
 gpfsl/algebra/lattice_cmra.v       |  2 +-
 gpfsl/gps/block_ends.v             |  2 +-
 gpfsl/gps/protocols.v              |  2 +-
 gpfsl/lang/lang.v                  |  2 +-
 {orc11 => gpfsl/orc11}/base.v      |  0
 {orc11 => gpfsl/orc11}/event.v     |  2 +-
 {orc11 => gpfsl/orc11}/location.v  |  2 +-
 {orc11 => gpfsl/orc11}/mem_order.v |  2 +-
 {orc11 => gpfsl/orc11}/memory.v    |  2 +-
 {orc11 => gpfsl/orc11}/progress.v  |  2 +-
 {orc11 => gpfsl/orc11}/thread.v    |  2 +-
 {orc11 => gpfsl/orc11}/tview.v     |  2 +-
 {orc11 => gpfsl/orc11}/value.v     |  2 +-
 {orc11 => gpfsl/orc11}/view.v      |  2 +-
 18 files changed, 25 insertions(+), 44 deletions(-)
 delete mode 100644 coq-orc11.opam
 rename {orc11 => gpfsl/orc11}/base.v (100%)
 rename {orc11 => gpfsl/orc11}/event.v (91%)
 rename {orc11 => gpfsl/orc11}/location.v (99%)
 rename {orc11 => gpfsl/orc11}/mem_order.v (97%)
 rename {orc11 => gpfsl/orc11}/memory.v (99%)
 rename {orc11 => gpfsl/orc11}/progress.v (99%)
 rename {orc11 => gpfsl/orc11}/thread.v (99%)
 rename {orc11 => gpfsl/orc11}/tview.v (99%)
 rename {orc11 => gpfsl/orc11}/value.v (95%)
 rename {orc11 => gpfsl/orc11}/view.v (99%)

diff --git a/_CoqProject b/_CoqProject
index fd0c5106..7e78b4c4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,5 @@
 # Search paths for all packages. They must all match the regex
 # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
--Q orc11 orc11
 -Q gpfsl gpfsl
 -Q gpfsl-examples gpfsl.examples
 # silence coq_makefile warning
@@ -12,16 +11,16 @@
 -arg -w -arg -redundant-canonical-projection
 
 # ORC11
-orc11/base.v
-orc11/value.v
-orc11/mem_order.v
-orc11/event.v
-orc11/location.v
-orc11/view.v
-orc11/memory.v
-orc11/tview.v
-orc11/thread.v
-orc11/progress.v
+gpfsl/orc11/base.v
+gpfsl/orc11/value.v
+gpfsl/orc11/mem_order.v
+gpfsl/orc11/event.v
+gpfsl/orc11/location.v
+gpfsl/orc11/view.v
+gpfsl/orc11/memory.v
+gpfsl/orc11/tview.v
+gpfsl/orc11/thread.v
+gpfsl/orc11/progress.v
 
 
 # Language Definitions
diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 078bc054..02f1e207 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,8 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2024-10-02.2.636308c8") | (= "dev") }
-  "coq-orc11" {= version}
+  "coq-iris"  { (= "dev.2024-10-03.0.4871f965") | (= "dev") }
 ]
 
 build: ["./make-package" "gpfsl" "-j%{jobs}%"]
diff --git a/coq-orc11.opam b/coq-orc11.opam
deleted file mode 100644
index 8e4ad170..00000000
--- a/coq-orc11.opam
+++ /dev/null
@@ -1,17 +0,0 @@
-opam-version: "2.0"
-maintainer: "Hoang-Hai Dang <haidang@mpi-sws.org>"
-authors: "The ORC11 semantics team"
-license: "BSD-3-Clause"
-homepage: "https://gitlab.mpi-sws.org/iris/orc11"
-bug-reports: "https://gitlab.mpi-sws.org/iris/orc11/issues"
-dev-repo: "git+https://gitlab.mpi-sws.org/iris/orc11.git"
-version: "dev"
-
-synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
-
-depends: [
-  "coq-stdpp" { (= "dev.2024-10-02.0.2dd41ab5") | (= "dev") }
-]
-
-build: ["./make-package" "orc11" "-j%{jobs}%"]
-install: ["./make-package" "orc11" "install"]
diff --git a/gpfsl-examples/list_helper.v b/gpfsl-examples/list_helper.v
index 531280a3..e1f3f49d 100644
--- a/gpfsl-examples/list_helper.v
+++ b/gpfsl-examples/list_helper.v
@@ -1,5 +1,5 @@
 From stdpp Require Import numbers sorting.
-From orc11 Require Import base.
+From gpfsl.orc11 Require Import base.
 
 From stdpp Require Import options.
 
diff --git a/gpfsl/algebra/lattice_cmra.v b/gpfsl/algebra/lattice_cmra.v
index 2d9e4aa7..e8d00bd8 100644
--- a/gpfsl/algebra/lattice_cmra.v
+++ b/gpfsl/algebra/lattice_cmra.v
@@ -1,6 +1,6 @@
 From iris.algebra Require Import cmra auth lib.frac_auth.
 From iris.base_logic.lib Require Import own.
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Require Import iris.prelude.options.
 
diff --git a/gpfsl/gps/block_ends.v b/gpfsl/gps/block_ends.v
index 938ab750..2985ca69 100644
--- a/gpfsl/gps/block_ends.v
+++ b/gpfsl/gps/block_ends.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap.
 From iris.bi Require Import bi big_op.
 
-From orc11 Require Import base.
+From gpfsl.orc11 Require Import base.
 
 Require Import iris.prelude.options.
 
diff --git a/gpfsl/gps/protocols.v b/gpfsl/gps/protocols.v
index 191aab5b..4244ddaa 100644
--- a/gpfsl/gps/protocols.v
+++ b/gpfsl/gps/protocols.v
@@ -1,4 +1,4 @@
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Record protocolT : Type := {
   pr_stateT     :> Type;
diff --git a/gpfsl/lang/lang.v b/gpfsl/lang/lang.v
index c3f5f361..1db41991 100644
--- a/gpfsl/lang/lang.v
+++ b/gpfsl/lang/lang.v
@@ -2,7 +2,7 @@ From stdpp Require Export binders strings.
 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.algebra Require Import ofe.
 
-From orc11 Require Export progress.
+From gpfsl.orc11 Require Export progress.
 
 Require Import iris.prelude.options.
 
diff --git a/orc11/base.v b/gpfsl/orc11/base.v
similarity index 100%
rename from orc11/base.v
rename to gpfsl/orc11/base.v
diff --git a/orc11/event.v b/gpfsl/orc11/event.v
similarity index 91%
rename from orc11/event.v
rename to gpfsl/orc11/event.v
index 16b546e4..6c9fc4a4 100644
--- a/orc11/event.v
+++ b/gpfsl/orc11/event.v
@@ -1,4 +1,4 @@
-From orc11 Require Export value mem_order.
+From gpfsl.orc11 Require Export value mem_order.
 
 Require Import stdpp.options.
 
diff --git a/orc11/location.v b/gpfsl/orc11/location.v
similarity index 99%
rename from orc11/location.v
rename to gpfsl/orc11/location.v
index b814262f..08294a51 100644
--- a/orc11/location.v
+++ b/gpfsl/orc11/location.v
@@ -1,5 +1,5 @@
 From stdpp Require Import sorting.
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Require Import stdpp.options.
 
diff --git a/orc11/mem_order.v b/gpfsl/orc11/mem_order.v
similarity index 97%
rename from orc11/mem_order.v
rename to gpfsl/orc11/mem_order.v
index 9cf20a56..167d4059 100644
--- a/orc11/mem_order.v
+++ b/gpfsl/orc11/mem_order.v
@@ -1,4 +1,4 @@
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Require Import stdpp.options.
 
diff --git a/orc11/memory.v b/gpfsl/orc11/memory.v
similarity index 99%
rename from orc11/memory.v
rename to gpfsl/orc11/memory.v
index e7e75d51..b1b949c5 100644
--- a/orc11/memory.v
+++ b/gpfsl/orc11/memory.v
@@ -1,5 +1,5 @@
 From stdpp Require Export gmap finite tactics sorting.
-From orc11 Require Export view value.
+From gpfsl.orc11 Require Export view value.
 
 Require Import stdpp.options.
 
diff --git a/orc11/progress.v b/gpfsl/orc11/progress.v
similarity index 99%
rename from orc11/progress.v
rename to gpfsl/orc11/progress.v
index 6f4e5e6d..3fc8d359 100644
--- a/orc11/progress.v
+++ b/gpfsl/orc11/progress.v
@@ -1,5 +1,5 @@
 From stdpp Require Import gmap.
-From orc11 Require Export thread.
+From gpfsl.orc11 Require Export thread.
 
 Require Import stdpp.options.
 
diff --git a/orc11/thread.v b/gpfsl/orc11/thread.v
similarity index 99%
rename from orc11/thread.v
rename to gpfsl/orc11/thread.v
index c9409b86..8850d957 100644
--- a/orc11/thread.v
+++ b/gpfsl/orc11/thread.v
@@ -1,5 +1,5 @@
 From stdpp Require Import numbers.
-From orc11 Require Export tview event.
+From gpfsl.orc11 Require Export tview event.
 
 Require Import stdpp.options.
 
diff --git a/orc11/tview.v b/gpfsl/orc11/tview.v
similarity index 99%
rename from orc11/tview.v
rename to gpfsl/orc11/tview.v
index 20c46e34..4e329ceb 100644
--- a/orc11/tview.v
+++ b/gpfsl/orc11/tview.v
@@ -1,5 +1,5 @@
 From stdpp Require Export gmap tactics.
-From orc11 Require Export view memory mem_order.
+From gpfsl.orc11 Require Export view memory mem_order.
 
 Require Import stdpp.options.
 
diff --git a/orc11/value.v b/gpfsl/orc11/value.v
similarity index 95%
rename from orc11/value.v
rename to gpfsl/orc11/value.v
index 0ab62274..fa0596c1 100644
--- a/orc11/value.v
+++ b/gpfsl/orc11/value.v
@@ -1,4 +1,4 @@
-From orc11 Require Export base.
+From gpfsl.orc11 Require Export base.
 
 Require Import stdpp.options.
 
diff --git a/orc11/view.v b/gpfsl/orc11/view.v
similarity index 99%
rename from orc11/view.v
rename to gpfsl/orc11/view.v
index 215c8b5a..d8259f6a 100644
--- a/orc11/view.v
+++ b/gpfsl/orc11/view.v
@@ -1,4 +1,4 @@
-From orc11 Require Export location.
+From gpfsl.orc11 Require Export location.
 
 Require Import stdpp.options.
 
-- 
GitLab