Acknowledge Iris Rocq License?

Stream: iris-lean

[Michael Sammler]

Given that we are porting Iris Rocq to Iris Lean, it seems like Iris Lean is derived work of Iris Rocq. If I understand it correctly, this means we should include the Iris Rocq license (BSD-3) in the Iris Lean repository. I would propose to add the following to the end of Readme of Iris Lean:

This work is derived from Iris (https://gitlab.mpi-sws.org/iris/iris), which is distributed under the following license:
<Iris Rocq license text>

Any thoughts on this?

[Markus de Medeiros]

If I am reading the license right we need to include this, yes. I'm not sure why our license is Apache.

[Shreyas Srinivas]

The original project was Apache 2.0. It implemented mosel in 2021-22. So historical reasons I guess.