get-mathlib-at-commit

Stream: general

[Yakov Pechersky]

We've had a lot of messages recently about people wanting to point their mathlib dep at a certain branch or commit. The directions have sometimes been: descend into the mathlib dep repo, git checkout the commit, make sure the toml points to that commit, leanproject get-m, possibly other steps. Should there be a leanproject get-m-at ... that can take a branch name, PR #, or commit hash? It would also fetch the built oleans. I'm starting to take a look at the git python library to see how leanproject currently does HEAD fetching.

[Floris van Doorn]

I have a related request: in the mathlib directory, I often want to do leanproject get-cache at a certain commit. My current workflow is the following, but I would also like something like leanproject get-cache origin/foo or something. (This typically happens when I have a few commits on top of a branch origin/foo.)

git checkout origin/foo
leanproject get-cache
git checkout <previous-branch>

[Gabriel Ebner]

It would be great if get-cache could default to HEAD and try any of the last 10 commits.

[Patrick Massot]

Please open issues (or PRs!). I'll try to find some leanproject time soonish.

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib-tools/issues/77

[Yakov Pechersky]

I've been trying to understand how get-mathlib-cache works currently, there's some implicit reliance on HEAD that I've been trying to understand how to modify. No PR yet, unfortunately.

[Patrick Massot]

Gabriel Ebner said:

It would be great if get-cache could default to HEAD and try any of the last 10 commits.

I've found some time to work on leanproject today. Earlier I cleanup a bit the list of open PRs and issues, and now I'm turning to feature requests. I'd like to work on that one, but I find it too poorly specified. What do you want if the current commit has several parents?

[Patrick Massot]

Note that this feature request is also dangerous if files are deleted. If leanproject is asked for cache and don't find it, then checks out an old commit, get oleans and checks out the head commit again then you'll get zombie oleans for any files that was deleted in the mean time. We could probably call delete-zombies as an intermediate step.

[Patrick Massot]

In fact I would probably need more explanations about the kind of workflow that triggers this need. I'm doing blind thinking here because I never see this need (neither when working on mathlib nor when working on the sphere eversion project that depends on mathlib).

[Bryan Gin-ge Chen]

What do you want if the current commit has several parents?

You could stop with an error, listing the possibilities (then the user has to specify the hash when calling leanproject again). Or you could even prompt the user to choose from the list of options.

[Bryan Gin-ge Chen]

In fact I would probably need more explanations about the kind of workflow that triggers this need.

I'm less sure about trying previous commits by default, but for getting the cache at a specific commit, see e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Refresh.20mathlib.20in.20local.20branch/near/212683837

[Eric Wieser]

Being forced to choose between the multiple parents sounds like the right choice to me.

[Patrick Massot]

Do I understand correctly that all those scenarios involve working on mathlib itself?

[Bryan Gin-ge Chen]

Yes, at least in my experience.

[Patrick Massot]

There are infinitely many ways to mess up with git, and we cannot turn leanproject into a full git frontend (and this would probably make things more complicated). But I think we could add the following two commands:

[Patrick Massot]

For people who want to start on some new contribution, leanproject pr my_branch would do:

• check repo is clean
• git checkout master
• git pull
• leanproject get-cache
• git checkout -b my_branch

[Patrick Massot]

For people who started work on some contribution on branch my_branch (or got it from leanproject get) but want to incorporate changes from master, leanproject rebase would do:

• get name of current branch my_branch, check it's not master
• check repo is clean
• git checkout master
• git pull
• leanproject get-cache
• git checkout my_branch
• git rebase master

Note how git rebase is the last command so hopefully any git mess can be sorted out without leanproject-added difficulty.

[Patrick Massot]

How does that sound?

[Patrick Massot]

And for more fine-tuned dangerous stunts, I can add an optional argument to leanproject get-mathlib-cache and leanproject get-cache that is a git sha, try to unpack the corresponding archive and run delete-zombie.

[Eric Wieser]

Are multiple local caches supported at the moment? Or is only the most recent kept locally?

[Bryan Gin-ge Chen]

Yes, they're all saved in .mathlib/. (Which reminds me, I should probably clean it up on my computer.)

[Eric Wieser]

If so, then the behavior that makes the most sense for me for get-cache is:

