Skip to content

Commit

Permalink
Use stdlib site for the library TLA files.
Browse files Browse the repository at this point in the history
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
  • Loading branch information
kape1395 committed Jun 6, 2023
1 parent 1892e10 commit 3c21d96
Show file tree
Hide file tree
Showing 5 changed files with 14 additions and 4 deletions.
7 changes: 6 additions & 1 deletion dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -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?
2 changes: 1 addition & 1 deletion library/dune
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
(install
(section lib)
(section (site (tlapm stdlib)))
(files (glob_files "*.tla")))
1 change: 1 addition & 0 deletions src/dune_site_mock/setup_paths.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
1 change: 1 addition & 0 deletions src/dune_site_mock/setup_paths.mli
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@

module Sites: sig
val backends : string list
val stdlib : string list
end
7 changes: 5 additions & 2 deletions src/params.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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] = '+'
Expand Down

0 comments on commit 3c21d96

Please sign in to comment.