Getting setup to contribute to Mathlib

Stream: new members

[Keefer Rowan]

This has probably already been asked or at least there probably info that would be pertinent online, but I can't figure it out. I'm unfamiliar with using GitHub and I'm not sure how I should set everything up for making a contribution to Mathlib. Should I start by making a new project with leanproject? How do I set it up to upload to a fork on GitHub then? Links to pertinent info would be highly appreciated. I've looked at the Mathlib tools page and am still confused.

[Johan Commelin]

@Keefer Rowan It's great that you want to contribute! https://leanprover-community.github.io/contribute/index.html

[Johan Commelin]

If there is anything unclear, feel free to ask

[Johan Commelin]

Note that the most important link is printed above the item list.

[Anne Baanen]

For the specific questions:

• To get the mathlib repository in order to work on it, I believe it's sufficient to run leanproject get mathlib.
• You can set git to push and pull from a specific fork with git remote set-url origin https://url/of/your/fork.git (you can find the specific URL on GitHub under the button "Clone or download" on the front page of your fork)

[Keefer Rowan]

That link was highly useful, somehow managed to miss it on first look. What's the deal with these .olean files? Why would I want to "up git hooks that will call cache the olean files when making a commit and fetching the olean files when checking out a branch."?

[Keefer Rowan]

Also I'm not sure what the deal is with building a project or getting mathlib oleans, as is talked about in the mathlib-tools page. It seems to suggest you want to build the project to get good speed when working with mathlib, but I tried to run leanproject build in my project folder, and it has been idling on lean --make src for a while now. I would imagine it take forever to build all of mathlib on some random computer.

[Johan Commelin]

On a random computer, a mathlib build will easily take > 1 hour. (And it used to be > 2hrs about 10 days ago.)

[Johan Commelin]

Hence you want to get compiled binaries that someone else built for you (-;

[Johan Commelin]

lean --make src should give some output... if it doesn't there's something wrong

[Johan Commelin]

It should tell you which file it is working on right now

[Reid Barton]

I think it doesn't on Windows, unless that changed

[Keefer Rowan]

On windows, wasn't giving output. I cancelled. Do I just get built binaries with leanproject get-mathlib-cache?

[Johan Commelin]

Yup

[Johan Commelin]

Probably lean --make src was compiling all the dependencies in _target/deps/mathlib

[Sebastien Gouezel]

On windows in a powershell console, it does give some output.

[ROCKY KAMEN-RUBIO]

I don’t know much about contributing to mathlib but I’ve been reading this book and it has helped me a lot with git in general https://git-scm.com/book/en/v2