Zulip Chat Archive

Stream: general

Topic: setup-update-mathlib.sh

Scott Morrison (Mar 18 2019 at 23:42):

Is there any documentation for setup-update-mathlib.sh? I ran it, but I'm not quite sure what to expect when I then run update-mathlib. Reading the code, I can see that it is for running in projects that have a dependency on mathlib. However, when I ran update-mathlib in a project with leanpkg.toml file:

[package]
name = "ITP-2019"
version = "0.1"
lean_version = "nightly-2019-01-13"
path = "src"

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

I just get the output

$ update-mathlib
Querying GitHub...
Error: no nightly archive found

Presumably I'm doing something wrong, and my leanpkg.toml is not "how it's meant to be".

Scott Morrison (Mar 18 2019 at 23:42):

Should I change the lean_version = ... line? Should I remove the branch = "master" key in the dependencies section?

Simon Hudon (Mar 18 2019 at 23:44):

select 3.4.2 as your lean version and do leanpkg upgrade first

Scott Morrison (Mar 18 2019 at 23:44):

Should I remove the branch="master" key then?

Simon Hudon (Mar 18 2019 at 23:46):

Yes, I believe so

Mario Carneiro (Mar 18 2019 at 23:47):

I want to second this request for documentation. I don't like running scripts when I don't understand what they do, especially if they change my configuration data

Mario Carneiro (Mar 18 2019 at 23:48):

Also I'm not talking about how to use the script, that's usually easy. I'm talking about what it is attempting to do specifically, what it looks for, and so on, so I can predict when and why it will fail

Scott Morrison (Mar 18 2019 at 23:53):

Also --- is there hope to have leanpkg upgrade call update-mathlib?

Simon Hudon (Mar 18 2019 at 23:54):

I'll get on the documentation. As for leanpkg, it's in the work. I was under the impression it wasn't wanted so I didn't put a high priority on it. I'll get back to it

Scott Morrison (Mar 18 2019 at 23:55):

Thanks, @Simon Hudon. I really appreciate this infrastructure work, and don't want to load too much stuff on your plate -- I could try writing some docs too (sometimes it's helpful if someone who doesn't actually understand stuff writes them :-)

Scott Morrison (Mar 18 2019 at 23:56):

The other question about infrastructure I had is --- what are the prospects for downloading cached olean files when switching branches inside mathlib?

Scott Morrison (Mar 18 2019 at 23:56):

This is still the killer for me.

Kevin Buzzard (Mar 18 2019 at 23:56):

Me too, but I couldn't really envisage a solution.

Kevin Buzzard (Mar 18 2019 at 23:56):

if I'm editing algebra.group then I know I'm in for a certain amount of pain anyway

Scott Morrison (Mar 18 2019 at 23:58):

From memory the two proposed solutions had just been:
1) every time we switch branches, stash away all the olean files, and pull out the stashed olean files for the other branch (if any have previously been stashed).
2) do everything mediated via sccache.

Simon Hudon (Mar 18 2019 at 23:59):

@Scott Morrison I would really appreciate your perspective on that. If you have time to do it, I'll fix any oversight or mistake

Scott Morrison (Mar 18 2019 at 23:59):

For 1, I think the problem was just that timestamps weren't working, and the deployed oleans weren't being used??

Scott Morrison (Mar 18 2019 at 23:59):

For 2, I never understood enough to know what the obstacles were.

Simon Hudon (Mar 19 2019 at 00:00):

@Scott Morrison That's right. I started over with 1) and started zipping the olean and lean files and hooking the cache into git. I still need to test more. I think I also need to integrate with update-mathlib when creating new branches from master or lean-3.4.2

Scott Morrison (Mar 19 2019 at 00:01):

Having option 1) would be really helpful.

Simon Hudon (Mar 19 2019 at 00:02):

for 2), I did some work, it proved harder and less reliable than I hoped so I put it aside

Scott Morrison (Mar 19 2019 at 00:03):

Great to know --- 2) did sound daunting; sccache was going to require us to jump through their hoops.

Simon Hudon (Mar 19 2019 at 00:04):

That's true. 1) might end up easier to use

Bryan Gin-ge Chen (Mar 28 2019 at 20:26):

I'm having trouble with update-mathlib:

Traceback (most recent call last):
  File "/Users/chb/.mathlib/bin/update-mathlib", line 21, in auth_github
    return Github(config.get('github', 'user'), config.get('github', 'password'))
  File "/Users/chb/Library/Python/3.7/lib/python/site-packages/git/config.py", line 79, in assure_data_present
    return func(self, *args, **kwargs)
  File "/usr/local/Cellar/python/3.7.3/Frameworks/Python.framework/Versions/3.7/lib/python3.7/configparser.py", line 780, in get
    d = self._unify_values(section, vars)
  File "/usr/local/Cellar/python/3.7.3/Frameworks/Python.framework/Versions/3.7/lib/python3.7/configparser.py", line 1146, in _unify_values
    raise NoSectionError(section) from None
configparser.NoSectionError: No section: 'github'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/Users/chb/.mathlib/bin/update-mathlib", line 63, in <module>
    g = auth_github()
  File "/Users/chb/.mathlib/bin/update-mathlib", line 22, in auth_github
    except configparser.NoOptionError:
NameError: name 'configparser' is not defined

Am I supposed to have my github username and password stored in my git config somehow?

