Cleanup Isabelle build a bit; run Isabelle examples/tests during dune…

… tests.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

deps/isabelle/.gitignore

@@ -0,0 +1,3 @@
+/Isabelle.exec-files
+/Isabelle.no-links
+/Isabelle/

deps/isabelle/Makefile

@@ -27,7 +27,7 @@ ISABELLE_URL=https://isabelle.in.tum.de/website-$(ISABELLE_VSN)/dist/$(ISABELLE_
 ISABELLE_DIR=Isabelle
 
 # Some defaults, for the case if makefile is called not by the dune build system.
-PROJECT_ROOT=../..
+PROJECT_ROOT=$(if $(DUNE_SOURCEROOT),$(DUNE_SOURCEROOT),../..)
 CACHE_DIR=$(PROJECT_ROOT)/_build_cache
 
 
@@ -63,11 +63,12 @@ $(ISABELLE_DIR)/src/TLA+: $(ISABELLE_DIR)
 		&& cp etc/settings etc/settings.target \
 		&& echo "ISABELLE_OUTPUT=$$HEAPS_PATH" >> etc/settings
 	mkdir -p $(ISABELLE_DIR)/src/TLA+ \
-		&& cp -a theories/TLA+/* $(ISABELLE_DIR)/src/TLA+/ \
+		&& cp -a ../../isabelle/* $(ISABELLE_DIR)/src/TLA+/ \
 		&& chmod -R u+w $(ISABELLE_DIR)/src/TLA+/
 	cd $(ISABELLE_DIR)/ \
 		&& ./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+
+		&& ./bin/isabelle build -o system_heaps -o document=false -b -c -v -d src/TLA+ TLA+ \
+		&& rm -rf ./heaps/polyml-*/log/*
 	cd $(ISABELLE_DIR) \
 		&& rm etc/settings \
 		&& mv etc/settings.target etc/settings

deps/isabelle/dune

@@ -2,9 +2,11 @@
 ; The source code for the TLA+ theory is in the $PROJECT_ROOT/isabelle directory.
 ; The generated heaps (Pure and TLA+) are in Isabelle/heaps/polyml-*/.
 (rule
- (deps "Makefile" (source_tree theories))
+ (alias default)
+ (mode (promote (until-clean)))
+ (deps "Makefile" (source_tree ../../isabelle))
  (targets (dir Isabelle) "Isabelle.no-links" "Isabelle.exec-files")
- (action (run "make" "-C" "." "PROJECT_ROOT=%{project_root}" "Isabelle.no-links" "Isabelle.exec-files")))
+ (action (run "make" "-C" "." "Isabelle.no-links" "Isabelle.exec-files")))
 
 (install
  (section (site (tlapm backends)))

dune-project

@@ -1,4 +1,4 @@
-(lang dune 3.8)
+(lang dune 3.12)
 
 (using dune_site 0.1)
 

isabelle/Makefile

@@ -1,4 +1,7 @@
-.PHONY: rebuild heap-only clean
+ISABELLE=isabelle
+SRC_ROOT=$(if $(DUNE_SOURCEROOT),$(DUNE_SOURCEROOT),..)
+
+.PHONY: rebuild heap-only dune-runtest 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,10 +10,17 @@
 # file etc/settings beneath the Isabelle home (i.e., where the Isabelle
 # distribution is installed).
 rebuild:
-	isabelle build -o document -o browser_info -b -c -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 .
+	$(ISABELLE) build -o document=false -o browser_info=false -b -c -v -D .
+
+# This is invoked from the dune file to run the tests.
+# The tex files might be readonly in the sandbox and Isabelle copies
+# them several times, and thus fails by overwriting a readonly file.
+dune-runtest:
+	chmod 644 examples/document/root.tex document/root.tex
+	$(SRC_ROOT)/deps/isabelle/Isabelle/bin/isabelle build -o document=false -o browser_info=false -c -v -D .
 
 clean:
-	rm -rf output/
+	rm -rf output/ examples/output/

isabelle/ROOT

@@ -21,7 +21,7 @@ session "TLA+Examples" in examples = "TLA+" +
 
   theories
     Allocator
-    AtomicBakeryG
+    (* AtomicBakeryG  TODO: Restore it here, when examples are fixed. *)
 
   document_files
     "root.tex"

isabelle/dune

@@ -0,0 +1,13 @@
+; We use the promoted version of the Isabelle here to have proper file permissions.
+; The promoted version is in the source tree, which is located based on ${DUNE_SOURCEROOT} environment variable.
+; We assume the project will be built before running the tests, otherwise the Isabelle is always rebuilt.
+
+(rule
+ (alias runtest)
+ (deps
+  ; (alias_rec ../deps/isabelle/default) -- We don't use it here, because otherwise the isabelle is always rebuilt.
+  (source_tree "."))
+ (action
+  (run make dune-runtest)))
+
+(data_only_dirs document examples tests)

tlapm.opam

@@ -25,7 +25,7 @@ authors: [
 homepage: "https://github.com/tlaplus/tlapm"
 bug-reports: "https://github.com/tlaplus/tlapm/issues"
 depends: [
-  "dune" {>= "3.8"}
+  "dune" {>= "3.12"}
   "ocaml"
   "dune-site"
   "dune-build-info"