gptf

Stream: new members

[Alex Zhang]

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]

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]

I asked this in #lean-gptf