Zulip Chat Archive

Stream: new members

Topic: Including updates from recent PR


view this post on Zulip Jakob Scholbach (Mar 19 2021 at 08:08):

I'm in the middle of working on a PR (#6671). I want to use / refer to recent changes that were made in another PR #6753.

  1. How do I conveniently update my copy of mathlib in my own PR? (In this particular case I could just manually copy the file changed in the other PR #6753, but I'm sure this is not how one is supposed to do it).
  2. How do I make sure updating my local mathlib copy in the PR is not eventually regarded as part of the submission of my own PR? (There is no overlap in the files touched by the two PRs.)?

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:09):

@Jakob Scholbach do you have leanproject installed?

view this post on Zulip Jakob Scholbach (Mar 19 2021 at 08:09):

yes

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:09):

great

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:10):

So you can do

git checkout master
leanproject up
git checkout branch_jakob
git merge master

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:11):

That will merge the newest version of master into your branch, and on the branch you will then have oleans from master. So you need to leanproject build to get oleans for you branch

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:11):

But if you change just 1 or 2 files, that is usually quite fast

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:12):

Git will take care of doing something sensible (when there is no overlap) so you don't have to worry about Q2

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:12):

If there is overlap, git will tell you during the git merge master, and ask you to resolve the conflicts.

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:13):

Now, if you have two branches, say exp_char and sep_degree, then you first do this process for exp_char, and then afterwards you do

git checkout sep_degree
git merge exp_char
git push

view this post on Zulip Johan Commelin (Mar 19 2021 at 08:13):

And that will make the 2nd PR incorporate all the changes made to PR 1

view this post on Zulip Jakob Scholbach (Mar 19 2021 at 08:25):

Works great, thanks! (Might be part of that tiny tutorial...)

view this post on Zulip Scott Morrison (Mar 19 2021 at 12:49):

If you make a pull request for the 2nd branch before the 1st branch's pull request has been merged, you'll also need to remember to note this in the pull request summary. (Read the template, it shows the format for describing dependent PRs.) (And then be patient... :-)

view this post on Zulip Benjamin Davidson (Mar 21 2021 at 02:51):

@Johan Commelin What does "leanproject up" do? Is that essentially the same as git pull (which is what I have been using at that point when merging)?

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:13):

Might depend on whether you're working in mathlib or in your own repo with mathlib as a dependency. If in your own repo it might well update the mathlib dependency to the latest mathlib and possibly download oleans too. What does leanproject --help say?

view this post on Zulip Benjamin Davidson (Mar 21 2021 at 08:21):

I generally work in mathlib. leanproject --help says "Upgrade mathlib (as a dependency or as the main..." for the command upgrade-mathlib.

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:23):

I never use the command when I'm working on mathlib, for me this is a command to bump mathlib when it's a dependency

view this post on Zulip Kevin Buzzard (Mar 21 2021 at 08:24):

If you have master checked out then I could imagine it would be the same as git pull followed by leanproject get-cache but you can easily find out by experimenting

view this post on Zulip Benjamin Davidson (Mar 21 2021 at 10:02):

Okay thanks! Was just curious to learn a new/potentially better way of doing things.

view this post on Zulip Julian Berman (Mar 21 2021 at 15:32):

That's somewhat annoying --help behavior (which obviously isn't leanproject's fault, I think it's a bad click default IIRC)

view this post on Zulip Julian Berman (Mar 21 2021 at 15:33):

But here's the code (and full docstring): https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/leanproject.py#L103 which calls https://github.com/leanprover-community/mathlib-tools/blob/master/mathlibtools/lib.py#L537-L540

view this post on Zulip Julian Berman (Mar 21 2021 at 15:33):

so it does appear it does slightly different things depending on if you're working on mathlib or not -- for mathlib it looks like it should just run git pull for the current branch and then fetch oleans. For not-mathlib it looks like it should discard local changes to mathlib as a dependency, then run leanpkg upgrade (which will update all dependencies, including mathlib), then fetch oleans for mathlib. And then thirdly if you run this outside a project repo it looks like it will upgrade a user-wide (i.e. non-project specific) mathlib install.

view this post on Zulip Patrick Massot (Mar 21 2021 at 21:06):

Julian Berman said:

That's somewhat annoying --help behavior (which obviously isn't leanproject's fault, I think it's a bad click default IIRC)

What is the annoying --help behavior? Truncating the help message? You can get the full version using leanproject upgrade-mathlib --help. About general remarks concerning click, note that I've very careful to separate the leanproject library from the client. One goal was to allow building more tools on top of the library, but the other was making sure we could change the client part in case we can find something better than click (or someone has courage to write custom code).

view this post on Zulip Julian Berman (Mar 21 2021 at 21:18):

Yeah, truncating --help without running it on the subcommand (I think it should just wrap and cut off at some much longer length even when you run it on the top level command) -- and FWIW I wasn't questioning the click choice, it's the best of the options, I just don't like this behavior. (And if I haven't said so before I find leanproject in general quite reasonably written!)

view this post on Zulip Mario Carneiro (Mar 21 2021 at 21:23):

Perhaps the help text could be changed so that it cuts off at a more reasonable point?

view this post on Zulip Patrick Massot (Mar 21 2021 at 21:27):

Feel free to PR changes to any help message.

view this post on Zulip Mario Carneiro (Mar 21 2021 at 21:28):

does the cutoff point depend on the terminal width?

view this post on Zulip Julian Berman (Mar 21 2021 at 21:30):

https://github.com/ansible-community/molecule/pull/2768/files#diff-2517335dce22ba8b2a7f7afd8ea59cad2997aa523b1c981031c22965b86b3856R221

view this post on Zulip Julian Berman (Mar 21 2021 at 21:30):

this is how you disable that behavior IIRC

view this post on Zulip Julian Berman (Mar 21 2021 at 21:31):

(if I get some cycles and someone else doesn't get to it first I can get to that at some point)

view this post on Zulip Mario Carneiro (Mar 21 2021 at 21:32):

It looks like the existing text is just barely over the limit (78-ish characters?). You could drop a word and bring it under that

  upgrade-mathlib    Upgrade mathlib (as a dependency or the main project).

Last updated: May 16 2021 at 21:11 UTC