Setting up a Lean4 project that can use mathlib3/synport

Stream: new members

[Thomas Murrills]

(I'm not sure if this topic belongs in "new members" or "mathlib4".)

I'd like to import mathlib3 files for use in Lean4 (I don't need the source), but I'm not sure what my actual options are for practically doing this.

My understanding is that mathport/synport allows Lean3 binaries to be used in Lean4. But does this require maintaining a local copy of the entirety of mathlib3-after-synporting? If so, how much space does that take up?

The page for mathport mentions an alternative involving a lake dependency, but I don't quite understand the nitty-gritty of setting this up even after reading the README for lake (or what doing so would actually achieve, or even what being an "artifact" really means).

If the size is prohibitive, is it possible to use VS code with remote repositories somehow to only download the binaries needed for a given project, instead of storing everything locally?

I realize these questions are kind of scattered, and might be XY-problem-esque. Overall, though, any guidance or templates that help with the details of setting up a Lean 4 project that can use mathlib3 would be great! Thanks in advance!