Subject: Re: gnu: Add metamath

From: Jakub Kądziołka <[email-masked]>
Date: Mon, 27 Apr 2020 14:12:48 +0200

On Mon, Apr 27, 2020 at 01:21:03PM +0900, [email-masked] wrote:
> > > +(define-public metamath
> > > +  (package
> > > +    (name "metamath")
> > > +    (version "0.182")
> > > +    (source
> > > +     (origin
> > > +       (method url-fetch)
> > > +       (uri "http://us2.metamath.org/downloads/metamath-program.zip")
> > 
> > This looks like an unversioned URL. That's not ideal, since when
> > upstream will release a new version, it will break the hash below. I
> > looked around on their website and couldn't find a versioned URL, but I
> > also couldn't find the one you're using. We could fetch from GitHub
> > instead...
> 
> This is a long story.
> 
> The official tar linked on upstream's homepage is also unversioned and gets
> updated daily via some automatic script. The reason being that they also
> provide snapshots of the databases from the set.mm repository.
> 
> To boot, the GitHub repository (https://github.com/metamath/metamath-exe) only
> contains a single, outdated release tar, which is simply a spurious byproduct
> of a prolonged discussion I had with upstream regarding the problems their
> release tars pose for package maintainers.

I notice, though, that the commits in the repository are up to date. We
could pin a specific commit ID. This practice is relatively common in
Guix and does not pose a problem.

Regards,
Jakub Kądziołka