new mathlib tools

Stream: general

[Patrick Massot]

I need infrastructure testers again. This thread is for you if you want to help users, especially beginners, and you have a working elan+python3+pip installation (and are not afraid of temporarily screwing up your mathlib tools). The install procedure is:

• git clone https://github.com/leanprover-community/mathlib-tools.git if you don't already have it
• cd mathlib-tools
• git checkout refactor

• sudo pip3 install .
  Then you should have a brand new leancli toy (whose name is up for discussion). It is meant to replace leanpkg+update-mathlib+cache_olean except that one task corresponds to one command. Things to try out:

• leancli new myprojet should create a new lean project with mathlib ready to go.

• in a project depending on mathlib, leancli upgrade-mathlib should upgrade mathlib, including oleans
• in mathlib, leancli upgrade-mathlib should upgrade mathlib, including oleans
• in a project not depending on mathlib (?!), leancli add-mathlib should make it a decent Lean project, including oleans
• in any project, leancli mk-cache and lean-cli get-cache should make and fetch olean cache. If this project is mathlib, that cache will live in $HOME/.mathlib, else it will live in _cache in the project
• in any project, leancli build should do a leanpkg build
• in any project, leancli hooks should do what setup-git-hooks used to do
• leancli get tutorials should give you the tutorials project, ready to use (alternative commands: leancli get leanprover-community/tutorials or leancli get https://github.com/leanprover-community/tutorials.git)

[Kevin Buzzard]

leancli new myprojet seems to work for me on Ubuntu 18.04, but probably that was the least of your worries.

[Patrick Massot]

This is still good to know!

[Alex J. Best]

On OSX: making new project works fine! When I go to mathlib and run leancli upgrade-mathlib (why did the name change from update-mathlib?) I get:

+alex:~/mathlib ((bcb63ebf...)) 🐌 leancli upgrade-mathlib
Traceback (most recent call last):
  File "/usr/local/bin/leancli", line 8, in <module>
    sys.exit(main())
  File "/usr/local/lib/python3.7/site-packages/mathlibtools/leancli.py", line 75, in main
    'hooks': hooks,
  File "/usr/local/lib/python3.7/site-packages/fire/core.py", line 138, in Fire
    component_trace = _Fire(component, args, parsed_flag_args, context, name)
  File "/usr/local/lib/python3.7/site-packages/fire/core.py", line 471, in _Fire
    target=component.__name__)
  File "/usr/local/lib/python3.7/site-packages/fire/core.py", line 675, in _CallAndUpdateTrace
    component = fn(*varargs, **kwargs)
  File "/usr/local/lib/python3.7/site-packages/mathlibtools/leancli.py", line 26, in upgrade_mathlib
    proj().upgrade_mathlib()
  File "/usr/local/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 306, in upgrade_mathlib
    rem = next(remote for remote in self.repo.remotes
StopIteration

[Alex J. Best]

I believe this is my bad for having my mathlib remote url still pointing to https://github.com/leanprover/mathlib.git which is the old url

[Alex J. Best]

But probably this situation should still be handled either with a nice error message, or it shouldn't be too hard to make this url work too.

[Alex J. Best]

e.g. "You do not appear to have leanprover-community/mathlib as a remote for this repository. Are you sure you are in a mathlib repository?"

[Alex J. Best]

After fixing that and making sure I was on the lean-3.5.1 branch it looks to work.
One annoyance is that I usually checkout origin/lean-3.5.1 which makes it error, maybe that was bad practice on my account still.

[Patrick Massot]

Thanks @Alex J. Best. About the upgrade name: this mess comes from the discrepancy between the existing leanpkg upgrade and update-mathlib. But I think I'll introduce aliases so that leancli upgrade-mathlib, leancli update-mathlib and leancli up all do the same.

[Patrick Massot]

About git pulling mathlib, this is clearly the trickiest part, because there can be a wild diversity of git situations. I'll add a couple more heuristics, but the documentation will need to point out that, if you are in a weird setup, you can always do git pull whatever && leancli get-cache.

[Patrick Massot]

It would be nice to have tests on Windows as well. By @Rob Lewis or @Sebastien Gouezel maybe?

[Patrick Massot]

Also I think @Scott Morrison recently complained about API rate limit errors. Would you mind trying this brand new toy which should never hit that error (unless you ask for ancient nightlies).

[Rob Lewis]

Thanks Patrick! I haven't tried it yet but this looks very nice. Can I bikeshed about the name? leancli sounds kind of awkward. What about leanproject? (Or lean-project?)

[Johan Commelin]

cliean?

[Gabriel Ebner]

I can confirm that leancli get-cache works for me. Regarding the name: since we already have all kinds of puns (elan, trepplein, lean forward, lean together, etc.), how about penche?

[Vaibhav Karve]

Another name suggestion: cline.

[Patrick Massot]

As I wrote in the first message of this thread, the name is definitely open for bike-shedding. But I don't get the pun with penche.

[Gabriel Ebner]

According to my French dictionary, "pencher" means "to lean".

[Patrick Massot]

Are there other remarks about how the tools work? I was teaching this morning, and at 2 I'll go back to teach for three hours, so you all have time for testing.

[Patrick Massot]

Oh, I didn't even think to try to read it as French.

[Patrick Massot]

Ok, so it does work.

[Johan Commelin]

What is "lean" as in "thin" in French?

[Patrick Massot]

"mince" or "svelte"

[Patrick Massot]

depending on context

[Johan Commelin]

Ha, mince sounds like you're try to turn the olean files into minced meat or something (-;

[Anne Baanen]

How about fuzhou, apparently the name of a prefecture in China which contains Le'an County?

[Gabriel Ebner]

Le'an County

:+1: for 乐安 new-project, this reduces the risk of name collision.

[Rob Lewis]

It's certainly more boring than 乐安, but the grammar of leanproject sounds nice. leanproject new, leanproject upgrade-mathlib, leanproject fetch-cache. When you have supporting tools that are going in peoples' paths, I think it's nice to make the name obviously connect to the main tool. If someone installed this and forgot about it, they'd have no idea after a while that penche and lean were connected.

[Patrick Massot]

Ok, let's name that leanproject. Should I make a couple of fixes and open a PR to mathlib-tools or are there still people who want to test this or ask for different features? Are there people who would miss the current update-mathlib, cache-olean and setup-git-hooks? Or course leanpkg will stay, even if its direct use will be somehow deprecated.

[Johan Commelin]

@Patrick Massot Thanks a lot for investing time in building this tool

[Sebastien Gouezel]

I just got a failure

PS C:\Users\sebas\Desktop\mathlib_master - Copie> leancli upgrade-mathlib
Looking for local mathlib oleans
Looking for Azure mathlib oleans
Trying to download https://oleanstorage.blob.core.windows.net/mathlib/8030469cccb4306230015df55ba50a5e280727bf.tar.gz to C:\Users\sebas\.mathlib\8030469cccb4306230015df55ba50a5e280727bf.tar.gz
Traceback (most recent call last):
  File "C:\Program Files\Python37\Scripts\leancli-script.py", line 11, in <module>
    load_entry_point('mathlibtools==0.0.3', 'console_scripts', 'leancli')()
  File "c:\program files\python37\lib\site-packages\mathlibtools\leancli.py", line 75, in main
    'hooks': hooks,
  File "c:\program files\python37\lib\site-packages\fire\core.py", line 138, in Fire
    component_trace = _Fire(component, args, parsed_flag_args, context, name)
  File "c:\program files\python37\lib\site-packages\fire\core.py", line 471, in _Fire
    target=component.__name__)
  File "c:\program files\python37\lib\site-packages\fire\core.py", line 675, in _CallAndUpdateTrace
    component = fn(*varargs, **kwargs)
  File "c:\program files\python37\lib\site-packages\mathlibtools\leancli.py", line 26, in upgrade_mathlib
    proj().upgrade_mathlib()
  File "c:\program files\python37\lib\site-packages\mathlibtools\leanproject.py", line 317, in upgrade_mathlib
    self.get_mathlib_olean()
  File "c:\program files\python37\lib\site-packages\mathlibtools\leanproject.py", line 227, in get_mathlib_olean
    unpack_archive(get_mathlib_archive(self.mathlib_rev),
  File "c:\program files\python37\lib\site-packages\mathlibtools\leanproject.py", line 117, in get_mathlib_archive
    download(AZURE_URL+fname, path)
  File "c:\program files\python37\lib\site-packages\mathlibtools\leanproject.py", line 96, in download
    with target.open('wb') as tgt:
  File "c:\program files\python37\lib\pathlib.py", line 1165, in open
    opener=self._opener)
  File "c:\program files\python37\lib\pathlib.py", line 1019, in _opener
    return self._accessor.open(self, flags, mode)
FileNotFoundError: [Errno 2] No such file or directory: 'C:\\Users\\sebas\\.mathlib\\8030469cccb4306230015df55ba50a5e280727bf.tar.gz'

