Only distribute metamath sources via GitHub

[wlammen]

Norm used to distribute sources via his website http://us2.metamath.org:88/index.html (look for Downloads) as an archive file (tar). Having multiple distribution paths besides this GitHub repository requires extra effort on the maintainer's side. Are there any objections to make the GitHub repository the ONLY way to distribute sources?

While you are looking at the web page mentioned above, shall we get rid of other habits as well? For example: shall we provide metamath.pdf as part of the repository? Looking forward to your suggestions.

[benjub]

If there are objections to favoring GitHub distribution or making it exclusive, they will probably not be expressed here. Maybe launch a discussion on the google group as well ?

More generally, I don't have an idea of who uses/reads metamath besides the dozen regular contributors here. Who has ? Norm had a better idea through the logs to the website and the emails he received...

[jkingdon]

I support "I think we should move to a release process entirely hosted on github, with the web site pointing to the https://github.com/metamath/metamath-exe/releases page, which will be semi-automatically populated with releases built in CI." as suggested on the mailing list. (I mean, unless something else would be easier for the maintainers).

shall we provide metamath.pdf as part of the repository?

I guess I'd distribute it separately but I don't really have that much of an opinion one way or the other.

More generally, I don't have an idea of who uses/reads metamath besides the dozen regular contributors here.

Notoriously hard to keep tabs on people who try it out casually (I agree that web logs and to a lesser extent incoming emails can be clues) but as long as the current parts of the web site which say "download here" will still have a similarly prominent "Download" link I don't think we need to worry that we are making things worse.

[david-a-wheeler]

Before a final decision we should prototype having a release process entirely hosted on GitHub.

But if we can make it work well I'm in favor of it. No site is perfectly reliable, but GitHub is pretty reliable (it makes the news when it goes down).

The automake generated Makefile can easily create a tarball with configuration file ("make dist").

[david-a-wheeler]

I think metamath.pdf shouldn't be in this repo, since its source isn't (it's in the book repo). This repo should instead distribute hyperlinks to the various related materials like metamath.pdf.

[neunenak]

I recently discovered this project via Aaron Stump's type theory podcast: https://podcasts.apple.com/us/podcast/metamath/id1493036757?i=1000558478643 . I'm just checking it out now, but one thing that occurred to me is that it was somewhat difficult to find this github page from the metamath website. If people still have access to http://us.metamath.org, it would be good to make it clear that this github organization exists and explain what the difference is between the code hosted here and the code distributed as a tarball on that webpage.

[tirix]

Very nice to hear about the podcast!

@david-a-wheeler is managing the page and could modify it, you're at the right place for discussing the distribution channel.

I think the tarball stored on the site is version 0.198, while the version you'll find here has improvements added since last August.