Skip to content

Do a clean build of lean-mathlib#267

Open
Yasaswinig7 wants to merge 2 commits into
daanx:masterfrom
Yasaswinig7:cleanbuild-lean-mathlib
Open

Do a clean build of lean-mathlib#267
Yasaswinig7 wants to merge 2 commits into
daanx:masterfrom
Yasaswinig7:cleanbuild-lean-mathlib

Conversation

@Yasaswinig7

@Yasaswinig7 Yasaswinig7 commented Jul 9, 2026

Copy link
Copy Markdown

find . -name '*.olean' -delete;;
The directory (extern/mathlib) does not have any .olean files, hence delete is ineffective.

Before Fix:

$../../bench.sh sys lean lean-mathlib
------------------------------------------------------------------
 test    alloc   time  rss    user  sys  page-faults page-reclaims
leanN       sys   13.05 245660 30.57 0.63 0 60346
mathlib     sys   **01.38** 104656 1.33 0.18 0 44799

After Fix:

$../../bench.sh sys lean lean-mathlib
------------------------------------------------------------------
# test    alloc   time  rss    user  sys  page-faults page-reclaims
leanN       sys   12.98 256568 30.51 0.70 0 63592
mathlib     sys   **13.81** 351104 30.64 1.01 0 154038

Comment thread bench.sh Outdated

@Yasaswinig7 Yasaswinig7 left a comment

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Updated the patch as per the feedback.

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