On Sunday, July 12, 2020 at 1:12:32 PM UTC-4, Giovanni Mascellani wrote: ...
> I now want to include some example databases too, in a package called > "metamath-databases". I see that set.mm, iset.mm and nf.mm are > maintained in [1], which can be probably considered their canonical > location (using branch "develop"). > > [1] https://github.com/metamath/set.mm > > For other databases mentioned by the Metamath readme (hol.mm, ql.mm, > demo0.mm, miu.mm, big-unifier.mm and peano.mm), it seems that they can > be downloaded at the URL > > http://us.metamath.org/metamath/NAME.mm > > Can this be considered the canonical location where to fetch the most > updated version, or is there anything better? > While I expect all of the .mm's will be kept updated in the http://us.metamath.org/metamath/ directory indefinitely, I suggest we add the missing ones (hol.mm ql.mm demo0.mm miu.mm big-unifier.mm peano.mm) to the https://github.com/metamath/set.mm directory. That will put them under version control (they aren't now) and will also be guaranteed to be the latest (us.metamath.org sometimes lags by a few days). I will do that tomorrow if there are no objections. > Also, I would like to note that: > > * the files big-unifier.mm, demo0.mm, hol.mm, miu.mm and ql.mm are > placed in the public domain using the Creative Commons Public Domain > Dedication (http://creativecommons.org/licenses/publicdomain/). The > linked web page notes that that tool has been retired and its usage is > now discouraged. It is suggested to port them to CC0, which is what > set.mm and iset.mm are currently using. I would ask to Norm and Mario, > if they agree, to switch to the new tool, so that the databases' legal > status is clearer. > > * nf.mm does not have any copyright or licensing indication. Or, at > least, I cannot find any. Could its status be cleared, so that it is > possible to distribute it without concerns? Once these are on github, they can be updated via pull requests with whatever CC0 wording is desired. For nf.mm, I would suggest making a PR with the desired changes, then wait for Scott Fenton's (@sctfn) approval (if he isn't reading this post now). Norm -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7994afaa-e9eb-4dfb-bb08-10a333b68723o%40googlegroups.com.
