## Stream: general

### Topic: bye decidable_linear_order

#### Yury G. Kudryashov (Oct 24 2020 at 04:16):

In lean#484 I merge linear_order with decidable_linear_order. In #4762 I'm trying to fix mathlib build. I could definitely use some help in this task. The PR already touches 100 files.

#### Heather Macbeth (Oct 24 2020 at 04:25):

Sure, what can I do? Do you want to give me some files to fix?

#### Johan Commelin (Oct 24 2020 at 04:26):

I can also help. I guess it's good to make sure that we don't step on each others toes...

Pushed

#### Yury G. Kudryashov (Oct 24 2020 at 04:27):

I'm fixing filter_product. You're free to fix any other file.

#### Yury G. Kudryashov (Oct 24 2020 at 04:29):

Main API changes:

• remove decidable_linear_order;
• remove all decidable_linear_* groups etc, including discrete_*field

#### Yury G. Kudryashov (Oct 24 2020 at 04:31):

I did some search&replace, so should be no more decidable_linear* in the repository

#### Yury G. Kudryashov (Oct 24 2020 at 04:31):

Once you choose a file, tell the others here, please.

#### Yury G. Kudryashov (Oct 24 2020 at 04:32):

I'm done with filter_product, moving to data/real/basic

#### Johan Commelin (Oct 24 2020 at 04:37):

Note: 24daef0aff0716188b82300b2d629ca04696057e has cached oleans available

#### Yury G. Kudryashov (Oct 24 2020 at 04:39):

I'm not sure what should we do with real.ordered_ring etc. Currently proofs rely on linear_order which is going to become noncomputable. @Mario Carneiro Do you want to rewrite some proofs, or should I just make more instances noncomputable?

#### Yury G. Kudryashov (Oct 24 2020 at 04:40):

Note that some failures are because of https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/conv.20in.20lean.20master

#### Johan Commelin (Oct 24 2020 at 04:40):

It's about the reals, right? Aren't those already noncomputable in every sense?

#### Yury G. Kudryashov (Oct 24 2020 at 04:40):

And possibly we should skip them and hope that @Gabriel Ebner and @Eric Wieser will fix it in lean.

#### Yury G. Kudryashov (Oct 24 2020 at 04:41):

(+) and (*) are formally "computable"

#### Yury G. Kudryashov (Oct 24 2020 at 04:41):

But I see no practical value in this "computable".

#### Yury G. Kudryashov (Oct 24 2020 at 04:42):

They're computable in the following sense: given sequences approximating a and b, you can write down a sequence approximating a + b.

#### Johan Commelin (Oct 24 2020 at 04:42):

So maybe real.comm_ring can be computable, and then real.ordered_ring is not?

#### Mario Carneiro (Oct 24 2020 at 04:44):

@Yury G. Kudryashov real.linear_ordered_comm_ring was chosen to be the strongest class which can be derived on real that is computable

#### Yury G. Kudryashov (Oct 24 2020 at 04:46):

But linear_order now includes decidable_*

#### Mario Carneiro (Oct 24 2020 at 04:46):

I would suggest proving all the maximal elements of the poset of instances that are computable

#### Yury G. Kudryashov (Oct 24 2020 at 04:46):

So it can't be computable anymore

#### Mario Carneiro (Oct 24 2020 at 04:46):

right, you've pushed the frontier down a bit

#### Mario Carneiro (Oct 24 2020 at 04:46):

so we need a partial_order real instance now, and possibly some partial_order based ring proof

#### Mario Carneiro (Oct 24 2020 at 04:46):

It's just a subset of fields

#### Yury G. Kudryashov (Oct 24 2020 at 04:47):

I would prefer to avoid dealing with cau_seq and the definition of real if possible.

#### Mario Carneiro (Oct 24 2020 at 04:47):

Basically, the idea is to have all the same instances as we do currently, but ensure that nothing is noncomputable unless it has to be

#### Mario Carneiro (Oct 24 2020 at 04:48):

so the question comes down to which instances are noncomputable

#### Yury G. Kudryashov (Oct 24 2020 at 04:48):

E.g., the proof of add_le_add_left relies on linear_order.

#### Yury G. Kudryashov (Oct 24 2020 at 04:49):

So it has to be adjusted.

#### Mario Carneiro (Oct 24 2020 at 04:49):

what instance is that part of?

#### Johan Commelin (Oct 24 2020 at 04:49):

I will attempt topology/algebra/ordered.lean

#### Yury G. Kudryashov (Oct 24 2020 at 04:49):

E.g., ordered_add_comm_group or ordered_ring

#### Yury G. Kudryashov (Oct 24 2020 at 04:49):

I know how to fix it.

#### Mario Carneiro (Oct 24 2020 at 04:51):

Actually you can probably prove it using linear_order real

#### Mario Carneiro (Oct 24 2020 at 04:52):

because it's in a proof

#### Yury G. Kudryashov (Oct 24 2020 at 05:01):