Simon Hudon (Mar 28 2019 at 20:27):

It would help but it's not supposed to fail if it's not there. Let me just have a look

Bryan Gin-ge Chen (Mar 28 2019 at 20:28):

Right now I authenticate using an SSH key which is stored in the macOS keychain.

Simon Hudon (Mar 28 2019 at 20:32):

Can you try again?

Bryan Gin-ge Chen (Mar 28 2019 at 20:35):

  File "/Users/chb/.mathlib/bin/update-mathlib", line 24
    continue
    ^
SyntaxError: 'continue' not properly in loop

Scott Morrison (Mar 28 2019 at 20:59):

Oh ---- I'd thought I'd updated this code, but it turns out it is repeated across update-mathlib.py and cache-olean.py, and only the second was updated.

Scott Morrison (Mar 28 2019 at 20:59):

We should factor that out into a module, and import it in both files.

Scott Morrison (Mar 28 2019 at 21:00):

Similarly, update-mathlib.py should use the ctrl-c protection on file operations that I put into cache-olean.py (in #858).

Scott Morrison (Mar 28 2019 at 21:00):

I won't have a chance to do any of this until the weekend.

Simon Hudon (Mar 28 2019 at 23:17):

@Bryan Gin-ge Chen I tried a quick fix (copy pasting with @Scott Morrison put in cache-olean.py). When you can, please try again.

Bryan Gin-ge Chen (Mar 28 2019 at 23:47):

Still no luck. I think this is the same error as I originally had:

Traceback (most recent call last):
  File "/Users/chb/.mathlib/bin/update-mathlib", line 21, in auth_github
    return Github(config.get('github', 'user'), config.get('github', 'password'))
  File "/Users/chb/Library/Python/3.7/lib/python/site-packages/git/config.py", line 79, in assure_data_present
    return func(self, *args, **kwargs)
  File "/usr/local/Cellar/python/3.7.3/Frameworks/Python.framework/Versions/3.7/lib/python3.7/configparser.py", line 780, in get
    d = self._unify_values(section, vars)
  File "/usr/local/Cellar/python/3.7.3/Frameworks/Python.framework/Versions/3.7/lib/python3.7/configparser.py", line 1146, in _unify_values
    raise NoSectionError(section) from None
configparser.NoSectionError: No section: 'github'

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/Users/chb/.mathlib/bin/update-mathlib", line 66, in <module>
    g = auth_github()
  File "/Users/chb/.mathlib/bin/update-mathlib", line 22, in auth_github
    except configparser.NoSectionError:
NameError: name 'configparser' is not defined

Simon Hudon (Mar 29 2019 at 00:06):

I'm hoping this time I tested it properly

Bryan Gin-ge Chen (Mar 29 2019 at 00:09):

OK, this seems like progress:

No github section found in 'git config'
Querying GitHub...
Error: no nightly archive found

Simon Hudon (Mar 29 2019 at 00:10):

ok good

Simon Hudon (Mar 29 2019 at 00:10):

Now try leanpkg upgrade it will give you the latest version in the lean-3.4.2 branch which always has a nightly associated

Simon Hudon (Mar 29 2019 at 00:10):

Then update-mathlib

Bryan Gin-ge Chen (Mar 29 2019 at 00:26):

OK, I think it's finally working! Thanks!

What's recommended for lean_version leanpkg.toml now? I've been using nightly there, which at least gets leanpkg upgrade to pull the latest commit of mathlib, though it also gives me this warning every time:

WARNING: Lean version mismatch: installed version is nightly-2019-01-13, but package requires nightly

When I use 3.4.2 as the version string, leanpkg upgrade used to pull a really old commit, though it looks like now it's just a few days old.

Bryan Gin-ge Chen (Mar 29 2019 at 00:27):

I think things happened to work for me just now because the latest nightly at mathlib-nightly just came out with the same tag as the most recent commit to mathlib.

Simon Hudon (Mar 29 2019 at 00:40):

Travis updates the lean-3.4.2 branch every time it uploads a nightly build so lean_version = 3.4.2 is the recommended setting.

Bryan Gin-ge Chen (Mar 29 2019 at 00:45):

Does it usually take a while? The lean-3.4.2 branch is currently pointing to commit 291a4f3 which is nightly-2019-03-25.

Bryan Gin-ge Chen (Mar 29 2019 at 01:02):

Ah, something is broken there https://travis-ci.org/leanprover-community/mathlib/jobs/512774251#L540

Bryan Gin-ge Chen (Mar 29 2019 at 01:05):

I guess the fact that there's both a tag named lean-3.4.2 and a branch named the same is a problem.

Bryan Gin-ge Chen (Mar 29 2019 at 01:09):

I think this line should be:

git push mathlib HEAD:refs/heads/$LEAN_VERSION || \

Bryan Gin-ge Chen (Mar 29 2019 at 02:50):

PR'd

Simon Hudon (Mar 29 2019 at 02:56):

merged! Is it some sort of record?

Johan Commelin (Mar 29 2019 at 07:57):

@Simon Hudon Could you please kickstart the system again? We are stuck with an ancient library-search-less mathlib because of the silly 3.4.2-tag

Johan Commelin (Mar 29 2019 at 12:02):

Do I understand correctly that @Bryan Gin-ge Chen's patch prevents the silly 3.4.2-tag from breaking the system if it resurrects itself in the future? Because that tag is very hard to kill.