# Zulip Chat Archive

## Stream: general

### Topic: (deterministic) timeout in PR #12949

#### FR (Mar 26 2022 at 11:30):

Why does this PR cause so many "(deterministic) timeout"s? Did I break something?

#### Alex J. Best (Mar 26 2022 at 11:33):

That PR is huge! Can you summarize what you did so we can try and understand what broke?

#### Yaël Dillies (Mar 26 2022 at 11:33):

Your diff is 4k lines. I honestly can't debug this!

#### Alex J. Best (Mar 26 2022 at 11:35):

Did you try running the linters locally on your machine, this would highlight some common issues. Perhaps adding `#lint`

near the start of one of the files that times out on CI would help

#### FR (Mar 26 2022 at 11:38):

Most of the differences are in `algebra/order/ring.lean`

. And almost all differences in the other files are name substitution. However, It causes many "(deterministic) timeout"s in unrelated files.

#### Yaël Dillies (Mar 26 2022 at 11:54):

A PR should be atomic, ie do one thing. Yours does at least two things: changing the algebraic order hierarchy and renaming existing classes. Further, it is humongous.

#### Yaël Dillies (Mar 26 2022 at 11:55):

I hope you will learn from this that a PR should be either be deep and focused on one file or wide and do a single thing in many files.

#### Yaël Dillies (Mar 26 2022 at 11:56):

Or neither of those. We love small PRs!

#### FR (Mar 26 2022 at 12:00):

OK, I will try to split it.

#### Yaël Dillies (Mar 26 2022 at 12:01):

Before you do that, please share your plans with us.

#### Yaël Dillies (Mar 26 2022 at 12:18):

It seems that you're introducing many many typeclasses. This goes against the conclusion we came about with @Damiano Testa, namely to give up on an extension algebraic order hierarchy.

#### Yaël Dillies (Mar 26 2022 at 12:18):

Instead, we want to use docs#covariant and docs#contravariant.

#### Yaël Dillies (Mar 26 2022 at 12:20):

You're attacking one of the most critical and technical bits of mathlib on your fourth PR! I would advise you to tackle easier problems first.

#### Damiano Testa (Mar 26 2022 at 12:20):

I agree with Yaël. This has also recently appeared in this thread.

#### Damiano Testa (Mar 26 2022 at 12:22):

There might be some consensus on changing the name `ordered_semiring`

to `ordered_cancel_semiring`

or something like that. Though the main effect of this would be to increase the number of characters to type. I suspect that introducing many more typeclasses will need to be carefully re-examined.

It might be the way to go in Lean 4, though...

#### Yaël Dillies (Mar 26 2022 at 12:27):

Several must-reads if you're still interested despite all my warnings (sorry, can't find the links right now):

- This blogpost explaining why mixins lead to exponential instance terms
- Leonardo's note on the new structure command
- Anne's hom typeclass paper

#### FR (Mar 26 2022 at 12:48):

As we discussed in the other thread, the assumptions of `ordered_ring`

are too strict. In most of the definitions I could find, `ordered_ring`

only requires monotonicity of multiplication by a non-negative number, and does not require additively cancellative. So I handled each case, keeping the original and adding the classes with weaker assumptions. This resulted in 2×2×2×3=24 type classes. I asked in the other thread if there was a way to separate the assumptions from the algebraic and order structures, but it doesn't seem easy to do now. If it is possible in the future, maybe it can be reduced to fewer type classes. And the combinations of assumptions for all possible lemmas still have 24 cases, corresponding to the current 24 type classes.

#### Yaël Dillies (Mar 26 2022 at 12:50):

Yaël Dillies said:

Instead, we want to use docs#covariant and docs#contravariant.

Read this :up:

#### FR (Mar 26 2022 at 12:58):

Does it mean the `ordered_[...]`

hierarchy will be deprecated in the future?

#### FR (Mar 26 2022 at 13:18):

How should we use the new way to represent the lemmas for the ordered rings? It looks like this part is still working in progress.

#### Damiano Testa (Mar 26 2022 at 13:39):

If you want to help with the refactor, you can port more of the lemmas that are currently in `algebra.order.monoid_lemmas`

to the file `algebra.order.monoid_lemmas_zero_lt`

. This entails replacing the assumption that multiplication by *all* elements is monotone, to only requiring that multiplication by all *positive* elements is monotone. This means using the typeclasses

```
* monotone left
* * `covariant_class α>0 α (λ x y, x * y) (≤)`, abbreviated `pos_mul_mono α`,
expressing that multiplication by positive elements on the left is monotone;
* * `covariant_class α>0 α (λ x y, x * y) (<)`, abbreviated `pos_mul_strict_mono α`,
expressing that multiplication by positive elements on the left is strictly monotone;
* monotone right
* * `covariant_class α>0 α (λ x y, y * x) (≤)`, abbreviated `mul_pos_mono α`,
expressing that multiplication by positive elements on the right is monotone;
* * `covariant_class α>0 α (λ x y, y * x) (<)`, abbreviated `mul_pos_strict_mono α`,
expressing that multiplication by positive elements on the right is strictly monotone.
* reverse monotone left
* * `contravariant_class α>0 α (λ x y, x * y) (≤)`, abbreviated `pos_mul_mono_rev α`,
expressing that multiplication by positive elements on the left is reverse monotone;
* * `contravariant_class α>0 α (λ x y, x * y) (<)`, abbreviated `pos_mul_reflect_lt α`,
expressing that multiplication by positive elements on the left is strictly reverse monotone;
* reverse reverse monotone right
* * `contravariant_class α>0 α (λ x y, y * x) (≤)`, abbreviated `mul_pos_mono_rev α`,
expressing that multiplication by positive elements on the right is reverse monotone;
* * `contravariant_class α>0 α (λ x y, y * x) (<)`, abbreviated `mul_pos_reflect_lt α`,
expressing that multiplication by positive elements on the right is strictly reverse monotone.
```

mentioned in the file `algebra.order.monoid_lemmas_zero_lt`

.

#### Damiano Testa (Mar 26 2022 at 13:40):

Alternatively, if you want to test this out, you can import the file `algebra.order.monoid_lemmas_zero_lt`

in your project and start using the lemmas that are there (although there are not so many at the moment and I have not placed any of the relevant instances).

#### Damiano Testa (Mar 26 2022 at 13:42):

My approach so far has been to port about 10 new lemmas for each PR, while keeping the file as a leaf of the import tree, so as to make builds quick.

Once the instances will start going in, this file will suddenly move much further inside the import tree and then it might be a good idea to add the instances one at a time, to make sure that everything still works (or, rather, that everything that breaks, breaks for a very precise reason that can be fixed!).

Last updated: Dec 20 2023 at 11:08 UTC