## 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: May 10 2021 at 19:16 UTC