compling one file in a project

Stream: lean4

[Kevin Buzzard]

Right now I'm playing around a lot with mathlib4, which takes a few minutes to compile. Sometimes I want to switch between branches quickly and just see what happens if I compile one specific file. In Lean 3 I could just do lean --make src/file/I/want/to/test.lean on the command line and generate the relevant oleans so that if I e.g. then crash VS Code with a large amount of trace output (which I just did) then I can just fire it up again and the file I'm testing compiles instantly. Is there a way of doing this in Lean 4 or am I thinking about things in the wrong way? If I type lake build then I end up building all of mathlib, which I don't want to do, and I'm always nervous about breaking out of lake build during the build process in case I end up with a borked repo.

[Ruben Van de Velde]

lake build +Mathlib.Algebra.Hom.GroupInstancesseems to work

[Kevin Buzzard]

Thank you so much!