Stream: coq-community devs & users

Topic: Advising against licenses?


view this post on Zulip Karl Palmskog (Oct 06 2020 at 13:28):

Given the recent trouble with CECILL-B and CECILL-C, etc., maybe we should actively discourage use of certain licenses in the coq-community manifesto? Personally, I would like to discourage the following:

view this post on Zulip Reynald Affeldt (Oct 07 2020 at 03:35):

Thanks for discussing this difficult topic. Isn't discouraging GPL a bit too much? I am no license specialist but previous discussions on Zulip seem to indicate that it can be accommodated and some people like it. Maybe "deadweight loss" is not the term that applies here.

view this post on Zulip Karl Palmskog (Oct 07 2020 at 09:54):

Assume coq-community members spend several workweeks reading license clauses and querying FSF to ensure GPL compatibility to be able to ensure a Docker image with .vo files is legal to distribute. Who benefits from this work in the end? I argue this is similar to when people devote workweeks to lower their tax burden, which is the usual textbook example of a deadweight loss in economics.

view this post on Zulip Paolo Giarrusso (Oct 07 2020 at 12:25):

You will probably need different language about the GPL, to achieve consensus. However, your argument is probably sufficient.

view this post on Zulip Paolo Giarrusso (Oct 07 2020 at 12:26):

If you want to use the GPL in a coq-community project, you have to ensure your use is clearly allowed, according to this list of compatible licenses.

view this post on Zulip Paolo Giarrusso (Oct 07 2020 at 12:27):

It seems the hard work is in dealing with the combo of licenses of questionable GPL-compatibility (such as mathcomp’s) + GPL.

view this post on Zulip Paolo Giarrusso (Oct 07 2020 at 12:31):

OTOH, I’m not sure that my idea works: I’m suggesting “to use the GPL _you_ have to ensure that _we_ can use it legally”, but the simplest way to comply is to not look hard and say “it seems fine to me” or similar.

view this post on Zulip Paolo Giarrusso (Oct 07 2020 at 23:11):

@affeldt-aist when you talked about previous discussions, were you including https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users/topic/CECILL.20licenses.20and.20(L)GPL.20compatibility ?

view this post on Zulip Paolo Giarrusso (Oct 07 2020 at 23:20):

Anyway, “math-comp is GPL-incompatible” (possibly with a link to the above thread) does need shouting from rooftops. I blame CeCILL-B (for the reason Théo Zimmermann explained), but that’s irrelevant.

view this post on Zulip Reynald Affeldt (Oct 08 2020 at 00:55):

Paolo Giarrusso said:

affeldt-aist when you talked about previous discussions, were you including https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users/topic/CECILL.20licenses.20and.20(L)GPL.20compatibility ?

Yes (but actually I only followed the first part of it).

view this post on Zulip Bas Spitters (Oct 08 2020 at 07:30):

We're trying to resolve the GPL issues with corn. It's a slow progress. My preliminary conclusion is that it is better to avoid GPL as it was not intended for formal proofs.
https://github.com/coq-community/corn/pull/99

view this post on Zulip Karl Palmskog (Oct 08 2020 at 12:25):

Paolo Giarrusso said:

If you want to use the GPL in a coq-community project, you have to ensure your use is clearly allowed, according to this list of compatible licenses.

An author violating the GPL at the outset is to me a nearly-irrelevant special case. The point I was making is that whenever you choose GPL or a similar strong-copyleft license, you impose untold amount of work on anybody distributing or modifying your project to be license-compliant. As can be seen in https://github.com/coq-community/manifesto/issues/114 pure usage is in many cases not exempt from license problems either.

My question is: who benefits from all this work to be compliant? If the project had used a permissive license, the work would nearly disappear, and it would greatly shrink with a weak copyleft license.

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:48):

Karl, I agree; to compromise with @affeldt-aist’s request, I am suggesting that a necessary condition of using GPL should be shifting all this work onto the GPL user.

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:49):

I am not implying that this necessary condition is satisfiable, or satisfiable with reasonable effort.

view this post on Zulip Karl Palmskog (Oct 08 2020 at 12:50):

but how would that work-shifting turn out in practice? We can't really make much of any demands on projects, except at entry

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:51):

That’s a great question, but answering that is part of the work, so it might be best to leave that as an exercise for @affeldt-aist .

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:52):