I then created by hand the directory 'C:\\Users\\sebas\\.mathlib and tried again, and it worked.

[Mario Carneiro]

It seems like the error reporting situation here is not great. When a big script like this fails I have no idea how to recover or what alternative steps to take

[Mario Carneiro]

Could you maybe sprinkle some try: around in the code and explain to the user what went wrong? User facing errors are not supposed to be stackdumps

[Patrick Massot]

Sure. We are at the testing phase where I do need to see tracebacks (not stackdumps...). But then I'll hide all that.

[Gabriel Ebner]

Or course leanpkg will stay

leanpkg doesn't do anything magic. There's nothing to stop you from replacing parts or all of it within leanproject if you want.

[Patrick Massot]

I could avoid calling it from leanproject, but I guess we shouldn't remove it from leanprover-community/lean

[Patrick Massot]

I pushed a new version. Everybody is welcome to test (again). Please see the first message in this thread, except that leancli is now called leanproject.

[Patrick Massot]

Note that leanproject up will have a hard time working on mathlib master. It may pull the lastest commit on master before CI builds it and pushes it to the cloud.

[Patrick Massot]

https://github.com/leanprover-community/mathlib-tools/pull/16

[Patrick Massot]

Now is a good time to test!

[Patrick Massot]

Oh, CI fails. I haven't modified any CI instructions. Is anyone familiar with CI on this repository and could try to port it to the new system?

[Patrick Massot]

Note that the PR does include tests, ran by tox against python 3.5, 3.6, 3.7 and 3.8.

[Patrick Massot]

I'll work on this CI tomorrow if nobody does it while I sleep, but everybody can already test by cloning the branch and installing. And everybody can review the python code.

[Scott Morrison]

Is the intention to eventually drop the separate repository, and just include this tool in the main (community) lean repository?

[Patrick Massot]

I don't know. I don't remember why we separated this repository.

[Simon Hudon]

We separated it because of how different the testing of the tools was from testing the mathlib PRs and it caused the mathlib builds to fail for unforeseen reasons

[Patrick Massot]

Sounds reasonable.

[Johan Commelin]

@Patrick Massot When I run leanproject get-cache I get

Trying to download https://oleanstorage.blob.core.windows.net/mathlib/5770369f6d3f28356be20931c9ade07be37a01ad.tar.gz to /home/jmc/.mathlib/5770369f6d3f28356be20931c9ade07be37a01ad.tar.gz

That's still the older slower URL, right?

[Johan Commelin]

Also, should leanproject up work in a mathlib directory? That's not clear to me from the output of --help

[Patrick Massot]

I thought I changed the url, but something went wrong. This should work now

[Patrick Massot]

About upgrade, how would you phrase the help message to make it clear it will work everywhere?

[Johan Commelin]

@Patrick Massot What is the difference with up?

[Johan Commelin]

I mean get-cache vs up.

[Patrick Massot]

In mathlib itself, up will try to git pull then get oleans

[Johan Commelin]

Aha, I see.

[Patrick Massot]

In a project depending on mathlib, up will do what leanpkg upgrade+leanpkg configure+update-mathlib did

[Patrick Massot]

without the occasional "is not a tree" weird error message.

[Johan Commelin]

Ok, that seems useful.

[Johan Commelin]

Is there a place where you want to document this, besides --help? Because this seems hard to summarise in one line.

[Johan Commelin]

Or is --help also for longer explanations?

[Patrick Massot]

Of course there will be longer help in a new version of https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

[Patrick Massot]

But leanproject up --help will also display more

[Johan Commelin]

Aah, @Patrick Massot I think it makes sense to show in the general --help that CMD --help will show more details.

[Patrick Massot]

I don't know if we can do that in the current setup, I'll investigate. Yesterday I switched from fire to click for command line handling and help building (because it seemed easier to create aliases).

[Rob Lewis]

Indeed, I think the output of leanproject --help could be expanded a bit. upgrade-mathlib in particular isn't clear. Maybe "Upgrade a mathlib dependency to the latest compatible version" or something like that?

[Patrick Massot]

I managed to make travis happy: https://travis-ci.org/leanprover-community/mathlib-tools?utm_medium=notification&utm_source=github_status. Now a much harder challenge will be AppVeyor.

[Patrick Massot]

Gabriel, I don't understand your latest comment on this PR. Could you clarify what you wish?

[Gabriel Ebner]

Let me rephrase it: when I run leanproject up on an up-to-date mathlib branch, it fetches oleans. But when I run leanproject up on something that is not a mathlib branch, I suddenly get an error message from git with no further explanation.
There is already a helpful error message when leanproject can't find the mathlib remote here: https://github.com/leanprover-community/mathlib-tools/blob/fc2d84d5cc798a79fb16cf29f433fc77d56b5a25/mathlibtools/lib.py#L373-L375
I would also like to see this error message when the pull fails two lines after that: https://github.com/leanprover-community/mathlib-tools/blob/fc2d84d5cc798a79fb16cf29f433fc77d56b5a25/mathlibtools/lib.py#L377 (at least that's where I think the error comes from)

[Patrick Massot]

Those lines will be executed when you are not working on mathlib.

[Patrick Massot]

When you are not working on mathlib, git pulling mathlib is handled by leanpkg.

[Gabriel Ebner]

AFAICT leanproject up executes proj().upgrade_mathlib(). The lines I've quoted are then executed if self.is_mathlib is true (which I hope is the case if I'm working on mathlib).

[Gabriel Ebner]

By "not a mathlib branch", I mean a branch in mathlib that is only on my own fork (i.e. no corresponding branch on leanprover-community), or I've checked out some random commit (which is on leanprover-community/mathlib but doesn't correspond to any branch).

[Patrick Massot]

Ok, I misunderstood "not a mathlib branch".

[Patrick Massot]

This should be fixed now.

[Patrick Massot]

I think I emptied the request stream. The only thing that is missing is upgrading mathlib to a new version of Lean. One thing we can do is leanproject upgrade-mathlib could ask GitHub whether there is a leanprover-community/mathlib branch named lean-X.Y.Z with X.Y.Z bigger than the Lean version currently used by the project (note this would cost a bit of time). Then we could change the project Lean version and upgrade mathlib. Do we want that? Do we want leanproject to ask for confirmation before doing that? Or should this be a manual only operation (or a new command in leanproject)?

[Gabriel Ebner]

leanproject upgrade-lean could also be part of the next PR. I think leanproject is sufficiently polished and tested now that we should merge the PR and make a new release on pypi.

[Patrick Massot]

This will be quick to implement, I can do it tonight if we decide what we want.

[Rob Lewis]

I think leanproject upgrade-lean should probably take an optional Lean version. So with no version given it upgrades to the newest Lean it can find, and leanproject upgrade-lean 3.6.1 does what you'd expect even after 3.6.2 is released.

[Patrick Massot]

Do I understand correctly that you both think leanproject upgrade-mathlib should not silently upgrade the lean version?

[Rob Lewis]

We could have a flag for it. leanproject upgrade-mathlib --upgrade-leanif the default is not to, or swap the default. I'm not sure which is better.

[Rob Lewis]

My instinct is to do less by default.

[Patrick Massot]

Given that we don't backport anything to old mathlib branches, I would say people who want to upgrade mathlib want to upgrade Lean. But we could at least ask for confirmation.

[Rob Lewis]

Actually, I'd skip the step of asking for confirmation. As long as there's an option upgrade-mathlib --no-lean-upgrade or whatever, I think it's fine.

[Rob Lewis]

Adding prompts just makes the directions for new users more confusing.

[Patrick Massot]

Currently leanproject check prompts before touching oleans.

[Rob Lewis]

That's fine, it's not part of the normal workflow, right?

[Patrick Massot]

It's part of making Jason feel safer (and also of helping debugging new users on Zulip).

[Patrick Massot]

So not part of the normal workflow.

[Sebastien Gouezel]

I just got a surprising error message from leanproject:

