update-mathlib

Stream: general

[Johan Commelin]

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

[Patrick Massot]

You have cache-olean for that

[Johan Commelin]

Huh? Did I miss something?

[Johan Commelin]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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]

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]

No way, more like 56% ...

[Simon Hudon]

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]

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]

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

[Scott Morrison]

Oh. I guess so.

[Scott Morrison]

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]

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

[Johan Commelin]

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

[Johan Commelin]

After all Travis is already doing that.

[Johan Commelin]

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

[Scott Morrison]

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)

[Johan Commelin]

You download them from Github.

[Scott Morrison]

That works too :-)