Zulip Chat Archive

Stream: general

Topic: write access to the repository


view this post on Zulip 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!)

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Mar 11 2020 at 05:17):

This has two big advantages.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 11 2020 at 05:18):

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

view this post on Zulip Scott Morrison (Mar 11 2020 at 05:18):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 15 2020 at 17:52):

Or leanproject up after switching branches

view this post on Zulip Bhavik Mehta (Apr 15 2020 at 18:10):

Great thanks!

view this post on Zulip Scott Morrison (Apr 16 2020 at 00:40):

[deleted; repeated above]

view this post on Zulip 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