Packaging Metamath for Linux distros

[heiph...@wilsonb.com]

Dear Metamath,

This outlines some of the issues I encounterd when attempting to package up
metamath for Void Linux. Need to make metamath more available!

The content here essentially reiterates that of a previous post of mine, which
just happened to go out right before the DNS debacle, causing it to fall
between the cracks, I believe.

Anyway, the primary issue with packaging up metamath is a lack of versioned
download URLs. The tar[0] on the main site appears to point at a source that
changes periodically. I assume this is to include updates to the set.mm and
other databases.

Unfortunately, this makes it particularly unfriendly for (Void) package
maintainers, as we need URLs that point to static content.

Perhaps a better packaging option would be to separate out the metamath
executable from the databases. Ideally, we could offer a package that includes
the executable along with a (wrapper?) script that lets users download and
update their local databases at will.

The only real hurdle to the latter option is that the metamath executable
repository doesn't seem to offer releases. As a workaround, package maintainers
could fork the repository and create releases themselves, but that has obvious
downfalls.

Is there much interest in this kind of issue?


[0]:http://us.metamath.org/downloads/metamath.tar.bz2

[Mario Carneiro]

Would it work for you to download the source? The metamath executable is versioned at https://github.com/metamath/metamath-exe , and the main library is at https://github.com/metamath/set.mm . I presume you have a method for handling github projects in Void Linux...?

I believe that Norm also keeps old versions of the tarball with names indexed by date, although I don't know if the dated copies include the most recent version or only start at the second most recent version. Norm will have to give the details on this.

Mario Carneiro

--
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/5df33749.SVDmi1t0L2Na3uit%25heiphohmia%40wilsonb.com.

[heiph...@wilsonb.com]

Thank you for the response.

> Would it work for you to download the source?

Unfortunately, no. Void Linux has a policy of only packing "stable" releases,
which in practice means no builds off repository branches and the like.
Upstream *might* accept a package off a git tag, but it looks like the
metamath-exe repository doesn't have those either.

> I believe that Norm also keeps old versions of the tarball...

This might work. My only concern would be with the frequency and
discoverability of updates. It looks like the metamath executable code is
stable, so does this mean that the tarball updates are only to include
snapshots of the set.mm repository?

If tarball updates are at all frequent, I would feel a bit bad about causing my
distro's build servers to recompile the same executable over and over just for
set.mm updates.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSv2qLXsobWJBJLGx3b-t1TLy7tk%3Dgx10f-9-xXzsNzLXg%40mail.gmail.com.

[Norman Megill]

On Friday, December 13, 2019 at 3:30:53 AM UTC-5, heiphohmia wilsonb.com wrote:

Thank you for the response.

> Would it work for you to download the source?

Unfortunately, no. Void Linux has a policy of only packing "stable" releases,
which in practice means no builds off repository branches and the like.
Upstream *might* accept a package off a git tag, but it looks like the
metamath-exe repository doesn't have those either.

The metamath program source without databases is available at http://us.metamath.org/downloads/metamath-program.zip (0.7MB). It is not yet documented because it was originally intended for the GitHub Travis runs, but I will make it "official" and add it to the downloads section on the home page.

It is relatively stable in that it changes only when I release a new numbered version of the metamath program (currently 0.180).  A history at the top of metamath.c shows how often releases have been made.  The zip file also includes configure.ac, Makefile.am, metamath.1 (man page), and a Windows executable metamath.exe.

Norm

[fl]

And why not a special Linux source distribution, a gzipped tarball, without Windows executable, 

without database, but with the manual page, the TeX file of the manual, the Makefile, a configure.ac, 

and a "configure" program. In short, the standard source distribution for Linux like the tar.gz on this page:

https://github.com/coq/coq/releases/tag/V8.10.2

With a static link so that special distributions packagers can easily find it. And also tips on finding 

the associated database and a procedure to recreate it on a personal computer with a warning message 

to explain to the reckless user that it will take a very long time to get it and that s.he might prefer using the

already compiled one on the net.

-- 

FL

[heiph...@wilsonb.com]

