5 ms·

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, educatio

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 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?

bombcar 5y ago
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.
alfu 5y ago
>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/ http://vst.cs.princeton.edu/) that connect with CompCert. at https://github.com/AbsInt/CompCert/issues/140 https://github.com/AbsInt/CompCert/issues/140 (2016); GPL -> LGPL in a later commit.
andi999 5y ago
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.
- tyingq 5y ago
  That is confusing. GCC specifically includes the "GCC runtime library exception" so that you can produce non-GPL binaries.
  - andi999 5y ago
    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)
    - tyingq 5y ago
      >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.
      - dwheeler 5y ago
        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.
        deleted 5y ago
        [deleted]
        deleted 5y ago
        [deleted]
        tyingq 5y ago
        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/04f499c632a76e460560fc9ec4e14d8216e7fc18 https://github.com/AbsInt/CompCert/commit/04f499c632a76e4605...
Denvercoder9 5y ago
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.
underdeserver 5y ago
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."
- LadyCailin 5y ago
  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.
  - jhauris 5y ago
    > 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.
  - underdeserver 5y ago
    Makes sense, thanks.
- dosshell 5y ago
  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.
zvr 5y ago
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.

bombcar 5y ago

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.

alfu 5y ago

>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/ http://vst.cs.princeton.edu/) that connect with CompCert. at https://github.com/AbsInt/CompCert/issues/140 https://github.com/AbsInt/CompCert/issues/140 (2016); GPL -> LGPL in a later commit.

andi999 5y ago

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.

tyingq 5y ago
That is confusing. GCC specifically includes the "GCC runtime library exception" so that you can produce non-GPL binaries.
- andi999 5y ago
  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)
  - tyingq 5y ago
    >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.
    - dwheeler 5y ago
      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.
      - deleted 5y ago
        [deleted]
      - deleted 5y ago
        [deleted]
      - tyingq 5y ago
        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/04f499c632a76e460560fc9ec4e14d8216e7fc18 https://github.com/AbsInt/CompCert/commit/04f499c632a76e4605...

Denvercoder9 5y ago

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.

underdeserver 5y ago

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."

LadyCailin 5y ago
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.
- jhauris 5y ago
  > 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.
- underdeserver 5y ago
  Makes sense, thanks.
dosshell 5y ago
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.

zvr 5y ago

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.