iFrame: Do not call `cbv` on user terms in contexts

I cannot believe these cbv calls survived for a such a long time!

I didn't find this due to the performance issues of calling cbv on user terms, oddly enough. I was investigating why relatively small proofs were taking upwards of 10GB of memory (with pretty permissive GC parameters).

Here's the change as reported by memtrace on a small file with a total of 6 iFrame calls throughout the proof. All calls are on pretty a small goals with <20 total premises but I guess the terms involved are not exactly trivial when fully normalized.

Before:

After:

The file also went from 1min to less than 45s.

changed the description

(I cannot edit the MR any more because it has been recognized as spam. Who am I to judge? Either way, the timings in the description are incorrect: the proof originally took a little more than a minute, not 1min 15s)

changed the description

@jung could you run a performance test? I am satisfied with the change as far as our code base is concerned. We don't really use iFrame at all but this change still got us a ~2 minute overall improvement and it really cut down on memory usage.

FWIW here's a list of all eval cbv in the repo before this MR:

iris/proofmode/ltac_tactics.v
157:  | [] => eval cbv in Hs
413:     let Hs := eval cbv in (env_dom (env_intuitionistic Δ)) in go Hs
422:     let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
888:       let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
1019:       let b := eval cbv [use_tac_specialize_intuitionistic_helper] in

iris/proofmode/ident_name.v
12:  eval cbv in (ltac:(clear; intros id; assumption) : unit → unit).

iris/proofmode/intro_patterns.v
182:  | intro_pat => eval cbv in (intro_pat_intuitionistic p)
183:  | list intro_pat => eval cbv in (forallb intro_pat_intuitionistic p)
186:     eval cbv in (forallb intro_pat_intuitionistic pat)

added 68 commits

• 8178efc8...8890e30a - 66 commits from branch iris:master
• 2fb6f61d - iFrame: Do not call `cbv` on user terms in contexts
• 088230ae - Turn two more uses of `cbv` into `lazy` that involve user terms.

Compare with previous version

I added documentation, please provide feedback.

added 1 commit

• 3cb7cf4b - Documentation.

Compare with previous version

added 1 commit

• 01656761 - Documentation.

Compare with previous version

added 24 commits

• 01656761...f11d6aab - 20 commits from branch iris:master
• 45b4a2d2 - iFrame: Do not call `cbv` on user terms in contexts
• 3e55344c - Turn two more uses of `cbv` into `lazy` that involve user terms.
• 77fd4c86 - Documentation.
• 6cbce385 - More documentation.

Compare with previous version

added 1 commit

• fd54023a - More documentation.

Compare with previous version

added 1 commit

• 13aa09a8 - More documentation.

Compare with previous version

resolved all threads

LGTM, thanks!

mentioned in commit 657b34ad

merged

@iris-users This is not a breaking change, but if you are writing your own Proof Mode tactics, you might want to check the new documentation in proofmode/reduction.v to see if you are using the reduction tactics correctly.