leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: gptf


Alex Zhang (Jul 11 2021 at 19:03):

I have trouble setting up the gptf. Where should I run the command leanpkg configure && leanpkg build?
image.png
https://github.com/jesse-michael-han/lean-gptf

Alex Zhang (Jul 11 2021 at 19:05):

I ran this command in a new lean project, but then I did not find the file src/example.lean in the next step.

Alex Zhang (Jul 11 2021 at 20:14):

I asked this in #lean-gptf


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll