License of Mathematics in Lean?

Stream: general

[David]

I am upgrading a syntax highlighting library from Lean 3 to Lean 4, and I would like to create a test case from Mathematics in Lean.

Surprisingly, I cannot find LICENSE, COPYING, or any section about copyright in its source repo or the deployed repo. Then how am I supposed to give attribution? Is the following sufficient?

The test.lean file has been adapted from Mathematics in Lean.

Previous discussions

• #lean4 > ✔ Translating `Mathematics in Lean` to Japanese
  where David Thrane Christiansen mentioned that Functional Programming in Lean is licensed under CC BY 4.0.

• #general > ✔ Status of Lean 3?
  where I asked whether maintaining compatibility with Lean 3 is necessary for the syntax highlighting library.

[David]

The test case is here: bat/tests/syntax-tests/source/Lean/test.lean.

[David]

Maybe it would be safer to reuse BirthdayProblem.lean from github linguist?

[Kevin Buzzard]

I'm sitting in the same room as the authors of MIL, I'll ask them!

[Jeremy Avigad]

Thanks for asking. We just didn't think about it! Patrick and I decided that it makes sense to release the text of MIL under CC BY 4.0 and the repository code (exercises, solutions, etc.) under Apache 2.0. We'll put the Apache license in the repo and figure out where to put the CC BY notice, but in the meantime, you can take this message as a declaration.

[David]

Hi! Any updates on the license?

where to put the CC BY notice

Maybe add it to the copyright variable in conf.py?

[Patrick Massot]

@David it should be good now. Sorry about the huge delay.