Including updates from recent PR

Stream: new members

[Jakob Scholbach]

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.)?

[Johan Commelin]

@Jakob Scholbach do you have leanproject installed?

[Jakob Scholbach]

yes

[Johan Commelin]

great

[Johan Commelin]

So you can do

git checkout master
leanproject up
git checkout branch_jakob
git merge master

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Jakob Scholbach]

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

[Scott Morrison]

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... :-)

[Benjamin Davidson]

@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)?

[Kevin Buzzard]

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?

[Benjamin Davidson]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Benjamin Davidson]

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

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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.

[Patrick Massot]

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).

[Julian Berman]

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!)

[Mario Carneiro]

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

[Patrick Massot]

Feel free to PR changes to any help message.

[Mario Carneiro]

does the cutoff point depend on the terminal width?

[Julian Berman]

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

[Julian Berman]

this is how you disable that behavior IIRC

[Julian Berman]

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

[Mario Carneiro]

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).