-
Notifications
You must be signed in to change notification settings - Fork 691
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.
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
Remove any remnant of the 'world' file #7746
Conversation
a3f83b8
to
60d7250
Compare
a579205
to
3f3eb53
Compare
Does I'm going to rat you out to v1- users in #6481 so that they protest the change sooner rather than later and we can come up with workarounds, etc. |
Looks good to me: git grep -i world
😢 |
Oh, I forgot to update documentation |
These seem related, don't they?
|
6b5ac29
to
d7e07b3
Compare
lgtm thanks for the clean up |
@fendor: is this ready for review? |
BTW, none of the v1- users is admitting to use |
d7e07b3
to
e46e181
Compare
I tried this PR with our Agda workflows and did not notice any problems. The only difference was that I was alerted of an unknown field |
@Mikolaj Yes it is! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You are right, this looks perfect.
Mergify seems stuck, so let me prod it. |
@Mergifyio rebase |
Stuck again. |
❌ Base branch update has failedNo oauth valid tokens |
@Mergifyio rebase |
❌ Base branch update has failedNo oauth valid tokens |
@fendor: mergifyIO is ded. Could you kindly rebase and manually merge? |
In v1-install, 'world' was used to trace what packages have been installed, and re-install on-demand everything listed in it. However, in v2-install, this is no longer needed and this file leads to code bloat. Additionally, 'world' code-path is probably not up-to-date, remove it instead of having partial features.
e46e181
to
35a6537
Compare
CI acted up again, so let me admin-override the merge. |
@Mikolaj @fendor so I realized a small problem with this pr. in particular, people like me still have old cabal configs that were created when world files existed. So using HEAD of cabal I get warnings like I know how to fix this (update my config) but I think this will be a confusing PITA for cabal users. Can we have a PR to somehow suppress this warning? |
As a general principle, if one removes a component of a language, like the See e.g. the removal of the |
That's a good idea. In particular, we could tell that it's usually just the matter of removing the "world-whatever" line from the config, because almost no users depend on it any more and so no further action is necessary. |
In this case I don't think we should give an error message or warning -- just silently discard. It was added by default in previous cabals and forcing users to all remove it by hand when it was never cared about before will cause friction. |
We could have a warning that only shows with |
In v1-install, 'world' was used to trace what packages have been
installed, and re-install on-demand everything listed in it. However, in
v2-install, this is no longer needed and this file leads to code bloat.
Additionally, 'world' code-path is probably not up-to-date, remove it instead of
having partial features.
closes #6767