Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[nomerge] New package: metamath-0.178 #15721

Closed
wants to merge 1 commit into from

Conversation

xelxebar
Copy link
Contributor

No description provided.

@xelxebar
Copy link
Contributor Author

xelxebar commented Oct 23, 2019

Oh boy. It looks like upstream's url to the source is getting ninja edited.
The proofs database is packaged together with the verifier, so I assume that upstream is retarring the source with updated databases while the verifier itself remains unchanged. Hence, the public version number and url remain the same, but the actual tar these point to is fluid.

@leahneukirchen
Copy link
Member

Changing tarballs are bad for us, they break rebuilds. Perhaps instead use githashes and assemble the repo yourself?

@Piraty
Copy link
Member

Piraty commented Nov 7, 2019

in case the exact same contents get repackaged, you could prepend @ do the checksum, see Manual.md

@xelxebar
Copy link
Contributor Author

Thanks @leahneukirchen and @Piraty. Unfortunately, the tar contents are changing. There are "source" files that the "interpreter" reads, and it is these "source" files that are getting periodically updated and refreshed in the tar.

Instead of rolling forking upstream and packaging, I am just talking to them directly. Apparently, Debian is also interested in packaging this up, so making upstream friendly to package managers seems like a good approach.

Unless someone objects, I will just leave this pull request alone until we get something situated upstream.

@Piraty Piraty changed the title New package: metamath-0.178 [nomerge] New package: metamath-0.178 Nov 13, 2019
@xelxebar xelxebar closed this Jan 27, 2020
@xelxebar xelxebar deleted the package/metamath branch January 27, 2020 15:19
@github-actions github-actions bot locked as resolved and limited conversation to collaborators Dec 12, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants