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.
Edited by Janno
Merge request reports
Activity
Please register or sign in to reply