Zulip Chat Archive

Stream: new members

Topic: Getting started contributing to mathlib

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?

Johan Commelin (Jul 21 2020 at 08:03):

Does #contrib help?

Johan Commelin (Jul 21 2020 at 08:04):

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

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: Dec 20 2023 at 11:08 UTC