Skip to content
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

Preformance enhancement for large projects: Avoid recomputing SourceToModule maps #6145

Closed
nad opened this issue Sep 29, 2022 · 4 comments · Fixed by #6183
Closed

Preformance enhancement for large projects: Avoid recomputing SourceToModule maps #6145

nad opened this issue Sep 29, 2022 · 4 comments · Fixed by #6183
Assignees
@nad
Labels
not-in-changelog This issue should not be listed in the changelog. performance Slow type checking, interaction, compilation or execution of Agda programs type: enhancement Issues and pull requests about possible improvements
Milestone
2.6.3

Comments

@nad
Copy link
Contributor

nad commented Sep 29, 2022

The computation sourceToModule is used in generateAndPrintSyntaxInfo, which is used repeatedly:

agda/src/full/Agda/TypeChecking/Monad/Base.hs

Lines 876 to 883 in 82b2b0f

-- | Creates a 'SourceToModule' map based on 'stModuleToSource'.
--
-- O(n log n).
--
-- For a single reverse lookup in 'stModuleToSource',
-- rather use 'lookupModuleFromSourse'.
sourceToModule :: TCM SourceToModule

For large developments this could have a non-trivial cost.
@nad nad added type: enhancement Issues and pull requests about possible improvements performance Slow type checking, interaction, compilation or execution of Agda programs labels Sep 29, 2022
@nad nad added this to the 2.6.4 milestone Sep 29, 2022
@nad nad self-assigned this Oct 12, 2022
@nad nad modified the milestones: 2.6.4, 2.6.3 Oct 12, 2022
nad added a commit that referenced this issue Oct 12, 2022
@nad
[ #6145, #6146 ] Removed SourceToModule.
49dd1d9 
Furthermore canonicalizeAbsolutePath is no longer used in the
serialiser.
@nad nad mentioned this issue Oct 12, 2022
Merged
nad added a commit that referenced this issue Oct 12, 2022
@nad
[ #6145, #6146 ] Removed SourceToModule.
1210b68 
Furthermore canonicalizeAbsolutePath is no longer used in the
serialiser.
nad added a commit that referenced this issue Oct 12, 2022
@nad
[ #6145, #6146 ] Removed SourceToModule.
c2cb1e7 
Furthermore canonicalizeAbsolutePath is no longer used in the
serialiser.
nad added a commit that referenced this issue Oct 14, 2022
@nad
[ #6145, #6146 ] Removed SourceToModule.
0d1b53d 
Furthermore canonicalizeAbsolutePath is no longer used in the
serialiser.
@nad nad closed this as completed in #6183 Oct 14, 2022
@nad
Copy link
Contributor Author

nad commented Oct 14, 2022

Fixed by the removal of SourceToModule.

@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
@andreasabel andreasabel changed the title Avoid recomputing SourceToModule maps Preformance enhancement for large projects: Avoid recomputing SourceToModule maps Oct 24, 2022
@nad
Copy link
Contributor Author

nad commented Oct 25, 2022

@andreasabel, have you verified that this particular change is a performance enhancement? The numbers that I presented (#6183) related to several changes.

@andreasabel
Copy link
Member

@andreasabel, have you verified that this particular change is a performance enhancement? The numbers that I presented (#6183) related to several changes.

No, but the alternative is to not mention this in the changelog at all. After all, it is an internal refactoring, which should be mentioned if it had performance benefits.

@nad
Copy link
Contributor Author

nad commented Oct 25, 2022

I don't think this should be mentioned in the changelog without any evidence that it makes a difference.

@nad nad added the not-in-changelog This issue should not be listed in the changelog. label Oct 25, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@nad nad

Labels
not-in-changelog This issue should not be listed in the changelog. performance Slow type checking, interaction, compilation or execution of Agda programs type: enhancement Issues and pull requests about possible improvements
Projects
None yet
Milestone
2.6.3
2 participants
@nad @andreasabel