The only potential solution would be if coq-community phrased a set of requirements on licenses, and “odd licenses” required approval by actual experts.

view this post on Zulip Karl Palmskog (Oct 08 2020 at 12:53):

I think also "discourage" has a very different semantics from "forbid", at least in the usual vernacular.

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:53):

But coq-community would still need to write those requirements, so this is not 0 work.

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:54):

True; I’d still expect pushback, but maybe I should stop producing noise and wait for the actual pushback to surface.

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:55):

It seems writing those requirements would be helpful only if it _replaced_ the ongoing license maintenance load.

view this post on Zulip Karl Palmskog (Oct 08 2020 at 12:55):

in any case, our basic problem is to me incentivizing projects to join coq-community, most directly by providing more automation up front. I think with the right incentives, we can push towards more easy-to-deal-with licenses too

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:56):

I’m probably indeed worrying too much about corner cases, as I’m prone to.

view this post on Zulip Paolo Giarrusso (Oct 08 2020 at 12:57):

I’ll leave this to you (but feel free to ask)

view this post on Zulip Karl Palmskog (Oct 08 2020 at 12:57):

@Paolo Giarrusso if I submit a change to the manifesto about licensing, I'll be sure to ping you in, thanks.

view this post on Zulip Reynald Affeldt (Oct 08 2020 at 13:18):

Paolo Giarrusso said:

That’s a great question, but answering that is part of the work, so it might be best to leave that as an exercise for affeldt-aist .

:fear: (yet, that may be worth doing)

view this post on Zulip Théo Zimmermann (Oct 08 2020 at 13:28):

Currently, the manifesto's FAQ contains:

The only strict requirement is to use an open source license. However, if you create a new project or propose to transfer a project of which you are the sole copyright owner, we strongly encourage you to (re)license your project under one of the following two licenses:

view this post on Zulip Théo Zimmermann (Oct 08 2020 at 13:30):

So it already contains a "strong encouragement". We can certainly add some points about explicitly discouraged licenses with some additional explanation, but that won't have much consequences IMHO.

view this post on Zulip Théo Zimmermann (Oct 08 2020 at 13:32):

If you want to create additional nudges for project owners transferring their repository, then what I suggest is to modify the issue template for requesting a project transfer with a checkbox asking whether you are the sole copyright owner or are in contact with all the copyright owners and if yes, whether you have read and understood our recommendations regarding licensing.

view this post on Zulip Théo Zimmermann (Oct 08 2020 at 13:33):

This would avoid having this recommendation staying as an obscure FAQ item.

view this post on Zulip Karl Palmskog (Oct 08 2020 at 13:35):

what I see happening in the future is that people might suggest projects with CC-0, GPL3, etc., and then I think it counts for something to already have specific commentary on why we (strongly) prefer not to use them for projects.

view this post on Zulip Karl Palmskog (Oct 08 2020 at 17:09):

interestingly, a here-unnamed Coq project switched recently from a permissive to an extremely tedious copyleft license. I see in this the basis of future competing forks, since old copies with the permissive license can't simply be recalled, no matter what upstream does. At least in coq-community, projects going from permissive to (more) copyleft is not something on my wishlist, although we can't reasonably forbid it.

view this post on Zulip Yishuai Li (Oct 20 2020 at 05:50):

I agree that (A)GPL should only be used on projects that are not (yet) intended to be utilized by others. I plan to use AGPL on some non-community project, and switch to MPL after a paper gets published. (Can the license prevent scooping?)

view this post on Zulip Karl Palmskog (Oct 20 2020 at 06:43):

in most cases, wouldn't scooping be copyright violation anyway? If scoopers don't care about copyright/attribution in the first place, I don't see how copyleft helps

view this post on Zulip Karl Palmskog (Oct 20 2020 at 06:45):

what matters for deterring scooping is probably independently checkable and widely disseminated publishing timestamps, like putting out a preprint on arXiv which references code on GitHub

view this post on Zulip Yishuai Li (Oct 20 2020 at 06:54):

One concern is that posting an under-polished paper to arXiv seems more pollutive than pushing raw code to GitHub.

view this post on Zulip Yishuai Li (Oct 20 2020 at 06:55):

If a repo is licensed under WTFPL, it grants permission to scoop without citing. Yes MIT or BSD should be enough for requiring attribution.

view this post on Zulip Karl Palmskog (Oct 20 2020 at 06:56):

GitHub is not really a stable reference/timestamp, unfortunately, since repos can be rewritten at any time. Better then to use Zenodo or similar service

view this post on Zulip Karl Palmskog (Oct 20 2020 at 06:58):

even with WTFPL, most higher-level conferences/journals will require proper attribution (i.e., beyond what law requires)

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:03):

Yes, academic requirements go beyond what legal requirements. And yes, I'm also not convinced of using a copyleft license to prevent anything except what they are meant to prevent, i.e. redistribution in modified form under a weaker or proprietary license.

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:04):

Note that choosing a stronger license with a plan to relicense in a future is likely to create additional hurdles because contributions can arrive before you expect them.

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:04):

And as soon as you have other people owning copyright, relicensing gets more complicated.

view this post on Zulip Yishuai Li (Oct 20 2020 at 07:05):

Is that blocking Coq from relicensing to MPL?

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:05):

Yep

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:05):

The copyright ownership of Coq is a mess.

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:05):

There are so many contributors.

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:06):

And for some, we are not even sure whether the copyright is owned by the individuals or their (past) employers.

view this post on Zulip Karl Palmskog (Oct 20 2020 at 07:08):

I guess the only thing we can hope for is for MetaCoq to eventually replace the critical parts, and then rebuild the rest with known copyright over many years...

view this post on Zulip Karl Palmskog (Oct 20 2020 at 07:10):

the more sinister view is that many copyright violations go ignored until some copyright holder can get a payout somehow, and as of yet it's not easy to make money off of Coq

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:14):

A French law mandating that copyright ownership of software produced in French academia be attributed to a single research institution could be enough to gather most of the copyright into the hands of Inria, actually.

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:14):

;-)

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 07:15):

While unlikely, this is not completely impossible. I recall @Maxime Dénès telling me about the existence of such a project.

view this post on Zulip Karl Palmskog (Oct 20 2020 at 07:15):

that would indeed solve everything in one sweep

view this post on Zulip Maxime Dénès (Oct 20 2020 at 08:49):

I got an update to today, it seems this is scheduled to happen in 2021

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 08:54):

Oh, that is great news! Does this mean that the law is already voted?

view this post on Zulip Paolo Giarrusso (Oct 20 2020 at 09:55):

Wait a second, what do you mean "attributed"?

view this post on Zulip Paolo Giarrusso (Oct 20 2020 at 09:56):

Ah, it consolidates the copyright that French academia already has I guess.

view this post on Zulip Paolo Giarrusso (Oct 20 2020 at 09:57):

(for a second I misread it as nationalizing ownership of all of Coq, including external contributors)

view this post on Zulip Maxime Dénès (Oct 20 2020 at 15:11):

@Théo Zimmermann It is just a decree, already in place IIUC, but gives some time for institutions to coordinate.

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 15:13):

If you happen to have a pointer or the name of the decree, I'd be happy to check it out.

view this post on Zulip Maxime Dénès (Oct 20 2020 at 15:14):

Yeah, my boss said he would give me a link, I'll forward it to you

view this post on Zulip Théo Zimmermann (Oct 20 2020 at 15:15):

cool

view this post on Zulip Yishuai Li (Oct 20 2020 at 18:55):

Even "nationalizing" Coq doesn't surprise me (from a nation that owns everything).
Copyright laws should only trouble our generation---our children should see the world united and the word "own" replaced by "exists".

view this post on Zulip Karl Palmskog (Oct 20 2020 at 19:11):

I think the most we can hope for is that permissive licenses become more prevalent and copyleft becomes less weaponized (i.e., used less to impose burdens on adversaries). With no default copyright, I think big organizations would just resort to even more technical restrictions and contractual burdens to access their "intellectual property".

view this post on Zulip Paolo Giarrusso (Oct 20 2020 at 19:43):

I was worried for a second they’d nationalize copyright from outside contributors, but then I realized I must have misread — otherwise that would surprise _me_, even from France :-)

view this post on Zulip Clément Pit-Claudel (Nov 17 2020 at 14:51):

Théo Zimmermann said:

Huh, I am misunderstanding the MPL? I thought it did lot less than "restrict the license under which modified versions of your project", at least for most modification. When I looked into it for Coq project I concluded it was much closer to weaker licenses like MIT/Expat or BSD than BSD but with extra complexities and verbiage.

IIUC, MPL wouldn't force redistribution of modifications like proving extra lemmas or defining extra functions (you can always put them in a separate file that's not MPL-covered), though it would force redistribution of more invasive changes like changing a type definition. Is that right?

view this post on Zulip Karl Palmskog (Nov 17 2020 at 15:05):

isn't this very similar to LGPL-2.1 (also usually called "weak copyleft")? I can make a new Coq file where I import LGPL'd stuff and prove new things, but this would be linking and so I can keep this proprietary even if I distribute the project somehow.

view this post on Zulip Karl Palmskog (Nov 17 2020 at 15:26):

my view is that we don't want to deal with strong copyleft at all, while MPL is a much less complex alternative to LGPL for weak copyleft, if some people prefer this [weak copyleft]. If you want people to release every lemma, you need strong copyleft.

view this post on Zulip Théo Zimmermann (Nov 17 2020 at 16:12):

That's right. MPL and LGPL are both weak copyleft but while MPL is straightforward weak copyleft, LGPL is technically-complex weak copyleft.

view this post on Zulip Clément Pit-Claudel (Nov 22 2020 at 20:23):

Yes, you're probably both right.

view this post on Zulip Yishuai Li (Apr 12 2022 at 01:30):

Say a library copies a file from coq/coq and compiles with it, should the library be relicensed to LGPL?

view this post on Zulip Guillaume Melquiond (Apr 12 2022 at 04:16):

Yes, this makes the whole thing a combined work that is no covered by the linking exclusion. So, it needs to be licensed to LGPL (or GPL).

view this post on Zulip Yishuai Li (Apr 12 2022 at 05:46):

Hope to see Coq relicensed to MPL-ish someday.

view this post on Zulip Karl Palmskog (Apr 12 2022 at 08:26):

I don't see how including a LGPL'd file in a repository automatically makes any distributions/programs/packages LGPL or GPL. A repository can include multiple standalone components under different licenses. If the modified/copied LGPL code is standalone, the non-LGPL code should be able to use it without having to relicense LGPL/GPL. However, if the modified/copied LGPL code is intermingled with the non-LGPL code, then it becomes a combined work.

view this post on Zulip Guillaume Melquiond (Apr 12 2022 at 08:35):

The original message stated that the copied file would be part of a library. Your mileage may vary, but as far as I am concerned, this falls into your "intermingled" category.

view this post on Zulip Karl Palmskog (Apr 12 2022 at 08:37):

OK, right, so licensing situation may depend on the specifics of what is meant by "library" here (it's at least conceivable it may still be just co-distribution in a GitHub repo)

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 09:07):

and IIUC relicensing is only one remedy to LGPL license violations: you can take out the offending code, as long as you get a non-derived work.

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 09:10):

also, the LGPL “dynamic linking” is a strange concept here: IIUC users must just retain the freedom to modify the LGPL components and use them in the combined work… Making linking dynamic rather than static is just a means to an end. Basing your design around the library is another matter.

view this post on Zulip Michael Soegtrop (Apr 12 2022 at 09:23):

I wonder if a lawyer ever went over the question what the GPL / LGPL actually mean for software which is distributed in source and binary form - as most Coq libraries are. It might be very different from what it means for software which is distributed in binary.

view this post on Zulip Guillaume Melquiond (Apr 12 2022 at 09:25):

Paolo Giarrusso said:

also, the LGPL “dynamic linking” is a strange concept here: IIUC users must just retain the freedom to modify the LGPL components and use them in the combined work… Making linking dynamic rather than static is just a means to an end. Basing your design around the library is another matter.

Careful there. The LGPL does not talk about "dynamic linking", only about "linking". More precisely, "When a program is linked with a library, whether statically or using a shared library, the combination of the two is legally speaking a combined work, a derivative of the original library."

view this post on Zulip Guillaume Melquiond (Apr 12 2022 at 09:30):

(And LGPL 3 made it clearer that a library does not have to be compiled for the "linking" concept to apply. But obviously, one could always argue that LGPL 2 is much more vague on the topic and thus does not apply to non-compiled libraries.)

