Zulip Chat Archive

Stream: general

Topic: cache-olean


Jeremy Avigad (Apr 16 2019 at 13:40):

@Simon Hudon cache-olean doesn't seem to be working for me. I am on branch lean-3.4.2, I fetched and merged the latest version, and did this:

avigad@avigad-ThinkPad-T460:~/projects/mathlib$ cache-olean --fetch
No github section found in 'git config'
Querying GitHub...
Downloading nightly...
... successfully extracted olean archive.
avigad@avigad-ThinkPad-T460:~/projects/mathlib$ lean --make

It is recompiling the whole library. That shouldn't happen, should it? Can you tell if I am doing something wrong?

Simon Hudon (Apr 16 2019 at 15:17):

That certainly shouldn't happen

Simon Hudon (Apr 16 2019 at 15:18):

what if you do cache-olean --fetch and leanpkg build instead?

Johan Commelin (May 08 2019 at 08:30):

@Simon Hudon I just want to give you a very big Thank You :trademark:. Using update-mathlib and cache-olean has made development so much smoother. It is so much easier to switch branches, and add quick contributions. Kudos!

Simon Hudon (May 08 2019 at 16:24):

I'm really glad it helps :)

Chris Hughes (May 08 2019 at 16:26):

What is cache-olean? How do I find out how to use it?

Bryan Gin-ge Chen (May 08 2019 at 16:27):

It looks like it's documented here: https://github.com/leanprover-community/mathlib/blob/master/docs/howto-contribute.md#caching-compilation

Chris Hughes (May 08 2019 at 16:52):

I get this error

dyn894-237:mathlib chrishughes$ cache-olean --fetch
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Error: no nightly archive found
no cache found

Simon Hudon (May 08 2019 at 16:54):

Did you cache a build?

Chris Hughes (May 08 2019 at 16:54):

How do I do that?

Chris Hughes (May 08 2019 at 16:55):

I was on the master branch

Simon Hudon (May 08 2019 at 16:55):

If you want to use the nightly, switch to the head of lean-3.4.2

Chris Hughes (May 08 2019 at 16:57):

And it works for my community branches right? How do I do that?

Chris Hughes (May 08 2019 at 16:57):

lean-3.4.2 works by the way. Thanks.

Simon Hudon (May 08 2019 at 17:00):

For your branches, you build it first, then you call cache-olean and it will cache your build. When you switch to another branch and then come back, git will restore your binaries and you can pick up where you left off

Johan Commelin (May 08 2019 at 17:00):

@Chris Hughes When we switch over to the archives on Scott's server you will have "nightlies" for every commit of every branch. Scott is polling github every minute, and then he just needs to compile. If I understand the setup correctly...

Simon Hudon (May 08 2019 at 17:00):

It is still not connected to Scott's server

Floris van Doorn (May 08 2019 at 21:27):

I tried using cache-olean, and it works for me. However, I'm on a Windows computer and configured git with autocrlf = true, so that my line endings are CRLF locally (that was what I was advised when I started using git). Running cache-olean changes all my line-endings to LF, and after doing git checkout -- . I think that Lean will try to rebuild the whole library from scratch.

