New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
modex: add modex analysis tool package #30571
Conversation
meta = { | ||
description = "Mechanical extraction of verification models from implementation level C code for spin."; | ||
platforms = stdenv.lib.platforms.all; | ||
license = stdenv.lib.licenses.free; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks like this is unfreeRedistributable
, from modex.c:
/* Copyright (c) 2000-2003 by Lucent Technologies - Bell Laboratories */
/* All Rights Reserved. This software is for educational purposes only. */
/* Permission is given to distribute this code provided that this intro- */
/* ductory message is not removed and no monies are exchanged. */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Software written by Gerard J. Holzmann based on the public domain */
/* ANSI-C parser Ctree Version 0.14 from Shaun Flisakowski */
/* Extensions (c) 2004-2014 by Caltech/JPL Pasadena, CA 91109 */
The "no monies" part I would say makes it nonfree.
buildInputs = [ bison flex ]; | ||
|
||
meta = { | ||
description = "Mechanical extraction of verification models from implementation level C code for spin."; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The description should not end with a period.
As noted in previous feedback, the license is found at the start of the modex.c source file: /* Copyright (c) 2000-2003 by Lucent Technologies - Bell Laboratories */ /* All Rights Reserved. This software is for educational purposes only. */ /* Permission is given to distribute this code provided that this intro- */ /* ductory message is not removed and no monies are exchanged. */ /* No guarantee is expressed or implied by the distribution of this code. */ /* Software written by Gerard J. Holzmann based on the public domain */ /* ANSI-C parser Ctree Version 0.14 from Shaun Flisakowski */ /* Extensions (c) 2004-2014 by Caltech/JPL Pasadena, CA 91109 */ This does not conform to any SPDX-identified license or other common license description (and unfortunately is only visible after unpacking the tarball). It does require that no monies are exchanged, but this doesn't preclude redistribution via a Nixpkgs channel as I understand it per https://nixos.org/nixpkgs/manual/#sec-meta-license, so this is identified as a free license.
@vyp Thanks for the feedback, and especially locating that copyright text. I have a different understanding of the "free"-ness aspect based on further research, and so I've updated it based on that understanding (and included that information in the patch comments to ensure it remains associated with the text in question for future reference), so please take a look at the patch and let me know if you agree or where I am misunderstanding the issue. |
@kquick From https://nixos.org/nixpkgs/manual/#sec-meta-license, for
"free software" refers to "the four essential freedoms" listed here: https://www.gnu.org/philosophy/free-sw.en.html. The important thing to realize, and this is confusing, is that "free software" isn't actually referring to gratis software, software that you don't have to pay money for. Whether or not it's gratis is irrelevant to whether it is "free software". Freedom 0 there says:
But the copyright header here says "This software is for educational purposes only.". I'm not a lawyer but that seems to suggest you may only use this software for educational purposes, so it's nonfree because it doesn't comply with freedom 0. The term "free software" is almost synonymous with "open source", even though open source has its own separate definition: https://opensource.org/osd-annotated. So if something is not open source, it's also most likely not free software. I mention this because the first criteria listed here:
makes it quite obvious that modex is not open source, because it doesn't allow to sell the software (the requirement that "no monies are exchanged" when distributing). Free software requires this through freedom 0 as well, but it's vague and not as explicit, so it's harder to explain. 🤷♀️ So for the above reasons, I recommend setting the license to Otherwise if you disagree with me, of course feel free to tell me why. The situation seems pretty clear to me though, but it's possible I may have overlooked things. |
@vyp, I agree that free and open are both distinct terms, and even considered separately there are multiple interpretations. You started with the GNU interpretation of "free" above, but there are many other interpretations of "free" (most of which are less stringent than the GNU version which embodies Stallman's perspective on the matter). You then referenced the OSI description of "open", which supplies their perspective on one aspect of that term. While both of these represent interesting perspectives on the matter, there is a wide range of meanings of "free" that can be applied and it's possible to find other licenses and perspectives which conflict with these two as well. Ultimately, the term "free" can be interpreted in a number of ways (some of which are conflicting), which is why I consulted https://nixos.org/nixpkgs/manual/#sec-meta-license to determine the Nixpkgs application of the term in order to conform most closely to the interpretation most applicable to this situation. The Nixpkg application of the term from the above reference describes "unfreeRedistributable" as "... can be redistributed in binary form. ... legal to distribute the output of the derivation.". The license expressed for modex does allow the redistribution of source code and is therefore less restrictive than unfreeRedistributable. The primary application of the term "free" from the Nixpkg perspective appears to be the concern over violation of the copyright holder's rights if the package is distributed in source or binary form via the nix channels, and both of these appear to be allowed for the modex license. By marking the modex package as "unfree", it also requires the user to enable unfree packages in order to install it, and I believe that gate should be reserved for controlling licenses with much more onerous restrictions than the one represented by modex. Does this information help explain why I've classified this license in this way for the pull request? |
Respectfully I disagree. To me, it's quite clear when the description of the attribute mentions "free software", it's referring to https://www.gnu.org/philosophy/free-sw.en.html. And as such, if anything doesn't meet these criteria, they must be I will say though, that if modex is allowed under
Yeah so I'd consider this a feature. I think what you're saying though, is that your issue is that you want to be able to use modex without enabling
FYI I wasn't really making or stressing this point, I don't think it's really relevant to this discussion anyhow. I just meant to say that "free software" is practically synonymous with "open source", to be able to make the point that modex is neither "free software" nor "open source". |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
See @vyp's comments
Stalled |
Motivation for this change
Add new tool not currently in nixpkgs.
Things done
build-use-sandbox
innix.conf
on non-NixOS)nix-shell -p nox --run "nox-review wip"
./result/bin/
)