Skip to content

Memoise mk_prec_matrix - #2063

Merged
mn200 merged 3 commits into
HOL-Theorem-Prover:developfrom
mrichards30:memo-parsing
Oct 1, 2026
Merged

mn200 merged 3 commits into
HOL-Theorem-Prover:developfrom
mrichards30:memo-parsing

Conversation

@mrichards30

Copy link
Copy Markdown
Contributor

Hi, I was playing around with some vibe coded profiling/flame graph tools I got Claude to put into my copy of PolyML, and found a few places when building theories that seem pretty straight forward to optimise. The first of them is that building the precedence matrix for the term parser in mk_prec_matrix shows up a surprising amount in the flame graph.

image

Here, mk_prec_matrix is in pink and it's showing as 11.4% of the build.

So it seems like the precedence matrix is being rebuilt a bit more often than it needs to. In this PR I've memoised it so it only re-computes when grammar rules and "specials" are changed (the only two fields mk_prec_matrix reads). This is cutting my build time (building kernel, core_theories, and more_theories) from an average of 957s to 876s.

After the change the flame graph shows mk_prec_matrix having gone down to 2.1% (still in pink).

image

@mrichards30
mrichards30 requested a review from mn200 September 15, 2026 12:14
@ordinarymath

Copy link
Copy Markdown
Contributor

Can this be done by having the partial application not become stale for useless updates like defining a constant instead?

@mn200

mn200 commented Sep 16, 2026

Copy link
Copy Markdown
Member

I think I'd prefer a world where the matrix is stored in the grammar as an option ref value. If :

  1. a new grammar is calculated from an old one,
  2. the change is one that won't require a recalculation, and
  3. there is a matrix already associated with the old grammar,

then the new grammar's pointer can point to the old matrix. Otherwise, the new grammar either gets a fresh pointer with NONE in it (change requires a recalculation), or the new grammar gets to copy the pointer.

Subsequently, the parse_term function's call to mk_prec_matrix looks at that reference and either uses what's there, or calculates it once.

If the rest of parse_term's prefix was super-quick (doubtful), this would also remove the need for the current code in Parse to track whether or not the grammar has been changed.

@mrichards30

Copy link
Copy Markdown
Contributor Author

@mn200 sorry this one took so long I've updated the PR

@mn200

mn200 commented Sep 30, 2026

Copy link
Copy Markdown
Member

Thanks! Do you have a cool new flame graph demonstrating an improvement?

@mrichards30

Copy link
Copy Markdown
Contributor Author

Thanks! Do you have a cool new flame graph demonstrating an improvement?

yep! re-recording on the new branch has taken my average from 966 to 869 seconds
and the new flame graph:
image

@mn200
mn200 merged commit 950081b into HOL-Theorem-Prover:develop Oct 1, 2026
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants