Collect and diff info trees from two branches?

Stream: Is there code for X?

[Joachim Breitner]

We don't, by any chance, already have a tool that I can run on a file in two mathlib branches and that shows me where the proof states on the respective branches differ?
(I fear this question can be considered rhetorical)

[Damiano Testa]

Leaff is supposed to do that. Searching for it, might yield some results! (I'm on mobile)

[Yaël Dillies]

Joachim, are you trying to debug proofs? I would suggest opening a second copy of mathlib (eg in gitpod) and having a second monitor. I don't know of a better solution currently :sad:

[Joachim Breitner]

Leaff seems to diff changes to the environment, not the proof states within the file.

[Joachim Breitner]

That’s what I expected, Yaël, but just checking. I wonder if such a tool becomes not too hard to build with verso underneath, but not today :-)

[Johan Commelin]

I wonder if this can be done in neovim (cc @Julian Berman). We can certainly open different mathlib clones/worktrees in different panes. Will they get their own lsp and their own infoviews? And can we then run the vimdiff tool on the two infoviews?

[Julian Berman]

If it's one specific proof you want to look at yeah then what you suggest is doable -- you open two tabs (because we don't have per window infoviews yet but we do have per tabpage ones) and then enable diff mode on the two infoview windows and vim will diff their contents already. If this sounds like what you're looking for I can write up better instructions if that's not specific enough.

[Joachim Breitner]

For now switching branches or using gitpod suffices, thanks!