Thank you. That definitely ticks all the boxes. I will get this packaged up and
share the result once it is published.

> --
> 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/497b5669-8f7f-4dba-9889-a06dd9548da2%40googlegroups.com.

[heiph...@wilsonb.com]

> And why not a special Linux source distribution...

The URL that Norm shared pretty much ticks all the boxes you outline. The only
substantive difference being that the metamath.exe is not excluded.

The source uses GNU autotools, so the standard build procedure Just Works if
you first generate the necessary files with

$ autoreconf -i

I do find it curious that the advice for *nix builds is to directly call gcc.
Perhaps the build instructions could be updated to this:

$ autoreconf -i && configure && make

The TeX source for the metamath book is located here[0]. Said URL is already
prominently on the homepage, and I

[0]:http://us.metamath.org/latex/metamath.tex

> And also tips on finding the associated database and a procedure to recreate

> it on a personal computer...

This reads to me like it is suggesting users generate set.mm. Since that
doesn't really make sense, I assume that I am just misreading something.

> --
> 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/7fba4251-4fe3-4578-b103-8c07f29dcf76%40googlegroups.com.

[fl]

> And why not a special Linux source distribution...

The URL that Norm shared pretty much ticks all the boxes you outline. The only
substantive difference being that the metamath.exe is not excluded.

I know perfectly well that the package currently available is perfectly usable. I simply point out that as long as you are dealing with linux distributions, the easiest way is to respect the standards specific to Linux source distributions: a configure (already generated by autoreconf) a README, an INSTALL, a Makefile. Everything that a person who installs a source on Linux expects to find. And no Windows hardware (we don't put the devil in the church!)

 

The source uses GNU autotools, so the standard build procedure Just Works if
you first generate the necessary files with

    $ autoreconf -i

I do find it curious that the advice for *nix builds is to directly call gcc.
Perhaps the build instructions could be updated to this:

    $ autoreconf -i && configure && make

It should be uptated to that:

configure && make && make install

 

The TeX source for the metamath book is located here[0]. Said URL is already
prominently on the homepage, and I

[0]:http://us.metamath.org/latex/metamath.tex

Okay, but I just want to point out that, if we' re going to do anything, we might as well put the TeX file in the source distribution. Documentation is always part of the source documentation.

 

This reads to me like it is suggesting users generate set.mm. Since that
doesn't really make sense, I assume that I am just misreading something.

It makes sense. Not everyone is connected 24 hours a day to the Internet. You may prefer that your computer is not likely to be hacked by smart people. Knuth never puts his computers on the Internet.

You may also want to have several successive states of the database. I must have half a dozen of them installed on my computer.

You may prefer to stay offline to cure your Internet addiction. 

You may want to think about the planet and relieve the network. The Internet consumes as much energy as aeronautics because of all the advertising and netflix crap that goes through it.

-- 

FL

[David A. Wheeler]

On December 16, 2019 8:33:44 AM EST, heiphohmia via Metamath

>The source uses GNU autotools, so the standard build procedure Just
>Works if
>you first generate the necessary files with
>
> $ autoreconf -i
>
>I do find it curious that the advice for *nix builds is to directly
>call gcc.
>Perhaps the build instructions could be updated to this:
>
> $ autoreconf -i && configure && make

That should certainly also be in the instructions. That said, some people do not have working autotools setups, so invoking GCC is simpler for some.

If you are creating a Linux package you should definitely use the autotools via autoreconf. The resulting metamath executable will be more optimized, resulting in some faster operations.

--- David A.Wheeler

[fl]

The configure is already generated in a source distribution. No autoreconf has to be done in a source distribution. Perhaps for the good reason

that the autotools on the end user's computer.

 

-- 

FL

[Norman Megill]

On Monday, December 16, 2019 at 8:34:02 AM UTC-5, heiphohmia at wilsonb.com wrote:

> And why not a special Linux source distribution...

The URL that Norm shared pretty much ticks all the boxes you outline. The only
substantive difference being that the metamath.exe is not excluded.

I could take it out if that is preferable.  I left it in in case a Windows user (who typically has no C compiler) wanted to download just the program and sources, although there is also a direct link to metamath.exe on the home page so it isn't really necessary.

Maybe you can let me know exactly what files you'd like to see in it.
 

The source uses GNU autotools, so the standard build procedure Just Works if
you first generate the necessary files with

    $ autoreconf -i

I do find it curious that the advice for *nix builds is to directly call gcc.
Perhaps the build instructions could be updated to this:

    $ autoreconf -i && configure && make

I could add this as an alternate build method, but these are Linux/Unix-specific and may not be available on all systems. The program is very portable and purposely calls no external libraries or does anything that isn't strictly part of ANSI C, with the only exception AFAIK that it doesn't support the EBCDIC character set.

(Personally I mostly use lcc during development because it compiles much faster than gcc, and occasionally use gcc for its better error messages and faster run time.  Also, autotools is painfully slow, issues screenfuls of messages I have to scroll through to find a real error, and clutters up the directory with dozens of unwanted files, making development annoying and inefficient.  Am I doing something wrong, and how do most people deal with this?)

I just tried to run autoreconf -i && configure && make, and it doesn't work with metamath-programs.zip because it presupposes the databases are there.  I'm not really that confident with autotools, and it would be best if someone else adjusts them.

Norm

[fl]

I do find it curious that the advice for *nix builds is to directly call gcc.
Perhaps the build instructions could be updated to this:

    $ autoreconf -i && configure && make

I could add this as an alternate build method, but these are Linux/Unix-specific and may not be available on all systems. The program is very portable and purposely calls no external libraries or does anything that isn't strictly part of ANSI C, with the only exception AFAIK that it doesn't support the EBCDIC character set.

A call to autoreconf doesn't belong to a standard source package. The file "configure" must have already been generated.

 

-- 

FL

[David A. Wheeler]

>I could add this as an alternate build method, but these are
>Linux/Unix-specific and may not be available on all systems.

The generated configure file from autotools should work on absolutely every system except windows.

> The
>program is
>very portable and purposely calls no external libraries or does
>anything
>that isn't strictly part of ANSI C

That's true, but if you allow the system to detect various settings the resulting executable is much faster.

>I'm not really that confident with autotools, and it would be best if
>someone else adjusts them.

I'm confident with them. Unfortunately I'm busy elsewhere right now, but I would be happy to resolve these issues once I have a little more time.

You don't really need to run autoreconf all the time. That forces a regeneration of everything. But again, I will help more once I get a chance.


--- David A.Wheeler

[fl]

You may want to think about the planet and relieve the network. The Internet consumes as much energy as aeronautics because of all the advertising and netflix crap that goes through it.

And the plane traffic it is that:

https://flight-radar.eu/fr/suivi-des-vols-en-temps-reel/

Terrifying.

-- 

FL

[heiph...@wilsonb.com]

> Maybe you can let me know exactly what files you'd like to see in it.

Thank you for engaging so openly.

Personally, my preferences align mostly with FL's. As a Linux user, the default
expectation I have for a source tarball (in this case metamath-program.zip) is
that I can do

$ ./configure && make install

and it Just Works (modulo concerns about external dependencies). To get this
working we just need to patch Makefile.am like this:

*** a/Makefile.am 2019-12-17 15:32:41.797498961 +0900
--- b/Makefile.am 2019-12-17 15:33:22.713276422 +0900
*************** metamath_SOURCES = \
*** 36,49 ****
mmwtex.c \
$(noinst_HEADERS)

- dist_pkgdata_DATA = \
- big-unifier.mm \
- demo0.mm \
- miu.mm \
- peano.mm \
- ql.mm \
- set.mm
-

EXTRA_DIST = \
LICENS@

followed by running

$ autoreconf -i

That should produce a source bundle that builds "as normal." If we really want
to make things look like bog standard *nix sysops, then I second FL's
suggestions:

1. Remove the metemath.exe executable,
2. Provide as a tar.bz2 instead of a zip, and
3. Include the Metamath book TeX source.

The only hanging thread is how to acquire the databases. The easiest solution
here is probably to just leave this detail to the package maintainers and/or
users. It might be nice to include a README in the tarball, explaining what the
source includes and what it does not.

On my own machine, I just clone the set.mm repo locally, set the environment
variable METAMATH_DIR pointing there, and then a wrapper shell function
provides easy loading of databases, automatic sizing, rlwrap, etc:

mm() {(
usage=$(cat <<-USAGE
Usage: mm [-hl] [-d <database>] [-r <rcfile>] [<args>]

OPTIONS
-d <database> Load <database>
-r <rcfile> Submit <rcfile> commands on startup, defaults to ~/.metamathrc
-l List available databases
-h Display this help message
USAGE
)

while getopts ':d:r:hl' opt "${@}"; do
case "${opt}" in
d) db="${OPTARG}";;
r) rc="${OPTARG}";;
l) find "${METAMATH_DIR}" -name '*.mm'; exit;;
h) >&2 echo "${usage}"; return 0;;
:) error "Expected argument: -${OPTARG}" "${usage}"
return 1;;
*) error "Unknown argument: -${OPTARG}" "${usage}"
return 1;;
esac
done
shift $((OPTIND - 1))

