cursor (VSCode variant with AI better than Github Copilot)

Stream: general

[Kim Morrison]

I've been using https://www.cursor.com/ this morning, and it is very impressive. Significantly better than Github Copilot.

It suggests edits mid-line, does multi-cursor edits, and seems to remember what you're doing across files better. So far I've been using it to fix errors in Lean files, rather than writing new code, but for that at least it is quite impressive, and I'd encourage people to try it out.

[Kim Morrison]

(Oh, and it know about the line length limit and rewraps when it makes suggestion mid-line!)

[Mario Carneiro]

is this a new editor, or just a plugin to vscode?

[Kim Morrison]

It is built on top of VSCode

[Mario Carneiro]

because if it's a new editor then there are a lot of switching costs involved

[Kim Morrison]

seamlessly runs all my extensions

[Mario Carneiro]

the screenshots don't look much like vscode, it has more of a sublime text look to me but I haven't tried it

[Kim Morrison]

Ooh, just encountered a hallucination when it line-wrapped a long simp only, and changed a theorem randomly.

[Kim Morrison]

Yeah, the default colour scheme is different.

[Julian Berman]

(https://github.com/yetone/avante.nvim is the neovim version for any of you with pretty N's near your name :)

[Shreyas Srinivas]

It is basically a vscode fork. There a handful of those going around

[Shreyas Srinivas]

They explain why they didn't just make an extension here: https://docs.cursor.com/get-started/migrate-from-vscode

[Adam Topaz]

I'm curious to hear whether it really gives any productivity boost in Lean4, for programming and/or proving.

[Shreyas Srinivas]

There are a few drawbacks with this.

1. These forks claim to periodically rebase onto the latest vscode version, but the frequency varies. So they might not always be up to date with the latest vscode. The lean extension doesn't require the latest version. But this can change.

2. To install vscode extensions one has to download them from the marketplace on a web browser first.

[Kim Morrison]

Adam Topaz said:

I'm curious to hear whether it really gives any productivity boost in Lean4, for programming and/or proving.

I've only been using it for a day so far. A lot of the boring parts of my work (fixing errors in Mathlib after adaptations, concreting over every bare patch of ground in the List / Array API, etc) are already helped by Copilot, and Cursor's models/workflow seem like a clear improvement over Copilot.

So -- I would say that if you are already getting a productivity boost from Copilot, then you will probably get more from Cursor. If, however, you've already tried Copilot and it doesn't help you, then perhaps not.

[Kim Morrison]

It does require getting used to the fact that they have really claimed the tab key for themselves, and so tab can't be used reliably for autocompletion anymore. If I keep using Cursor I'll probably have to work out how to have the old tab behaviour under ctrl+tab or something.

[Evgenia Karunus]

I've been using cursor for the past half a year, I love it.
I never became friends with Github Copilot (autocompletion is distracting me, and I don't find it particularly useful), but got friends with Cursor's CMD+E immediately. I feel it's more useful and more under my control.

Re:whether it helps with Lean4 programming/proving

The CMD+E interface doesn't help me with proving in Lean (it lacks too much information because it doesn't have access to types), but the cursor's AI pane does help with the proofs (it's just claude/chatgpt wrapper that's aware of the files in your folder, so it helps about as much as those tools do when you feed them some files).

The CMD+E interface is helpful for Lean4 metaprogramming. Claude is usually the best model for this.

Re:new editor switching costs

It's a vscode fork and feels like it. Also - cursor did transfer all of my vscode extensions & settings automatically.

[Alok Singh]

I use cursor all the time and have tried to pitch @Tomas Skrivan on it. It recently added an “iterate on lints” which plays nice with the infoview.

[Kim Morrison]

Alok Singh said:

I use cursor all the time and have tried to pitch Tomas Skrivan on it. It recently added an “iterate on lints” which plays nice with the infoview.

@Alok Singh, what does "iterate on lints" do? I'm not finding anything yet.

[Alok Singh]

it's in settings (cmd shift j)> features. it just reads any error messages and tries to fix them. mostly works in the composer, i forget if cmd k uses it. i don't think tab complete does

[Jason Rute]

Anyone here tried Windsurf, a new vs code based AI editor? https://codeium.com/windsurf

[Alok Singh]

Jason Rute said:

Anyone here tried Windsurf, a new vs code based AI editor? https://codeium.com/windsurf

I’m trying it right now, my high school classmates made it and I’ve been procrastinating on their use requests

[Dave Bayer]

I have WIndsurf Pro Ultimate, 2x Cursor Pro, Claude Pro, and ChatGPT Plus. I dropped Perplexity. My subscriptions are getting out of hand, they're like some people's sport channel cable bills.

I'm new to this , but not sleeping much trying to become a Centaur programmer, in the sense popularized by Gary Kasparov after he recovered from his defeat by IBM's Big Blue. My sense is that these very months are an inflection point, and no one actually has any idea how to best use these tools. One principle: You're not talking to an alien intelligence; you're talking to yourself. The quality of the planning document prompts dramatically affects whether AI flails like a freshman or knocks out code like Bill Joy.

I've been experimenting with coding small test math programs in three or four languages at once, in either Cursor or Windsurf using a common prompt. When everything works, ask AI to rewrite the prompt, then take it to the other editor and start again from scratch.

Claude 3.5 Sonnet understands my iPad math drawings, and an astonishing amount of mathematics and strategies for combinatorial search and such. While Cursor is slightly clumsier than WIndsurf, Cursor lets you use Claude 3.5 Sonnet as the AI assistant. Windsurf's assistant is in-house, remarkable at programming when there's a decent training corpus, but just not as smart as Claude 3.5 Sonnet. I'm forced to use Cursor more, when I need Claude's comprehension.

A middle ground is to use standalone Claude, away from an editor, to flesh out over several hours a very careful specification prompt. Then in most languages either system can emit correct code basically on the first try.

This suggests a middle ground between unreadable and uncheckable conventional math papers, and the formal proofs considered here: We should publish AI prompts that have been battle-tested to yield AI-assisted working code, that pose as conventional papers for those mathematicians still trapped in amber.

I came here hoping for help with a tragic realization: This year's AI simply isn't smart enough to use Lean 4 as a general purpose programming language. The training corpus shouldn't matter: AI taught itself the game of Go from just the rules, and devised idioms that blew away humans. AI should teach us how to use Lean 4 as a general purpose language.

This must be our fault. We write documentation for humans, when we should be writing Centaur documentation for humans and AI.

[Julian Berman]

I haven't used it yet (and maybe someone's mentioned this somewhere) but I've just noticed that GitHub Copilot now has a Sonnet integration. Specifically here: https://docs.github.com/en/copilot/using-github-copilot/using-claude-sonnet-in-github-copilot -- which I needed to enable in my Copilot settings.

