Zulip Chat Archive

Stream: general

Topic: Build time

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?

Johan Commelin (Jun 03 2020 at 11:13):

That seems a bit much for noise

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?

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.

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.)

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.

Gabriel Ebner (Jun 03 2020 at 12:14):

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

Johan Commelin (Jun 03 2020 at 12:15):

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

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.

Johan Commelin (Jun 03 2020 at 12:15):

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

Gabriel Ebner (Jun 03 2020 at 12:15):

Don't polynomiale have a function coercion?

Johan Commelin (Jun 03 2020 at 12:19):

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

Johan Commelin (Jun 03 2020 at 12:19):

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

Johan Commelin (Jun 03 2020 at 12:19):

Sometimes this leaks

Last updated: Dec 20 2023 at 11:08 UTC