Zulip Chat Archive

Stream: new members

Topic: How to get _target directory after checking out from github?

Martin C. Martin (Jun 20 2023 at 18:31):

I did a fresh checkout of my project from github. It has a leanpkg.toml file describing a dependency on mathlib. How do I check this out, i.e. _target/deps directory that contains the specified version of mathlib?

Kevin Buzzard (Jun 20 2023 at 18:33):

leanproject get-mathlib

Patrick Massot (Jun 20 2023 at 18:41):

This shouldn't be necessary if you use leanproject get username/projectname to get the project from GitHub.

Martin C. Martin (Jun 20 2023 at 18:43):

Oh interesting, thanks!

Last updated: Dec 20 2023 at 11:08 UTC