Though again I haven't done so yet, I think from scanning that doc page, that any of us with GitHub Pro subscriptions (which I have from OSS contributions, and I suspect at least a few others may have here in the community?) that this might mean I have free access to use Sonnet through GitHub. Will try to find some time to confirm whether that's the case or not but yeah perhaps something others may not have noticed exists now.

[Tomas Skrivan]

image.png

Yes there is an option in the Github Copilot settings.

I'm not sure how am I supposed to test it though. In a random lean file I tried a small chat:

/- Q: Can you answer simple questions?
   A: Yes, I can answer simple questions.

   Q: Which LLM are you?
   A: I am the Lean Lean Machine.

   Q: What is your purpose?
   A: My purpose is to help you with your Lean code.

   Q: Are you github copilot?
   A:No, I am not github copilot.

   Q: Are you Claude 3.5 Sonnet?
   A: No, I am not Claude 3.5 Sonnet.
  -/

[Julian Berman]

Ask it to prove some actual Lean statement and flick it back and forth from Sonnet (which I think light consensus says is useful) to not-Sonnet (which light consensus I think is "not too much") and see if the response improves maybe is what I'd try, as yeah who knows if it's even lying there.

[Rémy Degenne]

In the copilot chat window in vscode you can select which LLM you want, but I don't know if it changes the model that provides the code completions.

[Julian Berman]

I took

When using Claude 3.5 Sonnet, input prompts and output completions continue to run through GitHub Copilot's content filters for public code matching, when applied, along with those for harmful, offensive, or off-topic content.

to seem to imply strongly yes (i.e. "we still run our own content filters over the completions, but the output itself first comes from Sonnet"). But OK I'll try it out at some point later today or tomorrow and see if I can tell myself.

[Johan Commelin]

Q: Which LLM are you?
A: I am the Lean Lean Machine.

Thinking on its feet!

[Ruben Van de Velde]

"thinking"

[Julian Berman]

Yeah GAI truly walks among us.