lake new + LICENSE

Stream: lean4

[Julian Berman]

Can I re-raise (because I see Joachim mentioned it here) whether lake new should generate a LICENSE file by default?
Obviously this raises a "which license by default" question, but I think that in the context of Lean + mathematics, it is subjectively quite a bit more likely that users will not know they should add a LICENSE as early as possible when creating projects than it is that a user has a strong preference for which LICENSE they use -- and for the latter those users will know to change the LICENSE file.

Concretely I think Lake should generate an Apache 2.0 license by default, (and even if that's not the LICENSE I personally generally use). Has such a thing been considered / do others agree?

[Chris Bailey]

I'm not sure that would constitute an effective grant of a license by the author. Some options from other ecosystems are to have a "what license?" prompt when creating a new package with the build tool (npm), or to require that a license be specified before being allowed upload to the package registry (crates.io).

If lakefiles eventually support inclusion of license information, you can leave a comment to prompt users similar to rust's default Cargo.toml. Something like

...
lean_lib foo where
  -- Learn more about licensing your Lean project by reading the FAQ at <link>
  license := ""

[Kim Morrison]

While acknowledging that it is a little presumptious, I'd also be in favour of simply including the Apache 2.0 LICENSE by default. Users can delete or replace, but get a good default.

[Mario Carneiro]

I agree with Chris that this is not enough of "active consent" to be legally above-board. I think a suggestion to insert a specific license (e.g. apache 2.0) is fine, but it shouldn't be possible for someone to run lake new, not see any mention of a license, then push to github and have the release "presumptively licensed" under a license they did not say yes to

[Julian Berman]

To be clear I'm not specifically suggesting no confirmation, that's fine too, perhaps with a --license <SPDX identifier to pass a choice without interactivity. Not being a lawyer, I'm not sure what current case law considers regarding whether autogenerating one would be a reasonable presumption that the user is granting it if they then went and committed it (and if you'll forgive me for presuming no one else who's opined so far is, if there's one in the audience I'd be curious to know whether this is something that's been tested or not). My layman brain would think at very least it should slightly shift the burden onto presuming it was the license and someone would need to argue it wasn't (because it was implicitly granted) as opposed to the (subjectively) worse scenario where someone is immediately using something with no license. But it sounds like perhaps adding a confirmation just makes everyone (including me) so far happy?

[Chris Bailey]

Julian Berman said:

To be clear I'm not specifically suggesting no confirmation, that's fine too, perhaps with a --license <SPDX identifier to pass a choice without interactivity. Not being a lawyer, I'm not sure what current case law considers regarding whether autogenerating one would be a reasonable presumption that the user is granting it if they then went and committed it (and if you'll forgive me for presuming no one else who's opined so far is, if there's one in the audience I'd be curious to know whether this is something that's been tested or not). My layman brain would think at very least it should slightly shift the burden onto presuming it was the license and someone would need to argue it wasn't (because it was implicitly granted) as opposed to the (subjectively) worse scenario where someone is immediately using something with no license. But it sounds like perhaps adding a confirmation just makes everyone (including me) so far happy?

I'm a lawyer and work in this area; I would not recommend this approach precisely because of the uncertainty. I'm not aware of any case law specifically addressing the issue of legally significant files silently generated by something like a build tool, but under general contract principles I think in most cases it would shake out that there was not an effective agreement.

Mario touched on this already, but to address the second point, I think the expectation in the broader software world is that it's the responsibility of downstream users to make sure a work they want to use is licensed in a way that accommodates their use case. The worst case scenario is that Lean developers, businesses, etc. following this pattern start using stuff they believe is available under e.g. Apache-2.0 because they observe some generated default, but which suddenly becomes unlicensed when someone wins a lawsuit in the Southern District of New York or whatever.

I would be on board with either a confirmation that requires a key press or some interaction, or the manifest hints, with a preference for the latter.

[Julian Berman]

Aha! Thanks for saying so Chris (and for the info)!

[Eric Wieser]

I guess another option would be for lake build or lake new to emit a warning that the project is unlicensed

[Eric Wieser]

(with a way to explicitly mark no license as intended in the lakefile with unlicensed := true)

[Eric Wieser]

Including the actual license info in the lakefile sounds messy, since for example ProofWidgets and Verso include vendored javascript files that are not apache-licensed

[Julian Berman]

That's not unique to Lean though is it? Python and Rust and JS all have license fields in their packaging files. And if you vendor files with other licenses you manage

[Eric Wieser]

I guess licenses := [...] is sufficient

[Chris Bailey]

I agree with Julian on the vendored files issue though that's definitely a valid point. The minority of people who care about license details will have tools to find something like a package.json or additional LICENSE file nested within a larger Lean project, so Lean developers should only have to concern themselves selecting a license information for their contributions.

As far as implementation, the most convenient format for consumers and detection tools is what cargo does, license: string, license-file: string. The license key is for an SPDX expression, the license-file key is for people who would rather specify a path to a file containing the license, which is useful if it's some kind of commercial or custom license deal. The license-file one can be a list with multiple paths, but forcing "license" to be a single string is preferred, because licenses := [X, Y] is less clear than the SPDX X AND Y or X OR Y.

[Julian Berman]

(That's essentially what Python has these days as well -- https://peps.python.org/pep-0639/ )