Metamath in Debian

[Giovanni Mascellani]

Hello,

this morning I made a Debian package for metamath and uploaded it to
Debian. The package is currently in the so-called NEW queue, where from
it will have to be manually approved before actually entering Debian
(this is a standard procedure for all new Debian packages).

Once approved, it will be available first in the development versions of
Debian (called "unstable" and "testing") and, unless a grave bug is
found that cannot be fixed (and I trust this won't happen), will be
released with the upcoming Debian bullseye. It won't be fast, Debian
release cycles are notoriously veeeery long (order of one or two years).
That means that users of Debian bullseye will be able to have metamath
ready for use just using the command "apt install metamath". In due time
(actually, probably earlier than in Debian) the same package will also
land in Ubuntu, as most Ubuntu packages are just inherited from Debian.

For the moment I just packaged the program, but I am going to build
another package with the most prominent databases, including of course
set.mm.

There is a kind request that I would like to make to Norman or to
anybody who manages the metamath-exe repository: could you please make
tags for Metamath releases? This makes it possible for Debian tools to
automatically detect when a new release is available and trigger a light
on my dashboard. This is as simple as using these commands each time you
want to publish a new release:

git commit -m'Release version 0.1234.'
git tag v0.1234
git push
git push --tags

The tags will be published on GitHub[1] and will be available for
automatically knowing which versions are available and how to get a
specific version.

[1] https://github.com/metamath/metamath-exe/releases

Thanks, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Benoit]

Hi Giovanni,

I am wondering: what are the advantages of having a Debian package over the current method ?  (This is a genuine, not a rhetorical question.)  I am using Debian testing, and everytime I want a new version of Metamath (and I generally want the newest), I download the zip from http://us2.metamath.org/#downloads, then I read the README.TXT because I always forget that the command is

  gcc m*.c -o metamath -O3 -funroll-loops -finline-functions -fomit-frame-pointer -Wall -pedantic -DINLINE=inline

then I type it, and I'm good to go.

I also added the intructions in the README.TXT file about how to install the man page, although I think MM>HELP is very handy.

Also, how is the package updated ?  I mean : you uploaded version 0.180 this morning to the Debian queue, so the version we will have in the stable Debian two years from now, will it be 0.180, whereas the version then will be, say, 0.192 ?

Thanks,

Benoît

[Giovanni Mascellani]

Hi,

Il 28/12/19 11:32, Benoit ha scritto:

> Hi Giovanni,
> I am wondering: what are the advantages of having a Debian package over
> the current method ?  (This is a genuine, not a rhetorical question.)  I
> am using Debian testing, and everytime I want a new version of Metamath
> (and I generally want the newest), I download the zip from
> http://us2.metamath.org/#downloads, then I read the README.TXT because I
> always forget that the command is
>   gcc m*.c -o metamath -O3 -funroll-loops -finline-functions
> -fomit-frame-pointer -Wall -pedantic -DINLINE=inline
> then I type it, and I'm good to go.

That's a lot of work already, compared to just "apt install metamath"
without having to check out any file. And you haven't even considered
the problem of understanding what to download: the GitHub repository?
The source distributed on the metamath website? What is the relationship
between the two? For you and me this is obvious, not so much for someone
discovering metamath for the first time.

Then, granted, metamath is probably a software for which the convenience
ratio between packaged and not packaged is relatively small. But any
user might be interested in many programs, and in order to keep all of
them up-to-date they have to do a specific manual process for each of
them (and sometimes this process might change because of changes in the
build system, dependencies or whatever). Compared to just "apt update;
apt upgrade" for all packages at once. I'd say that even for something
as straightforward as metamath there is no race. Think also for people
administrating lots of computers, for example in a university: if you
have metamath in Debian, you just add the name to the list of packages
that must be installed on each computer in your system management tool
(Puppet, Ansible, whatever). Otherwise you have to sort everything out
by yourself.

If a package is really special for you, because you are a developer or
such a power user that even being one commit behind master is an
impairment for you, then by all means ignore the packaged version and
compile your own. But for all other users, I believe there is nothing
like the distribution's official repositories.

