Zulip Chat Archive

Stream: general

Topic: Build time


view this post on Zulip Sebastien Gouezel (Jun 03 2020 at 11:10):

Build time according to build bot was stable around 105 minutes, but the two last builds took 113 minutes and 117 minutes. Noise?

view this post on Zulip Johan Commelin (Jun 03 2020 at 11:13):

That seems a bit much for noise

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 11:13):

Isn't it obvious that the new C_inj lemma has increased build time by 10 minutes?

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 11:18):

I'm not sure if I am joking or not. C r = C s has several implicit arguments, multiple function coercions, and it is checked every time the simplifier sees an equation. I wouldn't rule out the possibility that unification happens to do something horribly expensive with this lemma.

view this post on Zulip Johan Commelin (Jun 03 2020 at 12:04):

Hmmm... in that case maybe we should kick it out of the simp set? (And leave a comment explaining why.)

view this post on Zulip Johan Commelin (Jun 03 2020 at 12:13):

@Gabriel Ebner Maybe I'm dense, but what is the coercion to function? C is an ordinary function.

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 12:14):

Oh, you're right. Only the seconden argument triggers the coercion.

view this post on Zulip Johan Commelin (Jun 03 2020 at 12:15):

I'm still confused. C is not a bundled morphism.

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 12:15):

In thuis case, it looks much lees problematic and I have no idea what's going on.

view this post on Zulip Johan Commelin (Jun 03 2020 at 12:15):

(Maybe it will be in the future, but it isn't right now.)

view this post on Zulip Gabriel Ebner (Jun 03 2020 at 12:15):

Don't polynomiale have a function coercion?

view this post on Zulip Johan Commelin (Jun 03 2020 at 12:19):

Not a reliable one. The API is to use polynomial.coeff.

view this post on Zulip Johan Commelin (Jun 03 2020 at 12:19):

But they are defeq to finsupp, which does have the function coercion.

view this post on Zulip Johan Commelin (Jun 03 2020 at 12:19):

Sometimes this leaks


Last updated: May 10 2021 at 19:16 UTC