diff options
| author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-09-21 15:24:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-09-21 15:24:17 +0200 |
| commit | 8fde5790b4f41cec33e994a0f7faa5326e503b7e (patch) | |
| tree | 0b206cde0ab9eff992cf5761d436f69b3c32fba4 | |
| parent | 3370615a7f1ad927ace45e268b694a184d2ffd43 (diff) | |
| download | nixlib-8fde5790b4f41cec33e994a0f7faa5326e503b7e.tar nixlib-8fde5790b4f41cec33e994a0f7faa5326e503b7e.tar.gz nixlib-8fde5790b4f41cec33e994a0f7faa5326e503b7e.tar.bz2 nixlib-8fde5790b4f41cec33e994a0f7faa5326e503b7e.tar.lz nixlib-8fde5790b4f41cec33e994a0f7faa5326e503b7e.tar.xz nixlib-8fde5790b4f41cec33e994a0f7faa5326e503b7e.tar.zst nixlib-8fde5790b4f41cec33e994a0f7faa5326e503b7e.zip | |
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.
| -rw-r--r-- | lib/licenses.nix | 5 | ||||
| -rw-r--r-- | 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 edf35ec035b2..a790b576032d 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 950c7f96b6fb..a12f1c42ba61 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 ]; |