Zulip Chat Archive
Stream: lean-gptf
Topic: Install?
Damiano Testa (Jul 03 2021 at 11:22):
Dear All,
I decided to try this out, since it seems very cool! I am a real beginner, though, so I think that I am missing something basic.
I donwloaded a fresh copy of mathlib, checked out the commit that is mentioned on the page, downloaded the oleans and now I am typing
leanpkg add jesse-michael-han/lean-gptf
The answer is:
lean-gptf: trying to update _target/deps/lean-gptf to revision lean-3.23.0
cannot find revision lean-3.23.0 in repository _target/deps/lean-gptf
I am not sure what I should do now...
If anyone can help, I would be very grateful!!
Huỳnh Trần Khanh (Jul 03 2021 at 12:16):
This error is pretty frustrating. In the meantime you can just clone the lean-gptf repo and edit the example.lean file when you want GPT-f suggestions.
That's what I do.
Damiano Testa (Jul 03 2021 at 12:21):
Huỳnh Trần Khanh, thank you! This works!
Jason Rute (Jul 03 2021 at 12:22):
I think we have to update lean-gptf to use the newest version of lean (and to include binaries). @Jesse Michael Han is there an easy way to keep it in sync? (There was a discussion about putting it in mathlib also, but I don’t know how far that has gotten.)
Jason Rute (Jul 03 2021 at 13:46):
Actually, wait. @Damiano Testa it looks like you are on a much older version of Lean than lean-gptf which is now on 3.30.0 I think.
Damiano Testa (Jul 03 2021 at 17:16):
Jason, thanks: I will update to a later version of mathlib, then!
Alex Zhang (Jul 11 2021 at 19:43):
I have trouble setting up the gptf. Where should I run the command leanpkg configure && leanpkg build?
image.png
https://github.com/jesse-michael-han/lean-gptf
Alex Zhang (Jul 11 2021 at 19:45):
I ran this command in a new lean project, but then I did not find the file src/example.lean mentioned in the next step.
Jesse Michael Han (Jul 11 2021 at 19:56):
Alex Zhang said:
I have trouble setting up the gptf. Where should I run the command
leanpkg configure && leanpkg build?
image.png
https://github.com/jesse-michael-han/lean-gptf
it should be run from the project root directory
Alex Zhang (Jul 11 2021 at 20:02):
I first ran leanproject new my_project in a terminal. Then opened the newly downloaded project, and ran that from the root directory of my_project. But then, I couldn't find the file src/example.lean.
Alex Zhang (Jul 11 2021 at 20:03):
Jesse Michael Han (Jul 11 2021 at 20:04):
you don't need to run leanproject new my_project, just clone lean-gptf, navigate inside that directory, and follow the instructions in the README
Alex Zhang (Jul 11 2021 at 20:06):
Hi, Jesse! I am extremely new to those things. Could you please explain where I should clone lean-gptf to, suppose I want to use tactic gptf in my_project (or in other settings perhaps)?
Jesse Michael Han (Jul 12 2021 at 02:25):
sorry for the late response, had to run an errand --- did you try running the commands in this section of the README from the root directory of your project? https://github.com/jesse-michael-han/lean-gptf#importing-lean-gptf-as-a-dependency-for-your-own-project
Alex Zhang (Jul 12 2021 at 08:59):
No worries, Jesse. No, as I thought they are the later steps.
Alex Zhang (Jul 12 2021 at 09:00):
Thanks! I will try to run those. What is this step for then?
image.png
Alex Zhang (Jul 12 2021 at 10:58):
gptf is working now in my project.
Is it normal that gptf gives different suggestions for the same example in different trials?
Alex Zhang (Jul 12 2021 at 10:59):
Alex Zhang (Jul 12 2021 at 10:59):
Jason Rute (Jul 12 2021 at 11:09):
This is normal. Lean-gptf is nondeterministic. (It randomly samples a set of strings according to a probability distribution.)
Kalle Kytölä (Jul 12 2021 at 22:03):
Thank you for the advice, Huỳnh Trần Khanh! Cloning the repo directly basically seems to work.
I did not get the OpenAI API key, though --- I never received an email after filling the form <https://bit.ly/3nNWMyB>. @Damiano Testa and @Alex Zhang, since you seem to have tried this recently, did you manage to get the API key? Or is there some way to try gptf without it?
Jesse Michael Han (Jul 12 2021 at 22:27):
^i think @Stanislas Polu might be able to get your request approved
Stanislas Polu (Jul 12 2021 at 22:43):
Sorry for the delay. Will do so first thing tomorrow morning CET!
Damiano Testa (Jul 13 2021 at 05:00):
Kalle, just to answer your question, I have received the API key and I have not tried using gptf without it.
Alex Zhang (Jul 13 2021 at 07:50):
Hi Kalle, I did get an email after waiting one week or so.
Stanislas Polu (Jul 13 2021 at 09:40):
Sorry for the delays, all requests have been answered. Don’t hesitate to ping here in the future!
Kalle Kytölä (Jul 13 2021 at 23:49):
Thank you very much! I also got it working and will try it. Looks impressive!
Last updated: Dec 20 2023 at 11:08 UTC