Skip to content

feat: improve compilation speed of CreateOp.lean - #1210

Open
math-fehr wants to merge 1 commit into
mainfrom
math-fehr/createOp-faster
Open

feat: improve compilation speed of CreateOp.lean#1210
math-fehr wants to merge 1 commit into
mainfrom
math-fehr/createOp-faster

Conversation

@math-fehr

Copy link
Copy Markdown
Collaborator

This was the slowest file to compile so far. I replaced all grind tactics with manual tactics, using simp_getset to make this more readable.

WIP as I want to split this before merging.

@math-fehr math-fehr self-assigned this Aug 5, 2026
@math-fehr

Copy link
Copy Markdown
Collaborator Author

!radar

@ineol

ineol commented Aug 5, 2026

Copy link
Copy Markdown
Collaborator

Benchmark results for 260501c against 67a1854 are in. There are significant results. @math-fehr

Large changes (13✅, 2🟥)

  • build//instructions: -355.3G (-7.45%)
  • build//task-clock: -47s (-6.45%)
  • build//wall-clock: -29s (-17.70%)
  • build/lakeprof/longest build path//wall-clock: -27s (-16.99%)
  • build/lakeprof/longest rebuild path//wall-clock: -22s (-21.80%)
  • 🟥 build/module/Veir.Analysis//instructions: +28.9M (+1.87%)
  • build/module/Veir.Rewriter.GetSet.CreateOp//instructions: -355.8G (-82.42%)
  • 🟥 build/module/Veir.Rewriter.WfRewriter.GetSetTactic//instructions: +211.0M (+5.63%)
  • build/profile/elaboration//wall-clock: -4s (-18.69%)
  • build/profile/grind ematch//wall-clock: -12s (-23.58%)
  • build/profile/grind mark subsingleton//wall-clock: -3s (-16.42%)
  • build/profile/grind simp//wall-clock: -23s (-19.20%)
  • build/profile/grind//wall-clock: -34s (-18.52%)
  • radar/run/main//time: -29s (-17.36%)
  • radar/run/main/script//time: -29s (-17.61%)

Medium changes (3✅)

  • build/profile/sym canon//wall-clock: -4s (-21.68%)
  • build/profile/sym typeclass inference//wall-clock: -5s (-12.51%)
  • build/profile/typeclass inference//wall-clock: -3s (-14.81%)

Small changes (6✅, 2🟥)

  • 🟥 build/module/Veir.Interpreter.Refinement//instructions: +10.2M (+0.55%)
  • build/module/Veir.Rewriter.GetSet.DetachOp//instructions: -106.9M (-0.33%)
  • 🟥 build/module/Veir.Rewriter.WfRewriter.GetSet//instructions: +214.7M (+0.43%)
  • build/profile/.olean serialization//wall-clock: -953ms (-5.71%)
  • build/profile/attribute application//wall-clock: -526ms (-17.43%)
  • build/profile/grind cutsat//wall-clock: -82ms (-20.53%)
  • build/profile/grind ring//wall-clock: -99ms (-14.65%)
  • build/profile/type checking//wall-clock: -3s (-6.70%)

@math-fehr
math-fehr force-pushed the math-fehr/createOp-faster branch 2 times, most recently from cba4975 to 866a198 Compare August 6, 2026 00:36
@math-fehr
math-fehr changed the base branch from main to math-fehr/simp-getset-rewriter August 6, 2026 00:36
@math-fehr
math-fehr marked this pull request as ready for review August 6, 2026 00:36
@math-fehr math-fehr changed the title WIP: improve compilation speed of CreateOp.lean feat: improve compilation speed of CreateOp.lean Aug 6, 2026
@math-fehr
math-fehr force-pushed the math-fehr/simp-getset-rewriter branch from 57ad749 to 9b11d50 Compare August 7, 2026 17:42
@math-fehr
math-fehr force-pushed the math-fehr/createOp-faster branch from 866a198 to 8648515 Compare August 7, 2026 17:42
Base automatically changed from math-fehr/simp-getset-rewriter to main August 7, 2026 18:06
@math-fehr
math-fehr force-pushed the math-fehr/createOp-faster branch from 8648515 to 2231949 Compare August 9, 2026 07:47
@math-fehr

Copy link
Copy Markdown
Collaborator Author

@tobiasgrosser @ineol, could one of you review this?

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.

2 participants