Do not build the Isabelle document when building heaps.

Signed-off-by: Karolis Petrauskas <[email protected]>

.github/workflows/main.yml

@@ -22,7 +22,7 @@ jobs:
               if: matrix.operating-system == 'ubuntu-latest'
               run: |
                 sudo apt-get update
-                sudo apt-get install --yes time texlive-latex-base texlive-plain-generic
+                sudo apt-get install --yes time
             - name: Set up Python
               uses: actions/setup-python@v2
               with:

.github/workflows/pr.yml

@@ -26,7 +26,7 @@ jobs:
               if: matrix.operating-system == 'ubuntu-latest'
               run: |
                 sudo apt-get update
-                sudo apt-get install --yes time texlive-latex-base texlive-plain-generic
+                sudo apt-get install --yes time
             - name: Set up Python
               uses: actions/setup-python@v2
               with:

.github/workflows/release.yml

@@ -71,7 +71,7 @@ jobs:
               if: matrix.operating-system == 'ubuntu-latest'
               run: |
                 sudo apt-get update
-                sudo apt-get install --yes time texlive-latex-base texlive-plain-generic
+                sudo apt-get install --yes time
             - name: Set up Python
               uses: actions/setup-python@v2
               with:

deps/isabelle/Makefile

@@ -65,8 +65,8 @@ $(ISABELLE_DIR)/src/TLA+: $(ISABELLE_DIR)
 		&& cp -a theories/TLA+/* $(ISABELLE_DIR)/src/TLA+/ \
 		&& chmod -R u+w $(ISABELLE_DIR)/src/TLA+/
 	cd $(ISABELLE_DIR)/ \
-		&& ./bin/isabelle build -b -v -d src/Pure -o system_heaps Pure \
-		&& ./bin/isabelle build -b -v -d src/TLA+ -o system_heaps TLA+
+		&& ./bin/isabelle build -o system_heaps -o document=false -b -v -d src/Pure Pure \
+		&& ./bin/isabelle build -o system_heaps -o document=false -b -c -v -d src/TLA+ TLA+
 	cd $(ISABELLE_DIR) \
 		&& rm etc/settings \
 		&& mv etc/settings.target etc/settings

isabelle/Makefile

@@ -1,4 +1,4 @@
-.PHONY: rebuild clean
+.PHONY: rebuild heap-only clean
 
 # Generate theory information (in HTML and PDF formats) as well as the main
 # heap file for the TLA+ object logic. By default these will be generated
@@ -7,7 +7,10 @@
 # file etc/settings beneath the Isabelle home (i.e., where the Isabelle
 # distribution is installed).
 rebuild:
-	isabelle build -b -v -D .
+	isabelle build -o document -o browser_info -b -c -v -D .
+
+heap-only:
+	isabelle build -o document=false -o browser_info=false -b -c -v -D .
 
 clean:
 	rm -rf output/

isabelle/ROOT

@@ -1,7 +1,7 @@
 (* build the session using "isabelle build -b -D ." *)
 chapter "TLA+"
 session "TLA+" = "Pure" +
-  options [document=pdf, document_output = "output", document_variants="document:outline=/proof"]
+  options [document_output = "output", document_variants="document:outline=/proof"]
 
   theories
     Constant (global)