Contribute a project

Stream: new members

[Alex Zhang]

I have finished a project on Hadamard matrices and relevant topics.
I would like to contribute it to mathlib.
Could anyone please let me know the proper procedure I should take to contribute a project?

[Alex Zhang]

I have a private repository for this project.

[Kevin Buzzard]

There's some information on the community website.

[Kevin Buzzard]

PS you do not "contribute a project" -- you make a series of PR's adding results in appropriate places.

[Alex J. Best]

You should definitely check out all of the documents about contributing in the bottom left sidebar so in addition to Pull request lifecycle, look at: Naming conventions, Code style guideline, Documentation style are all relevant and you can start making sure your code matches what is explained there.

[Alex Zhang]

Yeah. I did some PRs before. If so, it seems that I just need to do more individual PRs.

[Alex Zhang]

Should I public my repository here or somewhere?

[Kevin Buzzard]

That's entirely up to you, and is independent of the PR process.

[Alex J. Best]

Yeah when all the smaller lemmas are added you could make a PR introducing a file hadamard_matrices.lean that contains the crux of your project, or even break that up, first PRing the definitions, then later some results you proved about them. Smaller PRs tend to get reviewed better faster, so breaking it up will definitely help move things along.

[Alex Zhang]

Thanks for your suggestion. As I may not be quite sure about where to insert several topics into mathlib, I think I am going to share my repository here later.
The implementation of Hadamard matrices depends on several other PRs. I think I am going to do surrounding PRs first to make things ready.

[Alex Zhang]

I have written a file about symmetric matrices. For example, what is the correct place to insert this file?
All my files follow the contribution conventions and are in the correct styles (except for possible misuse or errors).

[Alex J. Best]

How long is the file?

[Alex Zhang]

Quite short now, 94 lines

[Alex J. Best]

Well it could go somewhere in the folder linear_algebra/matrix/

[Alex J. Best]

Probably as a new file symmetric.lean

[Alex Zhang]

I will leave for a moment and try to share the whole repository when I am back.

[Alex J. Best]

The other option, seeing as there isn't a lot of code is to add the material to the end of the file data/matrix/basic.lean

[Alex Zhang]

@Alex J. Best Alex, are you a mathlib maintainer?

[Alex J. Best]

Personally I prefer the second option, but others might disagree

[Alex J. Best]

Nope I'm not

[Alex Zhang]

(deleted)

[Yakov Pechersky]

data.matrix.basic is a beast as it is. My rule of thumb is that new definitions, unless intensely related to existing definitions and lemmas, should go into new files. New files are cheap, and easier to encapsulate. Having everything in a single file makes untangling from an import spaghetti much harder later on (cf data.equiv.basic).

[Yakov Pechersky]

This rule of thumb includes new instances as well. For example, I'm PRing integer powers of matrices, since we have a has_inv defined, so we can make matrices a div_inv_monoid and get integer powers for free. But I am doing that in a new file linear_algebra.matrix.fpow so that this new "definition" and all of the associated lemmas don't pollute nonsing_inv.

[Johan Commelin]

Alex J. Best said:

Well it could go somewhere in the folder linear_algebra/matrix/
Probably as a new file symmetric.lean

