Copilot for Lean

Stream: general

[Jason Rute]

Does anyone here use copilot for coding in Lean? If so what does it help with? Is it just good for boilerplate, or is it helpful for writing proofs? Also, would you be willing to send me a (zoomed in) screen shot of it in action that I could use in a talk this week?

[Bulhwi Cha]

I used it last summer. It was hit-or-miss; fun but not very helpful.

[Alex J. Best]

I use it, it's quite often fairly random but occasionally really helpful. I think there was a thread with examples sometimes before. But one of the times I remember being really impressed was when it autocompleted a matrix for me in correct syntax from something like t := ![[1,2,3 sorry on mobile so can't be more precise

[Sorawee Porncharoenwase]

Sorry for resurrecting an old thread, but Copilot really impressed me. It just autocompletes rw [List.mem_join] at h', even though I don't have List.mem_join anywhere in my program.

Does Copilot peek at the proof context window? It would be able to get a lot more localized information that way.

[Wojciech Nawrocki]

@Sorawee Porncharoenwase I don't think it does, which is all the more impressive! For me it has been mostly miss but in some cases, especially with repetitive steps that just differ by a few indices here and there, quite helpful.

[Michal Wallace (tangentstorm)]

Sorawee Porncharoenwase said:

Does Copilot peek at the proof context window? It would be able to get a lot more localized information that way.

It appears it is now possible for a VS Code extension to feed extra information into copilot :
https://code.visualstudio.com/blogs/2024/06/24/extensions-are-all-you-need

[Kim Morrison]

I read through this, and the linked documentation, but could only see things describing the chat bot interface, and nothing about how to add to the context that the code completion agent sees.

[Kim Morrison]

If anyone learns about how to add context for code completion, that would be great.

[Kim Morrison]

I am increasingly confident that the code completion agent is reading error messages, but haven't thought of a really definitive test for this. I'd be very curious if anyone knows for sure here.

[Josha Dekker]

Well if you were to change an error message locally into some bogus suggestion, you could easily test it, right?

[Kim Morrison]

Yes, but you'd need to set up the error message in another file, so that you could be sure it wasn't just reading the source. I've never actually sat down to do experiments, I'm just guessing from its predictions.