From d9360cdedc6a36cbd8765977a1ef5c191cade155 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 2 Aug 2022 12:41:58 -0400
Subject: [PATCH] rename staging to unstable
---
CHANGELOG.md | 4 ++++
Makefile.coq.local | 2 +-
_CoqProject | 12 ++++++------
coq-iris-staging.opam => coq-iris-unstable.opam | 4 ++--
{iris_staging => iris_unstable}/.keep | 0
{iris_staging => iris_unstable}/algebra/list.v | 0
{iris_staging => iris_unstable}/algebra/monotone.v | 0
{iris_staging => iris_unstable}/base_logic/algebra.v | 2 +-
.../base_logic/mono_list.v | 0
.../heap_lang/interpreter.v | 0
tests/heap_lang_interpreter.v | 2 +-
11 files changed, 15 insertions(+), 11 deletions(-)
rename coq-iris-staging.opam => coq-iris-unstable.opam (83%)
rename {iris_staging => iris_unstable}/.keep (100%)
rename {iris_staging => iris_unstable}/algebra/list.v (100%)
rename {iris_staging => iris_unstable}/algebra/monotone.v (100%)
rename {iris_staging => iris_unstable}/base_logic/algebra.v (94%)
rename {iris_staging => iris_unstable}/base_logic/mono_list.v (100%)
rename {iris_staging => iris_unstable}/heap_lang/interpreter.v (100%)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 89bc4ab23..bacea5391 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,8 @@ lemma.
affects `envs_entails_eq`, which is commonly used in the definition of
custom proof mode tactics. All other unsealing lemmas should be internal, so
in principle you should not rely on them.
+- Rename `coq-iris-staging` package to `coq-iris-unstable`, and also change the
+ import path from `iris.staging` to `iris.unstable`.
**Changes in `algebra`:**
@@ -138,6 +140,8 @@ sed -i -E -f- $(find theories -name "*.v") <<EOF
# excl_auth
s/\bexcl_auth_frag_validN_op_1_l\b/excl_auth_frag_op_validN/g
s/\bexcl_auth_frag_valid_op_1_l\b/excl_auth_frag_op_valid/g
+# staging → unstable
+s/\biris\.staging\b/iris.unstable/g
EOF
```
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 5a8ffd47d..136633147 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -15,7 +15,7 @@ style: $(VFILES) coq-lint.sh
./coq-lint.sh "$$FILE" || exit 1; \
done
# Make sure main Iris does not import other Iris packages.
- $(HIDE)if egrep 'iris\.(heap_lang|deprecated|staging)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
+ $(HIDE)if egrep 'iris\.(heap_lang|deprecated|unstable)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
.PHONY: style
# the test suite
diff --git a/_CoqProject b/_CoqProject
index a159af6bd..c04296734 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,7 +8,7 @@
-Q iris/base_logic iris.base_logic
-Q iris/program_logic iris.program_logic
-Q iris_heap_lang iris.heap_lang
--Q iris_staging iris.staging
+-Q iris_unstable iris.unstable
-Q iris_deprecated iris.deprecated
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
@@ -175,11 +175,11 @@ iris_heap_lang/lib/diverge.v
iris_heap_lang/lib/arith.v
iris_heap_lang/lib/array.v
-iris_staging/algebra/list.v
-iris_staging/base_logic/algebra.v
-iris_staging/base_logic/mono_list.v
-iris_staging/heap_lang/interpreter.v
-iris_staging/algebra/monotone.v
+iris_unstable/algebra/list.v
+iris_unstable/base_logic/algebra.v
+iris_unstable/base_logic/mono_list.v
+iris_unstable/heap_lang/interpreter.v
+iris_unstable/algebra/monotone.v
iris_deprecated/base_logic/auth.v
iris_deprecated/base_logic/sts.v
diff --git a/coq-iris-staging.opam b/coq-iris-unstable.opam
similarity index 83%
rename from coq-iris-staging.opam
rename to coq-iris-unstable.opam
index 6be6d4d66..4d77aa566 100644
--- a/coq-iris-staging.opam
+++ b/coq-iris-unstable.opam
@@ -18,5 +18,5 @@ depends: [
"coq-iris-heap-lang" {= version}
]
-build: ["./make-package" "iris_staging" "-j%{jobs}%"]
-install: ["./make-package" "iris_staging" "install"]
+build: ["./make-package" "iris_unstable" "-j%{jobs}%"]
+install: ["./make-package" "iris_unstable" "install"]
diff --git a/iris_staging/.keep b/iris_unstable/.keep
similarity index 100%
rename from iris_staging/.keep
rename to iris_unstable/.keep
diff --git a/iris_staging/algebra/list.v b/iris_unstable/algebra/list.v
similarity index 100%
rename from iris_staging/algebra/list.v
rename to iris_unstable/algebra/list.v
diff --git a/iris_staging/algebra/monotone.v b/iris_unstable/algebra/monotone.v
similarity index 100%
rename from iris_staging/algebra/monotone.v
rename to iris_unstable/algebra/monotone.v
diff --git a/iris_staging/base_logic/algebra.v b/iris_unstable/base_logic/algebra.v
similarity index 94%
rename from iris_staging/base_logic/algebra.v
rename to iris_unstable/base_logic/algebra.v
index ba0d2844e..511d95f55 100644
--- a/iris_staging/base_logic/algebra.v
+++ b/iris_unstable/base_logic/algebra.v
@@ -1,7 +1,7 @@
(* This is just an integration file for [iris_staging.algebra.list];
both should be stabilized together. *)
From iris.algebra Require Import cmra.
-From iris.staging.algebra Require Import list monotone.
+From iris.unstable.algebra Require Import list monotone.
From iris.base_logic Require Import bi derived.
From iris.prelude Require Import options.
diff --git a/iris_staging/base_logic/mono_list.v b/iris_unstable/base_logic/mono_list.v
similarity index 100%
rename from iris_staging/base_logic/mono_list.v
rename to iris_unstable/base_logic/mono_list.v
diff --git a/iris_staging/heap_lang/interpreter.v b/iris_unstable/heap_lang/interpreter.v
similarity index 100%
rename from iris_staging/heap_lang/interpreter.v
rename to iris_unstable/heap_lang/interpreter.v
diff --git a/tests/heap_lang_interpreter.v b/tests/heap_lang_interpreter.v
index de12d0ae2..bc91eac9d 100644
--- a/tests/heap_lang_interpreter.v
+++ b/tests/heap_lang_interpreter.v
@@ -1,5 +1,5 @@
From iris.heap_lang Require Import notation.
-From iris.staging.heap_lang Require Import interpreter.
+From iris.unstable.heap_lang Require Import interpreter.
Example test_1 :
exec 1000 ((λ: "x", "x" + #1) #2) = inl #3.
--
GitLab