Zulip Chat Archive

Stream: new members

Topic: Getting started contributing to mathlib


view this post on Zulip Eric Wieser (Jul 21 2020 at 08:01):

What's the preferred workflow for making a small change to mathlib? Can I work within the _target/deps/mathlib directory of an existing project? Or should I make a clean checkout? Is there anything special I have to do to get the oleans?

view this post on Zulip Johan Commelin (Jul 21 2020 at 08:03):

Does #contrib help?

view this post on Zulip Johan Commelin (Jul 21 2020 at 08:04):

In particular https://www.youtube.com/watch?v=Bnc8w9lxe8A

view this post on Zulip Eric Wieser (Jul 21 2020 at 08:17):

That's what I was looking for, thanks. Couldn't see the contributing.MD in the main repo, but forgot to look in .github.


Last updated: May 14 2021 at 07:19 UTC