Permission to port Coq-Combi to Mathlib

[SashaIr]

Hi,

First of all, apologies for not getting in touch earlier about this.

I am an algebraic combinatorist with an interest in Lean. Mathlib has very little material about combinatorics, and so I started working on a PR to port parts of Coq-Combi to Mathlib. The goal is to make the formalized results available in the Lean/Mathlib ecosystem and, where appropriate, adapt the existing developments to Mathlib's conventions and infrastructure. I used Aristotle to assist me with the project, and now have a PR-ready repository.

Some people reviewing/discussing the PR pointed out that there may be licensing issues involved in incorporating code from Coq-Combi into Mathlib. I had not properly considered this when I started the port, so I wanted to stop and ask for permission before proceeding further.

Would you be willing to grant permission for the relevant Coq-Combi code to be ported and incorporated into Mathlib under Mathlib's licensing terms? If there are particular conditions you would like to attach to such permission, or if a specific license/authorization is preferable, I would of course be happy to follow them. I am also willing to delete the repository and scrap the project if you so wish.

I apologize again for not asking about this beforehand, and thank you for your work on Coq-Combi.

[eric-wieser]

Note that your PR-ready repository itself consistutes a license violation, since it relicenses Coq-Combi (-derived?) code as Apache 2.

[SashaIr]

I am (now) aware, I will leave it up for the developers of Coq-Combi to check if they so wish, and I will close it upon request.

[hivert]

Dear @SashaIr, I've just seen your issue. Regardless of the licensing question, I think it would have been polite to ask for permission before starting the project...

Is an Apache 2 license mandatory for inclusion in mathlib? In any case, I need to check a few details before answering.

Also, before accepting, I'd like you to cite not only the Git repository, but also the peer-reviewed paper describing the work:
https://dl.acm.org/doi/10.1145/3703595.3705885

I'll try to answer quickly, but I'm still in the beginning-of-semester rush with teaching, so it may take me a little time.

[SashaIr]

Dear @hivert, thank you for your answer.

First, I wholeheartedly agree that I should have asked permission before starting the project. I just did not think it through, and I sincerely apologize. I was transparent in saying that your project is the source I used for mine, so I hope you can believe me if I say that I was not ill-intentioned. I do feel bad about it, in retrospect reaching out to you immediately was a very obvious and easy thing to do.

As far as the license is concerned, Mathlib maintainers are more qualified to answer than I am, but I do believe it is a requirement.

I am happy to add the paper as a reference: I updated the README and the bibliography of my branch, and if the PR is eventually accepted, it should also appear in the Mathlib bibliography. Let me know if you would like to have it mentioned elsewhere as well.

There is no rush at all, I understand that September is a busy time for everyone, myself included, so take all the time you need.

Thank you for your understanding, and once again, I apologize for my mistake.