rc="${rc:-${HOME}/.metamathrc}"
[ -r "${rc}" ] || unset rc

rlwrap --complete-filenames \
metamath "set width $COLUMNS" \
"set height $((LINES - 1))" \
${rc+"submit '${rc}'"} \
${db+"read '${METAMATH_DIR}/${db}'"} \
"${@}"
)}

The only missing piece that I currently want is a nice rlwrap perl script that
provides context-aware completion. Otherwise, I find the metamath executable
itself quite ergonomic!

> --
> 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/8c5bd45d-5b88-4507-a2ba-0d89d154c0d8%40googlegroups.com.

[Giovanni Mascellani]

Hi,

Il 16/12/19 19:05, David A. Wheeler ha scritto:

>> The
>> program is
>> very portable and purposely calls no external libraries or does
>> anything
>> that isn't strictly part of ANSI C
>
> That's true, but if you allow the system to detect various settings the resulting executable is much faster.

Are you sure? Why should a program that just depends on the standard
library be faster with autotools? In particular, how would autotools
change anything in how the program is compiled or ran?

(BTW, I personally don't like autotools very much, as they encourage
mixing hand-written and generated code; since I don't think they give an
important advantage when you don't depend on non-standard libraries, I
would suggest to not use them for Metamath)

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

[David A. Wheeler]

On December 17, 2019 11:46:21 AM EST, Giovanni Mascellani <g.masc...@gmail.com> wrote:
>Hi,
>
>Il 16/12/19 19:05, David A. Wheeler ha scritto:
>>> The
>>> program is
>>> very portable and purposely calls no external libraries or does
>>> anything
>>> that isn't strictly part of ANSI C
>>
>> That's true, but if you allow the system to detect various settings
>the resulting executable is much faster.
>
>Are you sure? Why should a program that just depends on the standard
>library be faster with autotools? In particular, how would autotools
>change anything in how the program is compiled or ran?

Yes, I measured a 20% improvement in metamath performance when compiled with the autotools. There are actually a large number of changes because the autotools detects the optimal way to invoke the compiler. It turns on various optimizations that make a difference.



--- David A.Wheeler

[fl]

That's true, but if you allow the system to detect various settings the resulting executable is much faster.

Just so we understand each other. I am completely convinced of the usefulness of "autotools". And your performance measures prove it. But I maintain that the use of "autoreconf" is the packager's responsibility. The user should only use "configure".  And anyway between "autoreconf" and "configure" I have no idea which of the two optimizes the compiler options.

--
FL

[David A. Wheeler]

>Just so we understand each other. I am completely convinced of the
>usefulness of "autotools". And your performance measures prove it. But
>I
>maintain that the use of "autoreconf" is the packager's responsibility.
>The
>user should only use "configure".

That is certainly the ideal. Autoreconf merely generates the file configure. However, directly using "configure" (as is commonly done with most software) would require that Norm commit to running autoreconf himself when certain changes are made, and then include that generated configure. That commitment would be necessary to ensure that the distributed configure file is up-to-date. But Norm typically does not use autoconf at all. If people run autoreconf themselves, to generate their own configure file, then they can be more confident that the generated configure file works for the current software, and Norm doesn't have run autoreconf himself.

