Use dune-site to locate backends (partial).

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

deps/isabelle/Makefile

@@ -19,6 +19,14 @@ $(ISABELLE_DIR).sexp: $(ISABELLE_TGZ)
 	cd $(ISABELLE_DIR) && echo "ISABELLE_OUTPUT=$(ISABELLE_OUT)" >> etc/settings
 	cd $(ISABELLE_DIR) && cp -r $(DUNE_SOURCEROOT)/isabelle src/TLA+
 	cd $(ISABELLE_DIR)/src/TLA+ && $(ISABELLE_EXE) usedir -b Pure TLA+
+	# ...
+	# TODO: Workaround BEGIN, until https://github.com/ocaml/dune/issues/7831 is resolved.
+	# Here we remove symlinks to directories, because dune install fails on them for now.
+	cd $(ISABELLE_DIR) && rm ./contrib/jre1.6.0_27_x86-linux/jre1.6.0_27/man/ja
+	cd $(ISABELLE_DIR) && rm ./contrib/polyml-5.4.0/src
+	cd $(ISABELLE_DIR) && rm ./contrib/polyml && mv ./contrib/polyml-5.4.0 ./contrib/polyml
+	# TODO: Workaround END
+	#
 	(echo "(" && (find $(ISABELLE_DIR) -type f) && echo ")") > $(ISABELLE_DIR).sexp
 
 .PHONY: all

deps/isabelle/dune

@@ -8,7 +8,6 @@
 
 (data_only_dirs Isabelle)
 
-; TODO: Blocked by <https://github.com/ocaml/dune/issues/7831>
-; (install
-;  (section lib)
-;  (dirs "Isabelle"))
+(install
+ (section (site (tlapm backends)))
+ (dirs "Isabelle"))

deps/ls4/dune

@@ -5,5 +5,5 @@
  (action (run "make" "-C" "." "ls4")))
 
 (install
- (section libexec)
+ (section (site (tlapm backends)))
  (files (ls4 as bin/ls4)))

deps/z3/dune

@@ -5,5 +5,5 @@
  (action (run "make" "-C" "." "z3")))
 
 (install
- (section libexec)
+ (section (site (tlapm backends)))
  (files (z3 as bin/z3)))

deps/zenon/dune

@@ -5,5 +5,5 @@
  (action (run "make" "-C" ".")))
 
 (install
- (section libexec)
+ (section (site (tlapm backends)))
  (files (zenon as bin/zenon)))

dune-project

@@ -1,5 +1,7 @@
 (lang dune 3.7)
 
+(using dune_site 0.1)
+
 (using directory-targets 0.1)
 
 (name tlapm)
@@ -12,4 +14,5 @@
  (name tlapm)
  (synopsis "TLA+ Proof Manager")
  (description "TLA+ Proof Manager")
+ (sites (lib backends)) ; will contain all the provers, approx lib/tlapm/backends/.
  (depends ocaml dune))

src/.depend

@@ -663,15 +663,13 @@ proof/p_visit.cmo: proof/p_visit.mlt \
     proof/p_t.cmi \
     util/ext.cmi \
     expr.cmi \
-    errors.cmi \
     util/deque.cmi \
     proof/p_visit.cmi
 proof/p_visit.cmx: proof/p_visit.mlt \
     util/property.cmx \
     proof/p_t.cmx \
     util/ext.cmx \
     expr.cmx \
-    errors.cmx \
     util/deque.cmx \
     proof/p_visit.cmi
 proof/p_gen.cmo: proof/p_gen.mlt \
@@ -1836,6 +1834,10 @@ module.cmx: module.mlt \
     module/m_elab.cmx \
     module/m_dep.cmx \
     module.cmi
+dune_site_mock/setup_paths.cmo: dune_site_mock/setup_paths.mlt \
+    dune_site_mock/setup_paths.cmi
+dune_site_mock/setup_paths.cmx: dune_site_mock/setup_paths.mlt \
+    dune_site_mock/setup_paths.cmi
 tlapm_args.cmo: tlapm_args.mlt \
     version.cmi \
     params.cmi \
@@ -1857,6 +1859,7 @@ tlapm.cmo: tlapm.mlt \
     tlapm_args.cmi \
     tla_parser.cmi \
     util/timing.cmi \
+    dune_site_mock/setup_paths.cmi \
     backend/schedule.cmi \
     util/property.cmi \
     proof.cmi \
@@ -1882,6 +1885,7 @@ tlapm.cmx: tlapm.mlt \
     tlapm_args.cmx \
     tla_parser.cmx \
     util/timing.cmx \
+    dune_site_mock/setup_paths.cmx \
     backend/schedule.cmx \
     util/property.cmx \
     proof.cmx \
@@ -2217,5 +2221,6 @@ module.cmi : \
     expr.cmi \
     util/deque.cmi \
     ctx.cmi
+dune_site_mock/setup_paths.cmi :
 tlapm_args.cmi :
 tlapm.cmi :

src/Makefile

@@ -139,10 +139,12 @@ MODULES = \
   backend \
   ${MODULE_PACK} \
   module \
+  dune_site_mock/setup_paths \
   tlapm_args \
   tlapm
 
 INC0 = \
+  -I ../dune_site_mock \
   -I ../backend \
   -I ../frontend \
   -I ../expr \

src/dune

@@ -1,11 +1,18 @@
 (executable
   (name tlapm)
   (public_name tlapm)
-  (libraries unix str)
+  (modules (:standard setup_paths))
+  (libraries unix str dune-site)
   (foreign_stubs (language c) (names sysconf_stubs)))
 
 (ocamllex alexer)
 
+(generate_sites_module
+ (module setup_paths)
+ (sites tlapm))
+
+(dirs (:standard \ dune_site_mock)) ; To avoid including the mocked Setup_paths module.
+
 (include_subdirs unqualified)
 
 (env

src/dune_site_mock/setup_paths.ml

@@ -0,0 +1,4 @@
+
+module Sites = struct
+  let backends : string list = []
+end

src/dune_site_mock/setup_paths.mli

@@ -0,0 +1,4 @@
+
+module Sites: sig
+  val backends : string list
+end

src/dune_site_mock/setup_paths.mlt

@@ -0,0 +1,3 @@
+(*
+ * Copyright (C) 2008-2013  INRIA and Microsoft Corporation
+ *)

src/tlapm.ml

@@ -583,6 +583,10 @@ let init () =
        end;
        exit 3
 
+let () = (* TODO: Handle it properly. *)
+    let x = Setup_paths.Sites.backends in
+    let _ = List.map (fun u -> (Printf.printf "TODO: path=%s\n" u)) x in
+        Printf.printf("TODO: paths printed.\n")
 
 exception Stacktrace;;