I would go with this option. That means you can have a self-contained PR of ~94 lines. (Don't forget copyright headers, module docstring, etc).
Seems like a good PR to start with.

[Eric Wieser]

Putting it in its own file also helps avoid the temptation to refactor everything else in the file you would otherwise insert your code into

[Alex Zhang]

Thanks for the suggestions, I will start with that PR tonight. What follow are circulant matrices, diagonal matrices(as a prop) etc…

[Alex Zhang]

I have made that PR.
What would be a good place for the definition of Hadamard matrices and basic APIs excluding any complicated constructions of Hadamard matrices?

[Alex Zhang]

:thinking:

[Eric Wieser]

Probably data/matrix/hadamard

[Eric Wieser]

Although I wonder if we just want to do something like

abbreviation hadamard := @has_mul.mul (matrix m n R) (pi.has_mul)

So that we get all the lemmas about mul for free

[Alex Zhang]

Eric, "Hadamard matrix" is different from the Hadamard product. Do we really want "Hadamard matrix" to be in data/matrix/hadamard?

[Yakov Pechersky]

The fact that matrices are just some thin layer on top of pi has bitten me before, when 1 is interpreted as pi.has_one instead of matrix.has_one

[Alex Zhang]

Eric Wieser said:

Although I wonder if we just want to do something like

abbreviation hadamard := @has_mul.mul (matrix m n R) (pi.has_mul)

So that we get all the lemmas about mul for free

Please let me know if we indeed want to change the definition to this.

[Eric Wieser]

I'll experiment tomorrow to see if that behaves well

[Eric Wieser]

Alex Zhang said:

Should I public my repository here or somewhere?

I would recommend making your repository public if you want to show off your work to anyone today; it will be much faster than waiting for every last line to make it into mathlib! If you have a project created with leanproject on github, you can even follow the instructions here to have it tested against the latest mathlib.

[Eric Wieser]

(it will also provide reviewers with context for what you plan to do with is_sym / hadamard etc, which is often useful)

[Alex Zhang]

Sure.

[Alex Zhang]

https://github.com/l534zhan/my_project
This is the link to my project. (I am still learning how to use GitHub properly...)

[Eric Wieser]

Lots of good stuff there, thanks! At a glance at main1, these look like two nice follow-up PR targets:

• A quick one about docs#matrix.kronecker: Kronecker.invertible_of_invertible, Kronecker.unit_of_unit, Kronecker.is_sym_of_is_sym
• The algebra morphism from the quaternions into 4x4 matrices, which you seem to have here: https://github.com/l534zhan/my_project/blob/febc91e76b7b00fe2517f258ca04d27b7f35fcf3/src/main2.lean#L1159-L1175. This would amount to constructing a docs#quaternion_algebra.basis R (-1) (-1)out of those three matrices, but I think you already have proofs for all the fields it needs.

[Alex Zhang]

Thanks for your suggestions, Eric. As I don't have a collaborator, I have to PR things myself bit by bit in my spare time.

[Eric Rodriguez]

theorem Hadamard_matrix.Hadamard_conjecture:
∀ k : ℕ, ∃ (I : Type*) [fintype I],
by exactI ∃ (H : matrix I I ℚ) [Hadamard_matrix H],
card I = 4 * k :=
sorry -- Here, `sorry` means if you ask me to prove this conjecture,
      -- then I have to apologize.

this gave me a nice chuckle :)

[Alex Zhang]

In future PRs, do I need to rewrite every non-finishing simp?

[Eric Wieser]

Yes. Maybe #style mentions that? (Edit: no, it doesn't)

[Kevin Buzzard]

Definitely. Nonterminal simps make for brittle code which is hard to maintain.

[Alex Zhang]

image.png

[Alex Zhang]

Why can't I see the just now merged symmetric.lean in the documentation?

[Johan Commelin]

Give it a bit of time :stuck_out_tongue_wink:

[Johan Commelin]

I think the docs are regenerated once per day.

[Alex Zhang]

I'll do another two PRs today (if I can)

[Eric Wieser]

I think the docs are more like every 4 hours or so

[Lucas]

is there a tutorial for how to initialize a lean project

[Lucas]

I am trying to use leanpkg but it seems like something is missing. When I open the project in VS code, the infoview is continually loading and my computer heats up, even with hardly anything in the file

[Kevin Buzzard]

https://leanprover-community.github.io/install/project.html

If you use leanpkg but want to use mathlib then you will have to spend a couple of hours compiling mathlib (i.e. letting your computer heat up). Using leanproject avoids this.

[Lucas]

thanks, this is exactly what I was looking for