## Stream: general

### Topic: PR 1000

#### Scott Morrison (May 08 2019 at 23:02):

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

me

#### Simon Hudon (May 08 2019 at 23:11):

Actually, I'm having trouble with your server.

#### Simon Hudon (May 08 2019 at 23:12):

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

uhoh

which archive?

#### Scott Morrison (May 08 2019 at 23:25):

or rather, which branch?

master

#### Simon Hudon (May 08 2019 at 23:26):

7f9717fdb0d0c75b61aa0f5a8fc829c2bfcb5cf8

hmm

#### Scott Morrison (May 08 2019 at 23:28):

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

#### Simon Hudon (May 08 2019 at 23:43):

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

#### Scott Morrison (May 08 2019 at 23:44):

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

#### Scott Morrison (May 08 2019 at 23:45):

and if there's a cache available, faster

#### Simon Hudon (May 08 2019 at 23:46):

that's pretty good

#### Simon Hudon (May 08 2019 at 23:46):

What if there are multiple commits at the same time?

#### Scott Morrison (May 08 2019 at 23:46):

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

#### Scott Morrison (May 08 2019 at 23:46):

that will slow down all of them

#### Scott Morrison (May 08 2019 at 23:46):

it only uploads the files once it has recompiled everything new

#### Scott Morrison (May 08 2019 at 23:47):

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 (May 08 2019 at 23:48):

That can be fixed

#### Simon Hudon (May 08 2019 at 23:50):

I'm still having trouble with master

Last updated: May 18 2021 at 16:25 UTC