From 8fde5790b4f41cec33e994a0f7faa5326e503b7e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Thu, 21 Sep 2017 15:24:17 +0200 Subject: [PATCH] compcert: fix license The license of CompCert is not a generic "INRIA" license. It is "INRIA Non-Commercial Agreement for the CompCert verified compiler". As unfortunate as it may seem, this is a non-free license (clearly mentioned as such in its preamble). See also #20256. --- lib/licenses.nix | 5 +++-- pkgs/development/compilers/compcert/default.nix | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/lib/licenses.nix b/lib/licenses.nix index edf35ec035b..a790b576032 100644 --- a/lib/licenses.nix +++ b/lib/licenses.nix @@ -292,9 +292,10 @@ lib.mapAttrs (n: v: v // { shortName = n; }) rec { fullName = "Independent JPEG Group License"; }; - inria = { - fullName = "INRIA Non-Commercial License Agreement"; + inria-compcert = { + fullName = "INRIA Non-Commercial License Agreement for the CompCert verified compiler"; url = "http://compcert.inria.fr/doc/LICENSE"; + free = false; }; ipa = spdx { diff --git a/pkgs/development/compilers/compcert/default.nix b/pkgs/development/compilers/compcert/default.nix index 950c7f96b6f..a12f1c42ba6 100644 --- a/pkgs/development/compilers/compcert/default.nix +++ b/pkgs/development/compilers/compcert/default.nix @@ -40,7 +40,7 @@ stdenv.mkDerivation rec { meta = with stdenv.lib; { description = "Formally verified C compiler"; homepage = "http://compcert.inria.fr"; - license = licenses.inria; + license = licenses.inria-compcert; platforms = platforms.linux ++ platforms.darwin; maintainers = with maintainers; [ thoughtpolice jwiegley vbgl ];