Skip to content
Snippets Groups Projects
Commit d9360cde authored by Ralf Jung's avatar Ralf Jung
Browse files

rename staging to unstable

parent 537d052b
No related branches found
No related tags found
No related merge requests found
......@@ -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
```
......
......@@ -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
......
......@@ -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
......
......@@ -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"]
File moved
File moved
File moved
(* 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.
......
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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment