On Sun, 12 Jul 2020 19:12:28 +0200, Giovanni Mascellani <[email protected]> wrote: > I now want to include some example databases too, in a package called > "metamath-databases".
What directories are you planning to install them in? I would like to modify mmj2 so that if it can't find a database anywhere else it would look there. Is your current plan to store them in: /usr/share/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").... That seems reasonable for now. The branch name might change eventually, but that seems like the current one. > * 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. That's up to them, but I would encourage that. --- David A. Wheeler -- 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/E1jufmA-0000n0-Ee%40rmmprod06.runbox.
