Zulip Chat Archive

Stream: general

Topic: PR 1000


view this post on Zulip Scott Morrison (May 08 2019 at 23:02):

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

view this post on Zulip Simon Hudon (May 08 2019 at 23:05):

me

view this post on Zulip Simon Hudon (May 08 2019 at 23:11):

Actually, I'm having trouble with your server.

view this post on Zulip Simon Hudon (May 08 2019 at 23:12):

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

view this post on Zulip Scott Morrison (May 08 2019 at 23:25):

uhoh

view this post on Zulip Scott Morrison (May 08 2019 at 23:25):

which archive?

view this post on Zulip Scott Morrison (May 08 2019 at 23:25):

or rather, which branch?

view this post on Zulip Simon Hudon (May 08 2019 at 23:26):

master

view this post on Zulip Simon Hudon (May 08 2019 at 23:26):

7f9717fdb0d0c75b61aa0f5a8fc829c2bfcb5cf8

view this post on Zulip Scott Morrison (May 08 2019 at 23:27):

hmm

view this post on Zulip Scott Morrison (May 08 2019 at 23:28):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 08 2019 at 23:45):

and if there's a cache available, faster

view this post on Zulip Simon Hudon (May 08 2019 at 23:46):

that's pretty good

view this post on Zulip Simon Hudon (May 08 2019 at 23:46):

What if there are multiple commits at the same time?

view this post on Zulip Scott Morrison (May 08 2019 at 23:46):

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

view this post on Zulip Scott Morrison (May 08 2019 at 23:46):

that will slow down all of them

view this post on Zulip Scott Morrison (May 08 2019 at 23:46):

it only uploads the files once it has recompiled everything new

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 08 2019 at 23:48):

That can be fixed

view this post on Zulip Simon Hudon (May 08 2019 at 23:50):

I'm still having trouble with master


Last updated: May 18 2021 at 16:25 UTC