Adopt a standard encoding of license names in project metadata and OPAM packages

[palmskog]

Meta-issue

As highlighted by @Zimmi48 in a recent pull request, we are currently using informal conventions to indicate project licenses in OPAM files, e.g., LGPL 3 and LGPL2.

To address this, I opened an issue in the Coq OPAM archive, which is the intended home for OPAM packages in Coq-community. As suggested by @Zimmi48, I proposed the archive should use the SPDX license name format, which is used by Elm packages.

Since we are dependent on the Coq OPAM archive for distribution, I believe we should wait to enforce SPDX until they have switched, rather than unilaterally adopting it and making the archive even less uniform in license naming.

[palmskog]

Note that projects can already start to use the SPDX license full names (used only in README.md) and include the SPDX license identifier in meta.yml as additional metadata. For example, in AAC tactics:

license:
  fullname: GNU General Public License v3.0 or later
  identifier: GPL-3.0-or-later
  shortname: GPL 3

[Zimmi48]

Right. We can then remove the "shortname" later on if there is a decision to standardize opam packages to use SPDX as well.

[palmskog]

For anyone following this (and for posterity), I have talked to the Coq OPAM repo maintainer, and we've decided to to use SPDX license strings for all Coq-community OPAM packages from now on. Conversion of old packages will happen as we go along.

[Zimmi48]

When should we close this issue?

[palmskog]

I think we should close this issue when:

• [ ] we have properly documented our SPDX requirements for projects
• [ ] all Coq-community projects have a meta.yml which contains an SPDX identifier
• [ ] all Coq-community OPAM packages have migrated to using SPDX identifiers

[Zimmi48]

We have a coq-community package (math-classes) that is not under an “open source” license per se but has a non-standard public domain dedication, thus it has no SPDX identifier. Since public domain allows everything, including changing the license, we should put a standard public domain license such as CC-0 or the Unlicense which both have a SPDX identifier.