Karl Palmskog (Oct 06 2020 at 13:28): 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:
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.
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.
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.
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.
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.
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.
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 ?
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.
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).
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
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.
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.
Paolo Giarrusso (Oct 08 2020 at 12:49):I am not implying that this necessary condition is satisfiable, or satisfiable with reasonable effort.
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
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 .
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.
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.
Paolo Giarrusso (Oct 08 2020 at 12:53):But coq-community would still need to write those requirements, so this is not 0 work.
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.
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.
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
Paolo Giarrusso (Oct 08 2020 at 12:56):I’m probably indeed worrying too much about corner cases, as I’m prone to.
Paolo Giarrusso (Oct 08 2020 at 12:57):I’ll leave this to you (but feel free to ask)
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.
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)
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:
MIT license: a very permissive and popular open source license. This is the best choice if you want to maximize the reusability of your project.
MPL-2.0 license: a weak copyleft license. You can use this license if you want to restrict the license under which modified versions of your project may be distributed. It does not limit how larger works may depend on your project. This license should be preferred over the (historically more prevalent) LGPL-2.1 license because it is technically simpler to understand and abide by.
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.
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.
Théo Zimmermann (Oct 08 2020 at 13:33):This would avoid having this recommendation staying as an obscure FAQ item.
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.
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.
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?)
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
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
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.
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.
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
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)
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.
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.
Théo Zimmermann (Oct 20 2020 at 07:04):And as soon as you have other people owning copyright, relicensing gets more complicated.
Yishuai Li (Oct 20 2020 at 07:05):Is that blocking Coq from relicensing to MPL?
Théo Zimmermann (Oct 20 2020 at 07:05):Yep
Théo Zimmermann (Oct 20 2020 at 07:05):The copyright ownership of Coq is a mess.
Théo Zimmermann (Oct 20 2020 at 07:05):There are so many contributors.
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.
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...
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
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.
Théo Zimmermann (Oct 20 2020 at 07:14):;-)
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.
Karl Palmskog (Oct 20 2020 at 07:15):that would indeed solve everything in one sweep
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
Théo Zimmermann (Oct 20 2020 at 08:54):Oh, that is great news! Does this mean that the law is already voted?
Paolo Giarrusso (Oct 20 2020 at 09:55):Wait a second, what do you mean "attributed"?
Paolo Giarrusso (Oct 20 2020 at 09:56):Ah, it consolidates the copyright that French academia already has I guess.
Paolo Giarrusso (Oct 20 2020 at 09:57):(for a second I misread it as nationalizing ownership of all of Coq, including external contributors)
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.
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.
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
Théo Zimmermann (Oct 20 2020 at 15:15):cool
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".
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".
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 :-)
Clément Pit-Claudel (Nov 17 2020 at 14:51):Théo Zimmermann said:
- MPL-2.0 license: a weak copyleft license. You can use this license if you want to restrict the license under which modified versions of your project may be distributed. […] This license should be preferred over the (historically more prevalent) LGPL-2.1 license because it is technically simpler to understand and abide by.
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?
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.
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.
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.
Clément Pit-Claudel (Nov 22 2020 at 20:23):Yes, you're probably both right.
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?
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).
Yishuai Li (Apr 12 2022 at 05:46):Hope to see Coq relicensed to MPL-ish someday.
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.
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.
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)
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.
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.
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.
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."
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.)
Karl Palmskog (Apr 12 2022 at 09:51):Coq is LGPL-2.1-only, so only definitions from that version would apply
Guillaume Melquiond (Apr 12 2022 at 10:33):Sure, and the sentence I quoted is from LGPL 2.1.
Paolo Giarrusso (Apr 12 2022 at 15:11):See gnu.org’s interpretation: https://www.gnu.org/licenses/gpl-faq.html#LGPLStaticVsDynamic.
Paolo Giarrusso (Apr 12 2022 at 15:16):In the LGPL v2.1 itself, see Section 6, options a and b.
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.
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.
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.
Paolo Giarrusso (Apr 12 2022 at 15:28):which one applies to your case is likely a million dollar question.
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:
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)
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:
LGPL-2.1-only or LGPL-2.1-or-later? 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.
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.
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.
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.
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.
Théo Zimmermann (Apr 15 2022 at 09:49):A few remarks:
EDITED: last sentence was cut.
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:
Note that nothing prevents you from going with option 2 at first, and then switching "back" to full MIT when you get permission.
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.
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:
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)uint63.ml in a new project (licensed under LGPL) and use it as a dependency (this feels silly and also like a loophole?)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[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?)
Ana de Almeida Borges (Apr 20 2022 at 13:05):Any tips / opinions on what we should do?
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.
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).
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
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
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.
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
Paolo Giarrusso (Apr 20 2022 at 13:11):What @Ana de Almeida Borges wrote sounds indeed like (true) "free software"
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
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.
Karl Palmskog (Apr 20 2022 at 13:13):an FSFer would probably relicense uint63.ml under GPL and release everything under GPL
Paolo Giarrusso (Apr 20 2022 at 13:14):I guess the question is about using uint63.ml in proprietary code
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.
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.
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?
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)
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.
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.
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
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.
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.
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
Ana de Almeida Borges (Apr 20 2022 at 13:21):Karl Palmskog said:
OK, then my answer is: assuming you are using
uint63.mlunchanged 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!
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.mlfrom 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
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.
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.
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
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")
Paolo Giarrusso (Apr 20 2022 at 13:29):@Li-yao 8.16, right?
Karl Palmskog (Apr 20 2022 at 13:30):maybe this is something for a Coq Call discussion before everyone leaps to action?
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?
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.
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)
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.
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?
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
Karl Palmskog (Apr 20 2022 at 13:41):based on the Coq Call, the next step could be a PR or an issue.
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.
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
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)
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.
Ana de Almeida Borges (Apr 20 2022 at 14:10):https://github.com/coq/coq/issues/15936
Last updated: Jun 06 2023 at 22:01 UTC