Commit 13f38761 authored by Ralf Jung's avatar Ralf Jung

CHANGELOG: mention the moving-things-around

parent a6921bfd
Pipeline #2920 passed with stage
in 9 minutes and 58 seconds
...@@ -3,14 +3,15 @@ way the logic is used on paper. We also mention some significant changes in the ...@@ -3,14 +3,15 @@ way the logic is used on paper. We also mention some significant changes in the
Coq development, but not every API-breaking change is listed. Changes marked Coq development, but not every API-breaking change is listed. Changes marked
`[#]` still need to be ported to the Iris Documentation LaTeX file(s). `[#]` still need to be ported to the Iris Documentation LaTeX file(s).
## Iris 3.0~rc1 ## Iris 3.0 (unfinished)
This version matches the ESOP submission.
* View shifts are radically simplified to just internalize frame-preserving * View shifts are radically simplified to just internalize frame-preserving
updates. Weakestpre is defined inside the logic, and invariants and view updates. Weakestpre is defined inside the logic, and invariants and view
shifts with masks are also coded up inside Iris. Adequacy of weakestpre shifts with masks are also coded up inside Iris. Adequacy of weakestpre
is proven in the logic. is proven in the logic.
* Renaming and moving things around: uPred and the rest of the base logic are
in [base_logic], while [program_logic] is for everything involving the
general Iris notion of a language.
* With invariants and the physical state being handled in the logic, there * With invariants and the physical state being handled in the logic, there
is no longer any reason to demand the CMRA unit to be discrete. is no longer any reason to demand the CMRA unit to be discrete.
* The language can now fork off multiple threads at once. * The language can now fork off multiple threads at once.
......
Markdown is supported
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