1 | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(pathes,[ | |
6 | set_search_pathes/0, % install run-time search pathes | |
7 | runtime_application_path/1 | |
8 | ]). | |
9 | ||
10 | :- use_module(module_information). | |
11 | ||
12 | :- module_info(group,infrastructure). | |
13 | :- module_info(description,'This module contains code to compute compile-time and runtime-pathes.'). | |
14 | ||
15 | :- use_module(library(system),[environ/2]). | |
16 | :- use_module(library(file_systems),[file_exists/1, | |
17 | current_directory/1]). | |
18 | :- use_module(library(lists),[reverse/2]). | |
19 | ||
20 | :- multifile user:file_search_path/2. | |
21 | :- dynamic user:file_search_path/2. | |
22 | ||
23 | % some pathes may be set by environment variables during compilation, | |
24 | :- dynamic compile_time_env_path/2. | |
25 | lookup_env_path(Pathname, Varname) :- | |
26 | ( environ(Varname,Value) -> | |
27 | print('Hard-wired path for alias '),print(Pathname),print(': '),print(Value),nl, | |
28 | assert(compile_time_env_path(Pathname,Value)) | |
29 | ; otherwise -> | |
30 | true). | |
31 | % compile-time pathes | |
32 | :- lookup_env_path(prob_comp_home,'PROB_COMP_HOME'). % hard-wired version of the runtime_application_path | |
33 | % This is used on systems where it absolutely clear where the | |
34 | % ProB's application directory will be, namely Debian/Ubuntu packages | |
35 | % run-time pathes | |
36 | :- lookup_env_path(prob_home,'PROB_HOME'). | |
37 | :- lookup_env_path(examples,'PROB_EXAMPLES'). % hard-wired pathes, see above (about Debian/Ubuntu packages) | |
38 | :- lookup_env_path(prob_lib,'PROB_LIB'). % hard-wired pathes, see above (about Debian/Ubuntu packages) | |
39 | :- lookup_env_path(prob_tcl,'PROB_TCL'). % hard-wired pathes, see above (about Debian/Ubuntu packages) | |
40 | ||
41 | % removes an (optional) trailing /src directory from the path, | |
42 | % the result will not end with a slash | |
43 | remove_src_dir(Orig,Dir) :- | |
44 | atom_codes(Orig,COrig), | |
45 | ? | ( append(CDir,"/src/",COrig) -> true |
46 | ; append(CDir,"/src",COrig) -> true | |
47 | ; append(CDir,"/src/proz",COrig) -> true | |
48 | ; append(CDir,"/src/proz/",COrig) -> true | |
49 | ; append(CDir,"/",COrig) -> true | |
50 | ; otherwise -> COrig=CDir), | |
51 | atom_codes(Dir,CDir). | |
52 | ||
53 | % returns the path to the application directory (at run-time) | |
54 | runtime_application_path(Dir) :- | |
55 | ( environ('PROB_HOME',Dir) -> % the user has set the environment variable PROB_HOME and thus overrides any other setting | |
56 | true % the Rodin plugin used this mechanism | |
57 | ? | ; application_path2(Dir),is_correct_prob_home_path(Dir) -> |
58 | true | |
59 | ; application_path2(D),absolute_file_name(D,D1),parent_dir(D1,Dir,_), | |
60 | is_correct_prob_home_path(Dir) -> | |
61 | true | |
62 | ; compile_time_env_path(prob_comp_home,Dir) -> % e.g. Debian/Ubuntu systems: the path was hard-wired at compile-time | |
63 | true | |
64 | ; otherwise -> % usually a run from source code, where we the current directory is prob/src | |
65 | current_directory(Current), remove_src_dir(Current,Dir)). | |
66 | application_path2(Dir) :- | |
67 | prolog_flag(system_type,development), | |
68 | % try and find location of src/module_information.pl | |
69 | current_module(module_information,MFile),parent_dir(MFile,SrcDir,_), | |
70 | remove_src_dir(SrcDir,Dir). | |
71 | application_path2(Dir) :- | |
72 | \+(prolog_flag(system_type,development)), | |
73 | environ('SP_APP_DIR',Dir). /* /usr/local/bin/sicstus on development systems */ | |
74 | application_path2(Dir) :- | |
75 | \+(prolog_flag(system_type,development)), | |
76 | environ('SP_STARTUP_DIR',Dir). | |
77 | ||
78 | % check if the path points to a directory with a lib subdirectory and the probcliparser.jar file | |
79 | is_correct_prob_home_path(D) :- % print(trying_as_prob_home_path(D)),nl,nl, | |
80 | atom_concat(D,'/lib/probcliparser.jar',ConParser), | |
81 | file_exists(ConParser). | |
82 | ||
83 | parent_dir(FullFile,Dir,Basename) :- | |
84 | atom_chars(FullFile,CFullFile), % "path/to/file" | |
85 | reverse(CFullFile,RCFullFile), % "elif/ot/htap" | |
86 | ? | append(RCFile,['/'|RCDir],RCFullFile),!, % "elif" "/ot/htap" |
87 | reverse(RCFile,CFile),reverse(['/'|RCDir],CDir), % "file" "path/to/" | |
88 | atom_chars(Basename,CFile),atom_chars(Dir,CDir). | |
89 | ||
90 | % we do not use our standard test case schema here because we do not | |
91 | % want to introduce a dependency to the test framework at this level | |
92 | parent_dir_test1 :- | |
93 | parent_dir('/aaaa/bbb/cc/d.app',D,B),D=='/aaaa/bbb/cc/',B=='d.app'. | |
94 | parent_dir_test2 :- | |
95 | parent_dir('/aaaa/bbb/cc/',D,B),D=='/aaaa/bbb/cc/',B==''. | |
96 | parent_dir_test :- | |
97 | parent_dir_test1, parent_dir_test2. | |
98 | :- ( parent_dir_test -> true | |
99 | ; otherwise -> write(user_error,'testcase for pathes:parent_dir/2 failed, aborted.\n'), | |
100 | halt(1)). | |
101 | ||
102 | % returns the path to the application directory (compile-time) | |
103 | compiletime_application_path(Dir) :- | |
104 | compile_time_env_path(prob_comp_home,Dir),!. | |
105 | compiletime_application_path(Dir) :- | |
106 | runtime_application_path(Dir). | |
107 | ||
108 | check_if_hard_wired(Alias, _Prefix, _Dir, Full) :- | |
109 | compile_time_env_path(Alias,Full),!. | |
110 | check_if_hard_wired(_Alias, Prefix, Dir, Full) :- | |
111 | atom_concat(Prefix,Dir,Full). | |
112 | ||
113 | set_search_path(Alias, Prefix, Dir) :- | |
114 | check_if_hard_wired(Alias, Prefix, Dir, Full), | |
115 | %% print(setting_path(Alias,Full)),nl, %% | |
116 | ( catch( user:file_search_path(Alias,Full), _, fail) -> true | |
117 | ; otherwise -> | |
118 | catch( retractall(user:file_search_path(Alias,_)), _, true), % remove any old defintion | |
119 | assertz(user:file_search_path(Alias,Full)) % , print(setting_search_path(Alias,Full)),nl | |
120 | ). | |
121 | ||
122 | % pathes that can be used by use_module(...), but | |
123 | % must not be used in run-time code | |
124 | set_compile_time_search_pathes :- | |
125 | compiletime_application_path(App), | |
126 | %format('~n ProB compile time application path: ~w~n~n',[App]), | |
127 | set_search_path(extension, App, '/extensions'), | |
128 | set_search_path(probsrc, App, '/src'), | |
129 | set_search_path(chrsrc, App, '/src/chr'), | |
130 | set_search_path(probcspsrc, App, '/src/cia'), | |
131 | set_search_path(probltlsrc, App, '/src/ltl'), | |
132 | set_search_path(probporsrc, App, '/src/por'), | |
133 | set_search_path(probpgesrc, App, '/src/pge'), | |
134 | set_search_path(prozsrc, App, '/src/proz'), | |
135 | set_search_path(kodkodsrc, App, '/src/kodkod'), | |
136 | set_search_path(symbolic_model_checker, App, '/src/symbolic_model_checker'), | |
137 | set_search_path(partial_evaluator, App, '/src/partial_evaluator'), | |
138 | %set_search_path(plugins, App, '/plugins'), | |
139 | %set_search_path(abstract_domains, App, '/plugins/absint/domains'), | |
140 | set_search_path(tclsrc, App, '/tcl'), | |
141 | %set_search_path(probpromela,App,'/src/promela'), | |
142 | set_search_path(prob_rewrite_rules, App, '/src/rewrite_rules'), | |
143 | set_search_path(smtlib_solver, App, '/src/smtlib_solver'), | |
144 | set_search_path(smt_solvers_interface, App, '/src/smt_solvers_interface'), | |
145 | set_search_path(synthesis, App, '/src/synthesis'), | |
146 | set_search_path(library_plspec, App, '/src/library_plspec'). % patched libraries for plspec | |
147 | :- set_compile_time_search_pathes. | |
148 | ||
149 | % pathes that can be used in run-time code; should not be called at compile time | |
150 | set_search_pathes :- | |
151 | runtime_application_path(App), | |
152 | %print(runtime_application_path(App)),nl, | |
153 | set_search_path(prob_home, App, ''), | |
154 | set_search_path(examples, App, '/../probprivate/public_examples'), | |
155 | set_search_path(prob_lib, App, '/lib'), | |
156 | set_search_path(prob_tcl, App, '/tcl'), | |
157 | ||
158 | check_if_hard_wired(prob_lib, App, '/lib', LibDir), | |
159 | ( catch(user:library_directory(LibDir), _, fail) -> true % ,print(already_set(LibDir)),nl | |
160 | ; otherwise -> | |
161 | catch( retractall(user:library_directory(_)), _, true), % remove any old defintion | |
162 | assertz(user:library_directory(LibDir))). |