Plugin needs a specific repository + commit hash?

[rnrand]

We were able to start up a server to host the LeanDojoGPTPlugin (private for now, since I don't expect it can handle a lot of traffic) and a corresponding GPT, but it looks like the engine can only prove something from the repository + commit hash given on initialization?

It this supposed to be the case? The paper says, "After exposing the APIs to ChatGPT, we can ask it to prove theorems by specifying the theorem’s name and path in any public Lean repo on GitHub." But I've been getting error when trying to access other repos.

Also, is there a reason it has to read from a Github repo, as opposed to a theorem provided (in Lean or plain English) by the prompt?

[yangky11]

Although main.py uses a fixed repo + commit hash, it's just a simple wrapper around LeanDojo, which supports any repo. I would suggest taking a look at LeanDojo and write a customized script for interfacing it with GPTs.

Nevertheless, currently LeanDojo does not support reading from a new Lean file in the prompt.