Move to apalache about apalache-tests HOT 6 CLOSED

What's involved in figuring out the bench mark licenses? Anything I can help with on that front?

from apalache-tests.

Most of the benchmarks are the modified versions of the specifications from https://github.com/tlaplus/Examples/tree/master/specifications, except Traffic that comes from "Practical TLA". I am just not sure what to do about the incompatible licenses.

from apalache-tests.

The traffic example is here: https://github.com/Apress/practical-tla-plus/blob/master/Chapter%206/traffic.tla

from apalache-tests.

As discussed in our meeting today, if we integrate this into the main Apalache repo we risk polluting our license with license from any models we may want to check. Additionally, there don't seem to be any obvious benefits to integrating the code, since even when this is under some kind of CI, it's not going to run on every commit (the bencmarks take too long).

On the other hand, keeping this as a separate repo gives us the freedom to add in any models we may find useful in the future, without taking on any risks to the source code for the tooling.

As such, I propose closing this issue, or, at the very least, "ice boxing" it, until we have the resources to evaluate all the possible licensing risks and a clear motivation for doing so.

from apalache-tests.

I'm going to close this for the reason given above (#1 (comment)). FYI @ebuchman, in case you'd like me to reopen this or discuss tradeoffs further.

from apalache-tests.

In my understanding it's not a problem to have different licenses for different code in a common repo, I see it all the time. You just need to be clear about it. Eg:

• https://github.com/ethereum/go-ethereum#license
• https://github.com/rust-lang/rust/blob/master/COPYRIGHT#L23

etc.

While repo compression is always nice, it doesn't seem urgent :)

from apalache-tests.