search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
79 stars 25 forks source link

Public domain release #7

Open kryptine opened 4 years ago

kryptine commented 4 years ago

Is there any plan to make this repository public domain yet?

david-a-wheeler commented 4 years ago

That's up to Norm. But it is already released as open source software.

nmegill commented 4 years ago

I'm perfectly happy to release all the code I've written as public domain or with an MIT-type license. The main issue is that patches have been contributed over time by other people, who may have assumed their contribution was under the GPL. Although most of them are small, it gets into a gray area, and I haven't been actively pursuing getting it resolved.

Do you have a specific project in mind that would require more liberal licensing?

kryptine commented 4 years ago

@nmegill If so please add a notice stating that your contributions are public domain and that the project includes code from other people which may be GPL licensed.

benjub commented 4 years ago

From what I understand from https://anydifferencebetween.com/difference-between-public-domain-and-open-source-software/ "open source software" already allows basically everything (?) I am quite happy that there is some kind of "reference implementation" and that the Metamath program stays associated with the name of Norm Megill.

digama0 commented 4 years ago

GPL v2 is one of the more aggressive open source licenses, and many people avoid it for the copyleft provisions. Basically, anything based on GPL v2 code must also be GPL v2. The idea is to give some incentive for companies to open source their code, but in practice it often means that GPL code is unusable in commercial contexts, while public domain code would be fine - there is no provision saying you can't put PD or MIT code inside a commercial product.

Taneb commented 4 years ago

@kryptine where did the suggestion that this code might become public domain come from?

nmegill commented 4 years ago

If people think it is useful, I can put (starting with next release) the following comment at the top of metamath.c:

/* Copyright notice:  All code in this program that was written by Norman
   Megill is public domain.  However, the project includes code contributions
   from other people which may be GPL licensed. */

The code or patches that have been contributed are the following, which are listed in the change history at the top of metamath.c. I don't think there were any others. Unfortunately, I didn't archive all of the early versions, so it might not always be possible to identify exactly what code was changed.

/* 0.111 22-Nov-2014 nm metamath.c, mmcmds.c, mmcmdl.c, mmhlpb.c - added
   /NO_NEW_AXIOMS_FROM qualifier to MINIMIZE_WITH; see HELP MINIMIZE_WITH.
   21-Nov-2014 Stepan O'Rear mmdata.c, mmhlpb.c - added ~ label range specifier
   to wildcards; see HELP SEARCH */
/* 0.110 2-Nov-2014 nm mmcmds.c - fixed bug 1114 (reported by Stefan O'Rear);
   metamath.c, mmhlpb.c - added "SHOW STATEMENT =" to show the statement
   being proved in MM-PA (based on patch submitted by Stefan O'Rear) */
/* 0.07.98 30-Oct-2013 Wolf Lammen mmvstr.c,h, mmiou.c, mmpars.c,
   mmdata.c  - improve code style and program structure */
/* 0.07.97 20-Oct-2013 Wolf Lammen mmvstr.c,h, metamath.c - improved linput();
   nm mmcmds.c, mmdata.c - tolerate bad proofs in SHOW TRACE_BACK etc. */
/* 0.07.96 20-Sep-2013 Wolf Lammen mmvstr.c - revised cat();
   nm mmwtex.c, mminou.c - change a print2 to printLongLine to fix bug 1150 */
/* 0.07.95 18-Sep-2013 Wolf Lammen mmvstr.c - optimized cat();
   nm metamath.c, mmcmds.c, mmdata.c, mmpars.c, mmpfas.c, mmvstr.c,
   mmwtex.c - suppress some clang warnings */
/* 0.07.94 28-Aug-2013 Alexey Merkulov mmcmds.c, mmpars.c - fixed several
   memory leaks found by valgrind --leak-check=full --show-possibly-lost=no */
/* 0.07.93 8-Jul-2013 Wolf Lammen mmvstr.c - simplified let() function;
   also many minor changes in m*.c and m*.h to assist future refactoring */
/* 0.07.51 9-Sep-2010 Stefan Allen mmwtex.c - put hyperlinks on hypothesis
   label references in SHOW STATEMENT * /HTML, ALT_HTML output */
