Skip to content

Consider dual-license existing code as MIT OR Apache-2.0 #1

@str4d

Description

@str4d

The codebase currently has three existing authors:

  • The original Lean 3 code by @JoeyLupo.
  • Two forks:
    • The extension by @oxarbitrage to focus on formal proofs of correctness of different ciphers.
    • The (I think?) academic continuation of the original code by @ashandoak.

I merged the two forks together, and have now set up a Lean 4 project into which I am porting all of the existing code.

The original codebase was licensed as Apache-2.0, which its forks preserved. This happens to match the Mathlib license, so that's convenient.

However, I (and several other people interested in this project) are interested in the cryptographic intersection of Lean and Rust. The Rust ecosystem generally dual-licenses code as both MIT and Apache-2.0, allowing code to be used under either license. (There are exceptions, but usually it's to instead use solely a BSD license.) It would therefore be very convenient if Cryptolib could also be dual-licensed as MIT OR Apache-2.0.

For now, I've set up the license declaration to be specific about which files are only licensed as Apache-2.0, and all new contributions will be dual-licensed. It wouldn't be too hard to maintain that going forward, but it would be simpler if all code were licensed the same way.

I am therefore asking the three existing authors: would you be willing to relicense your existing contributions from Apache-2.0 to MIT OR Apache-2.0?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions