Skip to content

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

Janno requested to merge janno/iris:janno/iframe-cbv into master

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:

image

After:

image

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

Edited by Janno

Merge request reports