(deterministic) timeout in PR #12949

Stream: general

[FR]

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

[Alex J. Best]

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

[Yaël Dillies]

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

[Alex J. Best]

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]

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]

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]

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]

Or neither of those. We love small PRs!

[FR]

OK, I will try to split it.

[Yaël Dillies]

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

[Yaël Dillies]

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]

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

[Yaël Dillies]

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]

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

[Damiano Testa]

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]

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]

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]

Yaël Dillies said:

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

Read this :up:

[FR]

Does it mean the ordered_[...] hierarchy will be deprecated in the future?

[FR]

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]

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]

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]

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