I think we can revisit and improve things, but whatever build and distribution process changes are made needs to be something that Norm is willing to accept. Norm has limited time and his own preferences.

> And anyway between "autoreconf" and
>"configure" I have no idea which of the two optimizes the compiler options.

It is actually configure, not autoreconf, that does the optimizations.




--- David A.Wheeler

[David A. Wheeler]

Just a quick follow-up, I created a three-part YouTube video on how to use the auto tools. The auto tools are still one of the most common ways to distribute C source programs on unix-like systems, including Linux. The first part is especially useful if you just want to get an idea of what these tools do. Here is the link:

https://m.youtube.com/watch?v=4q_inV9M_us
--- David A.Wheeler

[fl]

I think we can revisit and improve things, but whatever build and distribution process changes are made needs to be something that Norm is willing to accept. Norm has limited time and his own preferences.

Why does he let people waste their time talking if he knows he doesn't want it ?

--

FL

[fl]

https://m.youtube.com/watch?v=4q_inV9M_us

I have just looked at it. Well, that's good.

--

FL

[David A. Wheeler]

David A. Wheeler:

> > I think we can revisit and improve things, but whatever build and
> > distribution process changes are made needs to be something that Norm is
> > willing to accept. Norm has limited time and his own preferences.

On Fri, 20 Dec 2019 04:52:22 -0800 (PST), "'fl' via Metamath":

> Why does he let people waste their time talking if he knows he doesn't want
> it ?

It's not a waste of time.

Norm is happy to let *other* people use the autotools. After all,
using the autotools typically produces a Metamath executable with significantly
higher performance for certain operations.

However, Norm prefers using his own tools & doesn't use the autotools *himself*,
at least not at this time.

So the compromise has been for Norm to use whatever tools he wants, and Norm
simply includes various autotools files like configure.ac in the Metamath release.
That makes it *possible* for recipients to use the autotools.
Since Norm doesn't run the autotools himself, recipients can't be guaranteed that the
"configure" file is up-to-date. Instead, recipients who want to use the autotools
have to run "autoreconf" themselves to *generate* the configure file, and then use
the configure file as usual to do the rest of the build.

Yes, this is more steps than usual. However,
this is not completely unknown. You also have to do this extra step with some
GNU packages if you download a development version instead of an actual release.
It is unusual for *released* software. Typically *releases* of software that
support the autotools include a pre-generated configure file that was created by
the autotools as part of the process for creating a release.
But doing that would require Norm to install & run the autotools.
Norm might be willing to do that now, but he didn't want to do that in
the past & that change is up to him.

I'd be happy to modify the autotools files (e.g., configure.ac) to change things.
I just got back from a trip to Florida, & Christmas is coming, but once things get
a little quieter I'd be happy to help. I would just need to know what changes
need to be made.

--- David A. Wheeler

[heiph...@wilsonb.com]

Thank you, Dr. Wheeler, for sharing all this context with us.

For whatever it is worth, I am personally, quite happy with the URL that Norm
made public for us. It makes packaging *possible* which is huge.

FL's suggestions seem reasonable to me if the goal is to minimize friction for
package maintainers; however, if this poses problems/inconvenience upstream as
you suggest, then how about compromise with a README in the
metamath-program.zip for now? At a bare minimim, it might be nice to explain
the (mildly non-standard) compilation procedure, as well as link to the set.mm
repo.

I am currently holding off on submitting a packing to Void Linux until it
becomes clear what exactly source bundle we want Metamath to provide.

As a side note, what are thoughts on the idea of also providing a shell script
wrapper "codifies" things like downloading, updating, listing etc the *.mm
databases? This might make packaging more of a simple turn-key solution, so
that metamath installs files to more standard filesystem locations. I certainly
would not mind writing such a script, which would likely turn out a lot like
the one I shared in a previous post here.

Cheers,

> --
> 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/E1iiRY9-0007E6-Vq%40rmmprod07.runbox.