Canonical location for Metamath databases

[Giovanni Mascellani]

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 <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[David A. Wheeler]

On Sun, 12 Jul 2020 19:12:28 +0200, Giovanni Mascellani <g.masc...@gmail.com> 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

[Giovanni Mascellani]

Hi,

Il 12/07/20 19:28, David A. Wheeler ha scritto:

> Is your current plan to store them in:
> /usr/share/metamath-databases/
> ?

I would go for /usr/share/metamath/databases/, so that if in the future
metamath or other metamath-related programs have somthing to install, it
can go in /usr/share/metamath and only one direct child of /usr/share is
created for metamath.

>> 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.

Not a problem. This is just for me to know where to take the files from.
The string "develop" doesn't go anywhere relevant in the Debian package.

[Norman Megill]

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

[Giovanni Mascellani]

Hi,

Il 12/07/20 21:42, Norman Megill ha scritto:

> 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.

That looks like a good idea to me.

> 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).

Ok, thanks for the suggestions.

[Norman Megill]

hol.mm ql.mm demo0.mm miu.mm big-unifier.mm peano.mm have been added in PR 1722 https://github.com/metamath/set.mm/pull/1722
You or a volunteer can update these with the desired CC0 wording.  (I won't be doing that myself.)

Norm