Zulip Chat Archive

Stream: new members

Topic: Getting setup to contribute to Mathlib


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 26 2020 at 12:26):

If there is anything unclear, feel free to ask

view this post on Zulip Johan Commelin (May 26 2020 at 12:27):

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

view this post on Zulip 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)

view this post on Zulip 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."?

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (May 26 2020 at 12:44):

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

view this post on Zulip Johan Commelin (May 26 2020 at 12:44):

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

view this post on Zulip Johan Commelin (May 26 2020 at 12:44):

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

view this post on Zulip Reid Barton (May 26 2020 at 12:44):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 26 2020 at 12:47):

Yup

view this post on Zulip Johan Commelin (May 26 2020 at 12:47):

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

view this post on Zulip Sebastien Gouezel (May 26 2020 at 12:48):

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

view this post on Zulip 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: May 10 2021 at 19:16 UTC