Hi, as I wrote some time ago on this mailing list, I uploaded metamath as an official package in Debian (it is currently in the development version of Debian, and it will released when the new version of Debian will be released; but in the meantime I see it has already been released with Ubuntu 20.04 LTS Focal).
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? 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? Thanks for your help, Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/d34869d3-8339-a1ca-cd93-1cc670ad89b9%40gmail.com.
signature.asc
Description: OpenPGP digital signature
