leanpkg artifact storage location

Stream: general

[Keeley Hoek]

Hi there! Does anyone know of a particular reason why leanpkg copies dependencies into a "_target" directory in the project folder, as opposed to keeping a directory of artifacts in your home directory (e.g. like maven does)? It'd certainly avoid unnecessarily compiling mathlib multiple times when playing around with little projects.

[Reid Barton]

@Sebastian Ullrich ^ ?

[Mario Carneiro]

one of leanpkg add and leanpkg install is a global install

[Sebastian Ullrich]

leanpkg install, but that's intended for use in non-project files

[Kevin Buzzard]

I currently have two projects which are using different versions of mathlib, but I'm not usually in this situation. I'm running something with UGs where we're all using mathlib 3.4.1 because trying to get 25 people to upgrade their mathlibs is a pain when some of them can't even open a terminal. I'm also doing a project which uses bleeding edge mathlib. But if I could have two flavours of mathlib installed globally I'd be happier than I am now, because I often find myself recompiling. I sometimes cheat and copy and paste instead of recompiling.

[Sebastian Ullrich]

@Keeley Hoek I don't think there is a particular reason other than the current leanpkg being the minimum viable product

[Scott Morrison]

Potentially there's a problem for people who work like me, with two repositories repoA and repoB, with repoB depending on a particular commit from repoA, and both repositories change rapidly. In this case in the central ~/.leanpkg directory I suspect we will end up with lots of copies of repoA checked out at different commits.

[Scott Morrison]

This is probably a small price to pay (people in this situation can just clean out that directory every so often?) in exchange for having multiple projects be able to use the same compile version of mathlib, which would be really really lovely.

[Scott Morrison]

I'd be very happy to see central storage in any case.

[Sebastian Ullrich]

What Rust's cargo (which is the direct inspiration for leanpkg) does is it caches downloaded git repositories in a central cache (because these can be shared even if you're using different versions of them in different projects) and then stores build artifacts per project, probably to avoid flooding the central cache, as @Scott Morrison alluded to

[Scott Morrison]

I see, but that wouldn't save on rebuilding mathlib between different projects, which is the real payoff.