Zulip Chat Archive

Stream: general

Topic: multiple dependencies

Kevin Buzzard (Jul 21 2019 at 22:52):

I wanted to make a project which had Ramon's schemes repo as a dependency. Ramon's repo has mathlib as a dependency. I tried making them both dependencies of my projet but I couldn't get mathlib imports working in Ramon's repo. I'm sure there will be a standard way to set this up.

Kevin Buzzard (Jul 21 2019 at 23:02):

How many leanpkg.path files should there be in such a set-up?

Last updated: Dec 20 2023 at 11:08 UTC