Using gptf in mathlib development

Stream: lean-gptf

[Jason Rute]

(Moving a conversation from #general > Lean in the wild.)

Scott Morrison said:

https://github.com/jesse-michael-han/lean-gptf#importing-lean-gptf-as-a-dependency-for-your-own-project explains how to set it up as a dependency of a project. However this is not a viable approach for someone working directly in mathlib (e.g. many people here).

Do you have suggestions for using gptf regularly within mathlib?

Thanks for bring this up. One should just think of Lean gptf as just another powerful Lean tactic which is in currently in development, like rw_hint which won't be left in mathlib code. Given your expertise @Scott Morrison, I would probably come to you for advice on this subject. :smile:

[Jason Rute]

A few options I see (and @Jesse Michael Han or @Edward Ayers might have other thoughts).

1. Users could add it as a dependency, do their development, and then remove it as a dependency before making a PR. (They would have to also remember to remove install tactic.gpt in the header too.)
2. We could look at PRing gptf or something similar to mathlib. Most of the work is done by a call to an external API. However, I think Lean GPT-f is still probably too much in development right now to do that. (Also, unlike any other tactic, one would have to sign up for access to the API.)
3. Any other ideas?

[Jason Rute]

Sorry! I may have totally misunderstood the problem. Are you having trouble using it in mathlib? I'm trying to set it up now in a mathlib branch to see if it works. (I'm running into trouble, but I also have to go to work...)

[Jesse Michael Han]

it would take a nontrivial amount of work to prepare a PR that could pass review, but one approach that was suggested by @Mario Carneiro is to just copy-paste code in a branch of mathlib until it's in a minimum viable state and let people use that for mathlib development

[Scott Morrison]

As a viable branch of mathlib would be a prerequisite for 2. in any case, this seems like a good option.

[Scott Morrison]

For people to realistically use it (yes, please!) I think eventually PR'ing it into mathlib should be an aspiration.

[Jason Rute]

First, I was being a bit dense yesterday. I now assume the issue is that currently gptf depends on mathlib so it can't be used as a dependency inside mathlib, right? So yes, we either have to move gptf inside mathlib (or a branch), or remove the dependency on mathlib. I don't think the latter would be that hard. As far as I see, we don't use any theorems in mathlib. We just use some convince meta programming code which could be duplicated if needed. Right? I'm really fine with whatever approach is easiest to implement and maintain and most likely to get folks using it.

[Floris van Doorn]

If you move gptf in a branch of mathlib, it can depend on other files in mathlib. All the imports of mathlib files will still work, so that shouldn't be a problem.