Understanding PR github links

Stream: new members

[rtertr (Sonia)]

Happy weekend everyone,
I have a general question about Github links. Sometimes people send links in which they have proved or are working on proving something.
I am not sure how to approach it, since they are updates and different files. The example I am trying to understand is the following link #18649. I would like to look at the results on my Visual Studio but I am not sure how :D
Kind regards,
Sonia

[Kyle Miller]

A key line there is "mcdoll wants to merge 3 commits into master from mcdoll/schwartz_mul". This is saying that the contents of the PR are in the branch mcdoll/schwartz_mul. If you already have a mathlib repository locally, you can do git checkout mcdoll/schwartz_mul (maybe after a git fetch to synchronize what your local repository knows about all these branches).

[Kyle Miller]

Then you can do something like leanproject get-cache to get the branch's olean cache, so you don't have to recompile everything yourself.

[rtertr (Sonia)]

Kyle Miller said:

If you already have a mathlib repository locally, you can do git checkout mcdoll/schwartz_mul (maybe after a git fetch to synchronize what your local repository knows about all these branches).

I guess I have a local mathlib repository from January. What is a git checkout or fitch? Do I do that on my Visual Studio?:)

[Kyle Miller]

In VS Code, you can go over to Source Control, click the "..." menu, then click Fetch to do the synchronization

[Kyle Miller]

I don't really use VS Code for git, but I think to checkout a particular branch it's "Checkout to" in the same menu?

[rtertr (Sonia)]

Solution I found, in case people in the future are interested.
Clicked on 'files changed'. Under the green button 'review changes', clicked on the three dots, and clicked 'view file'. Copied the file to my Visual Studio :D

[Notification Bot]

rtertr (Sonia) has marked this topic as resolved.

[Kevin Buzzard]

That's not a good solution because the file you're looking at is compatible with a different version of mathlib to the one you randomly pasted it into. The correct approach is the one Kyle explained.

[Kevin Buzzard]

Mathlib undates several times a day and it's important to learn how to keep your local version updated and to get the compiled binaries for it. Within VS Code you can open a terminal at the bottom of your screen (pull up on the blue bar if it's not there) and then use leanproject in that command line.

[Notification Bot]

rtertr (Sonia) has marked this topic as unresolved.

[rtertr (Sonia)]

Okay, great, and then I say upgrade-mathlib? :D

[Kevin Buzzard]

nonono, the only reason you would ever say that is if you are working on a project of your own that has mathlib as a dependency and you want to update the version of mathlib it depends on to get the shiny new goodies that appeared recently.

Can you explain again exactly what it is you want to do? Have you managed to open a terminal in VS Code? It is not hard to do this but if you mess around with random git or leanproject commands then you can really screw up your Lean set-up.

[Kevin Buzzard]

Do you understand how git works? (it's OK if not, I just don't want to mansplain if you do)

[rtertr (Sonia)]

Hello again :big_smile:
No, I don't understand how it works at all. Not familiar with Visual Studio or GitHub, just had a TA help me install Lean on my computer.
I would love to be able to update my library everyday, as I find there are packages I cannot import at the moment.
I tried to make a new project, and import the library again, but when I checked #import topology, it did not find it, so now I went back to my old folder :) I would love to work on GitHub instead of on my computer as well!
Kind regards,
Sonia

[Kevin Buzzard]

So you can think of those github pages as links to "branches" of mathlib. There is a main, or "master" branch, which grows every day, and then other branches come off it where people are experimenting with new additions. If the new additions look good to the person who wrote them, they make a pull request and then the material in the branches is discussed by various people in the community and maybe changes are suggested. When everyone's happy, the relevant branch is "merged" into the master branch and growth continues.

You can't use mathlib without lean files but you also can't use it without olean files, which are compiled lean files. If you try using mathlib without the right olean files then you will end up in "orange bar hell", where the orange "compiling" bars never disappear and Lean become unresponsive.

Usually you just want to stick with the master branch, because this is a non-experimental branch on which everything is guaranteed to work. Lean doesn't work properly unless you're working in a project. There are two kinds of mathematics projects. There is mathlib itself, and then there are projects which depend on mathlib. If you are working on a project which depends on mathlib and you want to start using an experimental branch then this is quite complicated (but possible) so here's the (easier) description of how to work with mathlib itself.

Here's a picture of mathlib open with my cursor on the bottom blue bar.

