github copilot

Stream: general

[Johan Commelin]

Has anyone used this already? https://copilot.github.com/

[Gabriel Ebner]

Signed up for the waitlist.

[Adam Topaz]

Let us know how it goes when you get access... Just saw the link on HN.

[Bhavik Mehta]

On this note, TabNine could also be interesting to play with in the context of Lean

[Adam Topaz]

Oh and it looks like tabnine also works with the correct editor.

[Adam Topaz]

Just FYI, from the copilot waitlist signup:
Screenshot-2021-06-29-at-13-12-46-Build-software-better-together.png

[Matthew Ballard]

I poked at TabNine in Python and wasn’t impressed.

[Eric Rodriguez]

this looks kinda like lean-gptf

[Jason Rute]

Is there any reason to think that copilot or TabNine would support Lean, which has a very small user base?

[Jason Rute]

Also, for tactic proofs, I imagine lean-gptf would do better than any other solution which can't see the tactic state.

[Bhavik Mehta]

Jason Rute said:

Is there any reason to think that copilot or TabNine would support Lean, which has a very small user base?

TabNine certainly does support Lean - I've only been using it this evening but it's already been pretty convenient and helpful so far

[Jason Rute]

I stand corrected. I’d love to hear your thoughts!

[Bhavik Mehta]

It's like a smarter version of VSCode autocomplete - since it's easy to setup and fast it's mostly been convenient in practice; the suggestions are sometimes really weird but also sometimes pretty smart, it filled in a couple of proofs of me earlier today and I just had this example

[Bhavik Mehta]

image.png

[Bhavik Mehta]

What's cool to me here is that there was no instance of f.inv anywhere in this file, and no instances of to_nat_trans := f.inv in mathlib, so presumably it made an analogy with the hom := { to_nat_trans := f.hom earlier to make this suggestion (and it was what I wanted!)

[Eric Wieser]

Meanwhile it seems less smart for me:
image.png

[Huỳnh Trần Khanh]

is that copilot or tabnine

[Jason Rute]

So @Bhavik Mehta is using tabnine and @Eric Wieser is using copilot, right?

[Jason Rute]

@Stanislas Polu You should convince open ai to use gptf in copilot for lean. :rolling_on_the_floor_laughing: (More seriously, I could imagine a future when all of these coding helper tools use internal language-server-like information to make suggestions, either using the actual language server, or by training a world model to predict what the language server would say.)

[Jason Rute]

Actually, it looks like TabNine already makes use of LSP information. Since Lean 3's server is nonstandard, I assume it doesn't use it, but I can't be sure.

[Bhavik Mehta]

Jason Rute said:

Actually, it looks like TabNine already makes use of LSP information. Since Lean 3's server is nonstandard, I assume it doesn't use it, but I can't be sure. If it does, maybe TabNine and lean-gptf aren't so different (but I honestly have no idea how tabnine (or copilot) work, only speculation)????

I think a direct comparison isn't the most helpful thing here - in my mind the value of TabNine is to speed up filling in boilerplate and repetitive-looking code (eg I found it helpful when writing docstrings and my example above) whereas the value of lean-gptf is to suggest tactics in the middle of a non-trivial argument. I think their use-cases right now are somewhat orthogonal. That said, tabnine is easier to set up and integrate into my workflow than lean-gptf is - in my experience at least

[Jason Rute]

Totally. (I actually removed that comparison as I thought about it more.) Part of my speculation though is that tools like gptf which aim to provide proof completion, and tools like tabnine which aim to provide code completion, are starting to converge. We showed in gptf that combining the internal state of a theorem prover with lots of semantically aware training data and a powerful language model gave good prediction results (and even better if combined with a tree search). This is really possible with any programming language to some extent and language servers make it easier to access such internal information (and generate training data). Obviously we understand lean much better than TabNine likely does and our gptf training data is very well curated for the task at hand, but maybe one day the lean 4 language server will make its own language model autocomplete predictions based on semantic data, or maybe it will integrate seamlessly with external autocomplete tools like TabNice or CoPilot through LSP.

[Eric Wieser]

In copilot's defense, it did correctly fill in all the data fields for a structure I'd defined based on a similar definition within the same file

[Eric Wieser]

That is, it was able to fill out these lines based presumably on what it learned from the removed lines further down the patch

[Stanislas Polu]

Note that OpenAI Codex, the model behind Copilot, was never trained on Lean code and Copilot does not leverage the LSP either. Its current Lean capabilities are zero-shot capabilities of Codex, based on what it sees from the content of your file before the place of completion. Don't expect it to be good, but it's already quite exciting to see that it picks up the syntax generally correctly. We're looking to include Lean code in future version of Codex which would make copilot potentially useful when working with Lean.

Alternatively, it is clear from this thread that the UX of Copilot is the right one as it requires no effort from the user compared with lean-gptf. We have new models of GPT-f that are much more powerful than what is currently available to the current gptf tactic. We're looking to make them available and are thinking about leveraging the Lean VSCode extension. Obviously we can't use the same UX as copilot as GPT-f only works in tactic mode and you generally want to see >1 suggestions, but we could query the model in the background when working on a tactic state such that suggestions are displayed in the info view without user intervention.

Do you think it's the right direction? Any other idea? Happy to chat about these!

[Stanislas Polu]

Also, on top of picking the syntax, Copilot is not completely dumb (though these examples are probably memorized)
Screen-Shot-2021-06-18-at-14.47.52.png
Screen-Shot-2021-06-18-at-14.54.47.png

[Johan Commelin]

I think queries in the background are a very good move. The less the user needs to do, the better.

[Johan Commelin]

Whether this is computationally feasible, I don't know.

[Johan Commelin]

I can imagine that "fire a query when the user explicitly asks for it" vs "fire a query every time the user hits a key" is a difference of maybe almost two orders of magnitude.

[Stanislas Polu]

Definitely but I'm confident we'll make it work :+1: (by make it work I mean finding the compute to support the Lean community more than technically which is OK as demonstrated by Copilot)