Skip to content
Snippets Groups Projects

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

Merged 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

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading