From 3c21d96639069aaf404036b85736138ced4ab2e9 Mon Sep 17 00:00:00 2001
From: Karolis Petrauskas <k.petrauskas@gmail.com>
Date: Wed, 7 Jun 2023 00:28:54 +0300
Subject: [PATCH] Use stdlib site for the library TLA files.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
---
 dune-project                       | 7 ++++++-
 library/dune                       | 2 +-
 src/dune_site_mock/setup_paths.ml  | 1 +
 src/dune_site_mock/setup_paths.mli | 1 +
 src/params.ml                      | 7 +++++--
 5 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/dune-project b/dune-project
index 361a3120..98fb892d 100644
--- a/dune-project
+++ b/dune-project
@@ -14,5 +14,10 @@
  (name tlapm)
  (synopsis "TLA+ Proof Manager")
  (description "TLA+ Proof Manager")
- (sites (lib backends)) ; will contain all the provers, approx lib/tlapm/backends/.
+ (sites
+  (lib backends) ; will contain all the provers, approx lib/tlapm/backends/.
+  (lib stdlib))  ; TLA files composing the StdLib.
  (depends ocaml dune))
+
+; TODO: https://github.com/ocaml/dune/tree/main/example/with-configure-step.t
+;       to derive the current os to name the release?
\ No newline at end of file
diff --git a/library/dune b/library/dune
index 7dd2a2df..9b2e33cd 100644
--- a/library/dune
+++ b/library/dune
@@ -1,3 +1,3 @@
 (install
- (section lib)
+ (section (site (tlapm stdlib)))
  (files (glob_files "*.tla")))
diff --git a/src/dune_site_mock/setup_paths.ml b/src/dune_site_mock/setup_paths.ml
index 33418f9d..2d93789a 100644
--- a/src/dune_site_mock/setup_paths.ml
+++ b/src/dune_site_mock/setup_paths.ml
@@ -5,4 +5,5 @@ Hence this file inicates (by returning empty list) the absense of the dune-site-
 *)
 module Sites = struct
   let backends : string list = []
+  let stdlib : string list = []
 end
diff --git a/src/dune_site_mock/setup_paths.mli b/src/dune_site_mock/setup_paths.mli
index e6e7ca13..2ef92535 100644
--- a/src/dune_site_mock/setup_paths.mli
+++ b/src/dune_site_mock/setup_paths.mli
@@ -1,4 +1,5 @@
 
 module Sites: sig
   val backends : string list
+  val stdlib : string list
 end
diff --git a/src/params.ml b/src/params.ml
index a265180c..a2a89740 100644
--- a/src/params.ml
+++ b/src/params.ml
@@ -51,7 +51,7 @@ let noproving = ref false (* Don't send any obligation to the back-ends. *)
 let printallobs = ref false
 (* print unnormalized and normalized versions of obligations in toolbox mode *)
 
-
+(* The default library path. The relative paths (-I +some) are based on this. *)
 let library_path =
   let d = Sys.executable_name in
   let d = Filename.dirname (Filename.dirname d) in
@@ -253,7 +253,10 @@ let set_smt_logic logic = smt_logic := logic
 
 let max_threads = ref nprocs
 
-let rev_search_path = ref [library_path]
+(* The actual list if paths at which the library TLA files are searched. *)
+let rev_search_path = ref (library_path :: Setup_paths.Sites.stdlib)
+
+(* Additional paths are added to the search list by keeping the base path as the first one. *)
 let add_search_dir dir =
   let dir =
     if dir.[0] = '+'