mathlibterm.png

You can pull that blue bar up to get a terminal (click on "terminal" if it opens on another tab).

mathlibterm2.png

In this terminal you can type the commands which Kyle described above. Common ones for me are:

git pull (to update all your lean files, note that now your oleans are incompatible and you'll be in orange bar hell until you do the next thing)

leanproject get-cache (this will download the oleans for the branch you're on)

You usually want to be on the master branch:

git checkout master (again this will put you in orange bar hell unless you follow with leanproject get-cache)

git checkout mcdoll/schwartz_mul (this will put you on the branch for the PR you mentioned above).

After changing branches I always do git pull (to get the branch up to date) and then leanproject get-cache (to get the olean files). When you've finished with the terminal you can just close it with the X in the top right of the pane.

[rtertr (Sonia)]

That's great! But when I do git pull I get this message:
$ git pull
There is no tracking information for the current branch.

See git-pull(1) for details.

    git pull <remote> <branch>

If you wish to set tracking information for this branch you can do so with:

    git branch --set-upstream-to=<remote>/<branch> master

Then if I do this, I get

$ git branch --set-upstream-to=<remote>/<branch> master
bash: remote: No such file or directory

Also I tried get-cache

$ leanproject get-cache
Reference at 'refs/heads/master' does not exist

[Kevin Buzzard]

What does git checkout master then git pull do?

[Kevin Buzzard]

And more importantly what is your project? Is it mathlib or a project which depends on mathlib? What are the contents of your leanpkg.toml? That file contains this sort of data.

[Kevin Buzzard]

If you are on a project of your own which depends on mathlib then you can do leanproject upgrade-mathlib and this will get you back on track with today's mathlib master branch, but playing with a different branch of mathlib in your own project is harder; it's easier just to wait for the mathlib PR to be merged to master.

[rtertr (Sonia)]

it gives

$ git checkout master
error: pathspec 'master' did not match any file(s) known to git

and then the same message as before

[rtertr (Sonia)]

under leanpkg.toml it states

[package]
name = "my_project"
version = "0.1"
lean_version = "leanprover-community/lean:3.50.3"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "d7943885503965d07ccaeb390d65fbc3f45962e6"}

[rtertr (Sonia)]

now it is running leanproject upgrade-mathlib

[rtertr (Sonia)]

Now I can import new pages such as analysis.fourier.fourier_transform so that's great:)

[rtertr (Sonia)]

But yeah, I would love to start a new project where I could look at the current updates

[Kevin Buzzard]

Yeah you are not working in mathlib, you are working on a project which depends on mathlib.

Why not just get yourself a copy of mathlib itself, by changing directory on the command line to a directory which is not inside your project (e.g. cd .. will put you in the directory where my_project is) and then leanproject get mathlib wil get you a copy of today's mathlib. Then you can open that folder in VS Code and switch between mathlib branches.

[rtertr (Sonia)]

yes, that might be the right thing to do :D

[Eric Wieser]

rtertr (Sonia) said:

Then if I do this, I get

$ git branch --set-upstream-to=<remote>/<branch> master
bash: remote: No such file or directory

The message was expecting you to replace the placeholders <remote> and <branch>. You didn't replace them, so bash is now getting confused by the <>s

[rtertr (Sonia)]

hmm, I see :D I am currently stuck, it is orange for quite some time now :(

[rtertr (Sonia)]

What should I replace them by? :)

[rtertr (Sonia)]

It is just running in orange now :'(

[Kevin Buzzard]

right, you're in orange bar hell. If this is a project which depends on mathlib then leanproject get-mathlib-cache will fix it. If it's mathlib itself then leanproject get-cache will fix it. In both cases you should restart VS Code after the command has finished (it may take a minute or so, depending on things like your internet speed; don't close the terminal until you have a new prompt).

[Patrick Massot]

@rtertr (Sonia) I didn't carefully read all that discussion but I think people are making things more complicated than they need to be. If you simply want to play with code from Moritz then you can open a terminal and type leanproject get mathlib:mcdoll/schwartz_mul. This will create a folder mathlib_mcdoll/schwartz_mul with the content of mathlib as it appears in this PR, including compiled oleans. Then you can simply type code mathlib_mcdoll/schwartz_mul and start exploring files.

[Patrick Massot]

Note that the PR page also contains a link "Open in gitpod" that is very often sufficient to explore the changes interactively.