8000 Fix #6931: dead code: include module telescopes in reachability analysis by andreasabel · Pull Request #6932 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Fix #6931: dead code: include module telescopes in reachability analysis #6932

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 5 commits into from
Oct 20, 2023
Merged

Fix #6931: dead code: include module telescopes in reachability analysis #6932

merged 5 commits into from
Oct 20, 2023

Conversation

andreasabel
Copy link
Member

@andreasabel
Cosmetics: use er for erasure instead of e (which is usually an `…
79a2907 
…Expr`)
@andreasabel
Extra debug printing for #6931
f3a37d0
@andreasabel
Fix showQNameId to not use the show function of List1
30b1f07 
Because
`M.B4 :| [6]@ModuleNameHash 8387913242270124987`
is much worse to read than
`M.B[4,6]@ModuleNameHash 8387913242270124987`.
@andreasabel andreasabel added this to the 2.6.4.1 milestone Oct 19, 2023
@andreasabel andreasabel added the dead-code Concerning the dead-code removal optimization label Oct 19, 2023
@andreasabel
Fix #6931: dead code: include module telescopes in reachability analysis
d12ad84 
If you had an empty public module, the dead code analysis would not
consider names in the parameter telescope as used.

This is rectified by this commit, which includes the public module
telescopes as roots in the reachability analysis.
@andreasabel
CI: disable size-solver-test because it rebuilds Agda
be28b6e
@andreasabel andreasabel mentioned this pull request Oct 19, 2023
Closed
@andreasabel andreasabel self-assigned this Oct 20, 2023
@andreasabel andreasabel merged commit be28b6e into master Oct 20, 2023
@andreasabel andreasabel deleted the debug-Oskar branch October 20, 2023 05:04
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
dead-code Concerning the dead-code removal optimization
Projects
None yet
Milestone
2.6.4.1
Development

Successfully merging this pull request may close these issues.

Internal error with an empty parametrized module from a different file
1 participant
@andreasabel
0