Mark gset methods as simpl never to stop `cbn` from unfolding them

This clarifies what's meant to happen anyway, and is apparently needed for cbn. (I haven't yet tried doing this at the mapset level).

Example of the problem: without this change, cbn mangles the goal in the following:

  Goal {[1; 2; 3]} =@{gset nat} ∅.
  Fail progress simpl.
  progress cbn. Show.

I'd want progress cbn to fail, instead the above gives:

The command has indeed failed with message:
Failed to progress.
1 subgoal
  
  ============================
  {| mapset_car := {[1 := ()]} ∪ {[2 := ()]} ∪ {[3 := ()]} |} = ∅

It seems fine to me to make more definitions simpl never, but why does it make sense to do that proof proofs (e.g., gset_leibniz) too?

added 2 commits

• 28f6991d - gmap.v: reorder gset instances
• 0ac53934 - Mark gset methods as simpl never

Compare with previous version

resolved all threads

How about adding a test case so that we don't break this in the future? How about also adding the same test case for simpl?

(While we don't use cbn in std++, I am all in favor of improving support for cbn as long as that does not affect simpl. Thus using cbn in test cases would be perfectly fine.)

added S-waiting-for-author label

added 65 commits

• 0ac53934...c4a352b1 - 63 commits from branch iris:master
• eeb2ebd6 - gmap.v: reorder gset instances
• 38547507 - Mark gset methods as simpl never and add test

Compare with previous version

added 1 commit

• 1dbfdf20 - Mark gset methods as simpl never and add test

Compare with previous version

LGTM. Should we have a CHANGELOG entry here?

added 1 commit

• dc91e447 - Mark gset methods as simpl never and add test

Compare with previous version

Added a few Fail progress simpl/cbn tests; they should cover everything, including decidable operations (with at least one case).

FWIW, on these tests I only need the following — but I don't think reduction ever helps on gset so I'd stick to the current settings.

  Global Arguments gset_singleton : simpl never.
  Global Arguments gset_union : simpl never.
  Global Arguments gset_difference : simpl nomatch.

added 1 commit

• 64ae66ab - Candidate changelog

Compare with previous version

added 1 commit

• 8e0f82b0 - Changelog

Compare with previous version

Added a candidate changelog.

Changelog looks good! Feel free to add an attribution. (We usually try to do that for things not coming from Robbert or me.)

LGTM. I agree with what Ralf said about attribution.

added 1 commit

• 1ecabad2 - Changelog

Compare with previous version

resolved all threads

mentioned in commit ac04787b

merged

Merging, and thanks!

It looks like this MR was merged without having CI run on it? It introduced a regression on Coq 8.10.

@robbertkrebbers before merging, please make sure there is an explicit green CI status. When there is no CI status, it means CI didn't run for some reason that we should investigate.

In this case, @Blaisorblade's fork had CI disabled.

Because the MR was because the time it was enabled by default?

No, because Paolo's fork is ancient and back then CI on forks was acting up.

Old MRs would also be a problem, but I don't think we'll get more of those since people generally base their MR on something close to current master.

So, iris!616 (closed) is the only MR without pipeline status.

But old forks can keep haunting us for a bit, since those don't automatically fix themselves -- I need to use my admin powers to fix the fork configuration (or the user needs to do it themselves).

I'm sorry for the trouble and thanks for the fix in 653c819a!