write access to the repository

Stream: general

[Scott Morrison]

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]

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]

This has two big advantages.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Bhavik Mehta]

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]

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]

Or leanproject up after switching branches

[Bhavik Mehta]

Great thanks!

[Scott Morrison]

[deleted; repeated above]

[Scott Morrison]

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