Should I just burn down my whole git repository to the ground and reclone it using autocrlf = false or is there a simpler workaround? (I don't think that any of the programs I use care whether the line endings are CRLF or LF.)

Simon Hudon (May 08 2019 at 21:50):

I remember seeing a commit that does what you describe but I can't seem to find it. I think @Scott Morrison helped with this.

Bryan Gin-ge Chen (May 08 2019 at 21:53):

Does @Gabriel Ebner's fix to lean 3.4.2 here apply to this problem or not?

Simon Hudon (May 08 2019 at 21:55):

It looks like it would. @Floris van Doorn can you confirm that it actually causes you to recompile?

Floris van Doorn (May 08 2019 at 21:57):

It did. The following finishes in a couple of seconds:

git checkout blessed/lean-3.4.2
cache-olean --fetch
leanpkg build

The following ran for a couple of minutes until I killed it:

git checkout blessed/lean-3.4.2
cache-olean --fetch
git status
git checkout -- .
leanpkg build

Floris van Doorn (May 08 2019 at 22:00):

I did change my autocrlf setting to false, and that works well.

Rob Lewis (May 17 2019 at 14:09):

I'm finally getting around to setting up cache-olean. After moving scripts to their own repo, the install directions need to be updated, but that's easy enough. More worrying, I got this trace checking out a branch. Any idea what's up here?

Trying to fetch cached olean
Querying remote Mathlib cache...
Error: revision not found
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Downloading nightly...
Traceback (most recent call last):
  File "/home/rob/.mathlib/bin/cache-olean", line 145, in <module>
    fetch_mathlib(asset)
  File "/home/rob/.mathlib/bin/cache-olean", line 104, in fetch_mathlib
    f.write(req.data)
TypeError: __exit__() takes 1 positional argument but 4 were given

Rob Lewis (May 17 2019 at 14:16):

As for updating the docs. Perhaps setup_dev_scripts.sh should be moved back to mathlib, and should check mathlib-scripts on Github for the scripts it needs to download?

Simon Hudon (May 17 2019 at 17:25):

It's curious. The line info in this error is not consistent with the version in mathlib-tools. Are you sure you have a recent version?

Rob Lewis (May 17 2019 at 17:27):

I'm not at the office anymore so I can't check until Monday, but I think so... I had a fresh checkout of mathlib-tools for moving your PR over from mathlib.

Rob Lewis (May 17 2019 at 17:28):

Maybe not though. I'll check next week.

Simon Hudon (May 17 2019 at 17:28):

Ok, please keep me posted.

Floris van Doorn (May 17 2019 at 19:02):

Lately, whenever I run cache-olean --fetch I get an error that no nightly archive is found. This happens when I am on the master branch of mathlib-community (and also if I'm a couple commits behind master - is there a delay in the availability of binaries?).

Floris@MSI MINGW64 /d/projects/mathlib (master)
$ cache-olean --fetch
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Error: no nightly archive found
no cache found

Floris van Doorn (May 17 2019 at 19:05):

Oh wait, I forgot you had to be on the lean-3.4.2 branch. Is this what https://github.com/leanprover-community/mathlib-tools/pull/2 is implementing?

Simon Hudon (May 17 2019 at 19:06):

I forgot you had to be on the lean-3.4.2 branch

That's right

Simon Hudon (May 17 2019 at 19:07):

Is this what https://github.com/leanprover-community/mathlib-tools/pull/2 is implementing?

That's a project that Scott and I are working on so that you can get a binary for every commit. It's not there yet.

Johan Commelin (May 24 2019 at 19:29):

@Simon Hudon @Scott Morrison Any progress here?

Johan Commelin (Dec 06 2019 at 07:55):

mathlib is moving ever so slightly faster. I'm finding that if one works on a bunch of related PRs, then it's really nice to be able to work on master instead of yesterdays lean-3.4.2. Are there any options on the horizon of publishing binaries for every commit of the last 3 days (say) and only storing 1 set of binaries per day for older versions of master?

Simon Hudon (Dec 06 2019 at 17:04):

I have not looked into it. I think that's possible but you need every build of master to do a deployment. You can look in the travis file and in scripts/deploy-nightly.sh. scripts/deploy-nightly.sh should be changed a bit so that it does not push to lean-3.4.2 when deploying the build. As for deleting old releases, I'm not sure how to do that. We can try with a cron job on travis.

Simon Hudon (Dec 06 2019 at 17:04):

Another approach would be to look into Github actions. It might be easier to configure

Johan Commelin (Dec 06 2019 at 17:39):

Are there more people who think it would be useful to increase the frequency of binary releases? If it's just me, I don't think we should spend energy on this change.

Johan Commelin (Dec 06 2019 at 17:40):

So, thumbs up on this message, if you would like to have binary releases for every commit on master for the last 3 days. And thumbs down if you don't want/need that.

Patrick Massot (Dec 06 2019 at 17:44):

I even wish PRs buils would be available so that I have at least access to tactic state when reviewing complicated PRs.

Bryan Gin-ge Chen (Dec 06 2019 at 17:57):

Github actions supports attaching downloadable "artifacts" to every build (on every branch), so all this is possible. Probably that can be integrated into the cache-olean script in a clever way too.

Johan Commelin (Dec 06 2019 at 18:03):

Are there statistics on the average number of commits to the github repo per day? (So not master, but all branches.)

Simon Hudon (Dec 06 2019 at 18:55):

have a look at https://github.com/leanprover-community/mathlib/graphs/commit-activity

Johan Commelin (Dec 06 2019 at 19:02):

But that is commits to master, I guess

Simon Hudon (Dec 06 2019 at 19:19):

Right, then I don't know how to do better

Floris van Doorn (Dec 06 2019 at 19:20):

I would be happier with builds on PR commits (as Patrick mentions) than more frequent master builds.

  • master builds will be useful, but one question is when will they be available: the moment the commit happens or a couple hours later? In the latter case there is little improvement over the current situation.
  • PR builds (also of failing builds, if possible - in this case all the .olean files that were succesfully produced) will be very useful: to build on top of the PR before it has been merged, to review in VSCode, and for failing builds: to fix build failures more easily.

Simon Hudon (Dec 06 2019 at 19:24):

I think instead of going in the direction of picking the right commits to cache the build of, I think getting sccache to support Lean might do a better job. What it does is every time you try to compile one file it checks if this exact file (with its exact contents and the exact content of its dependencies) has been compiled by any other user in the past.

Rob Lewis (Dec 06 2019 at 20:02):

Github actions supports attaching downloadable "artifacts" to every build (on every branch), so all this is possible. Probably that can be integrated into the cache-olean script in a clever way too.

I wonder how long they're stored, how predictable the URLs are, and if there's a cap on the artifact size. If those all have reasonable answers, I think this is a great reason to switch.

Rob Lewis (Dec 06 2019 at 20:03):

Also I've been getting annoyed with the random Travis failures because a PR happened to be merged during the build.

Rob Lewis (Dec 06 2019 at 20:03):

I don't know the first thing about sccache, that sounds reasonable too.

Rob Lewis (Dec 06 2019 at 20:04):

But there are independent reasons to switch to GitHub Actions for CI, so if it will let us cache oleans for all PRs without much effort, let's go for it.

Bryan Gin-ge Chen (Dec 06 2019 at 20:14):

I wonder how long they're stored, how predictable the URLs are, and if there's a cap on the artifact size.

According to the page it looks like they're stored for 90 days, which is probably OK for PR's and non-cron master commits. For really old PRs, we would probably want to do a merge commit with master anyways, and that would trigger a new build.

Not sure about the URLs, but I did see this:

GitHub does not currently offer a REST API to retrieve uploaded artifacts.

So, this might be tricky.

I couldn't find any info about size caps, so my guess is that we'd be fine.


Last updated: Dec 20 2023 at 11:08 UTC