Zulip Chat Archive

Stream: new members

Topic: Understanding PR github links

rtertr (Sonia) (Mar 25 2023 at 17:31):

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,

Kyle Miller (Mar 25 2023 at 17:37):

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 (Mar 25 2023 at 17:38):

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) (Mar 25 2023 at 17:43):

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 (Mar 25 2023 at 17:44):

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

Kyle Miller (Mar 25 2023 at 17:46):

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) (Mar 25 2023 at 18:00):

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 (Mar 25 2023 at 18:00):

rtertr (Sonia) has marked this topic as resolved.

Kevin Buzzard (Mar 25 2023 at 18:16):

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 (Mar 25 2023 at 18:18):

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 (Mar 25 2023 at 18:23):

rtertr (Sonia) has marked this topic as unresolved.

rtertr (Sonia) (Mar 25 2023 at 18:24):

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

Kevin Buzzard (Mar 25 2023 at 19:17):

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 (Mar 25 2023 at 19:17):

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

rtertr (Sonia) (Mar 26 2023 at 12:15):

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,

Kevin Buzzard (Mar 26 2023 at 12:35):

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.


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


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) (Mar 26 2023 at 13:05):

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 (Mar 26 2023 at 13:08):

What does git checkout master then git pull do?

Kevin Buzzard (Mar 26 2023 at 13:08):

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 (Mar 26 2023 at 13:09):

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) (Mar 26 2023 at 13:13):

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) (Mar 26 2023 at 13:15):

under leanpkg.toml it states

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

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

rtertr (Sonia) (Mar 26 2023 at 13:16):

now it is running leanproject upgrade-mathlib

rtertr (Sonia) (Mar 26 2023 at 13:21):

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

rtertr (Sonia) (Mar 26 2023 at 13:22):

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

Kevin Buzzard (Mar 26 2023 at 13:33):

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) (Mar 26 2023 at 14:24):

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

Eric Wieser (Mar 26 2023 at 14:42):

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) (Mar 26 2023 at 14:44):

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

rtertr (Sonia) (Mar 26 2023 at 14:45):

What should I replace them by? :)

rtertr (Sonia) (Mar 26 2023 at 14:51):

It is just running in orange now :'(

Kevin Buzzard (Mar 26 2023 at 14:56):

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 (Mar 26 2023 at 15:14):

@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 (Mar 26 2023 at 15:15):

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

Last updated: Dec 20 2023 at 11:08 UTC