Fixing diamonds about `sup`/`inf`

Stream: general

[Yury G. Kudryashov]

Some time ago I created lean#609 (merged, not yet released). Yesterday I started porting mathlib to lean-master in order to actually fix these diamonds. Help is very welcome.

[Eric Rodriguez]

for those interested, branch#LO-min-max

[Eric Rodriguez]

two things; you can actually use elan override to not have to change the leanpkg.toml file. secondly, do you have a cache somewhere, or should I just recompile locally?

[Bryan Gin-ge Chen]

When we make a release we'll have to replace the changed line in leanpkg.toml with the next version of Lean anyways, so I think this is the easiest way.

[Bryan Gin-ge Chen]

leanproject and elan should work with this branch locally, I think.

[Bryan Gin-ge Chen]

BTW I can make a new release of Lean whenever we think it's ready.

[Eric Rodriguez]

I think @Mario Carneiro probably wants to get his tactic/AST PR in first, I guess, but I'm not too sure how far that is from done

[Mario Carneiro]

Daniel found a bug in testing but I don't think anything else has appeared since that was fixed

[Mario Carneiro]

so it's probably fine to merge

[Yury G. Kudryashov]

@Eric Rodriguez I changed leanpkg.toml to make CI build oleans for me.

[Eric Rodriguez]

ooh, I didn't know CI would build with custom lean

[Bryan Gin-ge Chen]

Mario Carneiro said:

Daniel found a bug in testing but I don't think anything else has appeared since that was fixed

Sorry, I'm having a little trouble interpreting this. I take it another PR to core Lean to fix this is forthcoming but not in the near future?

[Mario Carneiro]

No, a commit was added to the tactic PR lean#614, it has not been merged yet

[Eric Rodriguez]

your last commit seems to have built locally for me, Yury, so it may be done!

[Bryan Gin-ge Chen]

I'm planning to release Lean 3.33.0c on the current master this evening (3-4 hours from now) so if there are any objections let me know before then.

[Yaël Dillies]

If you can also rename int.sub_one_le_of_lt to int.sub_one_lt_of_le and int.lt_of_sub_one_le to int.le_of_sub_one_lt, that would be great. But that's a random suggestion.

[Bryan Gin-ge Chen]

Do you mind opening a PR?

[Yaël Dillies]

How shall I? This is not the usual mathlib process, right?

[Bryan Gin-ge Chen]

It's OK to open the PR from a fork. We can run bors try to check that nothing breaks.

[Yaël Dillies]

Ahah. Never used a fork :sweat_smile:

[Bryan Gin-ge Chen]

Actually if you turn on GitHub Actions in your fork settings (it might be on by default, I don't remember), that will also check your commits.

[Eric Rodriguez]

OK, so is lean#616 the last remaining PR before a new release?

[Eric Rodriguez]

neither of those lemmas seem to be used in mathlib either, which means that Yury's branch should be fine

[Yaël Dillies]

I'm using them soon :wink:

[Eric Rodriguez]

you can fix that :b