Zulip Chat Archive

Stream: lean-gptf

Topic: Using gptf in mathlib development

view this post on Zulip Jason Rute (Mar 08 2021 at 13:17):

(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:

view this post on Zulip Jason Rute (Mar 08 2021 at 13:24):

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?

view this post on Zulip Jason Rute (Mar 08 2021 at 14:38):

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...)

view this post on Zulip Jesse Michael Han (Mar 08 2021 at 14:59):

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

view this post on Zulip Scott Morrison (Mar 08 2021 at 22:08):

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

view this post on Zulip Scott Morrison (Mar 08 2021 at 22:08):

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

view this post on Zulip Jason Rute (Mar 09 2021 at 13:23):

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.

view this post on Zulip Floris van Doorn (Mar 09 2021 at 16:54):

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.

Last updated: May 18 2021 at 10:14 UTC