Zulip Chat Archive

Stream: lean-gptf

Topic: Lean GPT-f beta


view this post on Zulip Jesse Michael Han (Jan 18 2021 at 17:14):

The lean-gptf beta is now online! Sign up for an API key here and check out the lean-gptf repository here.

Currently the repository uses a custom fork of Lean 3.23; however, we are planning a new community Lean release soon with all the features needed by the gptf tactic.

view this post on Zulip Bryan Gin-ge Chen (Jan 18 2021 at 18:32):

I managed to get this working in VS Code :tada:

I'm passing the API key to vscode-lean by launching VS Code from the command line with OPENAI_API_KEY=key code . (Actually, I made an alias for this in my profile.)

One slightly annoying thing is that the curl output causes the Lean: Server Errors panel to pop up (see screenshot): Screen-Shot-2021-01-18-at-1.29.35-PM.png

Maybe there's some option you can use that makes curl more silent?

view this post on Zulip Jesse Michael Han (Jan 18 2021 at 18:36):

@Bryan Gin-ge Chen thanks for flagging, pushed a fix so that curl is invoked with the --silent flag --- does this solve the issue?

view this post on Zulip Bryan Gin-ge Chen (Jan 18 2021 at 18:37):

Yes, it does. Thanks!

view this post on Zulip Rob Lewis (Jan 18 2021 at 20:39):

Jesse Michael Han said:

Currently the repository uses a custom fork of Lean 3.23; however, we are planning a new community Lean release soon with all the features needed by the gptf tactic.

This means we need to compile mathlib locally to use it as a dependency in your lean-gptf repo, right?

view this post on Zulip Patrick Massot (Jan 18 2021 at 20:39):

I think the same as Rob: I'll definitely play with this toy, but I'll wait for the Lean release (and mathlib Lean version bump).

view this post on Zulip Rob Lewis (Jan 18 2021 at 20:40):

If you push a mathlib branch that changes leanpkg.toml to use your forked Lean, and then change the leanpkg.toml in lean-gptf to point to that mathlib commit, it should let us use leanproject like normal here

view this post on Zulip Rob Lewis (Jan 18 2021 at 20:42):

Note that I only suggest this because this is a cool toy and I trust Jesse! I'd prefer this not to become a standard way to interact with the CI :)

view this post on Zulip Rob Lewis (Jan 18 2021 at 20:48):

Patrick Massot said:

I think the same as Rob: I'll definitely play with this toy, but I'll wait for the Lean release (and mathlib Lean version bump).

(This isn't what I think btw, I'm compiling locally now)

view this post on Zulip Jesse Michael Han (Jan 18 2021 at 20:59):

Rob Lewis said:

Jesse Michael Han said:

Currently the repository uses a custom fork of Lean 3.23; however, we are planning a new community Lean release soon with all the features needed by the gptf tactic.

This means we need to compile mathlib locally to use it as a dependency in your lean-gptf repo, right?

correct, though this should hopefully only be necessary for a few more days :pray:

view this post on Zulip Rob Lewis (Jan 18 2021 at 21:02):

Bryan Gin-ge Chen said:

I managed to get this working in VS Code :tada:

I'm passing the API key to vscode-lean by launching VS Code from the command line with OPENAI_API_KEY=key code . (Actually, I made an alias for this in my profile.)

@Bryan Gin-ge Chen could you elaborate? What did you do before launching VS Code? Just setting the env variable and then launching from that shell doesn't seem to be enough.

view this post on Zulip Jesse Michael Han (Jan 18 2021 at 21:03):

^you can also set the private meta def OPENAI_API_KEY := some $KEY (in tactic.gptf.gptf) instead of none to hack around this

view this post on Zulip Rob Lewis (Jan 18 2021 at 21:04):

Thanks, that's easier for now

view this post on Zulip Bryan Gin-ge Chen (Jan 18 2021 at 21:21):

@Rob Lewis Hmm, strange, all I did was launch VS Code from the command line with the OPENAPI_API_KEY=my_key code .. The VAR=value should be setting the environment variable for the command that follows, in this case code ..

view this post on Zulip Rob Lewis (Jan 18 2021 at 21:28):

Hmm, alright, thanks. I'll keep fiddling

view this post on Zulip Jesse Michael Han (Jan 28 2021 at 15:52):

Patrick Massot said:

I think the same as Rob: I'll definitely play with this toy, but I'll wait for the Lean release (and mathlib Lean version bump).

@Patrick Massot new Lean release + mathlib version have been bumped, build time should be instantaneous now with leanproject get-mathlib-cache :pray:

view this post on Zulip Patrick Massot (Jan 28 2021 at 16:02):

Great! I'll definitely play with it

view this post on Zulip Stanislas Polu (Jan 29 2021 at 08:11):

Sorry for the small latency in getting the latest invites out. Everyone who requested access should have received an invite by now. Please do not hesitate to reach out if it's not the case.

view this post on Zulip Johan Commelin (Jan 29 2021 at 08:23):

Now that mathlib uses lean-3.26.0 should this be easier to setup?

view this post on Zulip Patrick Massot (Jan 29 2021 at 08:46):

Is there documentation about how to add this as a dependency to an existing project depending on mathlib? Say we want to play with it while working on the liquid tensor experiment, what should we do?

view this post on Zulip Jesse Michael Han (Jan 29 2021 at 14:59):

Patrick Massot said:

Is there documentation about how to add this as a dependency to an existing project depending on mathlib? Say we want to play with it while working on the liquid tensor experiment, what should we do?

now that it uses the same base Lean as mathlib, it's as easy as

leanpkg add jesse-michael-han/lean-gptf

leanpkg configure

leanproject get-mathlib-cache

leanpkg build

then remember to import tactic.gptf :)

view this post on Zulip Jesse Michael Han (Jan 29 2021 at 15:00):

i just checked and it was able to rederive a proof in for_mathlib/linear_algebra in lean-liquid:

lemma reindex_linear_equiv_sum_empty_symm :
  (reindex_linear_equiv (sum_empty _) (sum_empty _)).symm M = from_blocks M 0 0 0 :=
begin
  ext; simp, rcases i; rcases j; simp!,
    { cases j; simp },
    { rcases i with i },
    { cases i }

  -- ext (i|i) (j|j),
  -- { simp only [sum_empty_apply_inl, reindex_linear_equiv_symm_apply, from_blocks_apply₁₁] },
  -- { cases j },
  -- { cases i }
end

view this post on Zulip Jesse Michael Han (Jan 29 2021 at 15:04):

^updated the lean-gptf README as well, thanks for flagging

view this post on Zulip Patrick Massot (Jan 29 2021 at 21:39):

Thanks @Jesse Michael Han!

view this post on Zulip Johan Commelin (Jan 29 2021 at 21:58):

@Jesse Michael Han this is great! thanks a lot

view this post on Zulip Stanislas Polu (Mar 22 2021 at 07:56):

Batch of invites sent today. Sorry for the delay in responding some of the requests submitted at https://forms.gle/WaS7dbGjkP31uhS59


Last updated: May 18 2021 at 11:11 UTC