A technical question

Stream: general

[Ned Summers]

Hey all. A more technical question, I'm working in category theory (very new to this) and I think I want to fork Scott Morrison's mathlib (https://github.com/semorrison/lean-category-theory) as hardly anything is on the regular mathlib yet. I'm using VS code on my own windows laptop but I'm really amateur with pretty much any of the technical aspect (command line and upwards) so I'm not really sure how to even begin on this. I installed Lean (nightly) and mathlib from a tutorial originally. If anyone could even just direct me to what to google/a tutorial, I'd really appreciate it.

[Reid Barton]

You should be able to follow the instructions at https://github.com/kbuzzard/lean-stacks-project/ with obvious adjustments