From 8dc9347d507a734aeef7e5add96928bf7dc4de84 Mon Sep 17 00:00:00 2001 From: "B. Wilson" Date: Mon, 17 Jan 2022 19:17:05 +0900 Subject: [PATCH] WIP: gnu: Typset PDF documentation for metamath. To: bug-guix@gnu.org * gnu/packages/metamath.scm (metamath): Add build definition for docs. * gnu/packages/tex.scm (texlive-mathstyle, texlive-flexisym): New variables. (texlive-breqn, texlive-makecell, texlive-tabu): New variables. --- gnu/packages/maths.scm | 78 +++++++++++++++++++----- gnu/packages/tex.scm | 132 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 194 insertions(+), 16 deletions(-) diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm index b0944f307b..378237f472 100644 --- a/gnu/packages/maths.scm +++ b/gnu/packages/maths.scm @@ -38,7 +38,7 @@ ;;; Copyright © 2020 R Veera Kumar ;;; Copyright © 2020 Vincent Legoll ;;; Copyright © 2020 Nicolò Balzarotti -;;; Copyright © 2020 B. Wilson +;;; Copyright © 2020, 2022 B. Wilson ;;; Copyright © 2020, 2021 Vinicius Monego ;;; Copyright © 2020 Simon Tournier ;;; Copyright © 2020 Martin Becze @@ -3360,30 +3360,76 @@ (define-public python-slepc4py (define-public metamath (package (name "metamath") - (version "0.193") + (version "0.196") (source (origin (method git-fetch) (uri (git-reference - (url "https://github.com/metamath/metamath-exe") + (url "https://github.com/metamath/metamath-exe.git") (commit (string-append "v" version)))) - (file-name (git-file-name name version)) (sha256 - (base32 "1s9hyknfvhj86g3giayyf3dxzg23iij0rs7bdvj075v9qbyhqn9b")))) + (base32 "1i9x9rg7lxs0qrf2fv4cqczd8v9l1cxp6h0hdmdlr5dvzbjwg1zy")) + (file-name (git-file-name name version)))) (build-system gnu-build-system) - (native-inputs - (list autoconf automake)) + (inputs + `(("book" + ,(origin + (method url-fetch) + (uri (string-append "https://github.com/metamath/" + "metamath-book/archive/second_edition.tar.gz")) + (sha256 + (base32 + "1kbgajik9dn870db1zslqyvhn2j8g7shb8d6dm6njwqfkygiliir")))))) + (native-inputs `(("autoconf" ,autoconf) + ("automake" ,automake) + ("texlive" ,(texlive-updmap.cfg + (list texlive-amsfonts + texlive-bibtex + texlive-breqn + texlive-fonts-ec + texlive-hyperref + texlive-latex-anysize + texlive-latex-needspace + texlive-latex-tools + texlive-makecell + texlive-microtype + texlive-tabu))))) + (outputs '("out" "doc")) + (arguments + `(#:phases + (let ((book-builddir "metamath-book-second_edition")) + (modify-phases %standard-phases + (add-after 'unpack 'unpack-doc + (lambda* (#:key inputs #:allow-other-keys) + (let ((book-tar (assoc-ref inputs "book"))) + (invoke "tar" "xzf" book-tar)))) + (add-after 'build 'build-doc + (lambda _ + (with-directory-excursion book-builddir + (invoke "touch" "metamath.ind") + (invoke "pdflatex" "metamath") + (invoke "pdflatex" "metamath") + (invoke "bibtex" "metamath") + (invoke "makeindex" "metamath") + (invoke "pdflatex" "metamath") + (invoke "pdflatex" "metamath")))) + (add-after 'build-doc 'install-doc + (lambda* (#:key outputs #:allow-other-keys) + (let* ((pkg (strip-store-file-name (assoc-ref outputs "out"))) + (out-doc (assoc-ref outputs "doc"))) + (install-file (string-append book-builddir "/metamath.pdf") + (string-append out-doc "/share/doc/" pkg)) + #t))))))) (home-page "http://us.metamath.org/") (synopsis "Proof verifier based on a minimalistic formalism") - (description - "Metamath is a tiny formal language and that can express theorems in -abstract mathematics, with an accompyaning @command{metamath} executable that -verifies databases of these proofs. There is a public database, -@url{https://github.com/metamath/set.mm, set.mm}, implementing first-order -logic and Zermelo-Frenkel set theory with Choice, along with a large swath of -associated, high-level theorems, e.g.@: the fundamental theorem of arithmetic, -the Cauchy-Schwarz inequality, Stirling's formula, etc. See the Metamath -book.") + (description "Metamath is a tiny formal language and that can express +theorems in abstract mathematics, with an accompyaning @code{metamath} +executable that verifies databases of these proofs. There is a public +database, @url{https://github.com/metamath/set.mm, set.mm}, implementing +first-order logic and Zermelo-Frenkel set theory with Choice, along with a +large swath of associated, high-level theorems (e.g. the Fundamental Theorem of +Arithmetic, the Cauchy-Schwarz Inequality, or Striling's Formula). For more +details see the Metamath book provided in the @code{doc} output.") (license license:gpl2+))) (define-public minizinc diff --git a/gnu/packages/tex.scm b/gnu/packages/tex.scm index bd4c2461a2..12f69f7686 100644 --- a/gnu/packages/tex.scm +++ b/gnu/packages/tex.scm @@ -20,6 +20,7 @@ ;;; Copyright © 2021 Ivan Gankevich ;;; Copyright © 2021 Julien Lepiller ;;; Copyright © 2021 Thiago Jung Bauermann +;;; Copyright © 2022 B. Wilson ;;; ;;; This file is part of GNU Guix. ;;; @@ -9816,3 +9817,134 @@ (define-public bibtool sorting and merging of BibTeX databases, generation of uniform reference keys, and selecting references used in a publication.") (license license:gpl2+))) + +(define-public texlive-mathstyle + (package + (inherit (simple-texlive-package + "texlive-mathstyle" + (list "/tex/latex/breqn/mathstyle.sty" + "/doc/latex/breqn/mathstyle.pdf") + (base32 "0rqdbcigj0ipjq19j8rk7whcr5j33rvr6fxchvycnrnsv5i5hvrg") + #:trivial? #t)) + (propagated-inputs `(("texlive-latex-l3kernel" ,texlive-latex-l3kernel))) + (home-page "https://www.ctan.org/pkg/mathstyle") + (synopsis "Manage mathematics typesetting style") + (description "Flexisym converts mathematical symbol definitions to the form +they need for breqn to work. The package offers support for breqn and is part +of the bundle of the same name.") + (license license:lppl1.3c+))) + +(define-public texlive-flexisym + (package + (inherit (simple-texlive-package + "texlive-flexisym" + (list "/tex/latex/breqn/flexisym.sty" + "/tex/latex/breqn/cmbase.sym" + "/tex/latex/breqn/mathpazo.sym" + "/tex/latex/breqn/mathptmx.sym" + "/tex/latex/breqn/msabm.sym") + (base32 "0wba8fa9zffldpybwyzha3bxfhxyjpnxl22vvlga6hz2yyrlshjy") + #:trivial? #t)) + (propagated-inputs `(("texlive-latex-l3kernel" ,texlive-latex-l3kernel) + ("texlive-mathstyle" ,texlive-mathstyle))) + (home-page "https://www.ctan.org/pkg/flexisym") + (synopsis "Symbol manipulation for breqn") + (description "Flexisym converts mathematical symbol definitions to the form +they need for breqn to work. The package offers support for breqn and is part +of the bundle of the same name.") + (license license:lppl1.3c+))) + +(define-public texlive-breqn + (package + (inherit (simple-texlive-package + "texlive-breqn" + (list "/tex/latex/breqn/breqn.sty") + (base32 "000hf8sh41y197qj414fng88ig6b48zz5bd24n40z6wshh07qa4x") + #:trivial? #t)) + (propagated-inputs `(("texlive-latex-amsmath" ,texlive-latex-amsmath) + ("texlive-flexisym" ,texlive-flexisym) + ("texlive-latex-graphics" ,texlive-latex-graphics) + ("texlive-latex-l3kernel" ,texlive-latex-l3kernel) + ("texlive-latex-tools" ,texlive-latex-tools))) + (home-page "http://wspr.io/breqn/") + (synopsis "Automated line breaking of displayed equations") + (description "The package provides solutions to a number of common +difficulties in writing displayed equations and getting high-quality output. +For example, it is a well-known inconvenience that if an equation must be +broken into more than one line, @code{left...right} constructs cannot span +lines. The breqn package makes them work as one would expect whether or not +there is an intervening line break. The single most ambitious goal of the +package, however, is to support automatic linebreaking of displayed equations. +Such linebreaking cannot be done without substantial changes under the hood in +the way formulae are processed; the code must be watched carefully, keeping an +eye on possible glitches. The bundle also contains the flexisym and mathstyle +packages, which are both designated as support for breqn.") + (license license:lppl1.3c+))) + +(define-public texlive-makecell + (package + (inherit (simple-texlive-package + "texlive-makecell" + (list "/tex/latex/makecell/" + "/doc/latex/makecell/makecell.pdf") + (base32 "1zdcmya5dxrnjf7lf0wmnhcjlwdha5gdzdx7xrgyi61gqwj7cxin") + #:trivial? #t)) + (propagated-inputs `(("texlive-latex-tools" ,texlive-latex-tools))) + (home-page "https://www.ctan.org/pkg/makecell") + (synopsis "Tabular column heads and multilined cells") + (description "This package supports common layouts for tabular column heads +in whole documents, based on one-column tabular environment. In addition, it +can create multi-lined tabular cells. + +The Package also offers: + +@itemize +@item a macro which changes the vertical space around all the cells in a + tabular environment (similar to the function of the tabls package, but + using the facilities of the array); +@item macros for multirow cells, which use the facilities of the multirow + package; +@item macros to number rows in tables, or to skip cells; +@item diagonally divided cells; +@item horizontal lines in tabular environments with defined thickness. +@end itemize") + (license license:lppl))) + +(define-public texlive-tabu + (package + (inherit (simple-texlive-package + "texlive-tabu" + (list "/tex/latex/tabu/" + "/doc/latex/tabu/") + (base32 "156lkisyrpvn82ng2kxdlly60ny5vaz4lp9xlc66azy5ma06agvw") + #:trivial? #t)) + (propagated-inputs + `(("texlive-latex-tools" ,texlive-latex-tools) + ("texlive-latex-varwidth" ,texlive-latex-varwidth))) + (home-page "https://www.ctan.org/pkg/tabu") + (synopsis "Flexible LaTeX tabulars") + (description "The package provides an environment, @code{tabu}, which will +make any sort of tabular (that doesn’t need to split across pages), and an +environment @code{longtabu} which provides the facilities of @code{tabu} in a +modified longtable environment. (Note that this latter offers an enhancement +of ltxtable.) + +The package requires the array package, and needs e-TeX to run (since array.sty +is present in every conforming distribution of LaTeX, and since every publicly +available LaTeX format is built using e-TeX, the requirements are provided by +default on any reasonable system). The package also requires xcolor for +coloured rules in tables, and colortbl for coloured cells. The @code{longtabu} +environment further requires that longtable be loaded. The package itself does +not load any of these packages for the user. + +The @code{tabu} environment may be used in place of @code{tabular}, +@code{tabular*} and @code{tabularx} environments, as well as the @code{array} +environment in maths mode. It overloads @code{tabularx}’s X-column +specification, allowing a width specification, alignment (@code{l}, @code{r}, +@code{c} and @code{j}) and column type indication (@code{p}, @code{m} and +@code{b}). + +@code{\begin@{tabu@}} to @code{} specifies a target width, and +@code{\begin@{tabu@}} spread @code{} enlarges the environment’s +natural width.") + (license license:lppl1.3c+))) -- 2.34.0