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.
>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.
But of course it's not a "majority" decision, nor are all files equally important.
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."
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.
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.
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.
As far as I read your evaluation, probably it is gpl. But without the gpl linker exception you cannot create non gpl binaries.
Right. It's about a compiler with a GPL license but without a similar exception. I was making a comparison.
[1] https://github.com/AbsInt/CompCert/commit/04f499c632a76e4605...
> 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?