leanpkg and leanproject

Stream: new members

[Michael Beeson]

As Alex recommended I used "leanproject build" to compile my project (but only after a detour that involved recursively getting pipx and the Xcode command line tools installed). Fine, but there is also leanpkg. Is it now obsolete and superseded by leanproject? Or do the two serve different purposes?

[Bryan Gin-ge Chen]

leanproject should (eventually?) be able to do everything that leanpkg does. It's discussed a little bit on the page on the Lean tool chain.

[Michael Beeson]

Thanks. I note from that page: "For historical reasons, leanproject still calls leanpkg for some simple operations". Therefore leanpkg is not obsolete.

By the way, when I originally installed lean I tried to follow instructions, but
Lean installation broke on installing elan; eventually I downloaded elan directly from github,
bypassing the certificate-store problem that had blocked installation. So by this work-around I guess the
path to leanproject never got stored. Hence this morning's wrestling match with homebrew, pipx, Xcode command-line tools, etc. Anyway, all's well that ends well. But just for the record, the recommended installation instructions hit some "certificate store problem" and didn't work.

[Bryan Gin-ge Chen]

Thanks for the report. Do you remember any other details about the error message? I don't think we've seen that one before.

[Michael Beeson]

no, that was last April and I didn't make a complete record of my struggles.
By the way, after successfully compiling my project once, it failed later; mysteriously the path to leanpkg in Users/Beeson/.elan/bin
wasn't found; after adding it to my bash profile file it worked again. There's a file in my project directory called leanpkg.path.
I didn't manage to edit it successfully. I don't know where it came from, either, but it doesn't contain any valid path to leanpkg.
I emphasize, my system is working so there is no question in this post. Compiling it also solved my speed/responsiveness problems
so I am good to go!

[Bryan Gin-ge Chen]

leanpkg.path is what Lean actually looks at to find the olean files. It's generated from leanpkg.toml by leanpkg and leanproject and should almost never be edited by hand.