Check set.mm LaTeX in CI pipeline (#3100)

* Check set.mm LaTeX in CI pipeline Generate a list of symbols in TeX format, then try to generate a PDF. This will check if every symbol is valid TeX. I don't expect this specific commit to succeed, but hopefully it'll help us see what's left to do. Signed-off-by: David A. Wheeler <[email protected]> * Install TeX before using it Signed-off-by: David A. Wheeler <[email protected]> * Add a package to load phonetic.sty Signed-off-by: David A. Wheeler <[email protected]> * Add LaTeX "accents" package from CTAN. Signed-off-by: David A. Wheeler <[email protected]> * Initialize tlmgr so we can use it to install LaTeX packages Signed-off-by: David A. Wheeler <[email protected]> * Install LaTeX package manually into ~/texmf Signed-off-by: David A. Wheeler <[email protected]> * Install "accents.sty" from Debian repo Signed-off-by: David A. Wheeler <[email protected]> * Make pdflatex check fail if something is "invalid" Signed-off-by: David A. Wheeler <[email protected]> * Fix misspelling of "grep" Signed-off-by: David A. Wheeler <[email protected]> * Change comments to be clear TeX -> LaTeX We really depend on LaTeX, not just TeX, so make that clear in the comments about verification. Signed-off-by: David A. Wheeler <[email protected]> * Fix grep of 'invalid' for LaTeX output Signed-off-by: David A. Wheeler <[email protected]> --------- Signed-off-by: David A. Wheeler <[email protected]>
metamath · Apr 24, 2023 · 3e6b9b8 · 3e6b9b8
1 parent 1830cc5
commit 3e6b9b8
Showing 1 changed file with 16 additions and 0 deletions.
diff --git a/.github/workflows/verifiers.yml b/.github/workflows/verifiers.yml
@@ -75,6 +75,17 @@ jobs:
     if: ${{ needs.skip_dups.outputs.should_skip != 'true' }}
     steps:
       - uses: actions/checkout@v3
+      # Install LaTeX so we can test generated LaTeX. We use extended packages:
+      # texlive-extra-utils provides pdflatex
+      # texlive-fonts-extra provides phonetic.sty
+      # texlive-science provides accents.sty
+      - run: sudo apt-get install texlive-latex-extra texlive-extra-utils texlive-fonts-extra texlive-science
+      # Here's an eXample of how to install "extra" LaTeX packages. See: 
+      # https://tex.stackexchange.com/questions/38978/how-can-i-manually-install-a-latex-package-debian-ubuntu-linux/39259#39259
+      # - run: mkdir -p "$HOME/texmf"
+      # - run: wget https://mirrors.ctan.org/macros/latex/contrib/accents.zip -o "$HOME/texmf/accents.zip"
+      # - run: cd "$HOME/texmf"; unzip -j accents.zip
+      # - run: texhash texmf
       # Use GITHUB_PATH to set PATH. For details see:
       # https://docs.github.com/en/free-pro-team@latest/actions/reference/
       # workflow-commands-for-github-actions#setting-an-environment-variable
@@ -129,6 +140,11 @@ jobs:
       # The following checks are arbitrarily included in the metamath job.
       - run: echo 'Looking for tabs (not allowed)...' && ! grep "$(printf '\t')" set.mm
       - run: echo 'Looking for tabs (not allowed)...' && ! grep "$(printf '\t')" iset.mm
+      # Check generated LaTeX, to ensure the TeX definitions are okay. set.mm:
+      - run: python3 scripts/latex_collector.py set.mm list-set.tex
+      - run: pdflatex -halt-on-error list-set.tex 2>&1 | tee ,latex-output
+      # Complain if the pdflatex output says something is invalid
+      - run: ! grep ' invalid ' ,latex-output
 
   ###########################################################
   smetamath-rs: