Setting up development environment

Stream: new members

[Maarten Derickx]

Hi, I am trying to set up a development environment as described on https://leanprover-community.github.io/contribute/index.html
However I get the following problem executing the last few steps on that page:

vscode ➜ /workspaces/mathlib4 (tb_normal_closure) $ leanproject hooks
Could not find a leanpkg.toml
vscode ➜ /workspaces/mathlib4 (tb_normal_closure) $ locate leanpkg.toml #this finds nothing

So where should this leanpkg.toml come frome?

[Alex J. Best]

Unfortunately those instructions are old (see the big banner at the top of the page)

[Alex J. Best]

Anything mentioning leanproject is no longer needed. It should be enough to clone mathlib4, enter that folder run lake exe cache get and then get going I think. From there you can make branches etc and push them to a branch on github (once you have the invite if you don't already)

[Maarten Derickx]

Didn't ask for an invite yet, went for the fork, but if I could get an invite that would be nice

[Ruben Van de Velde]

You'll need to tell us your GitHub username

[Mario Carneiro]

mathlib4 does not accept PRs from forks

[Maarten Derickx]

I'm https://github.com/koffie

[Maarten Derickx]

Ah, so even the:

At https://github.com/leanprover-community/mathlib, click "Fork" in the top right, to make your own fork of the repository. Your fork is at https://github.com/USER/mathlib. Alternatively, if you've asked for write access you can just use https://github.com/leanprover-community/mathlib.

part of that page is outdated, didn't see that coming

[Mario Carneiro]

I mean, you can still have a fork if you want, you just can't use it to submit PRs

[Mario Carneiro]

you could develop on a fork and then copy the code into mathlib prior to PR'ing it, for example

[Alex J. Best]

Maarten Derickx said:

Ah, so even the:

At https://github.com/leanprover-community/mathlib, click "Fork" in the top right, to make your own fork of the repository. Your fork is at https://github.com/USER/mathlib. Alternatively, if you've asked for write access you can just use https://github.com/leanprover-community/mathlib.

part of that page is outdated, didn't see that coming

I think the paragraph above explains it ok, but we should probably make it clearer that in fact forking is not recommended for most people, esp if they are getting set up for the first time.

[Maarten Derickx]

Probably also my mistake for just skimming that text instead of reading it carefully. If you already know to use git one tends to skip over large parts of contributor guidelines that just seem to explain how to use git.

[Alex J. Best]

I think that is quite common, and we could do a better job highlighting very clearly what is nonstandard there in the process of fixing the instructions for Lean 4.