Contribute to Mathlib4

Stream: mathlib4

[Chenyi Li]

Hello! I may wonder how we can contribute to Mathlib4. I am currently working on some topics in convex ananlysis and convex optimization. We are working on formalizing some properties related to the properties of the convex functions and the convergence rate of some classical optimization methods. How should we organize our code so that it meets the relevant requirements of mathlib？How do we upload our written code？Can there be some documentation written with relative requirements? Thank you very much for answering!

[Anatole Dedecker]

Hi! You should have a look at the whole "Contributing" section of https://leanprover-community.github.io/index.html
Unfortunately most of the information there is still about Lean3, and I’m not sure we have it updated for Lean4 anywhere, so you’ll have to adapt it a bit based on existing Mathlib4 code.

[guiwan]

I am trying to configure mathlib according to the official tutorial. When I proceed to the following operation in VScode：

Run cd mathematics_in_lean
Run lake exe cache get

It always shows that :

fatal: unable to read tree (984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb)
error: external command 'git' exited with code 128

I have tried reinstalling git, but it still doesn't work.

[Julian Berman]

That sounds like somehow your cloned repository is corrupt. Assuming you haven't done any work in that directory, delete mathematics_in_lean, reclone it, and then let us know what you see from running that command.

[guiwan]

Julian Berman said:

That sounds like somehow your cloned repository is corrupt. Assuming you haven't done any work in that directory, delete mathematics_in_lean, reclone it, and then let us know what you see from running that command.

Thank you very much. The original error did not appear, but there is a new error. I will try to solve it first. Thank you again.