Repository navigation
Decide: a license for the org's code and documents #9
Description
No repo in the org has a license: not mission, tar or codec. Without one, all rights are reserved. GitHub's terms let people view and fork the code on GitHub, but not copy, change or reuse it anywhere else. The founding brief says the org "publishes the verified code as open source", and codec is meant as the material for Level 0 of the academy, where trainees build on it.
Options for code
- Apache-2.0. Lean 4, Mathlib and Batteries use it, so code can move into them, or take from them, with no relicensing. It includes a patent grant.
- MIT. Shorter, with no patent grant.
- MIT or Apache-2.0, at the user's choice, as most Rust projects do.
Also to decide
- The copyright holder: Foundation-0, or each contributor.
- Whether documents (the brief, the playbook, review records and the website) take their own license, such as CC BY 4.0.
Recommendation
Apache-2.0 for code, with Foundation-0 as the copyright holder, because it matches the Lean ecosystem the org builds on.
When decided
Add a LICENSE file to each repo, and the license field to each project's lakefile.toml (the bar check allows that field). New project repos start with the same license.
Current work
Apache-2.0 was selected for original code and documents. Contributors retain their copyright; outside material keeps its own license. The remaining repository and Lake metadata license PRs are linked from the policy PR.
Awaiting independent review: #26.
Activity
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
Set the Lake package license to Apache-2.0
zero-aska commentedon Oct 27, 2026
The code license is decided. On Foundation-0/proven-commons#5 (comment), ahrazzle chose Apache-2.0 for the org's repos.
Following the "When decided" plan above, there is now a pull request in each of the 24 library repos. Each adds
LICENSEwith the verbatim Apache-2.0 text. The 18 repos that have alakefile.tomlalso getlicense = "Apache-2.0"there, which Lake 4.35 reads and the bar check allows:LICENSEonly, no lakefile on main yet: bech32, cbor, hostname, http, messagepack, punycodeThe bar check passed on each repo that runs it. The approval hash does not cover
LICENSEorlakefile.toml, so no recorded approval is affected.Still open here:
mission,siteand.github. These pull requests leave them out. Those repos hold most of the documents in question.bar/templatehas noLICENSEyet, so a library started from it starts unlicensed.Generated by Claude Code