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.

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

post-new-merge delete old stuff megaticket #4989

Open
10 of 17 tasks
mitchellwrosen opened this issue May 20, 2024 · 2 comments
Open
10 of 17 tasks

post-new-merge delete old stuff megaticket #4989

mitchellwrosen opened this issue May 20, 2024 · 2 comments
Assignees

Comments

@mitchellwrosen
Copy link
Member

mitchellwrosen commented May 20, 2024

These commands can probably be deleted:

  • copy.patch
  • delete.patch
  • delete.term-replacement
  • delete.type-replacement
  • diff.namespace.to-patch
  • find.patch
  • merge.old
  • merge.old.preview
  • merge.old.squash
  • move.patch
  • patch
  • replace
  • todo
  • update.old
  • update.old.nopatch
  • update.old.preview
  • view.patch
@aryairani
Copy link
Contributor

I think we can delete all of these other than todo.

todo is meant to be the one-stop shop for orienting the user to what they need to fix up. (link tbd)
e.g. listing name conflicts, missing dependency names, failing merge pre-reqs, dependents of base.todo, and maybe some other stuff, probably including any non-patch-related stuff it may be doing today.

In the first version we can just have it list name conflicts (assuming it does this today) and list missing dependency names.

@mitchellwrosen
Copy link
Member Author

Here is what todo does today:

  1. Gets the set of "edited" (LHS) terms and types from the patch, computes the transitive closure of dependents of those things, and informs you about which ones you might want to fix up first (the "frontier" of that transitive closure, i.e. the nearest dependents to the "edited" set)
  2. Tells you about the conflicted names in the namespace

@mitchellwrosen mitchellwrosen self-assigned this May 28, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants