Make the new isabelle to work with the dune-based build.

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

deps/isabelle/Makefile

@@ -1,19 +1,20 @@
 OS_TYPE=$(patsubst CYGWIN%,Cygwin,$(shell uname))
 HOST_CPU=$(shell uname -m)
 
-ISABELLE_VSN=Isabelle2011-1
+ISABELLE_VSN=Isabelle2020
 
 ifeq ($(OS_TYPE),Linux)
-	ISABELLE_ARCHIVE=$(ISABELLE_VSN)_bundle_x86-linux.tar.gz
+	ISABELLE_ARCHIVE=$(ISABELLE_VSN)_linux.tar.gz
 	ISABELLE_ARCHIVE_TYPE=tgz
 	FIND_EXEC=-executable
 endif
 ifeq ($(OS_TYPE),Darwin)
-	ISABELLE_ARCHIVE=$(ISABELLE_VSN).dmg
+	ISABELLE_ARCHIVE=$(ISABELLE_VSN)_macos.tar.gz
 	ISABELLE_ARCHIVE_TYPE=dmg
 	FIND_EXEC=-perm +111
 endif
 ifeq ($(OS_TYPE),Cygwin)
+	# TODO: Fix this.
 	ISABELLE_ARCHIVE=$(ISABELLE_VSN)_bundle_x86-cygwin.tar.gz
 	ISABELLE_ARCHIVE_TYPE=tgz
 	FIND_EXEC=-executable
@@ -66,10 +67,9 @@ $(ISABELLE_DIR)/src/TLA+: $(ISABELLE_DIR)
 		&& echo "ISABELLE_OUTPUT=$$HEAPS_PATH" >> etc/settings
 	mkdir -p $(ISABELLE_DIR)/src/TLA+ \
 		&& cp -a theories/TLA+/* $(ISABELLE_DIR)/src/TLA+/
-	cd $(ISABELLE_DIR)/src/Pure \
-		&& ../../bin/isabelle make
-	cd $(ISABELLE_DIR)/src/TLA+ \
-		&& ../../bin/isabelle usedir -b Pure 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+
 	cd $(ISABELLE_DIR) \
 		&& rm etc/settings \
 		&& mv etc/settings.target etc/settings
@@ -79,9 +79,8 @@ $(ISABELLE_DIR)/src/TLA+: $(ISABELLE_DIR)
 .PRECIOUS: $(ISABELLE_DIR).no-links
 $(ISABELLE_DIR).no-links: $(ISABELLE_DIR) $(ISABELLE_DIR)/src/TLA+
 	rm -rf $@
-	cd $< && rm -f ./contrib/jre1.6.0_27_x86-linux/jre1.6.0_27/man/ja
-	cd $< && rm -f ./contrib/polyml-5.4.0/src
-	cd $< && rm -f ./contrib/polyml && mv ./contrib/polyml-5.4.0 ./contrib/polyml
+	cd $< && rm -f ./contrib/jdk-11.0.5+10/x86_64-linux/jre
+	cd $< && rm -f ./contrib/jdk-11.0.5+10/x86_64-linux/man/ja
 	touch $@
 
 # TODO: This is a workaround, because the dune install removes all the executable

src/isabelle_keywords.ml

@@ -1,5 +1,4 @@
 (* AUTOMATICALLY GENERATED by `update_isabelle_keywords.py` - DO NOT EDIT *)
-Revision.f "$Rev$";;
 let v = [
     "ML";
     "ML_command";

src/params.ml

@@ -61,12 +61,32 @@ let library_path =
   let d = Filename.concat d "tlaps" in
   d
 
+(* The backends directory should be resolved via the dune sites mechanism.
+   If the sites are not available, then we assume this file layout to locate
+   the Isabelle installation.
+    - bin/tlapm
+    - lib/tlapm/backends/Isabelle
+  *)
+let isabelle_base_path =
+  let rec find paths =
+    match paths with
+    | [] ->
+      let bin_dir = Filename.dirname Sys.executable_name in
+      let prefix = Filename.dirname bin_dir in
+      List.fold_left
+        Filename.concat
+        prefix
+        ["lib"; "tlapm"; "backends"; "Isabelle"]
+    | path :: other ->
+      let isabelle_base = Filename.concat path "Isabelle" in
+      match Sys.file_exists isabelle_base with
+      | true -> isabelle_base
+      | false -> find other
+  in find Setup_paths.Sites.backends
+
 let isabelle_tla_path =
-    let d = Sys.executable_name in
-    let d = Filename.dirname (Filename.dirname d) in
-    let d = Filename.concat d "lib" in
-    let d = Filename.concat d "isabelle_tla" in
-    d
+  List.fold_left Filename.concat isabelle_base_path ["src"; "TLA+"]
+
 
 type executable =
   | Unchecked of string * string * string (* exec, command, version_command *)
@@ -155,7 +175,7 @@ let isabelle =
                    isabelle_success_string
                    isabelle_tla_path
   in
-  make_exec "isabelle process" cmd "isabelle version"
+  make_exec "isabelle" cmd "isabelle version"
 ;;
 
 let set_fast_isabelle () =