Zulip Chat Archive

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?

Scott Morrison (May 03 2019 at 10:17):

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)

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

You download them from Github.

Scott Morrison (May 03 2019 at 10:19):

That works too :-)


Last updated: Dec 20 2023 at 11:08 UTC