Proposal
Clicking 'restart file' may have an effect between rebuilding just a few dependencies that were recently changed, and rebuilding all of mathlib. It would be a UX improvement to display this information. See also #693 which would interact with this.
-
User Experience: Clarify how heavy the restart action would be.
-
Beneficiaries: All users of large projects.
-
Maintainability: Likely requires additional code paths.
Community Feedback
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Lake.20UX.20problems/near/586341063
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
Proposal
Clicking 'restart file' may have an effect between rebuilding just a few dependencies that were recently changed, and rebuilding all of mathlib. It would be a UX improvement to display this information. See also #693 which would interact with this.
User Experience: Clarify how heavy the restart action would be.
Beneficiaries: All users of large projects.
Maintainability: Likely requires additional code paths.
Community Feedback
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Lake.20UX.20problems/near/586341063
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.