Can Cursor access Lean InfoView?

Stream: lean4

[Geoffrey Irving]

Has anyone on the FRO spoken with Cursor about what it would take for Cursor (either tab completion or agent chat) to see the Lean InfoView? There's some chance this is only a couple-day fix for them on their side, and they might be interested in doing it.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

What would be the benefit of using this over something like the lean_goal request in lean-lsp-mcp? Would you expect the Cursor agent to use interactive features like type popups?

[Geoffrey Irving]

Possibly that the right mechanism to do what I want. Really just any way for either out-of-the-box Cursor or a decent Lean-specific VSCode UX would be good; currently I don't have any AI agent setup that can see the error messages automatically.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hm, I think in VSC agents already see error messages. There is a subtlety here in that messages reported by Lean via default LSP methods (and which builtin VSC methods/agents would use) can sometimes differ from those seen in the infoview, but I think that only happens for traces.

[Geoffrey Irving]

1. Do you mean if an agent builds via the commandline? I suppose that’s right, but it’s much longer latency than the infoview when iterating on a proof or even within a file. A particular thing I would like is Cursor applying as many deprecation fixes as possible, and this would be much faster if it didn’t have to rebuild the whole file.
2. The smaller LLMs behind autocomplete would ge sufficient for a lot more things if they could see the infoview too.

Possibly I should just ping someone at Cursor to ask. And admittedly this may belong in the ML for Theorem Proving channel.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

(+1 on moving this to #Machine Learning for Theorem Proving).

Do you mean if an agent builds via the commandline?

No; I mean agents in the GitHub Copilot Chat extension see errors by default; e.g. here's a sample chat for a file containing def foo : Nat := 100. Perhaps I'm misunderstanding the question?
Screenshot 2025-08-05 at 6.09.55 PM.png

[Geoffrey Irving]

This is nice, but that’s Copilot, not Cursor.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ah sorry, I was replying to the "Lean-specific VSCode UX" part. I'm not sure about Cursor!

[Kim Morrison]

My experience in Cursor is that can see error messages, but can't see warnings or info messages. It can't see the InfoView at all. I'd be very surprised (but happy!) if they were interested in implemented such a niche (from their PoV) feature). It's also pretty hacky, as the InfoView is just a pile of HTML by the time Cursor would be getting to it.

[Julian Berman]

(this works in lean.nvim FWIW :), CopilotChat can see the infoview buffer just like any other)