view this post on Zulip Karl Palmskog (Apr 12 2022 at 09:51):

Coq is LGPL-2.1-only, so only definitions from that version would apply

view this post on Zulip Guillaume Melquiond (Apr 12 2022 at 10:33):

Sure, and the sentence I quoted is from LGPL 2.1.

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 15:11):

See gnu.org’s interpretation: https://www.gnu.org/licenses/gpl-faq.html#LGPLStaticVsDynamic.

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 15:16):

In the LGPL v2.1 itself, see Section 6, options a and b.

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 15:19):

It also specifically speaks of “a suitable shared library mechanism for linking with the Library” (in 6b), but the intent is pretty explicit: the user must retain means to patch the LGPL code and combine the result against the non-LGPL modules.

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 15:25):

hence, IANAL but I’d argue that in Coq distributing sources qualifies as a “suitable shared library mechanism”, and violating the LGPL from that angle seems essentially impossible.

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 15:26):

OTOH, the preamble adds

Pay close attention to the difference between a "work based on the library" and a "work that uses the library". The former contains code derived from the library, whereas the latter must be combined with the library in order to run.

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 15:28):

which one applies to your case is likely a million dollar question.

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 15:30):

But I don’t mean that the prize money for getting it right is a million dollar. Rather, it can get subtle enough that settling it in court could _cost_ a million dollar in lawyer’s fees :sweat_smile:

view this post on Zulip Paolo Giarrusso (Apr 12 2022 at 15:41):

(many cases are likely simpler, but I don't feel qualified to summarize what the text says)

view this post on Zulip Yishuai Li (Apr 14 2022 at 22:36):

Scenario: https://github.com/Lysxia/coq-simple-io/pull/51/
Abstract: We copied a file from coq/coq and recompiled it with SimpleIO.
Questions:

  1. Must SimpleIO be relicensed? (or will anyone from the Coq team sue us if not?)
  2. If yes, should the license be LGPL-2.1-only or LGPL-2.1-or-later?
  3. Is there a plan to relicense Coq this century?

view this post on Zulip Paolo Giarrusso (Apr 14 2022 at 23:35):

IANAL but I’d say the following: I think @Karl Palmskog ‘s comments apply, and this is not intermingling. While the combination is LGPL, simple-io itself can remain MIT.

view this post on Zulip Paolo Giarrusso (Apr 14 2022 at 23:36):

Concretely, the difference is that somebody could fork your repo, undo the patch https://github.com/Lysxia/coq-simple-io/pull/50 (with certain downsides), and they’d be able to use this under MIT terms.

view this post on Zulip Guillaume Melquiond (Apr 15 2022 at 03:43):

I tend to agree that this falls under the "aggregate work" category rather than the "combined work" one. However, you still need to change a few things. In particular, you can no longer use (license MIT) in your dune-project file. You need to switch to (license "MIT AND LGPL-2.1-only"). Same thing for coq-simple-io.opam.

view this post on Zulip Guillaume Melquiond (Apr 15 2022 at 03:44):

As for relicensing Coq, there are absolutely no plans. I suppose that is wishful thinking by some people who hope that, by repeating it again and again, it will somehow become true some day.

view this post on Zulip Karl Palmskog (Apr 15 2022 at 08:00):

what can already be done today is to run Coq with only permissively licensed (non-LGPL) libraries, that is, without using anything from stdlib. I think this will be much more common in the future.

view this post on Zulip Théo Zimmermann (Apr 15 2022 at 09:49):

A few remarks:

EDITED: last sentence was cut.

view this post on Zulip Karl Palmskog (Apr 15 2022 at 12:29):

I completely agree with Théo, here are the options I see in my order of preference, based on that LGPL is a difficult license to abide by, and the Coq community benefits from permissively license code, especially for Coq Platform projects:

  1. get permission from all relevant stdlib contributors to keep MIT license of coq-simple-io with stdlib files included
  2. copy stdlib files into coq-simple-io and carefully structure their use to make it an aggregation, i.e., license those files under LGPL-2.1-only and keep the MIT license for the rest of coq-simple-io
  3. relicense coq-simple-io under LGPL-2.1-only

Note that nothing prevents you from going with option 2 at first, and then switching "back" to full MIT when you get permission.

view this post on Zulip Li-yao (Apr 15 2022 at 13:20):

Thanks for the tips everyone! Invoice me for the legal fees. I will ask the contributors permission to relicense those files.

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:02):

