Lean Best Practices

Stream: metaprogramming / tactics

[Alena Gusakov]

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

[Markus Himmel]

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

[Alena Gusakov]

Ah, neat! Thank you!

[Jalex Stark]

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

[Kevin Buzzard]

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

[Scott Morrison]

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. :-)

[Bhavik Mehta]

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

[Scott Morrison]

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! :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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