It's not just a matter of convenience, but also of trust. Debian users
usually trust Debian packages: they know that most probably they will
just work, that they install files conforming to a well-known policy,
they know that if they uninstall the package then everything is just
gone. If you have to compile things yourself, you always need to check
manually of those things, if you care about keeping your filesystem clean.

> Also, how is the package updated ?  I mean : you uploaded version 0.180
> this morning to the Debian queue, so the version we will have in the
> stable Debian two years from now, will it be 0.180, whereas the version
> then will be, say, 0.192 ?

The version we will have in Debian bullseye when it will be released
will not (probably) be 0.180, but the last one that I uploaded before
bullseye enters its freeze stage. On the other hand, it is true that
that version will not be further updated during the bullseye life cycle:
Debian stable is meant to be stable (however, I will keep updating the
package in unstable and testing). This is what Debian users expect and
(hopefully) want. This is what happens for all other pieces of software
and it is perfectly normal.

If important bugs (like security bugs, or bugs that severely impact the
usability of the package) emerge after it has been released in Debian
stable, it is still possible to fix them with targeted patches. There
are dedicated repositories for that. But in that case we just fix the
important bug, not upload a completely new version. And the opportunity
to do this is carefully weighed against the risk of introducing new bugs
in working setups.

If a stable user really needs an updated version of a packaged software,
there is also another available channel, which is debian-backports. This
is not an official Debian distribution, but it is still endorsed by the
project, it upholds to the same Debian quality standards and is well
known and trusted by the users.

I think that all these options cover the needs of an important share of
users of most Debian packages. Again, metamath might be a bit of a
corner case because it is a simple software, with a rather targeted
users community. But given that the effort for me is so little, I
believe it is totally worth it.

BTW, most of what I say is probably true for any Linux distribution. I
am not saying that Debian is special. It just happens that I use and
contribute to it.

Hope this explains, Giovanni.

[Benoit]

Hope this explains

This explains very well, and you convinced me of the worthiness of the packaging.

Benoît

[heiph...@wilsonb.com]

Thank you for taking the time to craft such an extensive response!

I would also like to add that a distribution's packages also simply make
software more discoverable. There are times that the search function is my
initial foray into finding out about what software is available in a given
domain. For example, it would be nice if metamath showed up as a result when
searching for proof-related tooling.

Also, for whatever it is worth, I know of cases where people initially decided
to not pursue further research into metamath simply because it was not
packaged. There are comments to this effect in the PR attempting to introduce
metamath in my distribution's packages.

> --
> 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 metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c7213ef4-de9a-beab-eeab-0c9e60428c2f%40gmail.com.

[Giovanni Mascellani]

Il 28/12/19 13:44, heiphohmia via Metamath ha scritto:

> I would also like to add that a distribution's packages also simply make
> software more discoverable. There are times that the search function is my
> initial foray into finding out about what software is available in a given
> domain. For example, it would be nice if metamath showed up as a result when
> searching for proof-related tooling.

Yes, I wanted to write this in my reply, but then I forgot. Thanks for
bringing it up.

BTW, speaking of discoverability, here[1] is the package description
that I wrote for Debian. If anybody has improvements to suggest, please
let me know. The description text will appear in package managers and on
packages.debian.org when users browse the metamath package (this[2] is
what the Debian policy has to say on the description text).

[1]
https://ftp-master.debian.org/new/metamath_0.180-1.html#binary-metamath-control
[2]
https://www.debian.org/doc/debian-policy/ch-binary.html#the-description-of-a-package

Any other suggestion on the packaging work, especially by those actually
using it within Debian or any derivative, is welcome as well.

[Benoit]

For readers' convenience, here is the package description Giovanni wrote for Debian:

--------

Language for mathematical proofs Metamath is a tiny language for expressing theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. . This program is the reference implementation of the language. It provides a proof checker, a proof editor and tools to automatically render theorems and proofs to HTML and LaTeX files. . This package does not contain proof databases, but the tools to deal with them. The user can create their own databases, use those available on the Internet or provided by the metamath-databases package.

