PR 1000

Stream: general

[Scott Morrison]

so... who is going to make pull request (or issue) #1000?

[Simon Hudon]

me

[Simon Hudon]

Actually, I'm having trouble with your server.

[Simon Hudon]

I'm fetching an archive but lean still needs to rebuild

[Scott Morrison]

uhoh

[Scott Morrison]

which archive?

[Scott Morrison]

or rather, which branch?

[Simon Hudon]

master

[Simon Hudon]

7f9717fdb0d0c75b61aa0f5a8fc829c2bfcb5cf8

[Scott Morrison]

hmm

[Scott Morrison]

Ok, just nuked that cache file, let's see if it rebuilds successfully.

[Simon Hudon]

Do you have statistics about the delay between when a commit is pushed and when you have a cache file for it?

[Scott Morrison]

I think compile times from scratch are about 8 minutes on that computer, so it really shouldn't be above 10 minutes

[Scott Morrison]

and if there's a cache available, faster

[Simon Hudon]

that's pretty good

[Simon Hudon]

What if there are multiple commits at the same time?

[Scott Morrison]

it's recompiled master, as https://tqft.net/lean/mathlib/olean-8f5d240178d11b90e0bb79e777aef6055fb5cd8f.bz2

[Scott Morrison]

that will slow down all of them

[Scott Morrison]

it only uploads the files once it has recompiled everything new

[Scott Morrison]

that's a bit dumb, but the "is there anything to compile" logic lives inside cache-olean --build-new, and it can't upload stuff

[Simon Hudon]

That can be fixed

[Simon Hudon]

I'm still having trouble with master