@Mario Carneiro Could you please have a look at https://github.com/leanprover-community/mathlib/pull/4762/files#diff-6abf6bbce2c44f1e6e6680b121362215a4139aaeebe1c010f364b253eebbc5e9 ?

#### Yury G. Kudryashov (Oct 24 2020 at 05:04):

I'm going to fix data/complex/exponential

#### Mario Carneiro (Oct 24 2020 at 05:04):

I have some other stuff to attend to right now but I will be back in a few hours

#### Yury G. Kudryashov (Oct 24 2020 at 05:06):

Actually, data/complex/exponential is about conv+find

#### Johan Commelin (Oct 24 2020 at 05:08):

data/padics/padic_numbers.lean

real/hyperreal

#### Johan Commelin (Oct 24 2020 at 05:16):

padics/ring_homs

#### Johan Commelin (Oct 24 2020 at 05:22):

I think we're almost done!

#### Heather Macbeth (Oct 24 2020 at 05:23):

Indeed, I was just trying to find something to work on (I am slower than you!) and couldn't.

#### Yury G. Kudryashov (Oct 24 2020 at 05:25):

My computer already compiles manifold.times_cont_mdiff, and so far conv+find is the only remaining error.

#### Yury G. Kudryashov (Oct 24 2020 at 05:26):

@Heather Macbeth Then you can start reviewing the PR!

#### Johan Commelin (Oct 24 2020 at 05:26):

I've fixed complex/exponential

#### Johan Commelin (Oct 24 2020 at 05:26):

Didn't want to wait on the conv fix

#### Heather Macbeth (Oct 24 2020 at 05:27):

@Yury G. Kudryashov OK, but I am not qualified to review this computability-of-real.linear_ordered_comm_ring  issue which you were discussing with Mario.

#### Yury G. Kudryashov (Oct 24 2020 at 05:28):

I hope, Mario will review this part.

#### Johan Commelin (Oct 24 2020 at 05:29):

I have a version that compiles without errors

#### Yury G. Kudryashov (Oct 24 2020 at 05:30):

Now we need someone to make a new release of Lean before this PR rots.

#### Johan Commelin (Oct 24 2020 at 05:36):

@Yury G. Kudryashov This is how you make a new release: https://github.com/leanprover-community/lean/commit/cc729642c39f9a5d66e45c1c92066bd8bec7d282

#### Bryan Gin-ge Chen (Oct 24 2020 at 05:36):

Do you mind writing a few sentences on the motivation for this for the commit message of lean#484? I'd be happy to merge it and make a new release of Lean after Mario gives his OK.

#### Yury G. Kudryashov (Oct 24 2020 at 06:47):

I think that the new release should wait for https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/conv.20in.20lean.20master

#### Yury G. Kudryashov (Oct 24 2020 at 06:49):

After lean#482 some of conv in ... in mathlib started to fail.

#### Mario Carneiro (Oct 24 2020 at 09:32):

what am I supposed to be reviewing again?

#### Johan Commelin (Oct 24 2020 at 09:37):

Yury G. Kudryashov said:

Mario Carneiro Could you please have a look at https://github.com/leanprover-community/mathlib/pull/4762/files#diff-6abf6bbce2c44f1e6e6680b121362215a4139aaeebe1c010f364b253eebbc5e9 ?

:up:

I looked at it

#### Mario Carneiro (Oct 24 2020 at 10:08):

it looks like it's working

#### Bryan Gin-ge Chen (Oct 24 2020 at 15:04):

I approved lean#484. In the end I just added a link to this thread in the PR comment.

I don't feel qualified to figure out how to fix the issues related to lean#482.

#### Eric Wieser (Oct 24 2020 at 15:06):

Regarding lean#482, I think basically the contents of this discussion turned out to be a mistake:

https://github.com/leanprover-community/lean/pull/476#discussion_r503264366

#### Bryan Gin-ge Chen (Oct 24 2020 at 15:07):

Can you make a PR that resolves things? (Sorry, I haven't been following the discussion there or in the other thread in detail.)

#### Eric Wieser (Oct 24 2020 at 15:12):

Done in lean#485. Can someone else commit a test to that branch that demonstrates the behavior that broke?

#### Yury G. Kudryashov (Oct 24 2020 at 15:27):

I don't understand what exactly went wrong, so I guess I can't help creating a test that doesn't depend on mathlib.

#### Eric Wieser (Oct 24 2020 at 15:41):

I think even basic writing under binders broke

#### Yury G. Kudryashov (Oct 26 2020 at 15:04):

@Bryan Gin-ge Chen @Gabriel Ebner Are we ready for a new release?

#### Bryan Gin-ge Chen (Oct 26 2020 at 15:07):

I can make one this evening if Gabriel doesn't get to it before then.

#### Yury G. Kudryashov (Oct 26 2020 at 15:23):

In the meantime I made a tag in my repo and switched mathlib branch to this tag.

#### Yury G. Kudryashov (Oct 26 2020 at 15:46):

@maintainers #4762 is ready for review. It touches 103 files, so I'd love to see it merged soon (but no sooner than we actually have the corresponding lean release).

Last updated: May 08 2021 at 10:12 UTC