8000 Record UnifyIndices bench cost under Coverage by AndrasKovacs · Pull Request #6921 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Record UnifyIndices bench cost under Coverage #6921

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Oct 24, 2023
Merged

Record UnifyIndices bench cost under Coverage #6921

merged 1 commit into from
Oct 24, 2023

Conversation

AndrasKovacs
Copy link
Contributor

There was a call to unifyIndices' in Coverage which was not covered by the UnifyIndices benchmark account. This is now recorded. The new numbers:

Coverage                   25,586ms  (47,278ms)
Coverage.UnifyIndices      21,691ms

@AndrasKovacs
Record UnifyIndices bench cost under Coverage
ce1a7ff 
There was a call to unifyIndices' in Coverage which was not covered by the
UnifyIndices benchmark account. This is now recorded. The new numbers:

Coverage                          25,586ms  (47,278ms)
Coverage.UnifyIndices             21,691ms
@jespercockx
Copy link
Member

Oh no, all my horribly inefficient code for unifying indices of which I assumed that it did not impact the overall performance of Agda will now be exposed..

@AndrasKovacs
Copy link
Contributor Author
AndrasKovacs commented Oct 16, 2023 •
edited
Loading

@jespercockx Indeed, now it's the most expensive single account for the stdlib at 43s out of 326s total on my machine. I have a decent picture about the issues in LHS.Unify. I can talk about them next week. I'll probably work on that after I'm finished with the serialization.

@andreasabel andreasabel added performance Slow type checking, interaction, compilation or execution of Agda programs debug Concerning debug printing (not in changelog) labels Oct 24, 2023
@andreasabel andreasabel added this to the 2.6.4.1 milestone Oct 24, 2023
@andreasabel andreasabel self-assigned this Oct 24, 2023
@andreasabel andreasabel merged commit 08b79a6 into master Oct 24, 2023
@andreasabel andreasabel deleted the coverage-lhsunify-bench branch October 24, 2023 09:56
@AndrasKovacs
8000 Copy link
Contributor Author

What was the deal with the failing test? I did not understand it and just left it there for the time being.

@andreasabel
Copy link
Member

What was the deal with the failing test? I did not understand it and just left it there for the time being.

A common fluke. Haven't gotten to the bottom of it yet. Also have not tried seriously to do so.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@andreasabel andreasabel

Labels
debug Concerning debug printing (not in changelog) performance Slow type checking, interaction, compilation or execution of Agda programs
Projects
None yet
Milestone
2.6.4.1
Development

Successfully merging this pull request may close these issues.
3 participants
@AndrasKovacs @jespercockx @andreasabel
0