Zulip Chat Archive

Stream: general

I really don't understand how the _target directory works

I want to help Kevin so I clone his repo

Of course it depends on mathlib

So I try to copy _target from my own projects to avoid compiling mathlib

and it doesn't seem to work

or maybe it does

it seemed like VScode was taking forever to compile

which seemed like it was compiling lots of files

but maybe it was only Kevin's code

I have symlinked the _target dir before. It seems to work fine.

Last updated: Dec 20 2023 at 11:08 UTC