Motivation
This project looks very interesting and I am curious, if "universal undo" could be used for incremental verification (or other incremental program related executions like static/dynamic analysis or faster interactive proof inputs) by tracking all editor changes between user-specified snapshots to at least estimate or ideally compute the semantic difference between program changes.
Afaiu, currently the best one can get is decl/fn based invalidation and transitive recomputation of according proofs.
Not sure, if this is the correct place to do in-depth discussion and how you can be reached. Feel free to close or move to "Discussions".
That said, I have a few questions
- "git compatible" sounds reasonable until you have a big rebase forcing a specific patch order meaning "to squash snapshots for the rebase". The text does not explain this shortcoming of jujutsu very clearly and if or how you plan to address it.
- "combine snapshot-based and patch-based version control" is missing a summary sentence for "Based on the above, we can conclude that neither snapshots nor patches are "better"; they are better at different things. An ideal system would combine them to get the benefits of both." Is such ideal system possible or not and what trade-offs were chosen (for now)?
- "built-in TUI" sounds like wip, but good idea, if there is corresponding API functionality with tests.
- "store large/binary files efficiently" sounds good, but missing interface on how to mark files at binary and how to store large files out of band as required or optional
- "universal undo" is missing memory usage/growth over time and what happens on data base deletion. I'd expect that it contains user-added intermediate states, so there would need to be some "cleanup-logic", which so far is not explained (theoretically). Or is my understanding incorrect? Also unclear is if/how undo-tree functionality vim implements is planned or feasible. It reads like a few edge cases are missing, like what happens if remote commits were reordered to rebase feature branch on master by a colleague or bot.
- "clean implementation" sounds good
It would be nice, if there could be a roadmap and/or general overview of what things work and what things not to set properly user expectations.
Motivation
This project looks very interesting and I am curious, if "universal undo" could be used for incremental verification (or other incremental program related executions like static/dynamic analysis or faster interactive proof inputs) by tracking all editor changes between user-specified snapshots to at least estimate or ideally compute the semantic difference between program changes.
Afaiu, currently the best one can get is decl/fn based invalidation and transitive recomputation of according proofs.
Not sure, if this is the correct place to do in-depth discussion and how you can be reached. Feel free to close or move to "Discussions".
That said, I have a few questions
It would be nice, if there could be a roadmap and/or general overview of what things work and what things not to set properly user expectations.