GitLab

Right now, plainly is part of the BI interface, so every logic has to have this modality. Given that this modality is not at all needed for the proof mode to function, I think that's a bad choice. We already have some rather arbitrary-looking axioms for bi_persistently; let's try to minimize the amount of "strange modalities" in the interface(s) as much as possible.

The following proposals are on the table:

1. Follow !98 (closed) and treat plainly like fupd and bupd: As "standardized extensions" that come with their own separate interface, but once instantiated with proofs of the basic laws are automatically integrated into the proofmode (because a bunch of instances based on this interface already exist).
2. Put plainly into Sbi.
3. Have a new "IrisLikeLogic", extending Sbi, which contains plainly as well as the update modalities.

My own comments:

1. This is the most general and, absent technical concerns, "best" solution -- but handling the resulting hierarchie(s) could become annoying. We'd also have to decide which approach to use for these (bundled/unbundled, typeclasses/canonical structures). (I somehow thought @robbertkrebbers was able to solve all hierarchy problems in Coq as that's what you did so far; hearing even you say that this is getting too complicated is quite unsettling to be honest ;)
2. I see no motivation for doing this, it seems rather arbitrary.
3. seems okay to me -- a little sad, but given the state of affairs probably a reasonable compromise for the time being. We have no example of a logic that would benefit from plainly that doesn't also have the updates.

Ideally I'd prefer 1., but given that if @robbertkrebbers can't get the hierarchy to work, neither will I -- that makes 3. look appealing enough. ;) I don't like 2. at all.