--------

Maybe replace "tiny" with "low-level", to be reminiscent of assembly languages?

I do not like the expression "abstract mathematics". I would simply write "...for expressing theorems and their proofs, that can be..."

Typo: "databases, use those" --> "databases or use those"

A period at the end of the first line?

The only important thing: remove "abstract mathematics". Reading this phrase always makes me suspicious about the person who wrote it!

Benoît

[David A. Wheeler]

I'm very glad that Metamath has been packaged for Debian
(and eventually Ubuntu), that will greatly simplify installing it.

On Sat, 28 Dec 2019 06:00:23 -0800 (PST), Benoit <benoit...@gmail.com> wrote:
> For readers' convenience, here is the package description Giovanni wrote
> for Debian:
> --------
>
> Language for mathematical proofs
> Metamath is a tiny language for expressing theorems in abstract
> mathematics, accompanied by proofs that can be verified by a computer
> program.
> .
> This program is the reference implementation of the language. It
> provides a proof checker, a proof editor and tools to automatically
> render theorems and proofs to HTML and LaTeX files.
> .
> This package does not contain proof databases, but the tools to deal
> with them. The user can create their own databases, use those
> available on the Internet or provided by the metamath-databases
> package.
>
> --------
> Maybe replace "tiny" with "low-level", to be reminiscent of assembly
> languages?

I disagree; I think that would be confusing.
"Low-level" may also imply "unable to do useful things", and
in any case very few people use assembly today while there are an increasing
number of people using Metamath. "Tiny" is better than "low-level".

> I do not like the expression "abstract mathematics".

Yes, removing "abstract" is probably a good idea.
We removed this sentence from the current Metamath book title and description.

I suggest replacing the first paragraph with one or more
of the sentences used to explain it in the *current* Metamath book per
http://www.lulu.com/us/en/shop/norman-megill-and-david-a-wheeler/metamath-a-computer-language-for-mathematical-proofs/hardcover/product-24129769.html

Here they are; I suggest using at least the first sentence, but the whole thing could be useful:

Metamath is a computer language and an associated computer program for archiving, verifying, and studying mathematical proofs. The Metamath language is simple and robust, with an almost total absence of hard-wired syntax, and we believe that it provides about the simplest possible framework that allows essentially all of mathematics to be expressed with absolute rigor. While simple, it is also powerful; the Metamath Proof Explorer (MPE) database has over 23,000 proven theorems and is one of the top systems in the “Formalizing 100 Theorems” challenge.

--- David A. Wheeler

[Norman Megill]

On Saturday, December 28, 2019 at 3:56:37 AM UTC-5, Giovanni Mascellani wrote:

on my dashboard. This is as simple as using these commands each time you
want to publish a new release:

  git commit -m'Release version 0.1234.'
  git tag v0.1234
  git push
  git push --tags

The tags will be published on GitHub[1] and will be available for
automatically knowing which versions are available and how to get a
specific version.

OK, I can add this to my release process for the metamath program source code.

Currently I am the only maintainer of the source code (m*,c,m*.h), and I don't publish intermediate versions of the program without incrementing the version number.  However, others may make small changes to configure.ac etc. that aren't related to the code and don't cause the version number to change.  Should these be re-tagged with the same version number?  Or not tagged at all, and just wait for the next real version?

 

[Giovanni Mascellani]

Hi,

Il 28/12/19 20:51, Norman Megill ha scritto:

> OK, I can add this to my release process for the metamath program source
> code.

Thank you!

> Currently I am the only maintainer of the source code (m*,c,m*.h), and I
> don't publish intermediate versions of the program without incrementing
> the version number.  However, others may make small changes to
> configure.ac etc. that aren't related to the code and don't cause the
> version number to change.  Should these be re-tagged with the same
> version number?  Or not tagged at all, and just wait for the next real
> version?

No, the only commits that get tagged are those that are meant to be
released versions. The other commits simply stay without tag.