## Stream: general

### Topic: write access to the repository

#### Scott Morrison (Mar 11 2020 at 05:16):

Hi @Bhavik Mehta, I just gave you write access to the repository. (Also --- anyone who has successfully made a PR or two: please ask!)

#### Scott Morrison (Mar 11 2020 at 05:17):

It would be great if you could make PRs by pushing branches to the main repository (i.e. rather than making PRs from a branch on your repository).

#### Scott Morrison (Mar 11 2020 at 05:17):

This has two big advantages.

#### Scott Morrison (Mar 11 2020 at 05:17):

1. Our CI setup will generate oleans for the branch, so when someone checks it out everything should already be compiled.

#### Scott Morrison (Mar 11 2020 at 05:17):

1. It's easier for people to checkout a local copy, as they don't need to add a new remote.

#### Scott Morrison (Mar 11 2020 at 05:18):

No need to modify in progress PRs, but this would be helpful in future.

#### Scott Morrison (Mar 11 2020 at 05:18):

(This goes for everyone contributing... you'll get faster reviews this way. :-)

#### Bhavik Mehta (Apr 15 2020 at 17:39):

Scott Morrison said:

1. Our CI setup will generate oleans for the branch, so when someone checks it out everything should already be compiled.

Is this still true? If so, how do I get this to work? Doing git pull / git checkout (especially when switching between branches of mathlib) recompiles everything and takes ages

#### Bryan Gin-ge Chen (Apr 15 2020 at 17:49):

I believe you can either run leanproject get-cache after switching branches, or you can set up some git hooks which do something like this automatically with leanproject hooks.

#### Johan Commelin (Apr 15 2020 at 17:52):

Or leanproject up after switching branches

Great thanks!

#### Scott Morrison (Apr 16 2020 at 00:40):

[deleted; repeated above]

#### Scott Morrison (Apr 16 2020 at 00:54):

Even betterest, also use git worktree add ... to avoid switching branches

Last updated: May 18 2021 at 17:44 UTC