[bug#40815] gnu: Add metamath

[B. Wilson]

Well, after a good bit of wrangling, here is another round.

We have URLs pointing to static sources; I got upstream to fix things so we
don't need a patch; and now we're generating the doc output's pdf from the TeX
source.

The latter is what made this take so much time and effort.

On the one hand, it required packaging up 6 texlive dependencies, which are
included in the attached patches. On the other hand, it turns out that the
texlive-amsfonts package is broken, which we need to typset the metamath doc
output. This caused me tons of grief but turns out to be a known issue:

https://debbugs.gnu.org/cgi/bugreport.cgi?bug=40558

Thus, as of commit a1f84aca, the attached patch for metamath actually breaks.
However, with the proposed patched included in issue #40558 above, it builds
just fine.

Regarding the patches for the texlive packages, I did all of them as
simple-texlive-package templates with #:trivial? #t, grabbing the files from
tex/latex and doc/latex. Is this reasonable? Looking at other packages, I
cannot tell whether it'd be preferable to directly generate everything from the
*.dtx and *.sty sources.

Also, regarding texlive-mathstyle and texlive-flexisym, their files reside
under latex/breqn, but since they have their own ctan pages, I opted to split
them into separate packages and make the dependencies explicit. Does that seem
reasonable?

Anyway, thanks for taking a look! Hopefully, these look mergeable apart from
the texlive-amsfonts issue.

0001-gnu-Add-texlive-mathstyle.patch
Description: Text Data

0002-gnu-Add-texlive-flexisym.patch
Description: Text Data

0003-gnu-Add-texlive-breqn.patch
Description: Text Data

0004-gnu-Add-texlive-makecell.patch
Description: Text Data

0005-gnu-Add-texlive-microtype.patch
Description: Text Data

0006-gnu-Add-texlive-tabu.patch
Description: Text Data

0007-gnu-Add-metamath.patch
Description: Text Data

Jakub Kądziołka <address@hidden> wrote:
> On Mon, Apr 27, 2020 at 01:21:03PM +0900, address@hidden 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

signature.asc
Description: PGP signature