Topic: This is about general proof style concerns

Topic: concerns the siProp type and logic

Topic: better support for record-like invariants in the Iris Proof Mode

Topic: Bugs related to the proofmode and our tactic support in general

Topic: concerns the Iris program logic

Topic: concerns logical atomicity

Topic: this concerns specifically linear (non-affine) insteances of the proofmode

Topic: Bugs related to HeapLang

Topic: This concerns out general (S)BI interfaces

Topic: This concerns the Iris Base Logic

Topic: concerns resource algebras

Status: someone is assigned at should look at this

Status: waiting for the MR author to do something

Status: nominated for discussion at the next meeting

Status: this is a draft MR; more work by the author and/or reviewer is needed to fully flesh out its design

Status: issue is blocked by a Coq improvement or bugfix

This issue/MR is blocked on resolving some other issue or merging another MR

Impact: this is related to performance concerns

A good issue for a first contribution to Iris

Should be added to the changelog of the next release