Zulip Chat Archive

Stream: general

Topic: Lean 3.7

Gabriel Ebner (Mar 05 2020 at 14:32):

Now that we've finally completed the 3.6 transition, it is time to think about the future. After the 3.6 release, which focused on breaking the library, I think the 3.7 release should now focus on breaking the C++ code. We already have enough PRs to make porting mathlib interesting: https://github.com/leanprover-community/lean/milestone/2

I'm thinking about including the following features:

@Anne Baanen has been tweaking the congruence lemmas so that simp can rewrite subsingletons: https://github.com/leanprover-community/lean/pull/134
@Anne Baanen is currently working on tweaking unification so that (λ a b, a + b) = (+) is true by reflexivity. (PR should come in any moment now.)
I have tweaked the type class resolution a bit to make it faster: https://github.com/leanprover-community/lean/pull/135
I have also backported the change from Lean 4 that instance arguments are processed from right to left in type class resolution: https://github.com/leanprover-community/lean/pull/139
@Reid Barton has changed the type class resolution order in the apply tactic: https://github.com/leanprover-community/lean/pull/67

There's also various uncontroversial additions to the metaprogramming API by @Floris van Doorn and @Simon Hudon.
I don't want to merge any changes to the core library this time to keep the mathlib porting effort reasonable.

(As usual, I'm posting this here because I don't think too many people are closely following the core Lean repo. This is your chance to complain!)

Anne Baanen (Mar 05 2020 at 14:52):

The PR just came in: https://github.com/leanprover-community/lean/pull/141 :smile:

Floris van Doorn (Mar 05 2020 at 17:18):

When making a PR to leanprover-community/lean, is there currently a way to fetch build artifacts from somewhere?

Sebastian Ullrich (Mar 05 2020 at 17:35):

Btw, you might be interested in something like the trace.import trace class I added to Lean 4 before removing that file altogether: https://github.com/leanprover/lean4/commit/75b2b09c08be9206732bc7a9934c7c18b5f094b2

Sebastian Ullrich (Mar 05 2020 at 17:37):

Also https://github.com/leanprover/lean4/commit/15d11cc48362330f6e90791a2101444798734e21

Scott Morrison (Mar 05 2020 at 18:01):

Floris van Doorn said:

When making a PR to leanprover-community/lean, is there currently a way to fetch build artifacts from somewhere?

leanproject get-cache?

Scott Morrison (Mar 05 2020 at 18:01):

(you'll need to install leanproject from a branch, as it hasn't quite merged yet: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/new.20mathlib.20tools/near/188884880)

Floris van Doorn (Mar 05 2020 at 18:24):

Oh yes, I haven't been following all the development of leanproject, but I'll try that!

Scott Morrison (Mar 05 2020 at 18:29):

It is awesome, and hopefully merged real soon now. :-)

Last updated: Dec 20 2023 at 11:08 UTC