@Karl Palmskog thanks for the links!
A few notes on my understanding of the GPL 3:
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.
@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".
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.
I will draw a dependency tree.
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).
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.
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.
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 ...
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
ah yes sorry, DWG
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