Commit b0708b01 authored by Ralf Jung's avatar Ralf Jung
Browse files

fixup changelog

parent 8024a5d8
......@@ -17,22 +17,6 @@ lemma.
* Add `ghost_map`, a logic-level library for a `gmap K V` with an authoritative
view and per-element points-to facts written `k ↪[γ] w`.
The following `sed` script helps adjust your code to the renaming (on macOS,
replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
```
sed -i -E -f- $(find theories -name "*.v") <<EOF
# auth and view renames from frac to dfrac
s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
EOF
```
**Changes in `base_logic`:**
* Generalize the soundness lemma of the base logic `step_fupdN_soundness`.
It applies even if invariants stay open accross an arbitrary number of laters.
......@@ -42,7 +26,6 @@ EOF
(i.e., logical steps) for each physical step of the operational semantics,
depending on the number of physical steps executed since the begining of the
execution of the program. See merge request [!595](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595).
This implies several API-breaking changes, which can be easily fixed in client
formalizations in a backward compatible manner as follows:
- Ignore the new parameter `ns` in the state interpretation, which
......@@ -53,6 +36,19 @@ EOF
- Some proofs using lifting lemmas and adequacy theorems need to be adapted
to ignore the new step counter.
The following `sed` script helps adjust your code to the renaming (on macOS,
replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Note that the script is not idempotent, do not run it twice.
```
sed -i -E -f- $(find theories -name "*.v") <<EOF
# auth and view renames from frac to dfrac
s/\b(auth|view)_(auth|both|update)_frac_(is_op|op_invN|op_inv|inv_L|validN|op_validN|valid|op_valid|valid_2|valid_discrete|includedN|included|alloc|validI|validI_2|validI_1|validI|)\b/\1_\2_dfrac_\3/g
s/\bgset_bij_auth_frac_(\w*)\b/gset_bij_auth_dfrac_\1/g
s/\bgset_bij_auth_empty_frac_valid\b/gset_bij_auth_empty_dfrac_valid/g
s/\bbij_both_frac_valid\b/bij_both_dfrac_valid/g
EOF
```
## Iris 3.4.0
The highlights and most notable changes of this release are as follows:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment