Zulip Chat Archive

Stream: general

Topic: get-mathlib-at-commit


view this post on Zulip Yakov Pechersky (Sep 01 2020 at 18:39):

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.

view this post on Zulip Floris van Doorn (Sep 01 2020 at 19:07):

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>

view this post on Zulip Gabriel Ebner (Sep 01 2020 at 19:14):

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

view this post on Zulip Patrick Massot (Sep 01 2020 at 19:37):

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

view this post on Zulip Yakov Pechersky (Sep 01 2020 at 19:46):

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

view this post on Zulip Yakov Pechersky (Sep 01 2020 at 19:47):

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.

view this post on Zulip Patrick Massot (Oct 10 2020 at 15:51):

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?

view this post on Zulip Patrick Massot (Oct 10 2020 at 15:56):

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.

view this post on Zulip Patrick Massot (Oct 10 2020 at 15:57):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 15:58):

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.

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 16:00):

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

view this post on Zulip Eric Wieser (Oct 10 2020 at 16:03):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 16:05):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 16:08):

Yes, at least in my experience.

view this post on Zulip Patrick Massot (Oct 10 2020 at 16:12):

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:

view this post on Zulip Patrick Massot (Oct 10 2020 at 16:13):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 16:15):

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.

view this post on Zulip Patrick Massot (Oct 10 2020 at 16:15):

How does that sound?

view this post on Zulip Patrick Massot (Oct 10 2020 at 16:19):

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.

view this post on Zulip Eric Wieser (Oct 10 2020 at 16:20):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 16:22):

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

view this post on Zulip Eric Wieser (Oct 10 2020 at 16:24):

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.

view this post on Zulip Patrick Massot (Oct 10 2020 at 16:25):

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.

view this post on Zulip Patrick Massot (Oct 10 2020 at 20:45):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 20:46):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 20:48):

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.

view this post on Zulip Eric Wieser (Oct 10 2020 at 20:48):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 20:49):

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

view this post on Zulip Eric Wieser (Oct 10 2020 at 20:50):

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

view this post on Zulip Eric Wieser (Oct 10 2020 at 20:51):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 20:52):

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

view this post on Zulip Eric Wieser (Oct 10 2020 at 20:58):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 21:01):

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.

view this post on Zulip Eric Wieser (Oct 10 2020 at 21:02):

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

view this post on Zulip Patrick Massot (Oct 10 2020 at 21:04):

get-cache is overwriting your lean files.

view this post on Zulip Eric Wieser (Oct 10 2020 at 21:29):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 21:30):

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

view this post on Zulip Bryan Gin-ge Chen (Oct 10 2020 at 21:34):

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.

view this post on Zulip Patrick Massot (Oct 10 2020 at 21:39):

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

view this post on Zulip Eric Wieser (Oct 11 2020 at 06:29):

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

view this post on Zulip Eric Wieser (Oct 11 2020 at 13:32):

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)

view this post on Zulip Patrick Massot (Oct 11 2020 at 14:39):

@Eric Wieser can you try with current master?

view this post on Zulip Eric Wieser (Oct 11 2020 at 15:03):

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

view this post on Zulip Floris van Doorn (Oct 11 2020 at 23:41):

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.

view this post on Zulip Gabriel Ebner (Oct 12 2020 at 08:23):

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.

view this post on Zulip Gabriel Ebner (Oct 12 2020 at 08:24):

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.

view this post on Zulip Eric Wieser (Oct 12 2020 at 08:33):

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

view this post on Zulip Gabriel Ebner (Oct 12 2020 at 08:33):

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.

view this post on Zulip Gabriel Ebner (Oct 12 2020 at 08:34):

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.

view this post on Zulip Eric Wieser (Oct 12 2020 at 08:42):

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

view this post on Zulip Gabriel Ebner (Oct 12 2020 at 09:16):

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.

view this post on Zulip Floris van Doorn (Oct 12 2020 at 19:40):

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

view this post on Zulip Floris van Doorn (Oct 12 2020 at 19:51):

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?

view this post on Zulip Floris van Doorn (Oct 12 2020 at 19:54):

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.

view this post on Zulip Floris van Doorn (Oct 12 2020 at 19:56):

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

view this post on Zulip Floris van Doorn (Oct 12 2020 at 20:12):

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'

view this post on Zulip Floris van Doorn (Oct 12 2020 at 20:15):

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

view this post on Zulip Patrick Massot (Oct 31 2020 at 15:23):

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

view this post on Zulip Patrick Massot (Oct 31 2020 at 15:24):

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.


Last updated: May 15 2021 at 23:13 UTC