get-cache <commitish=HEAD>: find and download all caches that are the first in each line of ancestors from the current commit. If this is exactly one cache, activate it. If not, print out all the downloaded sha1s and ask the user to run the command again.

[Patrick Massot]

We could also check at each get-cache how many files there are in the cache and propose to delete the oldest when there are more that 50 or something. But we would need to find a way not to keep asking if people want to keep their cache.

[Patrick Massot]

I pushed these three new features, but there are not well tested at all. It would be nice if people who asked for this could test before release (it means you need to clone the repository and pip install from there). @Eric Wieser @Gabriel Ebner @Floris van Doorn @Yakov Pechersky

[Patrick Massot]

See leanproject pr --help, leanproject rebase --help and leanproject get-cache --help.

[Patrick Massot]

And let me repeat that using the --rev option of get-cache (and get-mathlib-cache) is at your own risk. I very much prefer workflows (as in pr and rebase) rather than hacking around randomly.

[Eric Wieser]

Thanks for the --rev command, I'll certainly be using that

[Patrick Massot]

I'm still interested in reading the workflow that makes you need that option.

[Eric Wieser]

My workflow is typically jumping between different branches, and wanting to get a cache copy of mathlib from either: a) the head or head~n commit of that branch, or b) the last copy of origin/master I merged into that branch

[Eric Wieser]

Where the choice between a) and b) depends how deep within mathlib my change is

[Patrick Massot]

When do you want to do that and leanproject pr or leanproject rebase wouldn't suffice?

[Eric Wieser]

I don't really like to let other scripts touch my working tree through git, and prefer to be in control of that myself - it makes it easier for me to recover from things like forgetting to switch branch before editing

[Patrick Massot]

leanproject is already doing that anyway. But your answer is enough for me, it means you want something hackish/low level, and hopefully you now have it.

[Eric Wieser]

In what sense is it doing it already? I suppose I've only run get-cache and delete-zombies in the last few weeks...

[Patrick Massot]

get-cache is overwriting your lean files.

[Eric Wieser]

It is? I thought it only overwrote olean files. (I'm using it mainly in mathlib)

[Bryan Gin-ge Chen]

I think caches did contain .lean files until a few months ago (#3616), but caches generated since then don't.

[Bryan Gin-ge Chen]

I remember @Rob Lewis talking about possibly changing leanproject to only extract .olean files from the archive, and that seemed like a good idea to me.

[Patrick Massot]

This is independent, get-mathlib-cache still does git reset --hard in the _target folder.

[Eric Wieser]

The target folder is git-ignored though, so morally doesn't feel like part of the working tree

[Eric Wieser]

I can confirm that --rev worked for me - thanks for adding that!

It would be great if it could resolve commitish objects for me; so I could write

leanproject get-cache --rev eric-wieser/monoid_algebra-reorder

instead of

leanproject get-cache --rev $(git rev-parse eric-wieser/monoid_algebra-reorder)

[Patrick Massot]

@Eric Wieser can you try with current master?

[Eric Wieser]

Patch looks good to me, thanks! Will try it later or tomorrow.

[Floris van Doorn]

I will try out these new features tomorrow. They are indeed exactly what I need for my workflow (which is indeed when working on mathlib itself), and they look great! My use cases will be:

• leanproject pr to make a new branch
• leanproject rebase to update my branch to the newest mathlib, while getting the best available olean files.
• leanproject get-cache --rev HEAD~n or leanproject get-cache --rev origin/master: I'm a couple commits ahead in my branch than origin and I need to get the best available olean files (either because I switched between branches or I messed something up). This will also be quicker than leanproject rebase because it usually doesn't require downloading new files.

[Gabriel Ebner]

Patrick Massot said:

Gabriel Ebner said:

It would be great if get-cache could default to HEAD and try any of the last 10 commits.

[..] I find it too poorly specified. What do you want if the current commit has several parents?

It should ask both of the parents (and grandparents, etc.) for oleans. My usecase is that I clone a PR branch from github where the author has just merged master, and I'd like leanproject to find a "close" commit with oleans. It doesn't matter if it's the previous commit on the branch, or on master. In this case, really anything is better than nothing.

[Gabriel Ebner]

Patrick Massot said:

Note that this feature request is also dangerous if files are deleted. If leanproject is asked for cache and don't find it, then checks out an old commit, get oleans and checks out the head commit again then you'll get zombie oleans for any files that was deleted in the mean time.

Indeed, this seems really dangerous. I would have expected that leanproject just unpacks the olean tarball without checking out different commits.

[Eric Wieser]

My understanding was that with the --rev argument, leanproject does no "checking out" at all

[Gabriel Ebner]

Maybe to illustrate my workflow issue, I just wanted to check out Eric's branch:

$ leanproject get mathlib:eric-wieser/monoid_algebra-tweaks
... Failed to download ...
$ cd mathlib_eric-wieser/monoid_algebra-tweaks/
$ leanproject get-mathlib-cache --rev=HEAD^
... Found mathlib oleans ...

Ideally, leanproject get would have tried a few commits so that I don't have to guess HEAD^. But --rev is already a big improvement.

[Gabriel Ebner]

Eric Wieser said:

My understanding was that with the --rev argument, leanproject does no "checking out" at all

The current implementation seems to be more sensible than the description I responded to, yes.

[Eric Wieser]

I think the algorithm for finding caches ought to be something like:

def find_parents(c):
    # breadth first search to find parents
    found = {}
    visited = set()
    queue = {c}
    while queue:
        new_queue = set()
        visited |= set(queue)
        for commit in queue:
            try:
                found[commit] = download(commit)
            except NotFound:
                new_queue |= set(commit.parents) - visited
        queue = new_queue

    # Prune ancestors - if a build is found for C and A, then we always prefer C
    #
    # A -- B -- D -- E
    #  \       /
    #   C------
    return {
        commit: cache
        for commit, cache in found.items()
        if not any (commit.is_ancestor_of(commit_2) for commit_2 in found)
    }

[Gabriel Ebner]

There's also the super-simple version in fetch_olean_cache.sh used for CI. It runs git log -20 (last 20 commits) and picks the first commit which has oleans.

[Floris van Doorn]

On Windows. What am I doing wrong?

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ python3 -m pip uninstall mathlibtools
Found existing installation: mathlibtools 0.0.5
Uninstalling mathlibtools-0.0.5:
  Would remove:
    c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\mathlibtools-0.0.5.dist-info\*
    c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\mathlibtools\*
    c:\users\floris\appdata\local\programs\python\python37-32\scripts\leanproject.exe
Proceed (y/n)? y
  Successfully uninstalled mathlibtools-0.0.5

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ python3 -m pip install mathlibtools
Collecting mathlibtools
  Downloading mathlibtools-0.0.10-py3-none-any.whl (21 kB)
Requirement already satisfied: certifi in c:\users\floris\appdata\roaming\python\python37\site-packages (from mathlibtools) (2019.6.16)
Requirement already satisfied: PyGithub in c:\users\floris\appdata\roaming\python\python37\site-packages (from mathlibtools) (1.43.7)
Requirement already satisfied: toml>=0.10.0 in c:\users\floris\appdata\roaming\python\python37\site-packages (from mathlibtools) (0.10.0)
Requirement already satisfied: PyYAML>=3.13 in c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages (from mathlibtools) (5.1.2)
Requirement already satisfied: pydot in c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages (from mathlibtools) (1.4.1)
Requirement already satisfied: requests in c:\users\floris\appdata\roaming\python\python37\site-packages (from mathlibtools) (2.22.0)
Requirement already satisfied: gitpython>=2.1.11 in c:\users\floris\appdata\roaming\python\python37\site-packages (from mathlibtools) (2.1.11)
Requirement already satisfied: Click in c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages (from mathlibtools) (7.1.1)
Requirement already satisfied: networkx in c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages (from mathlibtools) (2.3)
Requirement already satisfied: tqdm in c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages (from mathlibtools) (4.45.0)
Requirement already satisfied: deprecated in c:\users\floris\appdata\roaming\python\python37\site-packages (from PyGithub->mathlibtools) (1.2.5)
Requirement already satisfied: pyjwt in c:\users\floris\appdata\roaming\python\python37\site-packages (from PyGithub->mathlibtools) (1.7.1)
Requirement already satisfied: pyparsing>=2.1.4 in c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages (from pydot->mathlibtools) (2.4.7)
Requirement already satisfied: idna<2.9,>=2.5 in c:\users\floris\appdata\roaming\python\python37\site-packages (from requests->mathlibtools) (2.8)
Requirement already satisfied: chardet<3.1.0,>=3.0.2 in c:\users\floris\appdata\roaming\python\python37\site-packages (from requests->mathlibtools) (3.0.4)
Requirement already satisfied: urllib3!=1.25.0,!=1.25.1,<1.26,>=1.21.1 in c:\users\floris\appdata\roaming\python\python37\site-packages (from requests->mathlibtools) (1.25.3)
Requirement already satisfied: gitdb2>=2.0.0 in c:\users\floris\appdata\roaming\python\python37\site-packages (from gitpython>=2.1.11->mathlibtools) (2.0.5)
Requirement already satisfied: decorator>=4.3.0 in c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages (from networkx->mathlibtools) (4.4.0)
Requirement already satisfied: wrapt<2,>=1 in c:\users\floris\appdata\roaming\python\python37\site-packages (from deprecated->PyGithub->mathlibtools) (1.11.2)
Requirement already satisfied: smmap2>=2.0.0 in c:\users\floris\appdata\roaming\python\python37\site-packages (from gitdb2>=2.0.0->gitpython>=2.1.11->mathlibtools) (2.0.5)
Installing collected packages: mathlibtools
Successfully installed mathlibtools-0.0.10

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ leanproject --version
leanproject, version 0.0.10

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ leanproject get-cache -h
Usage: leanproject get-cache [OPTIONS]

  Restore cached olean files.

Options:
  --force     Get cache even if the repository is dirty.
  -h, --help  Show this message and exit.

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ leanproject rebase -h
Usage: leanproject [OPTIONS] COMMAND [ARGS]...
Try 'leanproject -h' for help.

Error: No such command 'rebase'.

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ leanproject pr --help
Usage: leanproject [OPTIONS] COMMAND [ARGS]...
Try 'leanproject -h' for help.

Error: No such command 'pr'.

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ leanproject -h
Usage: leanproject [OPTIONS] COMMAND [ARGS]...

  Command line client to manage Lean projects depending on mathlib. Use
  leanproject COMMAND --help to get more help on any specific command.

Options:
  -u, --from-url TEXT   Override base url for olean cache.
  -f, --force-download  Download olean cache without looking for a local
                        version.

  --no-lean-upgrade     Do not upgrade Lean version when upgrading mathlib.
  --debug               Display python tracebacks in case of error.
  --version             Show the version and exit.
  -h, --help            Show this message and exit.

Commands:
  add-mathlib        Add mathlib to the current project.
  build              Build the current project.
  check              Check mathlib oleans are more recent than their sources
  clean              Delete all olean files
  decls              List declarations seen from this project If no file...
  delete-zombies     Delete zombie oleans, .olean files with no matching...
  get                Clone a project from a GitHub name or git url.
  get-cache          Restore cached olean files.
  get-mathlib-cache  If mathlib is a dependency, upgrade mathlib lean and...
  global-install     Install mathlib user-wide.
  global-upgrade     Upgrade user-wide mathlib
  hooks              Setup git hooks for the current project.
  import-graph       Write an import graph for this project.
  mk-all             Creates all.lean importing everything from the project.
  mk-cache           Cache olean files.
  new                Create a new Lean project and prepare mathlib.
  set-url            Set the default url where oleans should be fetched.
  upgrade-mathlib    Upgrade mathlib (as a dependency or as the main...

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ leanproject --version
leanproject, version 0.0.10

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ cd ../mathlib
leanproject pr
Floris@MSI MINGW64 /d/projects/mathlib ((665cc13c0...))
$ leanproject pr foo
Usage: leanproject [OPTIONS] COMMAND [ARGS]...
Try 'leanproject -h' for help.

Error: No such command 'pr'.

Floris@MSI MINGW64 /d/projects/mathlib ((665cc13c0...))
$

[Floris van Doorn]

My impression from the README from https://github.com/leanprover-community/mathlib-tools was that if I ran

 python3 -m pip install mathlibtools

in the directory of /mathlib-tools I magically got the version from my repo. If that is false, how do I actually use the leanproject from the cloned repository?

[Floris van Doorn]

Ok, I fixed the above issue. The incantation is

Floris@MSI MINGW64 /d/projects/mathlib-tools (master)
$ pip3 install .

That should probably be mentioned in the README.

[Floris van Doorn]

Oh, I see now: that is the last sentence of the README.

[Floris van Doorn]

Some comments:

• Both leanproject rebase and leanproject pr work fine in the default case.
• They could print trace messages saying what it's doing (Checking out master...). Now they are just silent while they are pulling mathlib. They are also silent when the repo is dirty.
• Both of the following give an error

$ leanproject pr foo --debug
$ leanproject pr --debug foo

• Non-graceful error if branch foo already exists:

Floris@MSI MINGW64 /d/projects/mathlib (foo)
$ leanproject --debug pr foo
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/9379050719fa9f2605289bd85a0fb29100084eb3.tar.xz\xa0to C:\Users\Floris\.mathlib\9379050719fa9f2605289bd85a0fb29100084eb3.tar.xz
100%|##########| 30.1M/30.1M [00:06<00:00, 4.67MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/
Traceback (most recent call last):
  File "C:\Users\Floris\AppData\Local\Programs\Python\Python37-32\Scripts\leanproject-script.py", line 11, in <module>
    load_entry_point('mathlibtools==0.0.10', 'console_scripts', 'leanproject')()
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\mathlibtools\leanproject.py", line 359, in safe_cli
    handle_exception(err, str(err))
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\mathlibtools\leanproject.py", line 63, in handle_exception
    raise exc
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\mathlibtools\leanproject.py", line 357, in safe_cli
    cli() # pylint: disable=no-value-for-parameter
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\click\core.py", line 829, in __call__
    return self.main(*args, **kwargs)
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\click\core.py", line 782, in main
    rv = self.invoke(ctx)
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\click\core.py", line 1259, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\click\core.py", line 1066, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\click\core.py", line 610, in invoke
    return callback(*args, **kwargs)
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\mathlibtools\leanproject.py", line 342, in pr
    proj().pr(branch_name, force)
  File "c:\users\floris\appdata\local\programs\python\python37-32\lib\site-packages\mathlibtools\lib.py", line 759, in pr
    self.repo.git.checkout('-b', branch_name)
  File "C:\Users\Floris\AppData\Roaming\Python\Python37\site-packages\git\cmd.py", line 548, in <lambda>
    return lambda *args, **kwargs: self._call_process(name, *args, **kwargs)
  File "C:\Users\Floris\AppData\Roaming\Python\Python37\site-packages\git\cmd.py", line 1014, in _call_process
    return self.execute(call, **exec_kwargs)
  File "C:\Users\Floris\AppData\Roaming\Python\Python37\site-packages\git\cmd.py", line 825, in execute
    raise GitCommandError(command, status, stderr_value, stdout_value)
git.exc.GitCommandError: Cmd('git') failed due to: exit code(128)
  cmdline: git checkout -b foo
  stderr: 'fatal: A branch named 'foo' already exists.'

• leanproject rebase errors on merge conflicts (the expected behavior is just that it succeeds, since rebasing is the last step anyway).

Floris@MSI MINGW64 /d/projects/mathlib3 (stupid)
$ leanproject rebase
Looking for local mathlib oleans
Found local mathlib oleans
Cmd('git') failed due to: exit code(1)
  cmdline: git rebase master
  stdout: 'First, rewinding head to replay your work on top of it...
Applying: uglify
Using index info to reconstruct a base tree...
M       src/measure_theory/borel_space.lean
Falling back to patching base and 3-way merge...
Auto-merging src/measure_theory/borel_space.lean
CONFLICT (content): Merge conflict in src/measure_theory/borel_space.lean
Patch failed at 0001 uglify
Resolve all conflicts manually, mark them as resolved with
"git add/rm <conflicted_files>", then run "git rebase --continue".
You can instead skip this commit: run "git rebase --skip".
To abort and get back to the state before "git rebase", run "git rebase --abort".'
  stderr: 'error: Failed to merge in the changes.
hint: Use 'git am --show-current-patch' to see the failed patch'

[Floris van Doorn]

leanproject get-cache --rev seems to work well.

[Patrick Massot]

@Floris van Doorn I'm trying to empty my leanproject backlog, but I don't understand you last complain when rebasing with conflicts. What do you expect? The output you pasted is exactly the intended one. You need to see the git error message in order to take appropriate action, right?

[Patrick Massot]

Also I don't think I'm going to "fix" your issue with --debug. This is a global option of leanproject, it goes before typing a command. I don't see how duplicating it as an option to all commands would help.