Install package

Stream: new members

[Philip Stetson]

I am on a fresh install of Mathlib4 and I git cloned the directory for the new package PACKAGENAME I want to install into ~/mathlib4/lake-packages/PACKAGENAME. Then I ran lake exe cache get and and lake build ... no matter what I still get the error "unknown executable PACKAGENAME". I am not familiar with lake in lean4. I also can't find threads on this, so how I do install this/any new package?

[Ruben Van de Velde]

You're saying you want to make mathlib use a new package or do you want to create a new package that depends on mathlib?

[Philip Stetson]

The latter, I want to install a package which depends on my build of mathlib

[Ruben Van de Velde]

Then the documentation at https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency should be helpful

[Ruben Van de Velde]

In particular, touching anything inside lake-packages manually sets you up for a world of pain

[Shreyas Srinivas]

You can start a new mathlib project from inside vscode now. If you have the lean4 extension installed, and open vscode, you will see a big universal quantifier above your editor window. When you click it, you'll see a menu inside which you'll see the option to start a mathlib dependent project in a fresh folder.

[Philip Stetson]

OK I have both my new package and mathlib as a dependency and I get the error "invalid toolchain name" whenever I run lake exe cache get

[Philip Stetson]

I am not sure how to install the packages correctly