cache-olean

Stream: general

[Jeremy Avigad]

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

That certainly shouldn't happen

[Simon Hudon]

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

[Johan Commelin]

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

I'm really glad it helps :)

[Chris Hughes]

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

[Bryan Gin-ge Chen]

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

[Chris Hughes]

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]

Did you cache a build?

[Chris Hughes]

How do I do that?

[Chris Hughes]

I was on the master branch

[Simon Hudon]

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

[Chris Hughes]

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

[Chris Hughes]

lean-3.4.2 works by the way. Thanks.

[Simon Hudon]

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]

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

It is still not connected to Scott's server

[Floris van Doorn]

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]

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]

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

[Simon Hudon]

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

[Floris van Doorn]

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]

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

[Rob Lewis]

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]

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]

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]

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]

Maybe not though. I'll check next week.

[Simon Hudon]

Ok, please keep me posted.

[Floris van Doorn]

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]

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]

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

That's right

[Simon Hudon]

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]

@Simon Hudon @Scott Morrison Any progress here?

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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

[Simon Hudon]

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

[Johan Commelin]

But that is commits to master, I guess

[Simon Hudon]

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

[Floris van Doorn]

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]

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]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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]

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.