Enable cumulativity for telescopes

This fixes iris#461 (closed) by enabling cumulative universe polymorphism in telescopes.v, allowing tele at a fixed universe (such as the Quant universe in iris) to cumulatively contain telescopes at smaller universes.

I also re-arranged existing telescope tests slightly in order to make sure the test for Unset Universe Minimization ToSet has a chance to fail before the accessor test, which happens to fail for the same reason.

changed the description

mentioned in merge request iris!798 (merged)

LGTM modulo nit. Thanks for sorting this out.

added 2 commits

• 6d64bcb5 - Enable cumulativity for telescopes.
• 8eb17fc8 - Move `Universe Minimization ToSet` test case higher.

Compare with previous version

added 1 commit

• b0065fea - Move universe-related telescope tests closer together.

Compare with previous version

resolved all threads

merged

mentioned in commit 411eb445

In Iris itself, this caused an up to 1% slowdown in the files using logical atomicity: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1652721322297&to=1652746550563&var-metric=instructions&var-project=iris&var-branch=master&var-config=All&var-group=(.*)

Doesn't look like a coincidence. Those are all rather quick files though.

That's worse than I expected especially given how simple the uses in iris itself are. I hope the fix for https://github.com/coq/coq/issues/11741 also addresses this slowdown.

In examples it is still measurable on a per-file basis, but drowns in larger files: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=examples&var-branch1=master&var-commit1=69556864a2cbe2dab37d1589f17cdff2bccd7cd9&var-config1=build-coq.8.15.0&var-branch2=master&var-commit2=b3edc7adc87ea1074db10e3bf5f03f87d23672eb&var-config2=build-coq.8.15.0&var-metric=instructions&var-group=(.*).

Same for GPFSL: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=gpfsl&var-branch1=master&var-commit1=ca1ae832e0b53ae56a906ff27bf0f697670689b8&var-config1=build-coq.8.15.1&var-branch2=master&var-commit2=dd966699f4d033b22598b29131a72477df2b5907&var-config2=build-coq.8.15.1&var-metric=instructions&var-group=(.*)

iron, lambda-rust don't use atomic triples so as expected they are unaffected.

Actris also uses telescopes extensively. Do we have timings for that?

No, actris isn't on timing CI.

It used to be, until around 2 years ago. I guess we can add it back, though I am a bit worried about overloading our timing job. (We can only run one timing job in parallel.)

Actris seems to be barely affected: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=actris&var-branch1=master&var-commit1=5778d3353d52a752fdb87af98bdeab4a9fb27aac&var-config1=build-coq.8.15.1&var-branch2=master&var-commit2=788086ddebec9e788ecdd01ff224c17a74d9cfff&var-config2=build-coq.8.15.1&var-metric=instructions&var-group=(.*)

Thanks for the timings, Ralf.

I am not worried about these numbers: it only has a small affect, for very specific cases, and the repair of a Coq bug might fix it in the future.

Just to clarify, the bugfix was merged in master in question was merged in master: https://github.com/coq/coq/pull/15662.