Support Proof Diffs about coqtail HOT 3 CLOSED

This is a really cool features and I'd love to have this. Any ideas as to how one might implement this? I had a few ideas:

1. Use coqtop's Diffs option.

   • So of course the first thing I tried was to just evaluate Set Diffs "on". in the main buffer, and then seeing if it did anything. No joy. Is it clear if this is a limitation of Coqtop's XML protocol?
   • Of course, the downside to this is that it won't be backwards compatible---this won't be available to those working with older versions of Coqtop before this feature was available.

2. Use vim's builtin diff features.

   • I tried manually creating a second buffer, copying the goal buffer state there, taking a step in the main buffer, and then using :diffthis on both buffers. The results are kind of patchy.
   • I could experiment more and try to toy with the different diffopt settings and algorithms, but what can be done will ultimately be limited by vim's functionality. I haven't had a chance to look into diffexpr or what it can do for us.
   • That being said, this is also the most straightforward solution---just keep a hidden "shadow" goal buffer around that lags a step behind, and allow the user to turn on diffing between that and the actual goal buffer, showing only the goal buffer with the highlighted terms. It'll be difficult to see missing terms, but it at least show something. The shadow buffer can just be repopulated using the undo history of the goal buffer.

3. Use Python to implement the algorithm described in the reference manual.

   • If we can get the Python side to mark the highlight regions, we could pretty easily intercept the messages to and from Coqtop and do it from there. This can be done every time the goal buffer is updated.
   • This is also the most easily powerful option, and can also be used to implement cool features beyond what other IDEs have.
   • Probably also requires the most (invasive?) changes and work.

from coqtail.

I might even take a dip into #87 just to learn about how highlight regions work before trying anything here. I've mostly taken syntax highlighting for granted and it would be useful to learn about it by hacking on it.

from coqtail.

I had something in mind along the lines of option 1. When you enable diffs the XML protocol starts including messages with information about what changed in the proof state, which currently Coqtail ignores so it’s not visible. We’d just have to parse this information and then pass it to Vim to highlight with the appropriate color.

Option 2 is an interesting idea for a fallback for older versions of Coq without diff support. I’ve never really used Vim’s diffing capabilities much so I’d need to experiment and see what’s possible there.

Option 3 could potentially also work for older versions, but it does seem the most complicated. If Vim alone isn’t able to produce useful diffs then maybe some combination of 2 and 3 (using Python to preprocess the goal buffers a bit then passing it to Vim to actually do the Myers diff) would be best.

As for #87, I’ve started working on that a bit in a local branch. If you’re interested I could push it, you could fork it and open a pull request, and we could collaborate on it.

from coqtail.