Zulip Chat Archive

Stream: general

Topic: bye `decidable_linear_order`


view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Oct 24 2020 at 04:25):

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

view this post on Zulip 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...

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:27):

Pushed

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:27):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:31):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:31):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:32):

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

view this post on Zulip Johan Commelin (Oct 24 2020 at 04:37):

Note: 24daef0aff0716188b82300b2d629ca04696057e has cached oleans available

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 24 2020 at 04:40):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:41):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:41):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 24 2020 at 04:42):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:46):

But linear_order now includes decidable_*

view this post on Zulip Mario Carneiro (Oct 24 2020 at 04:46):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:46):

So it can't be computable anymore

view this post on Zulip Mario Carneiro (Oct 24 2020 at 04:46):

right, you've pushed the frontier down a bit

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:46):

Can you adjust the proofs?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 24 2020 at 04:46):

It's just a subset of fields

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 24 2020 at 04:48):

so the question comes down to which instances are noncomputable

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:48):

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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:49):

So it has to be adjusted.

view this post on Zulip Mario Carneiro (Oct 24 2020 at 04:49):

what instance is that part of?

view this post on Zulip Johan Commelin (Oct 24 2020 at 04:49):

I will attempt topology/algebra/ordered.lean

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:49):

E.g., ordered_add_comm_group or ordered_ring

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 04:49):

I know how to fix it.

view this post on Zulip Mario Carneiro (Oct 24 2020 at 04:51):

Actually you can probably prove it using linear_order real

view this post on Zulip Mario Carneiro (Oct 24 2020 at 04:52):

because it's in a proof

view this post on Zulip 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 ?

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 05:04):

I'm going to fix data/complex/exponential

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 05:06):

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

view this post on Zulip Johan Commelin (Oct 24 2020 at 05:08):

data/padics/padic_numbers.lean

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 05:12):

real/hyperreal

view this post on Zulip Johan Commelin (Oct 24 2020 at 05:16):

padics/ring_homs

view this post on Zulip Johan Commelin (Oct 24 2020 at 05:22):

I think we're almost done!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 05:26):

@Heather Macbeth Then you can start reviewing the PR!

view this post on Zulip Johan Commelin (Oct 24 2020 at 05:26):

I've fixed complex/exponential

view this post on Zulip Johan Commelin (Oct 24 2020 at 05:26):

Didn't want to wait on the conv fix

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 05:28):

I hope, Mario will review this part.

view this post on Zulip Johan Commelin (Oct 24 2020 at 05:29):

I have a version that compiles without errors

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 05:30):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 06:49):

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

view this post on Zulip Mario Carneiro (Oct 24 2020 at 09:32):

what am I supposed to be reviewing again?

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Oct 24 2020 at 10:08):

I looked at it

view this post on Zulip Mario Carneiro (Oct 24 2020 at 10:08):

it looks like it's working

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Oct 24 2020 at 15:41):

I think even basic writing under binders broke

view this post on Zulip Yury G. Kudryashov (Oct 26 2020 at 15:04):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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