> leanproject up
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/e0030149a7e753283e01c64f6ec8de94d2eebf93.tar.gz to C:\Users\Sebastien\.mathlib\e0030149a7e753283e01c64f6ec8de94d2eebf93.tar.gz
100%|████████████████████████████████████████████████████████████████████████████████████████| 215/215 [00:00<?, ?iB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/
C:\Users\Sebastien\.mathlib\e0030149a7e753283e01c64f6ec8de94d2eebf93.tar.gz is not a compressed or uncompressed tar file

If I understand correctly, the oleans are not yet on Azure, so it downloaded the .xml file and then realized it's not the right file. What is confusing to me is that it mentions a .tar.gz file, and then says it is not a compressed or uncompressed tar file.

[Patrick Massot]

Sébastien, when did you last upgrade leanproject? This xml thing should not happen anymore.

[Patrick Massot]

The fact that it mentions a tar.gz file is not suprising, leanproject is making up that file name from the commit hash.

[Sebastien Gouezel]

Yes, I was probably just working with an old version. Sorry for the noise.

(I have just updated and tried again, but now the oleans are already there on Azure so I can't conclude anything)

[Patrick Massot]

I hope @Rob Lewis and @Gabriel Ebner will have time to fix that Azure delay issue. This is the main thing blocking the release of leanproject. Until that is fixed, this tool will remain completely unreliable.

[Sebastien Gouezel]

That tool is already amazing. With a good error message explaining what is going on in case of failure, I think it can (and should?) be released now.

[Sebastien Gouezel]

I tried it now, just after a push to mathlib. Indeed I don't get any more the weird error message. Instead, I have

> leanproject up
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/2d1bd457d4da3383a8154528bb2df09a977523a2.tar.gz to C:\Users\sebas\.mathlib\2d1bd457d4da3383a8154528bb2df09a977523a2.tar.gz
Looking for GitHub mathlib oleans
Info: No github section found in 'git config', we will use GitHub with no authentication
Failed to fetch mathlib oleans

I think an error message like oleans not found on Azure. This is usually due to a delay between a push to master and the generation of oleans. Please retry in one hour would be helpful in this situation.

[Kevin Buzzard]

I don't want to wait an hour, I'd rather have the last mathlib for which the oleans are on Azure, right now. I never had to wait for update-mathlib and I don't care if I'm one day out of date. Or is this a problem which is only temporary?

My instinct is not to switch until I'm being assured that I don't have to wait for an hour.

[Kevin Buzzard]

PS should I worry about the "no authentication" line? I get this on at least one of the machines I use lean on

[Mario Carneiro]

it's not really a security concern, but it does mean that you get rate limited

[Johan Commelin]

@Kevin Buzzard leanproject get-cache should get you yesterdays oleans...

[Patrick Massot]

Kevin, I think you missed part of the discussion. There shouldn't be any need to wait. The issue is that our continuous integration keeps building the same lean files but with different git commits. Mergify creates merge commits with no added content compared to the successful build that prompted mergify to merge. Anyway, don't worry about this, Gabriel and Rob will fix it.

[Rob Lewis]

I thought about the delay a bit more, and I have most of a solution. It's kind of a subtle thing. What we want goes way against the grain of Mergify. And there are enough little things that Mergify does (queuing, setting the commit author, closing PRs, deleting branches) that it will be a huge pain to reimplement in e.g. Actions.

The big issue is that the final Mergify build has a different git hash than the merge commit that will get pushed to master. And we can't predict what the master commit will be until it happens. But what we can do is this. We store a table in Azure that maps file hashes to git hashes. By a file hash, I mean a hash computed from all .lean files in src and leanpkg.toml. When an archive gets uploaded to Azure, we add a row to the table.

If leanproject doesn't find an archive corresponding to the git hash, it can compute the file hash, and query the table; if there's a row for that file hash, it points to an archive built from a different commit, but with identical lean files. So it's safe to use that archive instead.

[Johan Commelin]

That sounds like a good solution. But where do the file hashes get computed for the entries in the table in Azure?

[Johan Commelin]

I currently don't know the system very well. Who is pushing the oleans to Azure. Is mergify doing this? Or some other part of CI?

[Rob Lewis]

GitHub Actions is in charge of pushing the archives to Azure. It can compute the file hashes. We need to make sure that Actions and leanproject compute the same hash, so I think they should use the same Python script.

[Johan Commelin]

This

find src | grep "[.]lean$" | sort | xargs sha512sum | sha512sum

is fast (instant, < 0.1s) on my machine, and makes sure that the order in which files are visited doesn't influence the hash.

[Rob Lewis]

Is it OS independent?

[Johan Commelin]

I really don't know what I can expect windows users to have nowadays

[Johan Commelin]

Do we expect them to have git bash?

[Johan Commelin]

Or is that no longer a prerequisite to installing mathlib and friends?

[Rob Lewis]

We'll have to do this from Python in leanproject. Instead of calling a bash script from Python that might not work on every OS, we should probably just implement it in Python.

[Johan Commelin]

Apparently you get all files in subdirectories with

import glob

files = glob.glob(my_path + '/**/*.lean', recursive=True)

[Rob Lewis]

I think something like this is right.

# adapted from https://stackoverflow.com/questions/24937495/how-can-i-calculate-a-hash-for-a-filesystem-directory-using-python
import os
import hashlib
from pathlib import Path


def md5_update_from_file(filename, hash):
    assert Path(filename).is_file()
    with open(str(filename), "rb") as f:
        for chunk in iter(lambda: f.read(4096), b""):
            hash.update(chunk)
    return hash

def md5_file(filename):
    return md5_update_from_file(filename, hashlib.md5()).hexdigest()

def md5_update_from_dir(directory, hash):
    assert Path(directory).is_dir()
    for path in sorted(Path(directory).iterdir()):
        if path.is_file() and path.suffix == '.lean':
            hash = md5_update_from_file(path, hash)
    return hash

def md5_dir(directory):
    return md5_update_from_dir(directory, hashlib.md5()).hexdigest()

def md5_dir_and_file(directory, file):
  dir_hash = md5_update_from_dir(directory, hashlib.md5())
  dir_file_hash = md5_update_from_file(file, dir_hash)
  return dir_file_hash.hexdigest()

root = os.getcwd()
src_dir = os.path.join(root, 'src')
toml_path = os.path.join(root, 'leanpkg.toml')
hash = md5_dir_and_file(src_dir, toml_path)
print(hash)

[Rob Lewis]

This will be sensitive to the presence of untracked .lean files in the src directory.

[Rob Lewis]

Maybe it should use the git Python library to only check files that are part of the repo.

[Johan Commelin]

Do you really want to use md5?

[Johan Commelin]

I thought that was deprecated half a century ago...

[Rob Lewis]

That was just from the StackOverflow example, but I don't think it really matters.

[Rob Lewis]

There's no security concern here.

[Johan Commelin]

Sure...

[Johan Commelin]

Good catch that you also take the toml into account

[Rob Lewis]

With this approach, there will only be a short delay between a commit hitting master and the correctly named archive being uploaded. We'll be able to grab the oleans and skip the build. The untracked file worry only matters in that minute in between.

[Johan Commelin]

https://gist.github.com/seveas/4318006 -- git-list-all-files

[Johan Commelin]

If we just filter for .lean and .toml, then we would be done, I guess.

[Rob Lewis]

That looks like major overkill, all files that have ever existed in the repo in any branch? We just want the current head.

[Rob Lewis]

But I'm sure there's a way to get this.

[Johan Commelin]

Hmmm, you are right.. I didn't read carefully

[Rob Lewis]

I need to do other things this afternoon, but I leave a challenge for @Patrick Massot . Give me a Python script that computes this hash, reliably across OSes. I'll give you a URL pattern to check if leanproject fails to find an archive at the git hash URL. If successful it will return JSON with an alternate git hash to look for.

[Rob Lewis]

You know what, ignore that. It will be better to keep this out of leanproject entirely. We can live with a delay of a couple minutes between a commit hitting master and the archive being available. Then this can stay entirely in CI.

[Johan Commelin]

In that case you can even resort to my 1-liner (-;

[Rob Lewis]

Gotta include leanpkg.toml too...

[Johan Commelin]

find . | grep '[.]lean$\|[.]toml$' | sort | xargs shasum | shasum

[Rob Lewis]

Only find lean files in src/, but include leanpkg.toml which is in .? :)

[Johan Commelin]

Hmmm, do we not want archive/ etc?

[Rob Lewis]

Nope. Why should we refuse to use olean files from a build that only changed something in archive?

[Gabriel Ebner]

Please also include the output of lean --version, if possible. Otherwise this is a bit flaky if you use leanprover-community/lean:nightly as the lean version in leanpkg.toml.

[Johan Commelin]

echo `find src | grep '[.]lean$' | sort | xargs shasum` `shasum leanpkg.toml` "lean --version:" `lean --version` | shasum | head -c 40; echo
ffd5c1d3c3db39f68d267a5f6d75696ccc8925b4

[Johan Commelin]

This was on a dirty mathlib, so you shouldn't be able to reproduce (-;

[Patrick Massot]

@Rob Lewis I'm not sure I understand the conclusion of this shasum discussion. Do you expect me to do something?

[Rob Lewis]

@Patrick Massot not at the moment. Although, a flag for leanproject get-cache to skip the mathlib-nightly lookup would be helpful! (Meaning, just fail if the cache doesn't exist on Azure.)

[Rob Lewis]

I have this mostly implemented. There seems to be a small bug in leanproject blocking it for now: https://github.com/leanprover-community/mathlib-tools/pull/16#issuecomment-594527235

[Rob Lewis]

When this lands, oleans should be available on Azure about a minute after a commit hits master, as long as that commit came from a PR from a mathlib branch.

[Patrick Massot]

Thanks. What you describe is not a bug, this is the intended behavior of this -u option. It was meant to provide the base url, not the tar.gz file url.

[Rob Lewis]

Oh, I see. Can I have an option to direct it to a different filename too?

[Rob Lewis]

Even better if I can give it the filename and not the full URL!

[Patrick Massot]

I don't understand what you want.

[Rob Lewis]

I want to say "even though the git hash is xyz, use the oleans from abc.tar.gz instead."

[Rob Lewis]

The idea being, abc and xyz are different commits that contain identical Lean files.

[Patrick Massot]

And who is providing the hashes xyz and abc?

[Patrick Massot]

We don't want end-users to see any of this trickery, right?

[Rob Lewis]

I provide abc. You're computing xyz from the current git hash but I want to ignore it in this case.

[Rob Lewis]

This is an option, nobody has to use this if they don't know what they're doing.

[Patrick Massot]

But let's say Kevin wants to upgrade mathlib, without needing to be lucky to want that one hour and a half after the lean-3.5.1 branch is moved to a new commit in the morning. Does he need to do anything?

[Rob Lewis]

No.

[Patrick Massot]

(I hope Kevin won't mind being used as the archetypal clueless user in this discussion).

[Patrick Massot]

So, who will be using this option. CI?

[Rob Lewis]

Yes, CI and users who know what they're doing.

[Patrick Massot]

Ok, fine.

[Patrick Massot]

I'll do that as soon as I'll be done with marking.

[Rob Lewis]

Thanks!

[Patrick Massot]

Rob Lewis said:

I want to say "even though the git hash is xyz, use the oleans from abc.tar.gz instead."

Which command do you this option to modify? Is it only leanproject get-cache? Or do you also want leanproject upgrade-mathlib to be also using it?

[Patrick Massot]

I tried to think about implementation but there is too much to guess here. I need to know precisely what you actually want to do on your side.

[Johan Commelin]

You probably have a function compute_hash somewhere. Can every command that uses this function get an option --use-hash that specifies a hash (without the .tar.gz suffix) that will be used instead of whatever result compute_hash returns?

[Patrick Massot]

Thanks Johan, but this kind of message is exactly what doesn't help ( trying to guess what leanproject does and running into XY problem).

[Gabriel Ebner]

@Johan Commelin In the worst case, you can always run curltar yourself:

curl https://oleanstorage.azureedge.net/mathlib/$MY_FAVORITE_HASH.tar.gz | tar xz
# or if you want a one-line replacement for `leanproject get-cache`:
curl https://oleanstorage.azureedge.net/mathlib/$(git rev-parse HEAD).tar.gz | tar xz

[Johan Commelin]

Is there anything else on the wishlist apart from Rob's item?

[Rob Lewis]

Patrick Massot said:

I tried to think about implementation but there is too much to guess here. I need to know precisely what you actually want to do on your side.

I only care about get-cache. I don't think it makes sense for upgrade-mathlib. Just like -u lets me change the base url where it looks for the archive, I'd like to change the filename as well.

[Rob Lewis]

So regardless of my current mathlib version, if I type leanproject -u mywebsite.com -n filename.tar.gz get-cache it will download the archive from mywebsite.com/filename.tar.gz.

[Gabriel Ebner]

We only use this for CI, right? Why not just curl https://mywebsite.com/filename.tar.gz | tar xz?

[Rob Lewis]

Well, first we check for the file in the normal place, and then there's the olean touching logic. So it would be repeating a bunch of features of leanproject get-cache. But we could.

[Gabriel Ebner]

I'm not sure we should be touching oleans in CI anyhow. The CI servers should all have the same timezone and time, so there shouldn't be any issues. And if there are issues, it's okay if they build twice.

[Gabriel Ebner]

Am I getting this right? We first check if there's the file for the current commit (in case somebody pushes the same commit to a different branch?), and then we check if there's a file for the current content hash? Isn't the first check redundant?

[Rob Lewis]

Big disclaimer, I'm home sick with a fever today, so yes you're probably right.

[Rob Lewis]

I'll try it out when I trust myself to code...

[Gabriel Ebner]

Please take care of yourself. You should take the day off.

[Rob Lewis]

Only here because I've been lying in bed all day and I'm bored ;)

[Scott Morrison]

I find myself often typing:

git checkout X    # this successfully downloads oleans, but git also tells me "Your branch is behind 'origin/X' by 25 commits"
git pull
leanproject get-cache # successfully downloads the latest oleans

[Gabriel Ebner]

@Scott Morrison This is just git checkout X && leanproject up

[Scott Morrison]

Ah, thanks! So I just stop using git pull. I wonder if there is a good way to steer people towards doing this?

[Scott Morrison]

(We know lack of oleans is a huge hurdle to newcomers.)

[Gabriel Ebner]

A big issue with leanproject up is that you don't get olean if the branch has been updated in the last two hours. It would be great if it could check out the latest commit where oleans are available.

[Simon Hudon]

that would be the HEAD of the branch lean-3.5.1, no?

[Scott Morrison]

I think Gabriel means the latest commit on whichever branch you're on, that has oleans.

[Scott Morrison]

So git pull gets you to the HEAD of your current branch, but leanproject up takes you to the latest with oleans.

[Scott Morrison]

Or maybe leanproject up should take you to HEAD, but with the latest available oleans, even if they haven't caught up with HEAD?

[Gabriel Ebner]

When checking out master, I typically want the latest one that has full oleans. When checking out feature branches, I want the latest one and I'll take whatever oleans I get.

[Scott Morrison]

I think it might be better not to have inconsistent behaviour for leanproject up on master and other branches.

[Scott Morrison]

For people who want guaranteed oleans, we should advertise to them the existence of the lean-3.X.X branches, which should always have oleans and stay close to master.

[Scott Morrison]

(Advertising could even be in the form of a message whenever leanproject fails to find oleans!)

[Scott Morrison]

We might also consider, as version numbers seem likely to keep moving for a while now, having a latest branch, that is guaranteed to have oleans, and tracks close to master, regardless of version numbers.

[Gabriel Ebner]

I think I've said it before: we should merge leanproject now. There are lots of nice suggestions here, and I believe they would be even better as PRs to mathlib-tools.
Patrick and Kevin have said that we should wait until we've improved the delay between commits to master and olean tarballs being available. But this is a red herring. This doesn't work with cache-olean either. And if you stay on the lean-3.6.1 branch like you had to with cache-olean then leanproject up will always find oleans without any delay.

[Johan Commelin]

Go for it!

[Gabriel Ebner]

Ok, now we just need to wait for @Patrick Massot to push the release to pypi.

[Mario Carneiro]

what is the documentation story? Is this live for users?

[Gabriel Ebner]

Oh yeah, this is a good point. I completely forgot about it. It is not yet live for users that use pip install mathlibtools. You only get it if you use the git version directly.

[Mario Carneiro]

Speaking as the old fart who can't be bothered to learn new things, there are too many mathlib tools. What do they all do? Are some superseding others? How do I use them in both simple and less simple use cases? A FAQ or documentation page addressing these questions would be very helpful.

[Gabriel Ebner]

Then you'll be delighted. All of the old tools are gone. Now there's only one tool called leanproject and it's wonderful.

[Mario Carneiro]

and pip, of course

[Mario Carneiro]

installing python has been the sticking point in lean setup for me on more than one occasion

[Gabriel Ebner]

Ok, this doesn't change. We've always required pip.

[Mario Carneiro]

lean itself isn't too hard to get running... can we distribute binary tools?

[Mario Carneiro]

or is CI for that too much work

[Sebastian Ullrich]

You mean, rewrite it in Rust?

[Gabriel Ebner]

I've made a basic PR to change all descriptions from update-mathlib to leanproject. #2093

[Patrick Massot]

I'm sorry I'm super busy all day. I'll push to pypi tonight.

[Gabriel Ebner]

No need to hurry. This can wait another day if it has to.

[Patrick Massot]

I'm using my phone in a train so I can't do much but I commented on the doc PR. You haven't explored the full power of leanproject yet.

[Gabriel Ebner]

You haven't explored the full power of leanproject yet.

I really haven't. You should have posted a leanproject tutorial! This is the first time I hear of leanproject get and leanproject new. BTW, leanproject get didn't work so I filed a PR: https://github.com/leanprover-community/mathlib-tools/pull/18

[Johan Commelin]

Gabriel Ebner said:

Then you'll be delighted. All of the old tools are gone. Now there's only one tool called leanproject and it's wonderful.

I think it still depends on elan. But olean-cache and update-mathlib seem to be superseded.

[Patrick Massot]

Yes, leanproject depends on elan. Internally it also depends on leanpkg (this is pure laziness from me), but from a user point of view it replaces leanpkg entirely. And elan is not meant to be directly used in a normal workflow.

[Patrick Massot]

I think I emptied the feature requests and bug reports. Tonight I'll write more documentation, and probably some more tests. But real world testing is still very welcome. Everybody is also welcome to write python tests. Up to now there are only end-to-end functional tests, in https://github.com/leanprover-community/mathlib-tools/blob/refactor/tests/test_functional.py, that actually run git commands and download stuff. But the python code is written is such a way that unit tests would be easy to build, so feel free to add those if you have too much time.

[Kevin Buzzard]

I would happily test if you tell me precisely what to type to get me from where I am now (no leanproject installed) to the command which upgrades a working lean project from Lean 3.4.2 to Lean 3.6.1. I have a student at Xena who would like to use the new case bash tactic but I've been refraining from updating everyone's set-up at Xena because my impression is that things aren't ready yet (I tried upgrading a student project to 3.6.1 last Thursday and it turned out that there were no mathlib oleans which was a disaster)

[Gabriel Ebner]

If you have already installed update-mathlib using pip (the current installation method), then you can do the following:

sudo pip3 install https://github.com/leanprover-community/mathlib-tools/archive/refactor.tar.gz
cd my-lean-project
leanproject up

If you don't have pip3 yet, then you need to run apt install python3-pip first (as described in our installation docs: https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian_details.md).

[Kevin Buzzard]

What if I'm on Ubuntu which is stuck with Python 2.something? Should I be doing all this in some virtual environment, or do I not need to worry about that extra hassle?

[Patrick Massot]

Kevin, you are not stuck with python 2. You can sudo apt install python3-pip and then clone the repository, checkout the refactor branch and sudo pip3 install .. You don't need to be in a virtual environment if you don't really know what it means.

[Patrick Massot]

I'm done for tonight. I put documentation at https://github.com/leanprover-community/mathlib-tools/blob/refactor/README.md. Everybody is welcome to comment on the documentation, even without trying the tools.

[Patrick Massot]

For instance, every native speaker is welcome to translate this documentation into actual English without asking for permission.

[Patrick Massot]

Gabriel, did you find time to read the new documentation and test more stuff?

[Rob Lewis]

Patrick Massot said:

I hope Rob Lewis and Gabriel Ebner will have time to fix that Azure delay issue. This is the main thing blocking the release of leanproject. Until that is fixed, this tool will remain completely unreliable.

Look at this nice speedy master build: https://github.com/leanprover-community/mathlib/runs/498569708

[Johan Commelin]

26 minutes for linting :shock:

[Gabriel Ebner]

Speedy? I think it still takes an hour. But it's nice that the oleans are already available.

[Johan Commelin]

But otherwise, I agree that it's quite impressive

[Gabriel Ebner]

@Johan Commelin Actually linting is two times 30 minutes. The second time we regenerate the nolints.txt file.

[Rob Lewis]

30 seconds to push the oleans, that's what matters.

[Johan Commelin]

Ooh boy. I didn't realise that linting took that long.

[Rob Lewis]

I think the linters in #2089 slowed it down a bunch.

[Gabriel Ebner]

It's cumulative. The first simp-normal form linter added 7 minutes, the second one added another 15 minutes or so. We have 16 linters now in total.

[Gabriel Ebner]

It shouldn't be hard to run the linters in parallel, in case somebody is motivated.

[Johan Commelin]

I fear that we'll need that pretty soon, if we continue adding linters like this (-;

[Johan Commelin]

Which is probably a good thing.

[Reid Barton]

I'm not familiar with the new CI infrastructure, do we actually get multiple cpus?

[Gabriel Ebner]

According to the github documentation, we have a Standard_DS2_v2 virtual machine. That should be 2 CPUs: https://docs.microsoft.com/en-us/azure/virtual-machines/dv2-dsv2-series#dsv2-series

[Kevin Buzzard]

Does it make sense to say "we only need to run the linters on the files that changed" (or at least some of the linters)? Or can a change in one file make a linter fail on a file which imports it?

[Gabriel Ebner]

At least the simp and type-class linters (which take the majority of the time) are global.

[Gabriel Ebner]

The caching didn't work for the last PR: https://github.com/leanprover-community/mathlib/runs/498865888
Apparently the merge commits created by mergify don't run the push action, only the pull_request action. And the pull_request action doesn't upload to azure: https://github.com/leanprover-community/mathlib/runs/498571556

[Rob Lewis]

Apparently the merge commits created by mergify don't run the push action, only the pull_request action.

God damn it, what?

[Rob Lewis]

Does Mergify do something different than the "update branch" button?

[Rob Lewis]

Because I'm pretty sure that triggers a push build, right?

[Rob Lewis]

Oh, that last PR was from an external repo.

[Rob Lewis]

We won't get oleans in that case.

[Rob Lewis]

No oleans were ever uploaded from that PR because external repos don't have write credentials for Azure.

[Gabriel Ebner]

You're right, of course.

[Patrick Massot]

This is a good opportunity to remind every occasional contributors that they shouldn't hesitate to ask for write access to branches of our main repository. Opening PRs from such branches have more and more advantages. I sent an invitation to @Markus Himmel who is the author of the PR we are discussing.

[Reid Barton]

Please don't hesitate too long, though

[Patrick Massot]

Corrected, thanks

[Rob Lewis]

Heh, I just realized something. Our slowness to change the PR process "saved" us here. Unlike in Travis, PR builds in Actions are consistently a merge commit between the PR branch and master. So Mergify's "update branch" step is unnecessary -- if the PR build succeeds, the branch can be safely merged. We could have gotten rid of this with the switch to Actions. EXCEPT, the "update branch" step is now what allows us to have oleans ready to go immediately.

[Rob Lewis]

Oh, wait, I guess that's not really true, never mind.

[Rob Lewis]

It doesn't re-run the PR builds when master changes.

[Rob Lewis]

Actually, is there any point at all in running the PR builds in our current setup?

[Rob Lewis]

Even in PRs from external repos, the branch builds should happen, right? Because the Actions config is part of the repo?

[Patrick Massot]

Maybe forks need to activate GitHub action? I'm saying that at random

[Rob Lewis]

It is opt-in, but there's a big green button to do it.

[Koundinya Vajjha]

Hi @Patrick Massot , I tried this out today, but I get the following error with leanproject new myproject :

error: ill-formed search path entry '/home/kody/projects/lean4/library', should be of form 'pkg=path'
Traceback (most recent call last):
  File "/usr/bin/leanproject", line 11, in <module>
    load_entry_point('mathlibtools==0.0.3', 'console_scripts', 'leanproject')()
  File "/usr/lib/python3.8/site-packages/click/core.py", line 764, in __call__
    return self.main(*args, **kwargs)
  File "/usr/lib/python3.8/site-packages/click/core.py", line 717, in main
    rv = self.invoke(ctx)
  File "/usr/lib/python3.8/site-packages/click/core.py", line 1137, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "/usr/lib/python3.8/site-packages/click/core.py", line 956, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "/usr/lib/python3.8/site-packages/click/core.py", line 555, in invoke
    return callback(*args, **kwargs)
  File "/usr/lib/python3.8/site-packages/mathlibtools/leanproject.py", line 55, in new
    LeanProject.new(Path(path), url)
  File "/usr/lib/python3.8/site-packages/mathlibtools/lib.py", line 296, in new
    proj = cls.from_path(path)
  File "/usr/lib/python3.8/site-packages/mathlibtools/lib.py", line 161, in from_path
    repo = Repo(path, search_parent_directories=True)
  File "/home/kody/.local/lib/python3.8/site-packages/git/repo/base.py", line 130, in __init__
    raise NoSuchPathError(epath)
git.exc.NoSuchPathError: /home/kody/projects/myproject

I am on Arch Linux and on python 3.8.1 as it shows. I do have a built-from-source copy of Lean4 which is maybe messing it up.

[Koundinya Vajjha]

The script is picking up the Lean4 library path (which doesn't exist) for some reason...?

[Patrick Massot]

I knew there would be people waiting for the release to start testing...

[Patrick Massot]

I need more information. Is there a lean4 folder in projects? Can you paste the output of elan toolchain list?

[Patrick Massot]

Could you try to run leanpkg new my_test and tell us whether this succeeds?

[Koundinya Vajjha]

Patrick Massot said:

I need more information. Is there a lean4 folder in projects? Can you paste the output of elan toolchain list?

Yes. I do have such a folder.
Output of elan toolchain list:

stable
nightly
nightly-2018-06-21
nightly-2018-11-13
nightly-2019-01-13
leanprover-community-lean-3.5.1
master (default)
3.4.1
3.4.2

[Koundinya Vajjha]

leanpkg new my_test gives the same error:

error: ill-formed search path entry '/home/kody/projects/lean4/library', should be of form 'pkg=path'

[Koundinya Vajjha]

I remember changing the default toolchain on elan a long while back to be able to use Lean4.

[Patrick Massot]

Ok, so this is indeed a leanpkg bug. Maybe even a Lean4 bug if this is leanpkg from Lean4.

[Koundinya Vajjha]

Oh yes. Any leanpkg incantation is giving me that error.

[Patrick Massot]

So we should really stop relying on leanpkg in leanproject. I need to do other things this afternoon but PR is welcome.

[Patrick Massot]

In the meantime the workaround is to change your default elan toolchain to leanprover-community-lean-3.6.1

[Sebastian Ullrich]

Alright, to avoid future confusion: https://github.com/leanprover/lean4/commit/10f161353e361f20ac18a7383f46466b149fdfa5

[Patrick Massot]

Nice. I don't know if you followed the discussion around our new package management tool, but I think nobody from the Lean core development team should waste time working on this kind of tooling. It would be much easier if Lean could at least report why it recompiles files (maybe when ran with some debug flag), but otherwise this is all engineering grunt work that is best done by the user community.

[Sebastian Ullrich]

Yeah, I doubt Lean 4 will come with a package manager in the core repo. You might have already heard that the lean main process will not recompile dependencies anymore at all, though if we have a language server in the core repo, then I suppose it will want to reimplement that.

[Sebastian Ullrich]

I've already linked to the import trace I added to Lean 4 before we ripped out that whole module, feel free to adapt: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.203.2E7/near/189816815

[Wojciech Nawrocki]

How does one get oleans for the mathlib revision stored in leanpkg.toml? It seems that leanproject up always pulls the most recent revision, while leanproject build in a directory with no _target/ just clones mathlib, but doesn't download oleans and then starts building everything including mathlib.

[Gabriel Ebner]

leanproject get-cache

[Patrick Massot]

I just created https://github.com/leanprover-community/lean/issues/145 so that we don't forget again. What do you mean by "the lean main process will not recompile dependencies anymore at all"? Will Lean trust every declaration from every import after parsing their statement?

[Sebastian Ullrich]

It only cares about .olean files for imports. It doesn't look at their .lean files at all.

[Wojciech Nawrocki]

Gabriel Ebner said:

leanproject get-cache

This tells me "Failed to fetch mathlib oleans"

[Patrick Massot]

Gabriel's answer is not correct if you work on a project depending on mathlib (as opposed to working on mathlib) itself.

[Patrick Massot]

Your use case is not covered by leanproject. Are you sure you really want to do that?

[Patrick Massot]

To be more explicit: typing leanproject get-cache asks leanproject to find oleans for the current project, not for its dependencies.

[Patrick Massot]

Adding a command leanproject get-mathlib-cache would be trivial to implement if you really want this.

[Gabriel Ebner]

Without get-mathlib-cache, how would you work on an external project like lean-perfectoid-spaces? You definitely don't want to upgrade the mathlib version there.

[Wojciech Nawrocki]

Yep, as Gabriel says : the problem is that I might work on a project at mathlib revision a, then push it to GitHub, and because in the meanwhile mathlib got updated to revision b s.t. the project doesn't compile under b, the CI will fail after leanproject upgrade-mathlib runs (it has to, since it seems to be the only way currently to get the .oleans). It'd be better to allow users to update mathlib when they want with leanproject upgrade-mathlib, but for CI to just pull the .oleans as update-mathlib used to do.

[Patrick Massot]

leanproject get perfectoid-spaces will get you mathlib oleans.

[Edward Ayers]

We are having problems with leanproject and github actions, the action actions/checkout@v2 doesn't create a .git in the working directory but leanproject crashes if the working directory is not a valid git repository.

[Patrick Massot]

But I agree we still need something if mathlib is upgraded upstream and you git pull.

[Patrick Massot]

Ed, where do you see this issue?

[Wojciech Nawrocki]

Patrick Massot said:

Ed, where do you see this issue?

This is the failing build : https://github.com/b-mehta/topos/runs/501075989

[Gabriel Ebner]

I think you need to upgrade git in your docker container:

To create a local Git repository instead, add Git 2.18 or higher to the PATH

[Gabriel Ebner]

$ docker run --rm edayers/lean git version
git version 2.17.1

[Edward Ayers]

Hi I don't think this is right, everything works if I do this in docker run -it --rm edayers/lean:

git clone https://github.com/b-mehta/topos.git
cd topos
# this works:
leanproject upgrade-mathlib
rm -rf .git
# this fails:
leanproject upgrade-mathlib

I think the problem is that leanproject upgrade-mathlib is assuming it's in a git repo.

[Edward Ayers]

We worked around this by using uses actions/checkout@v1 in the github actions yaml. The problem was that actions/checkout@v2 is worse than actions/checkout@v1.

[Gabriel Ebner]

Let me rephrase that: the checkout@v2 action usually creates a git repository. But it only does it if you have git >=2.18 installed. If you have an old git version it will fall back and download a tarball.

[Edward Ayers]

Ah ok

[Edward Ayers]

This actions file works for us: :+1: :+1:

on: [push]

jobs:
  build_job:
    runs-on: ubuntu-latest
    container: edayers/lean
    name: Run leanproject build
    steps:
    - uses: actions/checkout@v1
    - run: leanproject upgrade-mathlib
    - run: leanproject build

[Patrick Massot]

Edward Ayers said:

git clone https://github.com/b-mehta/topos.git
cd topos
# this works:
leanproject upgrade-mathlib
rm -rf .git
# this fails:
leanproject upgrade-mathlib

I think the problem is that leanproject upgrade-mathlib is assuming it's in a git repo.

I can't reproduce this issue. At don't get any failure here.

[Gabriel Ebner]

I get the same error as Ed:

Traceback (most recent call last):
  File "/nix/store/gfy9cp7iinqqpbqq7d175j912wj90yah-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/lib.py", line 233, in from_path
    repo = Repo(path, search_parent_directories=True)
  File "/nix/store/m1y8zxyzbsqijnkw5qj76sxm3nwngiqv-python3.7-GitPython-3.0.5/lib/python3.7/site-packages/git/repo/base.py", line 184, in __init__
    raise InvalidGitRepositoryError(epath)
git.exc.InvalidGitRepositoryError: /home/gebner/tmp2/topos

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/nix/store/gfy9cp7iinqqpbqq7d175j912wj90yah-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 89, in upgrade_mathlib
    proj().upgrade_mathlib()
  File "/nix/store/gfy9cp7iinqqpbqq7d175j912wj90yah-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 40, in proj
    lean_upgrade)
  File "/nix/store/gfy9cp7iinqqpbqq7d175j912wj90yah-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/lib.py", line 235, in from_path
    raise InvalidLeanProject('Invalid git repository')
mathlibtools.lib.InvalidLeanProject: Invalid git repository

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/nix/store/gfy9cp7iinqqpbqq7d175j912wj90yah-mathlib-tools-0.0.3/bin/.leanproject-wrapped", line 9, in <module>
    sys.exit(cli())
  File "/nix/store/vis123mfyi0ajqg6f321h16wzs595cqw-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 764, in __call__
    return self.main(*args, **kwargs)
  File "/nix/store/vis123mfyi0ajqg6f321h16wzs595cqw-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 717, in main
    rv = self.invoke(ctx)
  File "/nix/store/vis123mfyi0ajqg6f321h16wzs595cqw-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 1137, in invoke
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "/nix/store/vis123mfyi0ajqg6f321h16wzs595cqw-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 956, in invoke
    return ctx.invoke(self.callback, **ctx.params)
  File "/nix/store/vis123mfyi0ajqg6f321h16wzs595cqw-python3.7-click-7.0/lib/python3.7/site-packages/click/core.py", line 555, in invoke
    return callback(*args, **kwargs)
  File "/nix/store/gfy9cp7iinqqpbqq7d175j912wj90yah-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 95, in upgrade_mathlib
    project.upgrade_mathlib()
  File "/nix/store/gfy9cp7iinqqpbqq7d175j912wj90yah-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/lib.py", line 474, in upgrade_mathlib
    if mathlib_lean > self.lean_version:
  File "/nix/store/gfy9cp7iinqqpbqq7d175j912wj90yah-mathlib-tools-0.0.3/lib/python3.7/site-packages/mathlibtools/lib.py", line 289, in lean_version
    return parse_version(self.pkg_config['lean_version'])
KeyError: 'lean_version'

[Kevin Buzzard]

Many many thanks @Patrick Massot , I'm at Xena and I've updated three people (some not remotely computer-literate but all of whom had carefully followed the old installation instructions) to Lean 3.6.1 + mathlib master + oleans completely painlessly with leanproject :heart: :heart: :heart:

[Kevin Buzzard]

It was important because one of them needed interval_cases which isn't in 3.4.2.

[Kevin Buzzard]

How do I do cache-olean --fetch now? I have leanproject and I've just pulled mathlib and I want to work on a (existing) branch, which is pretty up to date with master. Can I get oleans from master and then just compile the few changed files? I can't see it in these docs

[Patrick Massot]

leanproject get-cache

[Patrick Massot]

See also https://github.com/leanprover-community/mathlib-tools/blob/master/README.md for more information.

[Kevin Buzzard]

gaargh I just successfully ran pip3 install mathlibtools on Ubuntu 18.04 and leanproject isn't in my path :-/

[Johan Commelin]

Did you login again?

[Johan Commelin]

Maybe your path isn't updated yet

[Kevin Buzzard]

no

[Kevin Buzzard]

~/.mathlib/bin is in my path but there's no leanproject in there.

[Kevin Buzzard]

oh my .profile doesn't seem to have changed. I just want to fix it manually but I don't know where it is and find is taking an age

[Johan Commelin]

No, it's installed in some python path thingy...

[Kevin Buzzard]

I am reluctant to log out and in again because I don't see what this would do right now -- source .profile doesn't fix the problem.

[Johan Commelin]

Weird...

[Johan Commelin]

$ which leanproject
/home/jmc/.local/bin/leanproject

[Gabriel Ebner]

That's why we have sudo pip3 install mathlibtools in the documentation. That installs the binaries in /usr/local/bin, which should already be in your path.

[Gabriel Ebner]

If you run pip as a normal user, you need to add ~/.local/bin to your path. Unfortunately, I don't think it is in the default path on any distribution.

[Kevin Buzzard]

I read the documentation as "try it without sudo, and if you get an error try it again with sudo"

[Kevin Buzzard]

I ran it with sudo and got warnings and it didn't fix the problem ;-)

The directory '/home/buzzard/.cache/pip/http' or its parent directory is not owned by the current user and the cache has been disabled. Please check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag.
The directory '/home/buzzard/.cache/pip' or its parent directory is not owned by the current user and caching wheels has been disabled. check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag.
Requirement already satisfied: mathlibtools in ./.local/lib/python3.6/site-packages
Requirement already satisfied: gitpython in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: requests in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: Click in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: PyGithub in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: toml in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: certifi in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: tqdm in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: paramiko in ./.local/lib/python3.6/site-packages (from mathlibtools)
Requirement already satisfied: gitdb<5,>=4.0.1 in ./.local/lib/python3.6/site-packages (from gitpython->mathlibtools)
Requirement already satisfied: idna<3,>=2.5 in ./.local/lib/python3.6/site-packages (from requests->mathlibtools)
Requirement already satisfied: urllib3!=1.25.0,!=1.25.1,<1.26,>=1.21.1 in ./.local/lib/python3.6/site-packages (from requests->mathlibtools)
Requirement already satisfied: chardet<4,>=3.0.2 in ./.local/lib/python3.6/site-packages (from requests->mathlibtools)
Requirement already satisfied: deprecated in ./.local/lib/python3.6/site-packages (from PyGithub->mathlibtools)
Requirement already satisfied: pyjwt in ./.local/lib/python3.6/site-packages (from PyGithub->mathlibtools)
Requirement already satisfied: cryptography>=2.5 in ./.local/lib/python3.6/site-packages (from paramiko->mathlibtools)
Requirement already satisfied: pynacl>=1.0.1 in ./.local/lib/python3.6/site-packages (from paramiko->mathlibtools)
Requirement already satisfied: bcrypt>=3.1.3 in ./.local/lib/python3.6/site-packages (from paramiko->mathlibtools)
Requirement already satisfied: smmap<4,>=3.0.1 in ./.local/lib/python3.6/site-packages (from gitdb<5,>=4.0.1->gitpython->mathlibtools)
Requirement already satisfied: wrapt<2,>=1.10 in ./.local/lib/python3.6/site-packages (from deprecated->PyGithub->mathlibtools)
Requirement already satisfied: six>=1.4.1 in ./.local/lib/python3.6/site-packages (from cryptography>=2.5->paramiko->mathlibtools)
Requirement already satisfied: cffi!=1.11.3,>=1.8 in ./.local/lib/python3.6/site-packages (from cryptography>=2.5->paramiko->mathlibtools)
Requirement already satisfied: pycparser in ./.local/lib/python3.6/site-packages (from cffi!=1.11.3,>=1.8->cryptography>=2.5->paramiko->mathlibtools)

[Johan Commelin]

Do you have a leanproject in the .local/bin/ in your home directory?

[Kevin Buzzard]

Yes, it's working now.

[Johan Commelin]

Because otherwise I would just add that dir to your path

[Kevin Buzzard]

exactly what I did

[Gabriel Ebner]

@Kevin Buzzard Which ubuntu version are you on? All ubuntu versions I could quickly test actually add ~/.local/bin to your PATH. (But only if it exists, so you might have to restart your shell.)

[Kevin Buzzard]

All I did was source .profile and it didn't work. I don't know what else happens if you actually log out and log in again (and don't want to find out right now). I'm on 18.04

[Gabriel Ebner]

That should've actually worked.. at least it does in a docker container. I guess we should keep in mind now that sudo pip3 install mathlibtools doesn't help if you've already installed without sudo.

[Vincent Beffara]

Is it expected that leanproject up triggers a git clone of mathlib at each invocation, rather than a git pull or something lighter like that?

[Johan Commelin]

No, it shouldn't clone

[Johan Commelin]

Only leanproject get should clone

[Gabriel Ebner]

Apparently, leanproject actually removes the mathlib directory first: https://github.com/leanprover-community/mathlib-tools/blob/dbc357d2cf8f3edba8394052ede26796548f04fd/mathlibtools/lib.py#L468

[Rob Lewis]

Patrick Massot said:

Adding a command leanproject get-mathlib-cache would be trivial to implement if you really want this.

I wasn't really following this discussion before, but now I find myself needing this! Yes, we really want this.

[Rob Lewis]

I can mimic it by running leanproject get-cache in _target/deps/mathlib

[Kevin Buzzard]

If I am working on some random (non-master) branch of mathlib, and I just pulled someone else's latest commits, should I expect leanproject get-cache to return the correct olean files?

[Kevin Buzzard]

[I ask because I just tried it and it didn't fail but it gave me a broken system, and I've just tried manually compiling and it seems OK actually it's not OK, I think the branch might be broken. Is leanproject get-cache really that amazing?]

[Johan Commelin]

At least the branch of a PR should give you oleans

[Johan Commelin]

Other branches, I don't know

[Kevin Buzzard]

Is it possible that Scott somehow pushed oleans from a WIP branch and then I could pick them up?

[Johan Commelin]

Hmm... I don't know

[Johan Commelin]

Maybe we could have

leanproject export-current-oleans foobar.tar.gz
# and then send foobar.tar.gz to your collaborator who writes
leanproject import-foreign-oleans foobar.tar.gz

Alternatively, we could have a server where we can push the oleans... but I don't know how easy it would be to set that up.

[Rob Lewis]

Oleans get uploaded from every branch of leanprover-community/master, whether or not the build succeeds, whether or not there's a PR. If it doesn't compile, you get the oleans up to the point where it fails. Obviously there's a delay here since it has to run the build.

[Rob Lewis]

Allowing this from arbitrary branches (away from the community repo) is equivalent to letting anyone upload anything they want to our server, so that's not going to happen.

[Kevin Buzzard]

every branch of leanprover-community/master

What does that mean? Is the enriched branch of mathlib a "branch of leanprover-community/master" or "an arbitrary branch"?

[Gabriel Ebner]

Rob meant to say "branch in leanprover-community/mathlib".

[Gabriel Ebner]

And yes, the enriched branch has oleans available. It does not matter whether there is a PR or not.

[Kevin Buzzard]

Oh ok so I will go back to my original position of "wow"! This has just made collaborative work on a branch of mathlib much easier. Scott seems to be able to see a route to abelian categories which would be a pretty cool milestone and hopefully I can help him get there. Many thanks to everyone who has made this tooling and these backups, they make a genuine difference further down the line!

[Rob Lewis]

Gabriel Ebner said:

Rob meant to say "branch in leanprover-community/mathlib".

Ah, yes, thanks. I shouldn't post here before my morning coffee.

[Patrick Massot]

Please create issues in the mathlib-tools GitHub when you have issues or feature requests

[Kevin Buzzard]

Currently I just have love, although I have found myself writing "notes to self" about how to do the leanproject things which form my usual workflow. This is just because I have to do something ten times before I can remember it though :-)

[Patrick Massot]

This would still be good to have those notes. Maybe the README is not clear enough, or doesn't focus on the right things

[Kevin Buzzard]

currently they just tell me "leanproject get-cache gets oleans (works on mathlib and on non-mathlib projects); leanproject new makes a new project IN THE CURRENT DIRECTORY SO MAKE A SUBDIRECTORY FIRST and it uses up to date Lean and also pulls mathlib oleans"

[Kevin Buzzard]

Note that leanpkg new made a project in a new directory and I will need to be told 10 times that this is not the behaviour of leanproject new (I'm not suggesting you change it, I'm suggesting I'm a slow learner)

[Kevin Buzzard]

I will add a third line on the day I clone another Lean project from github and want to figure out the analogue of leanpkg configure, update-mathlib

[Kevin Buzzard]

The point is simply that my notes file (in my lean-projects directory) is easier for me to find than the leanproject documentation.

[Kevin Buzzard]

OK I added it: "leanproject get git@github.com/leanprover-community/lean-perfectoid-spaces.git gets a project from github and creates it in a subdirectory and also downloads mathlib oleans"

[Kevin Buzzard]

and that's all I personally need to know right now.

[Patrick Massot]

I don't get your complain about new. How do you want leanproject to guess the folder name you want if you don't write it?

[Patrick Massot]

leanproject new my_shiny_folder_name should work just fine

[Patrick Massot]

leanproject get lean-perfectoid-spaces should work too

[Gabriel Ebner]

Oh wow, you can leave out the project name in leanpkg new?

[Patrick Massot]

leanproject new without a project name is a better version of leanpkg init

[Patrick Massot]

which acts on the current directory

[Patrick Massot]

/me really wonders what is unclear in https://github.com/leanprover-community/mathlib-tools/blob/master/README.md#creating-a-new-projet

[Gabriel Ebner]

I only read the code snippets, and the only example specifies the project name. I expected an error message if I leave out the argument.

[Kevin Buzzard]

Patrick Massot said:

I don't get your complain about new. How do you want leanproject to guess the folder name you want if you don't write it?

I'm not saying anything other than "I am a stupid old man" but often before I use a command I often write command --help to remind myself how to use it. leanpkg --help tells me leanpkg new <dir> so I write the directory, leanproject --help tells me leanproject new so I don't. I write notes to help me use command line commands because my own notes are easier for me to read. I am not suggesting my notes are useful for anyone else other than to help my stupid self, I only posted them because you asked. I just like to know exactly what to type in the very few use cases I have.

[Patrick Massot]

Gabriel Ebner said:

Apparently, leanproject actually removes the mathlib directory first: https://github.com/leanprover-community/mathlib-tools/blob/dbc357d2cf8f3edba8394052ede26796548f04fd/mathlibtools/lib.py#L468

Yes, this is a bit brutal, but it is meant to avoid the weird problems we used to have with leanpkg upgrade where git would sometimes complains things are not a tree or something like this. This also avoids having zombie oleans when lean files are deleted.

[Patrick Massot]

Yesterday and today I found a bit of time for mathlibtools, so I added the get-mathlib-cache command, and also improved troubleshooting capabilities. Did I miss any feature request? (Again, creating GitHub issues for bug reports and feature requests would help a lot). I know I still have the refactor request to drop dependency on leanpkg, but this has pretty low priority for me. If there are no more obvious requests then I'll release a 0.0.4 version on PyPi.

[Patrick Massot]

But before that it would be nice to hear about some real world test of leanproject get-mathlib-cache. In order to test this, you only need to clone the master branch and pip install it.

[Kevin Buzzard]

How is this different to get-cache?

[Patrick Massot]

If you are editing mathlib this is the same thing. In another project this will get you mathlib oleans without changing the mathlib version mentioned in leanpkg.toml.

[Patrick Massot]

(contrasting with upgrade-mathlib that will give you the latest mathlib)

[Kevin Buzzard]

upgrade-mathlib might also change your lean version. Is this correct? I hadn't expected this.

[Kevin Buzzard]

But how is get-mathlib-cache different to get-cache?

[Patrick Massot]

Say you are in the perfectoid spaces project. Then get-cache will try to find cached perfectoid oleans, whereas get-mathlib-cache will try to find cached mathlib oleans.

[Kevin Buzzard]

Oh --- to do this I just change into target deps mathlib and get cache :-)

[Patrick Massot]

Yes, this also works, but it's arguably less nice.

[Edward Ayers]

Ok so suppose that I have a project and I have a leanpkg.toml and I don't want to upgrade anything I just want to get the oleans for mathlib and build. How do I do that with leanproject?

[Bryan Gin-ge Chen]

(deleted)

[Johan Commelin]

No, leanproject get-mathlib-cache

[Johan Commelin]

If that is merged already

[Johan Commelin]

Otherwise cd _target/mathlib/ ; leanproject get-cache

[Bryan Gin-ge Chen]

Yes, Johan is right. get-mathlib-cache been merged, here it is in the readme.

[Edward Ayers]

is it available upon calling pip3 install mathlibtools?

[Johan Commelin]

Who knows?? :stuck_out_tongue_wink:

[Edward Ayers]

I don't think it is

[Johan Commelin]

It certainly will be rather soon

[Edward Ayers]

Ok, I'll wait

[Patrick Massot]

I was waiting for people to test it locally before pushing to PyPi.

[Patrick Massot]

Ok, I can see people won't test it if it's not released. https://pypi.org/project/mathlibtools/0.0.4/

[Rob Lewis]

FYI, get-mathlib-cache just worked very nicely for me. Thanks!

[Kevin Buzzard]

Thanks as ever Patrick. I should probably here openly that this tooling has really changed my workflow. Patrick asked some technical elaboration question here, which involved having to use some branch of mathlib; I have a local clone of mathlib, so I used the command line to update mathlib and switch to the branch in question, and then I downloaded the fully compiled oleans in a matter of seconds.

[Kevin Buzzard]

I felt that this was a very clean and effective way of passing a sorry between two people.

[Scott Morrison]

Yes, thank you Patrick, the new leanproject is great. Thanks also to the work Rob and Gabriel have put into speeding up CI, that has been hugely productive as well.

[Kevin Buzzard]

Many thanks to Patrick, Rob, Gabriel, Simon and everyone else who was involved.

[Shing Tak Lam]

Hello, when I ran leanproject new derivations it started downloading lean 3.4.2. Is this correct?

$ leanproject new derivations
> mkdir -p derivations
> cd derivations
> mkdir src
> git init -q
> git checkout -b lean-3.4.2
Switched to a new branch 'lean-3.4.2'
configuring derivations 0.1
Adding mathlib
Adding mathlib
info: downloading component 'lean'

[Kevin Buzzard]

That confused me too when it happened -- but I think when it says downloading component 'lean' it might be downloading 3.7.1 or anything -- depending on what it in the toml. I think it is just randomly making a branch in your project called lean-3.4.2 for no obvious reason.

[Shing Tak Lam]

Yeah I see now. It does seem to be downloading 3.7.2

[Kevin Buzzard]

When it's all over, look at the file leanpkg.toml in the root of the project, and also _target/deps/mathlib/leanpkg.toml. They should both say lean_version = "leanprover-community/lean:3.7.2"

[Kevin Buzzard]

While you're in _target/deps/mathlib you can go into src/data and see if you have just .lean files, or also a bunch of .olean files. If you have the oleans, you're in good shape.

[Shing Tak Lam]

Alright, thank you.

[Kevin Buzzard]

~/tmp$ leanproject get git@github.com:ImperialCollegeLondon/real-number-game.git
Cloning from git@github.com:ImperialCollegeLondon/real-number-game.git
configuring real-number-game 0.1
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> mkdir -p _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 58, done.
remote: Counting objects: 100% (58/58), done.
remote: Compressing objects: 100% (49/49), done.
remote: Total 39653 (delta 19), reused 18 (delta 9), pack-reused 39595
Receiving objects: 100% (39653/39653), 19.02 MiB | 9.96 MiB/s, done.
Resolving deltas: 100% (30230/30230), done.
> git checkout --detach f86abc7781d85564a9fba9f3deafe73453d22e8d    # in directory _target/deps/mathlib
HEAD is now at f86abc77 fix(*): lower instance priority (#1724)
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/f86abc7781d85564a9fba9f3deafe73453d22e8d.tar.gz to /home/buzzard/.mathlib/f86abc7781d85564a9fba9f3deafe73453d22e8d.tar.gz
Looking for GitHub mathlib oleans
Warning: This does not seem to be a git repository. Expect weird things...
Trying to download https://github.com/leanprover-community/mathlib-nightly/releases/download/nightly-2019-11-23/mathlib-olean-nightly-2019-11-23.tar.gz to /home/buzzard/.mathlib/f86abc7781d85564a9fba9f3deafe73453d22e8d.tar.gz
100%|████████████████████████████████████████████████████████████████████████████████████████████████████| 21.2M/21.2M [00:01<00:00, 15.0MiB/s]
Found GitHub mathlib oleans
~/tmp$

Why does it say Warning: This does not seem to be a git repository. Expect weird things...?

[Alex J. Best]

After leanproject hooks I get

hint: The '.git/hooks/post-checkout' hook was ignored because it's not set as executable.
hint: You can disable this warning with `git config advice.ignoredHook false`.