/* 0.07.44 12-May-2009 Stefan Allan, nm metamath.c, mmcmdl.c, mmwtex.c -
   added SHOW STATEMENT / MNEMONICS - see HELP SHOW STATEMENT */
/* 0.07.29 6-Feb-2007 Jason Orendorff mmpfas.c - Patch to eliminate the
   duplicate "Exceeded trial limit at step n" messages */
/* 0.07x:  [date unknown; before 22-Jun-05] Fixed to work with AMD64 with 64-bit
   longs by Waldek Hebisch; deleted unused stuff in mmdata.c */

FYI these are the versions archived before the date range above: mm-0.06-4-May-1997 mm-0.06b-30-Jun-1998 mm-0.06c-20-Feb-1999 mm-0.06d-27-Jun-1999 mm-0.07.0e-9-Dec-2000 mm-0.07.0i-10-Feb-2002 mm-0.07.0m-17-Nov-2002 mm-0.07.0r-8-Sep-2003 mm-0.07.0v-27-Feb-2004 mm-0.07.50-21-Feb-2010 mm-0.07.73-26-Dec-2011 mm-0.07.82-16-Sep-2012 mm-0.07.92-28-Jun-2013 mm-0.07.94-28-Aug-2013 mm-0.07.95-18-Sep-2013 mm-0.07.96-20-Sep-2013 mm-0.07.97-20-Oct-2013 mm-0.07.98-30-Oct-2013 mm-0.07.99-01-Nov-2013 mm-0.100-30-Nov-2013 mm-0.101-27-Dec-2013 mm-0.102-02-Jan-2014 mm-0.103-04-Jan-2014 mm-0.104-14-Feb-2014 mm-0.105-15-Feb-2014 mm-0.106-30-Mar-2014 mm-0.107-21-Jun-2014 mm-0.108-25-Jun-2014 mm-0.109-20-Aug-2014 mm-0.110-02-Nov-2014 mm-0.111-22-Nov-2014 mm-0.112-15-Apr-2015

david-a-wheeler commented 4 years ago

Open source software, including their licenses, is part of my day job.

The usual metamath databases are in the public domain, but metamath-exe has long been released under the GPLv2. That may be the initial confusion.

Is there a specific problem / use case the current license doesn't support for you? The GPLv2 is an open source software license, so anyone can use it, redistribute it, modify it, and redistribute the modified version as well. What exactly does it prevent you from dong?

in practice it often means that GPL code is unusable in commercial contexts,

That's not correct. Many companies including Red Hat, IBM, Ubuntu, GitHub, AdaCore, Oracle, MariaDB Corporation, and Microsoft use & sell GPL code, and they would be surprised to hear that they're not commercial companies. Red Hat, since its founding, has long preferred the GPL when releasing code it writes. Many widely-used programs including the Linux kernel and git are released using the GPL. It's true that some specific practices used by some commercial companies aren't allowed by the GPL, but that's not at all the same thing.

Norm: If you're thinking about relicensing to either the MIT or CC0 license, I would recommend the MIT license for code and not using CC0 or "public domain" for code:

kryptine commented 4 years ago

If people think it is useful, I can put (starting with next release) the following comment at the top of metamath.c:

/* Copyright notice:  All code in this program that was written by Norman
   Megill is public domain.  However, the project includes code contributions
   from other people which may be GPL licensed. */

The code or patches that have been contributed are the following, which are listed in the change history at the top of metamath.c. I don't think there were any others. Unfortunately, I didn't archive all of the early versions, so it might not always be possible to identify exactly what code was changed.

/* 0.111 22-Nov-2014 nm metamath.c, mmcmds.c, mmcmdl.c, mmhlpb.c - added
   /NO_NEW_AXIOMS_FROM qualifier to MINIMIZE_WITH; see HELP MINIMIZE_WITH.
   21-Nov-2014 Stepan O'Rear mmdata.c, mmhlpb.c - added ~ label range specifier
   to wildcards; see HELP SEARCH */
/* 0.110 2-Nov-2014 nm mmcmds.c - fixed bug 1114 (reported by Stefan O'Rear);
   metamath.c, mmhlpb.c - added "SHOW STATEMENT =" to show the statement
   being proved in MM-PA (based on patch submitted by Stefan O'Rear) */
