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

On Fri, Dec 13, 2019 at 2:01 AM heiphohmia via Metamath <
[email protected]> wrote:

> 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
>
> --
> 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 [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/5df33749.SVDmi1t0L2Na3uit%25heiphohmia%40wilsonb.com
> .
>

-- 
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 [email protected].
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CAFXXJSv2qLXsobWJBJLGx3b-t1TLy7tk%3Dgx10f-9-xXzsNzLXg%40mail.gmail.com.

Reply via email to