Porting flocq, confusion about licenses

Stream: mathlib4

[MinusGix]

I've been considering porting Flocq, a Coq library for reasoning about floating point numbers. Unfortunately, it is under the LGPLv3, which presumably means that I can't directly port it due to the difference in licenses. I presume I would have to ask permission for them to relicense it, if I went for a direct port.

They do have the book 'Computer Arithmetic and Formal Proofs: Verifying Floating-Point Algorithms with the Coq System' which goes into good detail about the foundations and various proofs relating to floating point numbers, is it allowed to use that as the basis of implementation? The book is more high-level and I know various places in Mathlib cite a book that they're based on, but I'm unsure of the whole etiquette / licensing around this beyond the minimum of 'cite the book which you formalized proofs from'.

But actually looking at the book, it does have discussion relating to Coq, though for the most part only really writing out the type definition or a proposition in Coq (instead of words) without the proofs written in Coq.

[Yury G. Kudryashov]

You can port it as a separate LGPLv3 licensed library without an explicit permission. It can depend on Mathlib but we won't be able to take parts of it into Mathlib or other Apache licensed libraries.

[Kim Morrison]

I would suggest asking the authors for permission to port as an Apache licenced library! It can't hurt to ask here, I think.

[Yury G. Kudryashov]

Commit history shows several contributors. Formally, you may need permission from all of them (disclaimer: not a lawyer, this is not a legal advice).

[Henrik Böving]

I think the whole licensing question becomes much more interesting when someone is doing porting work. Maybe we should in fact consult a lawyer to these kinds of questions at some point.

[Yury G. Kudryashov]

A lawyer will probably tell you how it works in 1 jurisdiction.

[MinusGix]

I'd be surprised if they allow relicensing as Apache, given the challenges of asking past contributors, and that they may very well have based it on their past (also LGPL) work on floating-point numbers. The Coq ecosystem seems to use the license a lot. Still tempting to formalize it as a separate library, though unfortunate that it wouldn't be able to be used in mathlib.
(I think a library like this could be useful for coding, such as a tactic to provide suggestions to reorder floating point expressions for better accuracy)

Separately:
What are the more typical rules for formalizing from a book that doesn't run headlong into code-licensing? I had trouble searching around for information.
Before I stumbled upon the existence of Flocq, I was considering formalizing math results from the 'Handbook of Floating-Point Arithmetic', which doesn't have the problem of being inextricably linked to an LGPL code/proof library, so presumably is much the same as formalizing from a typical maths textbook... but what are the rules around that?

[Peter Nelson]

Even if one tried to follow a maths textbook closely, formalized maths looks in practice so different from informal mathematical prose (both on a small scale and organizationally) that it seems hard to imagine a credible argument of copyright violation.