Zulip Chat Archive

Stream: general

Topic: update-mathlib


view this post on Zulip Johan Commelin (May 02 2019 at 15:09):

@Simon Hudon How far are we from having update-mathlib work for mathlib itself (vs projects that depend on mathlib)?

view this post on Zulip Patrick Massot (May 02 2019 at 15:09):

You have cache-olean for that

view this post on Zulip Johan Commelin (May 02 2019 at 15:10):

Huh? Did I miss something?

view this post on Zulip Johan Commelin (May 02 2019 at 15:10):

What is cache-olean? Where do I get it? How much does it cost?

view this post on Zulip Simon Hudon (May 02 2019 at 15:12):

In mathlib, run scripts/setup-dev-scripts.py

view this post on Zulip Simon Hudon (May 02 2019 at 15:12):

then you can run setup-lean-git-hooks and you're all set

view this post on Zulip Simon Hudon (May 02 2019 at 15:13):

It will cache your compiled files when you commit and will try to fetch things when you check out a branch. If the branch you're checking out has a nightly, it will use it

view this post on Zulip Johan Commelin (May 02 2019 at 15:24):

Ok, so I ran cache-olean --fetch in my mathlib directory, and of course it didn't find a nightly on Github. Does this mean I will still have to recompile mathlib myself in 57% of the cases?

view this post on Zulip Simon Hudon (May 02 2019 at 15:26):

No way, more like 56% ...

view this post on Zulip Simon Hudon (May 02 2019 at 15:27):

What you can do is find a version that does have a nightly, do cache-olean --fetch then checkout your branch and you should have less to rebuild

view this post on Zulip Johan Commelin (May 02 2019 at 15:40):

Sure... that does help a bit. But if the latest commits touch some basic files in the hierarchy (which does happen quite often) it is the difference between recompiling 70% or 60% of mathlib...
Anyway, I very much appreciate all the work you are doing to make these things easy for users. Maybe we can still find a place to host all these nightlies for us?

view this post on Zulip Johan Commelin (May 02 2019 at 15:41):

@Scott Morrison Can't you just run a cronjob to all the new nightlies from github every day...? That solves the "pushing to your server" issue, right?

view this post on Zulip Scott Morrison (May 03 2019 at 10:17):

Oh. I guess so.

view this post on Zulip Scott Morrison (May 03 2019 at 10:18):

So I'd just have a script that
1) pulls all branches on leanprover-community
2) runs cache-olean --build in each of them
3) posts the resulting olean archive file somewhere public

view this post on Zulip Scott Morrison (May 03 2019 at 10:18):

and we'd update cache-olean --fetch so that it also looks there

view this post on Zulip Johan Commelin (May 03 2019 at 10:19):

Ooh, I thought you might not even have to do the compiling...

view this post on Zulip Johan Commelin (May 03 2019 at 10:19):

After all Travis is already doing that.

view this post on Zulip Johan Commelin (May 03 2019 at 10:19):

Travis should just post them to some temporary space (e.g., Github)

view this post on Zulip Scott Morrison (May 03 2019 at 10:19):

I won't get to this immediately, but if someone wants to write that script for me (just a stub for step 3 is fine, I'll fill in scp to my server)

view this post on Zulip Johan Commelin (May 03 2019 at 10:19):

You download them from Github.

view this post on Zulip Scott Morrison (May 03 2019 at 10:19):

That works too :-)


Last updated: May 13 2021 at 21:12 UTC