From 9fe5a8d200105895ae44b60b1565425db762cdc5 Mon Sep 17 00:00:00 2001 From: Karolis Petrauskas Date: Fri, 2 Jun 2023 00:05:10 +0300 Subject: [PATCH] Use dune-site to locate backends (partial). Signed-off-by: Karolis Petrauskas --- deps/isabelle/Makefile | 8 ++++++++ deps/isabelle/dune | 7 +++---- deps/ls4/dune | 2 +- deps/z3/dune | 2 +- deps/zenon/dune | 2 +- dune-project | 3 +++ src/.depend | 9 +++++++-- src/Makefile | 2 ++ src/dune | 9 ++++++++- src/dune_site_mock/setup_paths.ml | 4 ++++ src/dune_site_mock/setup_paths.mli | 4 ++++ src/dune_site_mock/setup_paths.mlt | 3 +++ src/tlapm.ml | 4 ++++ 13 files changed, 49 insertions(+), 10 deletions(-) create mode 100644 src/dune_site_mock/setup_paths.ml create mode 100644 src/dune_site_mock/setup_paths.mli create mode 100644 src/dune_site_mock/setup_paths.mlt diff --git a/deps/isabelle/Makefile b/deps/isabelle/Makefile index 9af056c4..3e866514 100644 --- a/deps/isabelle/Makefile +++ b/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 diff --git a/deps/isabelle/dune b/deps/isabelle/dune index bd23329e..d58ab2ad 100644 --- a/deps/isabelle/dune +++ b/deps/isabelle/dune @@ -8,7 +8,6 @@ (data_only_dirs Isabelle) -; TODO: Blocked by -; (install -; (section lib) -; (dirs "Isabelle")) +(install + (section (site (tlapm backends))) + (dirs "Isabelle")) diff --git a/deps/ls4/dune b/deps/ls4/dune index 78d887c7..27c9bebd 100644 --- a/deps/ls4/dune +++ b/deps/ls4/dune @@ -5,5 +5,5 @@ (action (run "make" "-C" "." "ls4"))) (install - (section libexec) + (section (site (tlapm backends))) (files (ls4 as bin/ls4))) diff --git a/deps/z3/dune b/deps/z3/dune index 110133bb..9b422175 100644 --- a/deps/z3/dune +++ b/deps/z3/dune @@ -5,5 +5,5 @@ (action (run "make" "-C" "." "z3"))) (install - (section libexec) + (section (site (tlapm backends))) (files (z3 as bin/z3))) diff --git a/deps/zenon/dune b/deps/zenon/dune index bc08624e..32cf6d69 100644 --- a/deps/zenon/dune +++ b/deps/zenon/dune @@ -5,5 +5,5 @@ (action (run "make" "-C" "."))) (install - (section libexec) + (section (site (tlapm backends))) (files (zenon as bin/zenon))) diff --git a/dune-project b/dune-project index c8f40321..361a3120 100644 --- a/dune-project +++ b/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)) diff --git a/src/.depend b/src/.depend index 387ff075..16c52237 100644 --- a/src/.depend +++ b/src/.depend @@ -663,7 +663,6 @@ 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 \ @@ -671,7 +670,6 @@ proof/p_visit.cmx: proof/p_visit.mlt \ 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 : diff --git a/src/Makefile b/src/Makefile index 38d8d8cf..54082f56 100644 --- a/src/Makefile +++ b/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 \ diff --git a/src/dune b/src/dune index 154f5a15..5730b927 100644 --- a/src/dune +++ b/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 diff --git a/src/dune_site_mock/setup_paths.ml b/src/dune_site_mock/setup_paths.ml new file mode 100644 index 00000000..95ce37ff --- /dev/null +++ b/src/dune_site_mock/setup_paths.ml @@ -0,0 +1,4 @@ + +module Sites = struct + let backends : string list = [] +end diff --git a/src/dune_site_mock/setup_paths.mli b/src/dune_site_mock/setup_paths.mli new file mode 100644 index 00000000..e6e7ca13 --- /dev/null +++ b/src/dune_site_mock/setup_paths.mli @@ -0,0 +1,4 @@ + +module Sites: sig + val backends : string list +end diff --git a/src/dune_site_mock/setup_paths.mlt b/src/dune_site_mock/setup_paths.mlt new file mode 100644 index 00000000..4de8fdf7 --- /dev/null +++ b/src/dune_site_mock/setup_paths.mlt @@ -0,0 +1,3 @@ +(* + * Copyright (C) 2008-2013 INRIA and Microsoft Corporation + *) diff --git a/src/tlapm.ml b/src/tlapm.ml index c7ab1dc6..7cd4141d 100644 --- a/src/tlapm.ml +++ b/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;;