Comment by exikyut | Hacker News Reader

Comment by exikyut | Hacker News Reader

As noted in the License section of the readme,

> CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version of CompCert, without this restriction and with professional support and extra features, can be purchased from AbsInt. See the file LICENSE for more information.

However, https://github.com/AbsInt/CompCert/blob/master/LICENSE goes onto say that

> The following files in this distribution are dual-licensed both under the INRIA Non-Commercial License Agreement and under the Free Software Foundation GNU Lesser General Public License, either version 2.1 or (at your option) any later version: ...

and then lists a bunch of specific files and paths, which may or may not (this is the key question) constitute a majority of the repo. Looking around, I see a few references to the LGPL and LGPLv3.

The LICENSE also makes clear (immediately following the file list) that

> If you opt for the GNU Lesser General Public License, these files are free software and can be used both in commercial and non-commercial contexts, subject to the terms of the GNU Lesser General Public License.

So, broadly speaking: am I just looking at a standard smoke-and-mirrors routine (creating just enough uncertainty that most commercial operations would reasonably pursue the custom license) or are there any actual intuition-violating footguns hiding anywhere in the codebase?

It appears that the LGPL does NOT cover the "meat" of the codebase (see the directories arm, x86, etc) and instead covers the "edges" where their code may interact with other code.

A comment indicates they relicensed some of it GPL->LGPL so I assume they hold the copyright.

The BSD licensed stuff seems to be imported code.

>The files in question are, from a formal verification standpoint, the interface to CompCert. They are licensed under the non-commercial license (NCL) so that they can be used together with the rest of CompCert (the implementation of the compiler, so to speak), which is NCL-only.

>Additionally, the interface files in question are also licensed under the GPL so that they can be used in other, open-source projects such as VST (http://vst.cs.princeton.edu/) that connect with CompCert.

at https://github.com/AbsInt/CompCert/issues/140 (2016); GPL -> LGPL in a later commit.

The copyright holder doesn't have to adhere to the GPL themselves. Even if the complete repository bar one file is GPL, as long as you keep that file, you can't use the project under the GPL. You can replace that file and then use it under the GPL though.

FYI: the directory contains 957 files; 798 of these files are NOT dual-licensed.

But of course it's not a "majority" decision, nor are all files equally important.

Wait, what? I thought the whole point of GPL is that it is viral, i.e. if you use GPL in a part of your shipped program you must release the whole thing.

From GPLv2:

"These requirements apply to the modified work as a whole. If identifiable sections of that work are not derived from the Program, and can be reasonably considered independent and separate works in themselves, then this License, and its terms, do not apply to those sections when you distribute them as separate works. But when you distribute the same sections as part of a whole which is a work based on the Program, the distribution of the whole must be on the terms of this License, whose permissions for other licensees extend to the entire whole, and thus to each and every part regardless of who wrote it."

That only applies to people who don’t own the copyright. If you wrote the original code base, you can license it GPL, but continue to sell it under closed source license as well.

On the other hand, if someone forms it under the GPL, and adds some additional features, the original code base cannot pull those features back in the original closed source project, without ceasing to distribute the whole thing as closed source.

Choosing GPL effectively forms your code, and further code added by others can no longer be added to the “proprietary” branch. But you can continue adding code yourself in parallel in both branches.

> code added by others can no longer be added to the “proprietary” branch

One thing to keep in mind, if you sign over your copyright by agreeing to contribute using a Contributor License Agreement (CLA), the person or organization can take your contributions proprietary.

Makes sense, thanks.

INAL

LGPL is not GPL. You are for example allowed to dynamic link from proprietary code to LGPL libraries. This is not the case with GPL shared libraries. You should take look at the LGPL license agreement and then see how the code is used.

You can link to GPL libraries from proprietary code if you buy a commercial license from the library's copyright owner.

It is not a question if some files constitute a majority, since this is not majority vote based.

As far as I read your evaluation, probably it is gpl. But without the gpl linker exception you cannot create non gpl binaries.

That is confusing. GCC specifically includes the "GCC runtime library exception" so that you can produce non-GPL binaries.

Yes. Gcc does that and there is no problem, but the post is not about gcc (as far as I can tell from my tiny mobile screen)

>but the post is not about gcc

Right. It's about a compiler with a GPL license but without a similar exception. I was making a comparison.

The CompCert compiler is not under the GPL or LGPL, it is under a proprietary license. Some parts may be released with other licenses, but that is different.

That's not the point going down this thread. If part of it is GPL (and not LGPL), it makes it impossible to release compiled binaries made with it that are not GPL. It appears they attempted to switch to LGPL to fix that two months ago[1], but perhaps missed some parts.

[1] https://github.com/AbsInt/CompCert/commit/04f499c632a76e4605...

Reply on news.ycombinator.com