/* 0.07.98 30-Oct-2013 Wolf Lammen mmvstr.c,h, mmiou.c, mmpars.c,
   mmdata.c  - improve code style and program structure */
/* 0.07.97 20-Oct-2013 Wolf Lammen mmvstr.c,h, metamath.c - improved linput();
   nm mmcmds.c, mmdata.c - tolerate bad proofs in SHOW TRACE_BACK etc. */
/* 0.07.96 20-Sep-2013 Wolf Lammen mmvstr.c - revised cat();
   nm mmwtex.c, mminou.c - change a print2 to printLongLine to fix bug 1150 */
/* 0.07.95 18-Sep-2013 Wolf Lammen mmvstr.c - optimized cat();
   nm metamath.c, mmcmds.c, mmdata.c, mmpars.c, mmpfas.c, mmvstr.c,
   mmwtex.c - suppress some clang warnings */
/* 0.07.94 28-Aug-2013 Alexey Merkulov mmcmds.c, mmpars.c - fixed several
   memory leaks found by valgrind --leak-check=full --show-possibly-lost=no */
/* 0.07.93 8-Jul-2013 Wolf Lammen mmvstr.c - simplified let() function;
   also many minor changes in m*.c and m*.h to assist future refactoring */
/* 0.07.51 9-Sep-2010 Stefan Allen mmwtex.c - put hyperlinks on hypothesis
   label references in SHOW STATEMENT * /HTML, ALT_HTML output */
/* 0.07.44 12-May-2009 Stefan Allan, nm metamath.c, mmcmdl.c, mmwtex.c -
   added SHOW STATEMENT / MNEMONICS - see HELP SHOW STATEMENT */
/* 0.07.29 6-Feb-2007 Jason Orendorff mmpfas.c - Patch to eliminate the
   duplicate "Exceeded trial limit at step n" messages */
/* 0.07x:  [date unknown; before 22-Jun-05] Fixed to work with AMD64 with 64-bit
   longs by Waldek Hebisch; deleted unused stuff in mmdata.c */

FYI these are the versions archived before the date range above: mm-0.06-4-May-1997 mm-0.06b-30-Jun-1998 mm-0.06c-20-Feb-1999 mm-0.06d-27-Jun-1999 mm-0.07.0e-9-Dec-2000 mm-0.07.0i-10-Feb-2002 mm-0.07.0m-17-Nov-2002 mm-0.07.0r-8-Sep-2003 mm-0.07.0v-27-Feb-2004 mm-0.07.50-21-Feb-2010 mm-0.07.73-26-Dec-2011 mm-0.07.82-16-Sep-2012 mm-0.07.92-28-Jun-2013 mm-0.07.94-28-Aug-2013 mm-0.07.95-18-Sep-2013 mm-0.07.96-20-Sep-2013 mm-0.07.97-20-Oct-2013 mm-0.07.98-30-Oct-2013 mm-0.07.99-01-Nov-2013 mm-0.100-30-Nov-2013 mm-0.101-27-Dec-2013 mm-0.102-02-Jan-2014 mm-0.103-04-Jan-2014 mm-0.104-14-Feb-2014 mm-0.105-15-Feb-2014 mm-0.106-30-Mar-2014 mm-0.107-21-Jun-2014 mm-0.108-25-Jun-2014 mm-0.109-20-Aug-2014 mm-0.110-02-Nov-2014 mm-0.111-22-Nov-2014 mm-0.112-15-Apr-2015

Thanks! This is exactly what I want.

david-a-wheeler commented 4 years ago

Thanks! This is exactly what I want.

Why?

kryptine commented 4 years ago

Thanks! This is exactly what I want.

Why?

Most of the code is written by Norman, so if he releases his code into the public domain then only the problem of dealing with other contributions (which are mostly minor) remains.

digama0 commented 4 years ago

@kryptine The question is why you want to change the already open source license of this project. What are your constraints, or is this just a ethical stance?

kryptine commented 4 years ago

@kryptine The question is why you want to change the already open source license of this project. What are your constraints, or is this just a ethical stance?

I've seen it mentioned on Metamath website that Norman might want to change the license of this project to public domain or similar. And I also happen to like these licenses.