Check set.mm LaTeX in CI pipeline

.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: