WIP: unfold typeclass opaque definitions in proof mode

added 36 commits

• 919e19e2...71abda4d - 34 commits from branch master
• bb060202 - use a separate Db for proofmode classes
• 1efa2efe - use the 'separate Db' approach for all proofmode classes except for framing

Compare with previous version

added 1 commit

• 8938309e - use the 'separate Db' approach for all proofmode classes except for framing

Compare with previous version

Is this still needed? Isn't there currently less need for making auxiliary definitions type class opaque since we have:

• fixed some exponential blowups in type class search (c.f. 766dbcd2)
• fixed iNext to not unfold definitions (c.f. 5241c33d and #55 (closed))

As far as I know, things still get much slower if you don't make your definitions typeclasses opaque. Framing goes down very far into the term without making any progress. We can easily test this in lambda Rust.

Actually, no need to go so far -- Iris itself contains tons of "Typeclasses Opaque"

Hm, indeed https://gitlab.mpi-sws.org/FP/iris-coq/commit/e6aeb885abf7f636949e7b148ae6898ce9ca89e2 doesn't change the timing. I will test lambaRust tmr.

FWIW, in order to improve performance it may be a good idea to seal off the lifetime logic instead of making definitions type class opaque. As we have seen with many widely used definitions in iris (like fancy updates, weakestpre, invariants) this may give quite a speed-up because it avoids Coq's unification from looking through definitions. Note that unification does not happen only during type class search, but in many other cases (like when applying a lemma, rewriting, and so on).

In the lifetime logic, removing the typeclasses opaque leads to a diverging proof in primitive.v... see https://gitlab.mpi-sws.org/FP/LambdaRust-coq/tree/no-opaque

We may want to seal off the definitions that are actually exported, but I wouldn't want to also do that for all the intermediate definitions.

Btw, I recall @janno also made definitions typeclass opaque in GPS to improve performance. If you could at some point try whether that's still necessary with latest Iris, that would be appreciated.

We may want to seal off the definitions that are actually exported, but I wouldn't want to also do that for all the intermediate definitions.

Agreed. Ideally we should neither seal intermediate definitions off, nor make them type class opaque.

I will look into the diverging proof later today.

mentioned in issue #76 (closed)

mentioned in merge request !67 (merged)

closed