Stream: Coq Platform devs & users

Topic: Mere aggregation vs larger work


view this post on Zulip Michael Soegtrop (Sep 05 2020 at 15:36):

@Karl Palmskog thanks for the links!

A few notes on my understanding of the GPL 3:

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Sep 05 2020 at 16:19):

I will draw a dependency tree.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ...

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Sep 05 2020 at 16:38):

ah yes sorry, DWG

view this post on Zulip 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: Jan 30 2023 at 10:03 UTC