Zulip Chat Archive

Stream: new members

Topic: Getting setup to contribute to Mathlib

Keefer Rowan (May 26 2020 at 12:24):

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 (May 26 2020 at 12:26):

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

Johan Commelin (May 26 2020 at 12:26):

If there is anything unclear, feel free to ask

Johan Commelin (May 26 2020 at 12:27):

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

Anne Baanen (May 26 2020 at 12:31):

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 (May 26 2020 at 12:38):

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 (May 26 2020 at 12:41):

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 (May 26 2020 at 12:43):

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

Johan Commelin (May 26 2020 at 12:44):

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

Johan Commelin (May 26 2020 at 12:44):

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

Johan Commelin (May 26 2020 at 12:44):

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

Reid Barton (May 26 2020 at 12:44):

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

Keefer Rowan (May 26 2020 at 12:45):

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

Johan Commelin (May 26 2020 at 12:47):


Johan Commelin (May 26 2020 at 12:47):

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

Sebastien Gouezel (May 26 2020 at 12:48):

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

ROCKY KAMEN-RUBIO (May 26 2020 at 16:42):

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

Last updated: Dec 20 2023 at 11:08 UTC