Re: [Metamath] Packaging Metamath for Linux distros

[heiph...@wilsonb.com]

Hello Norm,

This is in reply to

https://groups.google.com/forum/#!searchin/metamath/Packaging$20Metamath$20for$20Linux%7Csort:date/metamath/z2kKJYgnz-g/xmRVy0KhCQAJ

For whatever reason my direct replies to the above seem to be falling into
Google's black hole, so I am sending this as a new thread:


At the risk of summoning a zombie from long dead discussion, let me bring this
issue up again.

I am attemtping to package metamath again, this time for Guix[0], and am
hitting a snag. The problem is that the `metamath-program.zip' link points to a
non-constant source, i.e. it changes every time metamath gets a version update.

Anyway, instead of blasting you with the nitty-gritty details this time, I have
a proposal. How about we git rid of `metamath-program.zip' altogether (which
URL I can no longer find on the home page, anyway) and instead let GitHub take
care of it for us?

Previously, at the 0.181 update Giovanni asked you to incant the following:

git commit -m'Release version 0.181.'
git tag v0.181
git push
git push --tags

It looks like this automatically created zip and tar archives for us on the
"release" page (https://github.com/metamath/metamath-exe/releases) with all the
properties that keep us package maintainers happy. Would it be reasonable to
include this git workflow into your process/script for version updates?


On a related note, the current repository ends up generating broken `install'
and `dist' make targets. The fix is quite simple, for which I submitted a pull
request: https://github.com/metamath/metamath-exe/pull/6. It simply removes the
refereces to the missing `*.mm' databases. Is this a reasonable thing to merge?

Cheers!


[0]:https://www.gnu.org/software/guix/

heiph...@wilsonb.com wrote:
> 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,
>
>
> "David A. Wheeler" <dwhe...@dwheeler.com> wrote:
>
> > 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
> >
> > --
> > 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.

----- End forwarded message -----

[Norman Megill]

metamath-program.zip has never been on the home page.  It was originally added so Travis could download just the program without being slowed down by unnecessarily including the .mm files, and it is still used for that.  Later it also become used for Linux distribution, and the compiled Windows version was removed.  Later I took it out of the site build script because the sha256 changed each time it was regenerated, so now I regenerate it by hand only whenever a new version of the metamath program is released.

However, I'm not really competent to decide what is needed.  If GitHub can take care of it that would be great, and I could then put it back into the site build script for Travis use.  It's currently one more thing I have to remember to do after updating the program (and I forgot to regenerate it last time which caused some problems but hopefully will remember in the future).

Norm

[Norman Megill]

On Monday, April 27, 2020 at 3:11:43 AM UTC-4, heiphohmia wrote:

...

>Previously, at the 0.181 update Giovanni asked you to incant the following:

    git commit -m'Release version 0.181.'
    git tag v0.181
    git push
    git push --tags

It looks like this automatically created zip and tar archives for us on the
"release" page (https://github.com/metamath/metamath-exe/releases) with all the
properties that keep us package maintainers happy. Would it be reasonable to
include this git workflow into your process/script for version updates?

I thought I had done that but maybe I forget that also or did something wrong.  I just did it again to be sure.

Norm

[David A. Wheeler]

> On Monday, April 27, 2020 at 3:11:43 AM UTC-4, heiphohmia wrote:
> ...
> >Previously, at the 0.181 update Giovanni asked you to incant the following:
> > git commit -m'Release version 0.181.'
> > git tag v0.181
> > git push
> > git push --tags

Yes, that will work just fine for tagging a version and distributing it via GitHub.
Lots of software is distributed this way. Then anyone can get, for example,
the source code of version 0.182 as a .tar.gz file via:
https://github.com/metamath/metamath-exe/archive/v0.182.tar.gz
It git parlance these are "lightweight tags" and should be fine for the purpose.

Once a particular source code version has a particular tag, that tag
should always refer to that specific version of the source code for all time.
You can modify the software, of course, just give the new version a new tag.
This is what the Linux distributions want: a URL that always gives exactly
the same version of the software. That way they can do rebuilds, etc.

If you forget to tag a release, you can add a tag to an old version this way:
git tag -a vWhATEVER SHA-OF-COMMIT
git push --tags

However... on GitHub "releases" and "tags" are related but not exactly the same thing.
Here's my attempt to de-confuse, and I've mis-stated something please let me know.
GitHub is one of many systems that build on git. Git has tags built-in.
GitHub has an *additional* concept called a "release"; that is GitHub-specific.
A "release" is intended for releasing binaries built from a tagged instance.
To create a release, you must first create a git *tag* of the source code
as described above. Then, to create a release, you identify the git tag, and
add whatever files you want (generally these are compiled executables, like
the compiled result from source code).

What confuses things further is that on GitHub, to see the list of tags OR releases,
you click on the little word "releases". You can then select between the tab
that lists tags, or the tab that lists releases. It's confusing.

The Linux distros don't want your prebuilt compiled code, just the source code,
so using git tags should be quite fine.

--- David A. Wheeler

[heiph...@wilsonb.com]

Norm, thank you for tagging v0.182 as well as merging the pull request.

I am getting the impression that this thread has mostly increased your
maintenance burden. That's really counter to my intent and needn't be the case!

The whole release process on the GitHub side can be made very automatic. It
could boil down to a single git command on your end that pushes a commit,
triggering Travis, which then publishes a tar release if everything checks out
or emailing you if Travis encounters a problem.

If this kind of thing sounds worthwhile, I would be willing to help set it up!

Cheers,


"David A. Wheeler" <dwhe...@dwheeler.com> wrote:

[David A. Wheeler]

On Tue, 28 Apr 2020 11:23:08 +0900, heiphohmia via Metamath <meta...@googlegroups.com> wrote:
> Norm, thank you for tagging v0.182 as well as merging the pull request.
> I am getting the impression that this thread has mostly increased your
> maintenance burden. That's really counter to my intent and needn't be the case!
>
> The whole release process on the GitHub side can be made very automatic.

Agreed.

I took a step in that direction. This pull request:
https://github.com/metamath/set.mm/pull/1615
modifies the current Travis build process so that it always pulls and uses
the Metamath source code with the newest tag.
Norm simply needs to use "git tag" to tag each Metamath release.

That doesn't create a full GitHub release, but it may be enough, and if a
full GitHub release is wanted this could be a step in that direction.

--- David A. Wheeler

[Norman Megill]

On Monday, April 27, 2020 at 10:46:41 PM UTC-4, David A. Wheeler wrote:

I don't have a problem adding a git tag for every release.  I can continue to do that.

David's mod now makes metamath-program.zip no longer needed on the Metamath site for Travis purposes.  It is somewhat inconvenient for me to hand-regenerate metamath-program.zip only after each release (rather than each website build) in order to maintain a stable sha256.  Does your (heiphohmia's) proposal to access GitHub directly eliminate the need for this file?

Norm

[heiph...@wilsonb.com]

Thank you, Norm. Yes, the GitHub tar achive is exactly what I need so will no longer be using metamath-program.zip. Looks like we can get rid of it!