## Stream: general

### Topic: update-mathlib

#### 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)?

#### Patrick Massot (May 02 2019 at 15:09):

You have cache-olean for that

#### Johan Commelin (May 02 2019 at 15:10):

Huh? Did I miss something?

#### Johan Commelin (May 02 2019 at 15:10):

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

#### Simon Hudon (May 02 2019 at 15:12):

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

#### Simon Hudon (May 02 2019 at 15:12):

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

#### 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

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

#### Simon Hudon (May 02 2019 at 15:26):

No way, more like 56% ...

#### 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

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

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

Oh. I guess so.

#### 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

#### Scott Morrison (May 03 2019 at 10:18):

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

#### Johan Commelin (May 03 2019 at 10:19):

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

#### Johan Commelin (May 03 2019 at 10:19):

After all Travis is already doing that.

#### Johan Commelin (May 03 2019 at 10:19):

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

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