Attempt to build DafnyRef using Tectonic (#5056)

We've frequently had trouble building `DafnyRef.pdf` because installing TeXLive fails in some way. This updates the build to use Tectonic, instead. It downloads less data to install, and has better version-pinning support. By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
dafny-lang · Feb 6, 2024 · 8e0682e · 8e0682e
1 parent b3b5b23
commit 8e0682e
Show file tree

Hide file tree

Showing 3 changed files with 17 additions and 30 deletions.
diff --git a/.github/workflows/publish-release-reusable.yml b/.github/workflows/publish-release-reusable.yml
@@ -98,33 +98,29 @@ jobs:
       # version.
       run: dotnet nuget push --skip-duplicate "dafny/Binaries/Dafny*.nupkg" -k ${{ secrets.NUGET_API_KEY }} -s https://api.nuget.org/v3/index.json
 
-    - name: Install latex pandoc - Linux
+    - name: Install pandoc - Linux
       if: runner.os == 'Linux'
       run: |
-        sudo apt-get update
-        sudo apt-get install texlive-full
         wget https://github.com/jgm/pandoc/releases/download/3.1.7/pandoc-3.1.7-1-amd64.deb
         sudo dpkg -i *.deb
         rm -rf *.deb
         pandoc -v
-        which latex || echo NOT FOUND latex
-        which xelatex || echo NOT FOUND xelatex
         sudo gem install rouge
-    - name: Install latex pandoc - MacOS
+    - name: Install pandoc - MacOS
       if: runner.os == 'MacOS'
       run: |
         unset HOMEBREW_NO_INSTALL_FROM_API
         brew untap Homebrew/core
         brew update-reset && brew update
         brew install pandoc
-        brew install --cask basictex
-        eval "$(/usr/libexec/path_helper)"
-        sudo tlmgr update --self
-        sudo tlmgr install framed tcolorbox environ trimspaces unicode-math
         pandoc -v
-        which latex || echo NOT FOUND latex
-        which xelatex || echo NOT FOUND xelatex
         sudo gem install rouge -v 3.30.0
+    - name: Install Tectonic
+      uses: wtfjoke/setup-tectonic@v3
+      with:
+        github-token: ${{ secrets.GITHUB_TOKEN }}
+        tectonic-version: 0.15
+
     - name: Clean Dafny
       run: dotnet clean dafny/Source/Dafny.sln
     # First we build the ZIPs (which do not include the refman)

diff --git a/.github/workflows/refman.yml b/.github/workflows/refman.yml
@@ -20,7 +20,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ ubuntu-20.04 ]
+        os: [ ubuntu-22.04 ]
     steps:
     - name: OS
       run: echo ${{ runner.os }} ${{ matrix.os }}
@@ -35,33 +35,28 @@ jobs:
         path: dafny
     - name: Build Dafny
       run: dotnet build dafny/Source/Dafny.sln
-    - name: Install latex pandoc - Linux
+    - name: Install pandoc - Linux
       if: runner.os == 'Linux'
       run: |
-        sudo apt-get update
-        sudo apt-get install texlive-full
         wget https://github.com/jgm/pandoc/releases/download/3.1.7/pandoc-3.1.7-1-amd64.deb
         sudo dpkg -i *.deb
         rm -rf *.deb
         pandoc -v
-        which latex || echo NOT FOUND latex
-        which xelatex || echo NOT FOUND xelatex
         sudo gem install rouge
-    - name: Install latex pandoc - MacOS
+    - name: Install pandoc - MacOS
       if: runner.os == 'MacOS'
       run: |
         unset HOMEBREW_NO_INSTALL_FROM_API
         brew untap Homebrew/core
         brew update-reset && brew update
         brew install pandoc
-        brew install --cask basictex
-        eval "$(/usr/libexec/path_helper)"
-        sudo tlmgr update --self
-        sudo tlmgr install framed tcolorbox environ trimspaces unicode-math
         pandoc -v
-        which latex || echo NOT FOUND latex
-        which xelatex || echo NOT FOUND xelatex
         sudo gem install rouge -v 3.30.0
+    - name: Install Tectonic
+      uses: wtfjoke/setup-tectonic@v3
+      with:
+        github-token: ${{ secrets.GITHUB_TOKEN }}
+        tectonic-version: 0.15
     - name: Build reference manual
       run: |
         eval "$(/usr/libexec/path_helper)"

diff --git a/docs/DafnyRef/Makefile b/docs/DafnyRef/Makefile
@@ -1,9 +1,5 @@
-XELATEXF := /usr/local/texlive/2020/bin/x86_64-darwin/xelatex
-XELATEXB := /usr/local/texlive/2020basic/bin/x86_64-darwin/xelatex
-XELATEX := $(shell (test -x ${XELATEXF} && echo ${XELATEXF}) || (test -x ${XELATEXB} && echo ${XELATEXB}) || echo "xelatex")
-
 all: features numbers options
-	./concat DafnyRef.md | sed -e '/numbered toc/d' -e '/:toc/d' -e '/PDFOMIT/d'  -e 's/<!--PDF NEWPAGE-->/\\newpage/' -e 's/<!--.*-->//' | pandoc --citeproc --toc --syntax-definition="../KDESyntaxDefinition/dafny.xml"  --syntax-definition="../KDESyntaxDefinition/grammar.xml" --highlight-style=../KDESyntaxDefinition/dafny.theme --pdf-engine=xelatex --bibliography=DafnyRef.bib --bibliography=krml250.bib --bibliography=poc.bib --bibliography=paper-full.bib --bibliography=references.bib -H head.tex -B header.tex -V colorlinks=true -t pdf -o DafnyRef.pdf
+	./concat DafnyRef.md | sed -e '/numbered toc/d' -e '/:toc/d' -e '/PDFOMIT/d'  -e 's/<!--PDF NEWPAGE-->/\\newpage/' -e 's/<!--.*-->//' | pandoc --citeproc --toc --syntax-definition="../KDESyntaxDefinition/dafny.xml"  --syntax-definition="../KDESyntaxDefinition/grammar.xml" --highlight-style=../KDESyntaxDefinition/dafny.theme --pdf-engine=tectonic --bibliography=DafnyRef.bib --bibliography=krml250.bib --bibliography=poc.bib --bibliography=paper-full.bib --bibliography=references.bib -H head.tex -B header.tex -V colorlinks=true -t pdf -o DafnyRef.pdf
 
 numbers:
 	javac Numbers.java && java Numbers -r DafnyRef.md