unable to use gptf

Stream: lean-gptf

[Alex Zhang]

What does the use of gptf report the following error?

import tactic.gptf
example : 1 = 1 := by gptf

[gptf_proof_search_step] run_best_beam_candidate UNEXPECTED MESSAGE:
---
["ERROR { \"error\":{ \"code\":null, \n    \"message\":\"Invalid URL (POST /v1/engines/formal-lean-wm-to-tt-m1-m2-v4-c4/completions)\", \n    \"param\":null, \n    \"type\":\"invalid_request_error\"}}"]
---

[gptf_proof_search_step] run_best_beam_candidate UNEXPECTED MESSAGE:
---
["ERROR { \"error\":{ \"code\":null, \n    \"message\":\"Invalid URL (POST /v1/engines/formal-lean-wm-to-tt-m1-m2-v4-c4/completions)\", \n    \"param\":null, \n    \"type\":\"invalid_request_error\"}}"]
---

no predictions succeeded

[Jason Rute]

@Jesse Michael Han

[Jesse Michael Han]

thanks for the ping, we are moving some engines around on the API --- just pushed a fix

[Alex Zhang]

Is the problem fixed? Could you let me know how I can update my project? @Jesse Michael Han

[Jesse Michael Han]

git pull origin master

[Alex Zhang]

image.png

[Jesse Michael Han]

i don't use VSCode but you might have to stash your local changes first

[Alex Zhang]

The problem is my local project is connected to my own repository my_project. Do you know what I should do before git pull origin master

[Jesse Michael Han]

maybe try leanpkg configure && leanpkg build?

[Alex Zhang]

(deleted)

[Alex Zhang]

(deleted)

[Alex Zhang]

gptf is failing again now with the error

[gptf_proof_search_step] run_best_beam_candidate UNEXPECTED MESSAGE:
---
["ERROR { \"error\":{ \"code\":null, \n    \"message\":\"Invalid URL (POST /v1/engines/formal-lean-wm-to-tt-m1-m2-v4-c4/completions)\", \n    \"param\":null, \n    \"type\":\"invalid_request_error\"}}"]
---

[gptf_proof_search_step] run_best_beam_candidate UNEXPECTED MESSAGE:
---
["ERROR { \"error\":{ \"code\":null, \n    \"message\":\"Invalid URL (POST /v1/engines/formal-lean-wm-to-tt-m1-m2-v4-c4/completions)\", \n    \"param\":null, \n    \"type\":\"invalid_request_error\"}}"]
---

no predictions succeeded

[Alex Zhang]

@Jesse Michael Han

[Jesse Michael Han]

what branch of lean-gptf is your project using?

[Alex Zhang]

Hi Jesse. Sorry that I am not quite sure what you mean by branch here. How can I figure this out? @Jesse Michael Han

[Jesse Michael Han]

leanpkg configure will download and checkout a git branch of lean-gptf, judging from the error above, it probably does not contain the fixes which i pushed to lean-gptf earlier

[Alex Zhang]

After leanpkg configure, import tactic.gptf reports

file 'tactic\gptf' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

[Alex Zhang]

Is what I should do to manually add path _target/deps/lean-gptf/src in leanpkg.path? @Jesse Michael Han

[Alex Zhang]

This is the current content in leanpkg.path

builtin_path
path _target/deps/mathlib/src
path ./src

[Alex Zhang]

Alex Zhang said:

Is what I should do to manually add path _target/deps/lean-gptf/src in leanpkg.path? Jesse Michael Han

No, this doesn't work. Reports the same long error as above.

[Alex Zhang]

Could you please let me know what I should do? @Jesse Michael Han

[Alex Zhang]

I have
image.png

[Kevin Buzzard]

Why don't you change the commit in your project's toml to point to a recent commit for gptf? Your toml says exactly which versions of mathlib and gptf to use.

[Alex Zhang]

I have solved this issue. Thanks for the help!

[Arthur Adjedj]

Hi, I tried setting up everything in order to use lean-gptf, but when trying to use the tactic, I end up with the following error message :

[gptf_proof_search_step] run_best_beam_candidate UNEXPECTED MESSAGE:
---
["ERROR { \"error\":{ \"code\":null, \n    \"message\":\"No such organization: org-kuQ09yewcuHU5GN5YYEUp2hh.\", \n    \"param\":null, \n    \"type\":\"invalid_request_error\"}}"]
---

I tried changing the org name to my personal one, but it lead to a new error saying the engine doesn't exist since it should be tied to the other, first org. What can I do to correct this ? Thanks in advance for the help

[Jesse Michael Han]

the gptf tactic is currently working for me with that org id, can you give exact steps to reproduce your bug?

[Arthur Adjedj]

There aren't many steps to my bug, I simply followed the guide over on https://github.com/jesse-michael-han/lean-gptf:
-used these commands while in my lean project :

leanpkg add jesse-michael-han/lean-gptf

leanpkg configure

leanproject get-mathlib-cache

leanpkg build

-changed my key inside the code on gptf.lean to
private meta def OPENAI_API_KEY : option string := some "the_key"

-imported tactic.gptf in a file and tried using the tactic