api suggestion vscode integration

Stream: general

[Timothee Lacroix]

Hey everyone, a heads up that @Gabriel Ebner just merged some integration for API based tactic suggestions in the vscode plugin.
The PR adds two settings in the lean extension settings :

• Suggestion API Key
• Suggestion URL
  Then, tactic suggestions can be activated / de-activated from the ? symbol in the upper right corner of the infoview.

If you want to try this out, feel free to use :
key : wlGINGVQMB6CtXZ1MndJz2F3z0sSuCFo7dbIB7m0
url : https://dtvst8cdg8.execute-api.us-east-1.amazonaws.com/dev/suggest
I'll try to maintain this as best I can, but I guarantee zero stability, production engineering isn't my forte ...

This api will serve suggestions from the model described in https://arxiv.org/abs/2205.11491 . It was specialized on minif2f problems (which probably aren't of interest to most of you here) and trained on an old mathlib commit, hopefully most theorems are still relevant ...

If you want to develop your own suggestion API, interaction is pretty simple. API key is given in the x-api-key header, then :

• receive {"tactic_state": "some_string", "prefix": "some_other_string"}
• answer {"tactic_infos": List[{"tactic": "some_string"}]}

[Jason Rute]

Interesting. Is tactic_state a single goal or the whole goal stack? Is it exactly what comes out of the pretty printer? What pp settings does it use?

[Jason Rute]

Also, can one use a localhost url (for testing, for locally running agents, and for modifying another API, such as OpenAI’s gptf, to fit your API)?

[Jason Rute]

Also, I assume we have to wait until a new Lean 3 vs code plugin is released?

[Jason Rute]

FYI @Edward Ayers @Bartosz Piotrowski @Wojciech Nawrocki @Zhangir Azerbayev

[Timothee Lacroix]

• tactic_state is the whole goal stack and is affected by pretty printing options. I think it's exactly what's displayed in the infoview. Further work could be done on the lean3 server side to get more information on the tactic state, but strings are a good start :)
• yeah definitely use localhost urls for testing out your API
• I think Gabriel already made a new release ?

[Jason Rute]

I just tested it. Very nice.

[Jason Rute]

As for UI, I think the question mark with a circle looks like "help" and is very unintuitive.

[Timothee Lacroix]

Jason Rute said:

As for UI, I think the question mark with a circle looks like "help" and is very unintuitive.

Well, the provided suggestions supposedly should be helpful ? :p Happy to change the symbol for something else that makes more sense :)

[Jason Rute]

Maybe a bouncing paperclip in the lower right corner? :paperclip: :stuck_out_tongue:

[Jason Rute]

Here is a screen shot: Screen-Shot-2022-09-14-at-9.36.39-AM.png

[Adam Topaz]

Whoa! This is very nice!

[Adam Topaz]

One very minor thing I noticed: when clicking the suggestions, it seems that the indentation for the text it adds to the lean file is a bit off.

[Adam Topaz]

But again this is really really nice! How long do you expect the API key above to work?

[Timothee Lacroix]

Adam Topaz said:

But again this is really really nice! How long do you expect the API key above to work?

There is no current limit for how long this API will be running. I might shut it down if no requests are received for a while, and wait for a new model to revive it :)
For the API key, the plan for now is to leave it as the only api key for this API and see what happens. Please ping me if you notice any unusual lag, as I might have to increase capacity / lower throttling.