Coincidentally I'm part of a library that is facing a similar issue with exactly the same files. We are about to release it to the public and are picking a license. Unfortunately it seems that it won't be a true open source license, even though the source will be public (but not usable for commercial purposes). We also copied uint63.ml, but since it's LGLP my understanding is that it would be incompatible with such a non-open license. Our options, as far as I can tell, are:

  1. pick a different license for our project (I tried, no success)
  2. write our own version of uint63.ml (this feels silly and pointless, and I'm not sure what would count as a different version, since it would probably end up being very similar)
  3. quarantine uint63.ml in a new project (licensed under LGPL) and use it as a dependency (this feels silly and also like a loophole?)
  4. ask the 10 or so authors of uint63.ml to use it in our context, or better yet, re-license those files with MIT, which would solve both mine and Li-yao's (and future people's [1]) problems
  5. ?

[1] I believe anyone who uses Coq's primitive objects will eventually run into this issue. Consider the following paragraph from the manual (emphasis mine):

The extraction of these primitives can be customized similarly to the extraction of regular axioms (see Program extraction). Nonetheless, the ExtrOCamlInt63 module can be used when extracting to OCaml: it maps the Coq primitives to types and functions of a Uint63 module (including signed functions for Sint63 despite the name). That OCaml module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq.

That's uint63.ml. The manual itself suggests people do this, but Coq doesn't provide a neat way of doing it other than copy-pasting (or does it? Did I miss it?)

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:05):

Any tips / opinions on what we should do?

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:07):

what's "true open source license"? Do you mean permissive license?

As usual with LGPL, you can make an argument that you are only bundling the file and the other code, and they are under different licenses. Seems clear to me that uint63.ml is a form of interface, and mere users of this interface as originally defined do not become (L)GPL. They'd normally have to modify the interface in some way and connect it to other code, at least.

view this post on Zulip Paolo Giarrusso (Apr 20 2022 at 13:08):

To me, the TLDR is that option 3 is not a loophole, and the extra library isn't actually necessary (except to simplify the legal argument).

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:09):

if many people actually use uint63.ml, you can actually pull it out of the Coq sources and package it on opam, sure

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:09):

"true open source" as defined by FSF; ie, not only open source in the literal sense that the source is public, but also in the sense that it preserves peoples "freedoms" as defined by FSF

view this post on Zulip Paolo Giarrusso (Apr 20 2022 at 13:10):

The intent (and the text) of LGPL only demands that users can still modify the LGPL code (uint63.ml) and link it against your app.

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:10):

FSF doesn't like talking about "open source", they only want to use "free software", which is quite different semantically

view this post on Zulip Paolo Giarrusso (Apr 20 2022 at 13:11):

What @Ana de Almeida Borges wrote sounds indeed like (true) "free software"

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:12):

then s/true open source/free software in my original post, sorry for the confusion

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:12):

then I don't really understand... according to FSF, LGPL is a free software license. But some people in "open source" don't like it much, since it's so hard to abide by.

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:13):

an FSFer would probably relicense uint63.ml under GPL and release everything under GPL

view this post on Zulip Paolo Giarrusso (Apr 20 2022 at 13:14):

I guess the question is about using uint63.ml in proprietary code

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:15):

OK, but that is to me a pure legal-technical question, not a license choice question... All the relevant licenses have been fixed.

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:15):

I'm really not trying to argue in favor or against LGPL or enter the free software debate. I realize I brought it up with my Option 1 above, and I probably could have asked the same question without mentioning it.

view this post on Zulip Paolo Giarrusso (Apr 20 2022 at 13:16):

And I agree that relicensing this file under something MIT-like would save lots of headaches; especially since that's already happening, so one should just upstream the dual licensing?

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:16):

ah OK, I see now. A "non-commercial" license is not free software and it's not open source either (by OSI definition)

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:16):

So yes, I'd like to rephrase my original question under the clear premise that all licenses have been fixed.

view this post on Zulip Paolo Giarrusso (Apr 20 2022 at 13:17):

