Stream: Coq Platform devs & users

Topic: Mere aggregation vs larger work

Michael Soegtrop (Sep 05 2020 at 15:36):

@Karl Palmskog thanks for the links!

A few notes on my understanding of the GPL 3:

• as far as I understand this one does not need to accept the GPL terms to receive or use GPL software, only to convey it. This is stated in section 9 of the GPL. So as I read this there is no issue with combining GPL and non GPL software as a user as long as one does not convey the result.
• most of the severe restriction of the GPL apply only to Conveying Non-Source Forms (chapter 6 of the GPL)
• there are some restrictions on Conveying Modified Source Versions (chapter 5 of the GPL)
• conveying in the sense of the GPL requires a transfer of a copy of the work - this is explicitly stated in chapter 0.
• the coq platform as of today is a pure source distribution and does not convey any of the bundled works and absolutely does not convey modified work. It transfers unmodified works from their original sources (these are the conveyors then) and any modifications are done as patches on the machine of the user. So a transfer of modified work does never happen which excludes by definition the possibility that the coq platform conveys modified work. In this sense neither section 5 nor 6 of the GPL3 apply to the coq platform (as it is today).
• before I create an installer with binary forms I will study the license situation in more detail and contact the FSF for advice. Creating a binary distribution of Coq of cause means to convey modified work and to convey binary form. But I don't think the FSF objects to something which is a pure optimization for an entirely source based distribution system
• creating a docker image is in this sense is also critical and something I would refrain from doing before the situation is clarified

Théo Zimmermann (Sep 05 2020 at 15:40):

https://www.gnu.org/licenses/gpl-faq.en.html#MereAggregation

To me it is clear that the Coq platform is an example of "mere aggregation". However, the patching part creates "modified works", so it is important to provide the code source at the same time as the binary version.

Michael Soegtrop (Sep 05 2020 at 16:16):

@Théo Zimmermann : I don't agree that the Coq platform is an aggregation. Many of the libraries provided link other libraries. In this sense they build "a larger program".

Théo Zimmermann (Sep 05 2020 at 16:19):

Some of them sure, let's say an aggregation of larger programs if that fits more with your view. But in the end, the complete combination is clearly more on the side of aggregation than on the side of larger program as many libraries will not be combined together.

Michael Soegtrop (Sep 05 2020 at 16:19):

I will draw a dependency tree.

Michael Soegtrop (Sep 05 2020 at 16:21):

In the end one solution might be to restrict binary distributions to either aggregates (independent) or license wise compatible stuff. The rest must be compiled from sources then if needed. I hope VST is not part of it (it takes a while to compile).

Michael Soegtrop (Sep 05 2020 at 16:22):

But I wonder what the FSF has to say to mere compile cashes. I don't think it was their intention to hinder software which is entirely open source. On the other hand if I look at the discussion on the Gnu DSW (AutoCad file format) library it doesn't look good.

Michael Soegtrop (Sep 05 2020 at 16:24):

For those note aware: the FSF create a library for DSW support in free software under GPL3 and pretty much all of the large open source CAD projects said they can't use it because they link to GPL2 only libraries. There was a lengthy discussion with the result that the FSF denied to change the license to GPL2+, which was more or less the death of the DSW library.

Michael Soegtrop (Sep 05 2020 at 16:29):

Maybe one should start a discussion on binary distribution of open source software under the environmental aspect. Compiling the Coq platform likely takes 1/2 kWh each time it is done. So in the end the license restrictions say that every user - and much worse every CI run - has to spend 1/2 kWh to comply to the license. This is not very 2020ish. I wonder if GitLab build cashes are legal after all ...

Karl Palmskog (Sep 05 2020 at 16:35):

I think you mean the DWG format, cf. https://web.archive.org/web/20161109103213/http://libregraphicsworld.org/blog/entry/libredwg-drama-the-end-or-the-new-beginning

Michael Soegtrop (Sep 05 2020 at 16:38):

ah yes sorry, DWG

Michael Soegtrop (Sep 05 2020 at 17:00):

A few dependency dumps (in a Coq platform with all modules as in the old installer):

opam list --depends-on coq-mathcomp-ssreflect --recursive --installed --columns=name,version,license:
# Packages matching: installed & rec-depends-on(coq-mathcomp-ssreflect)
# Name                   # Version # License
coq-coquelicot           3.1.0     "LGPL-3.0-or-later"
coq-interval             4.0.0     "CeCILL-C"
coq-mathcomp-algebra     1.11.0    "CECILL-B"
coq-mathcomp-bigenough   1.0.0     "CeCILL-B"
coq-mathcomp-character   1.11.0    "CECILL-B"
coq-mathcomp-field       1.11.0    "CECILL-B"
coq-mathcomp-fingroup    1.11.0    "CECILL-B"
coq-mathcomp-finmap      1.5.0     "CECILL-B"
coq-mathcomp-real-closed 1.1.1     "CECILL-B"
coq-mathcomp-solvable    1.11.0    "CECILL-B"
coq-mathcomp-ssreflect   1.11.0    "CECILL-B"
coq-quickchick           1.4.0     "MIT"

opam list --required-by coq-vst --recursive --installed --columns=name,version,license:
# Packages matching: installed & rec-required-by(coq-vst)
# Name              # Version             # License
base-threads        base
base-unix           base
camlp5              7.12                  "BSD-3-Clause"
conf-findutils      1                     "GPL-3.0-or-later"
conf-g++            1.0                   "GPL-2.0-or-later"
conf-m4             1                     "GPL-3.0-only"
coq                 8.12.0                "LGPL-2.1-only"
coq-compcert        3.7+8.12~coq_platform "INRIA Non-Commercial License Agreement"
coq-flocq           3.3.1                 "LGPL-3.0-or-later"
coq-menhirlib       20200624              "LGPL-3.0-or-later"
coq-vst             2.6                   "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"
dune                2.6.2                 "MIT"
menhir              20200624
menhirLib           20200624
menhirSdk           20200624
num                 1.3                   "LGPL-2.1-only with OCaml-LGPL-linking-exception"
ocaml               4.07.1
ocaml-base-compiler 4.07.1
ocaml-config        1
ocamlbuild          0.14.0                "LGPL-2.1-only with OCaml-LGPL-linking-exception"
ocamlfind           1.8.1

So VST seems to be fine (OCaml and the coq-menhir lib are LGPL 2+ or so).
A binary distribution of coq-interval and coquelicot might be illegal.
So all in all it doesn't look that bad.
I will do a few PRs to fix the license info in opam.

Last updated: Jun 03 2023 at 03:01 UTC