Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Lean Best Practices


view this post on Zulip Alena Gusakov (May 22 2020 at 16:43):

So I don't know if this is best place to post this but I'm wondering if there are some sorts of informal style guidelines people like to follow for Lean? Best ways of writing definitions/proofs, that sort of thing. It seems like there are multiple ways of writing Lean proofs, which is true of regular math proofs too, but I wonder if there's more to it on the Lean side of things

view this post on Zulip Markus Himmel (May 22 2020 at 16:49):

There are the mathlib contribution guidelines: style guide, naming conventions and documentation guidelines.

view this post on Zulip Alena Gusakov (May 22 2020 at 16:52):

Ah, neat! Thank you!

view this post on Zulip Jalex Stark (May 22 2020 at 16:54):

by the way "metaprogramming" refers to writing code that involves the meta keyword. This is how things like finish, cc, and ring are written.

view this post on Zulip Kevin Buzzard (May 22 2020 at 17:34):

At the Xena project we don't have any style guidelines -- if it compiles, you won.

view this post on Zulip Scott Morrison (May 23 2020 at 02:33):

But those are just the introductory levels. When Xena advances to the boss levels (getting PRs merged in mathlib) it helps to have practice with the right techniques. :-)

view this post on Zulip Bhavik Mehta (May 23 2020 at 03:13):

Can confirm getting PRs merged and making the linter happy is the real boss fight of lean

view this post on Zulip Scott Morrison (May 23 2020 at 05:15):

Beyond that there's reviewing other people's PRs, and beyond that, convincing all the bright young things doing lovely maths in Lean to put in the effort to PR it all! :-)

view this post on Zulip Kevin Buzzard (May 23 2020 at 07:19):

My take on it is that one way to find 5 people who will take it seriously and make good PRs is to tell 500 people about Lean

view this post on Zulip Kevin Buzzard (May 23 2020 at 07:20):

I am not sure I am capable of teaching things like good coding practice because at the end of the day I am not actually a good computer scientist


Last updated: May 09 2021 at 22:13 UTC