@Ana de Almeida Borges still, is anybody shipping binaries without source? It doesn't seem the case, so you wouldn't be violating the LGPL.

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:18):

OK, then my answer is: assuming you are using uint63.ml unchanged and purely as a library, you can normally bundle it together with your other code, regardless of the license of the other code. LGPL allows this under most circumstances

view this post on Zulip Guillaume Melquiond (Apr 20 2022 at 13:18):

Note that most of the original issue is that uint63.ml is being compiled with option -rectypes, which is kind of dumb (and can be seen as a bug of Coq's build system). If not for this option, it would be trivial to import the file in any project, irrespective of the license.

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:20):

if you want to be extra sure, you could for example create a custom opam package which only picks out uint63.ml from a Coq release tarball and compiles this file into its own directory. This could live in the Coq opam archive.

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:21):

but in my view, just bundling uint63.ml in a new tarball / source tree with clear indication that it is under LGPL-2.1-only is fine

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:21):

Karl Palmskog said:

OK, then my answer is: assuming you are using uint63.ml unchanged and purely as a library, you can normally bundle it together with your other code, regardless of the license of the other code. LGPL allows this under most circumstances

Ok, then I misunderstood LGPL and this is great news!

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:23):

Karl Palmskog said:

if you want to be extra sure, you could for example create a custom opam package which only picks out uint63.ml from a Coq release tarball and compiles this file into its own directory. This could live in the Coq opam archive.

I think this would be nice even if there was no possible confusion wrt licenses, because it would be more straightforward to install an opam package than figure out how to link to a couple of files living in the Coq kernel

view this post on Zulip Li-yao (Apr 20 2022 at 13:25):

Having it in its own package would be most convenient, in my opinion. Having Coq compile/package it better is okay, but that would only become available on Coq 8.17 or later.

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:26):

if Coq devs allow it, would be great if the package could live in the Coq repo (coq-uint63.opam). Then they could set up fancy Dune tricks to build it, and we could add a package at each new release. But no problem adding an ad-hoc (post-hoc) package now.

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:27):

A similar thing applies to the other primitive objects in Coq btw. There could be other packages for them or they could all live in the same one

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:29):

but also, based on what Guillaume says, an even better solution would be to allow people to use the module directly by just installing Coq (fix the rectype "bug")

view this post on Zulip Paolo Giarrusso (Apr 20 2022 at 13:29):

@Li-yao 8.16, right?

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:30):

maybe this is something for a Coq Call discussion before everyone leaps to action?

view this post on Zulip Paolo Giarrusso (Apr 20 2022 at 13:31):

I wonder if some clients would depend from the separate package — IIUC, this is needed in the extracted code, which might not depend on Coq?

view this post on Zulip Li-yao (Apr 20 2022 at 13:31):

Paolo Giarrusso said:

Li-yao 8.16, right?

idk, maybe, big numbers all look the same to me.

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:32):

right, this is another reason it might be packaged separately. You could install it without installing Coq (but you still need to download Coq's source)

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:38):

Ok, so I think I'll bundle the files with our library and also support the idea of making an opam package with those files so that I can switch to depending on that package when it exists.

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:38):

Should I open an issue or do you want to discuss in the Coq Call first?

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:41):

the procedure is to put an item here: https://github.com/coq/coq/wiki/Coq-Call-2022-04-27

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:41):

based on the Coq Call, the next step could be a PR or an issue.

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 13:42):

That's a lot of postponing ahaha. Next week is not particularly good for me either. Perhaps I can add it to the call for two weeks from now then.

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:44):

OK, you might want to create the issue in the meantime then. Coq issues are not usually where things happen most quickly, but can serve as memento when PRs arrive

view this post on Zulip Karl Palmskog (Apr 20 2022 at 13:45):

the key thing here is that there are many ways the packaging could be handled, and if it's an ongoing package, someone not in the Coq core team will likely have to maintain it (i.e., at least make sure it appears on the Coq opam archive for Coq releases)

view this post on Zulip Li-yao (Apr 20 2022 at 13:59):

I might be able to join the call next week to prod the team on the issue.

view this post on Zulip Ana de Almeida Borges (Apr 20 2022 at 14:10):

https://github.com/coq/coq/issues/15936


Last updated: Feb 05 2023 at 15:03 UTC